diff options
| author | Andreas Grois <andi@grois.info> | 2024-08-04 12:40:29 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-08-04 12:40:29 +0200 |
| commit | d53610ae89d3da780b9beee52c8bfe88f45d5826 (patch) | |
| tree | e591ec2dfd1d96184f3c5817eecc554eddf95a57 | |
| parent | 9d331e60152ac7660dea8fe16a414c5899575ee6 (diff) | |
Continue heapUpdateRootOnlyUpdatesRoot
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean index 3333f1f..71accaa 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean @@ -108,5 +108,16 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α else -- index was in r simp only [h, ↓reduceDite] at h₃ - sorry + split + case isTrue h₄ _ _ _ _ _ => + simp + rw[contains_as_root_left_right _ _ (Nat.succ_pos _)] + right + right + rw[←h₃, contains_iff_index_exists', right_unfold] + have h₄ : j < oo + 1 + (pp + 1) := Nat.lt_of_succ_lt_succ h₄ + have : oo + 1 ≤ j := Nat.le_of_not_gt h + have : j - (oo + 1) < pp + 1 := Nat.sub_lt_left_of_lt_add this h₄ + exists ⟨j-(oo+1), this⟩ + case isFalse => sorry termination_by n |