diff options
4 files changed, 19 insertions, 6 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean index 726f5d7..e99617b 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Contains.lean @@ -1,5 +1,5 @@ import BinaryHeap.CompleteTree.AdditionalOperations -import BinaryHeap.CompleteTree.Lemmas +import BinaryHeap.CompleteTree.AdditionalProofs.Get namespace BinaryHeap.CompleteTree.AdditionalProofs diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean index 50d1ece..b8cd934 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean @@ -3,6 +3,8 @@ import BinaryHeap.CompleteTree.Lemmas namespace BinaryHeap.CompleteTree.AdditionalProofs +theorem get_eq_get' {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (index : Fin (n+1)) : tree.get' index = tree.get index (Nat.succ_pos n) := rfl + theorem get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ h₁ := by unfold get match n with diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 866cc7a..5f7b62c 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -894,6 +894,19 @@ protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap case isTrue h₁ => apply CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt assumption - split - case isFalse.isTrue h₁ h₂ => sorry - case isFalse.isFalse h₁ h₂ => sorry + case isFalse h₁ => + have h₁ : (Internal.heapRemoveLastWithIndex heap).2.snd ≥ index := Fin.not_lt.mp h₁ + split + case isTrue h₂ => sorry + case isFalse h₂ => + --have h₂ : (Internal.heapRemoveLastWithIndex heap).2.snd ≤ index := Fin.not_lt.mp h₂ + have : (index.val < (Internal.heapRemoveLastWithIndex heap).2.snd.val) = False := Fin.lt_iff_val_lt_val.subst (p := λx ↦ x = False) $ eq_false h₂ + have h₃ : index = (Internal.heapRemoveLastWithIndex heap).2.snd := + Nat.lt_or_eq_of_le h₁ + |> this.subst (motive := λx ↦ x ∨ index.val = (Internal.heapRemoveLastWithIndex heap).snd.snd.val) + |> (false_or _).mp + |> Fin.eq_of_val_eq + exact + CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex heap + |> h₃.substr + |> Eq.symm diff --git a/BinaryHeap/CompleteTree/Lemmas.lean b/BinaryHeap/CompleteTree/Lemmas.lean index e7a7e7b..01bb9c7 100644 --- a/BinaryHeap/CompleteTree/Lemmas.lean +++ b/BinaryHeap/CompleteTree/Lemmas.lean @@ -60,8 +60,6 @@ theorem CompleteTree.heqContains {α : Type u} {n m : Nat} {a : CompleteTree α have h₃ : a = b := eq_of_heq h₃ congr -theorem CompleteTree.get_eq_get' {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (index : Fin (n+1)) : tree.get' index = tree.get index (Nat.succ_pos n) := rfl - theorem CompleteTree.leftLenLtN {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n>0) : tree.leftLen h₁ < n := by unfold leftLen split |