diff options
| author | Andreas Grois <andi@grois.info> | 2024-06-29 00:12:17 +0200 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-06-29 00:12:17 +0200 |
| commit | 7ee65a922723cc810d85e0f2b511bb663ca9ab93 (patch) | |
| tree | 8ec8e1f76545eb7050e887ccb75ca9e2b7c1e92e | |
| parent | cffb8812c10db44b7eea3ef49d331231e5496ce3 (diff) | |
CompleteTree.popLastIsHeap finished.
| -rw-r--r-- | Common/BinaryHeap.lean | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/Common/BinaryHeap.lean b/Common/BinaryHeap.lean index faac226..96f3c27 100644 --- a/Common/BinaryHeap.lean +++ b/Common/BinaryHeap.lean @@ -511,6 +511,7 @@ theorem CompleteTree.popLastLeavesRoot (heap : CompleteTree α (n+1)) (h₁ : n simp +set_option linter.unusedVariables false in -- Lean 4.2 thinks h₁ is unused. It very much is not unused. theorem CompleteTree.popLastIsHeap {heap : CompleteTree α (o+1)} {le : α → α → Bool} (h₁ : HeapPredicate heap le) (h₂ : transitive_le le) (h₃ : total_le le) : HeapPredicate (heap.popLast.snd) le := match o, heap with | (n+m), .branch v l r _ _ _ => @@ -542,11 +543,22 @@ theorem CompleteTree.popLastIsHeap {heap : CompleteTree α (o+1)} {le : α → simp[h₁.right.left, h₁.right.right.right, popLastIsHeap h₁.left h₂ h₃] unfold HeapPredicate.leOrLeaf simp - rw[←(popLastLeavesRoot l (Nat.zero_lt_of_ne_zero $ Nat.succ_ne_zero nn))] + rw[←popLastLeavesRoot] exact h₁.right.right.left else by simp[h₅] - sorry + cases m + case zero => + simp_arith at h₄ -- n ≠ 0 + simp_arith[Ne.symm h₄] at h₅ -- the second term in h₅ is decidable and True. What remains is ¬(0 < n), or n = 0 + case succ mm h₆ h₇ h₈ => + simp + unfold HeapPredicate at * + simp[h₁, popLastIsHeap h₁.right.left h₂ h₃] + unfold HeapPredicate.leOrLeaf + cases mm <;> simp + rw[←popLastLeavesRoot] + exact h₁.right.right.right /--Removes the element at a given index. Use `CompleteTree.indexOf` to find the respective index.-/ --def CompleteTree.heapRemoveAt {α : Type u} (lt : α → α → Bool) {o : Nat} (index : Fin (o+1)) (heap : CompleteTree α (o+1)) : CompleteTree α o := |