diff options
3 files changed, 28 insertions, 1 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean index 796130f..fb5b81b 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean @@ -24,6 +24,11 @@ theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1) have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree tree simp only [h₃, heapUpdateRootReturnsRoot, h₂] +/-- + Shows that each element contained before removing the root that is not the root is still contained after removing the root. + This is not a rigorous proof that the rest of the tree remained unchanged, as (1 (1 (1 1)) (2)).heapPop = (1 (2 (2 _)) (2)) would pass it too... + Imho it is still a good indication that there are no obvious bugs. + -/ theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index (Nat.succ_pos _) := by unfold heapPop split <;> simp diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 92efdbc..b852995 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -425,6 +425,12 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea have h₆ : (⟨index.val, hi⟩ : Fin (o + (pp+1))) > ⟨0,Nat.succ_pos _⟩ := h₂₂ rw[get_left' _ h₆ h₅] +/-- + Shows that for each index in the original tree there is a corresponding index in the resulting tree of heapRemoveLast, + except for the element returned by heapRemoveLast (WithIndex). + This is a rigourous proof that heapRemoveLast does not modify the tree in any other ways than removing + the last element. + -/ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)): let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap if h₁ : index > oldIndex then @@ -461,7 +467,10 @@ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap |> Eq.symm -/--If the resulting tree contains all elements except the removed one, and contains one less than the original, well, you get the idea.-/ +/-- + Shows that each element contained before removing the last that is not the last is still contained after removing the last. + This is not a rigorous proof that the rest of the tree remained unchanged. Such a proof exists in heapRemoveLastWithIndexRelation + -/ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : let (newHeap, _, removedIndex) := Internal.heapRemoveLastWithIndex heap (h₁ : index ≠ removedIndex) → newHeap.contains (heap.get index (Nat.succ_pos n)) @@ -483,6 +492,10 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n case isFalse h₅ => omega --contradiction +/-- + Shows that each element contained before removing the last that is not the last is still contained after removing the last. + This is not a rigorous proof that the rest of the tree remained unchanged. Such a proof exists in heapRemoveLastWithIndexRelation + -/ protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : let (newHeap, removedElement, _) := Internal.heapRemoveLastWithIndex heap newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n) @@ -498,6 +511,10 @@ protected theorem heapRemoveLastWithIndexEitherContainsOrReturnsElement {α : Ty subst index exact h₂.symm +/-- + Shows that each element contained before removing the last that is not the last is still contained after removing the last. + This is not a rigorous proof that the rest of the tree remained unchanged. Such a proof exists in heapRemoveLastWithIndexRelation + -/ protected theorem heapRemoveLastEitherContainsOrReturnsElement {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : let (newHeap, removedElement) := Internal.heapRemoveLast heap newHeap.contains (heap.get index (Nat.succ_pos n)) ∨ removedElement = heap.get index (Nat.succ_pos n) diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean index bc7ca14..9912bf3 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean @@ -11,6 +11,11 @@ namespace BinaryHeap.CompleteTree.AdditionalProofs abbrev heapUpdateRootReturnsRoot {α : Type u} {n : Nat} (le : α → α → Bool) (value : α) (heap : CompleteTree α n) (h₁ : n > 0) := CompleteTree.heapUpdateRootReturnsRoot le value heap h₁ +/-- + Shows that each element contained before updating the root that is not the root is still contained after updating the root. + This is not a rigorous proof that the rest of the tree remained unchanged. See comment on heapPopOnlyRemovesRoot. + Imho it is still a good indication that there are no obvious bugs. + -/ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α → Bool) (tree : CompleteTree α n) (h₁ : n > 0) (index : Fin n) (h₂ : index ≠ ⟨0, h₁⟩) (value : α) : (tree.heapUpdateRoot le value h₁).fst.contains $ tree.get index h₁ := by generalize h₃ : (get index tree h₁) = oldVal unfold get at h₃ |