Continue on heapRemoveLastWithIndexRelation

4 files changed, 40 insertions, 12 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
index f86fd76..8922b76 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
@@ -3,6 +3,15 @@ import BinaryHeap.CompleteTree.Lemmas
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
+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
+  | nn+1 =>
+    unfold get'
+    split
+    case h_2 hx => exact absurd (Fin.mk.inj hx) (Nat.zero_ne_add_one _)
+    case h_1 => trivial
+
 theorem get_right {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₁ : n > 0) (h₂ : index > tree.leftLen h₁) :
   have h₃ : ↑index - tree.leftLen h₁ - 1 < tree.rightLen h₁ := by
     revert h₂
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index ad5cb32..df8941f 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -746,7 +746,6 @@ private theorem Fin.ne_zero_of_gt {n : Nat} {i j : Fin (n+1)} (h₁ : i > j) : i
   have : 0 ≤ j := Fin.zero_le _
   by omega
 
-
 protected theorem heapRemoveLastWithIndexRelationGt {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)) (h₁ : index > (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd) :
   have : (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd ≥ 0 := Fin.zero_le _
   have : index > 0 := by omega
@@ -806,8 +805,36 @@ case isFalse h₃ =>
     simp[this, h₉]
 case isTrue h₃ =>
   --removed left
-  sorry
---termination_by n
+  simp[h₃] at h₁ ⊢
+  cases o
+  case zero => exact absurd h₃.left $ Nat.not_lt_zero p
+  case succ oo _ _ _ _ =>
+    simp at h₁ ⊢
+    if h₄ : index > oo + 1 then
+      -- get goes into the right branch
+      rw[get_right' _ h₄]
+      have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁
+      have h₆ : index.pred h₅ > oo := by simp; omega
+      rw[get_right]
+      case h₂ =>
+        rw[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
+        rw[leftLen_unfold]
+        assumption
+      simp[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
+      simp only[leftLen_unfold]
+      have h₇ :=
+        right_sees_through_cast (by simp_arith : oo + p + 1 = oo + 1 + p) (
+            branch v
+            (
+              (Internal.heapRemoveLastAux (β := λn ↦ α × Fin n) l (fun a => (a, 0))
+                  (fun {prev_size curr_size} x h₁ => (x.fst, Fin.castLE (by omega) x.snd.succ))
+                  fun {prev_size curr_size} x left_size h₁ => (x.fst, Fin.castLE (by omega) (x.snd.addNat left_size).succ)).fst
+            )
+            r (by omega) (by omega) (by simp[Nat.power_of_two_iff_next_power_eq, h₃])) (Nat.succ_pos _) (by omega)
+      sorry
+    else
+      -- get goes into the left branch
+      sorry
 
 protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)):
   let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
index b5ad9c6..7ac98c9 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
@@ -1,6 +1,7 @@
 import BinaryHeap.CompleteTree.HeapOperations
 import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateRoot
 import BinaryHeap.CompleteTree.Lemmas
+import BinaryHeap.CompleteTree.AdditionalProofs.Get
 import BinaryHeap.CompleteTree.AdditionalProofs.Contains
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
diff --git a/BinaryHeap/CompleteTree/Lemmas.lean b/BinaryHeap/CompleteTree/Lemmas.lean
index b37dda1..e7a7e7b 100644
--- a/BinaryHeap/CompleteTree/Lemmas.lean
+++ b/BinaryHeap/CompleteTree/Lemmas.lean
@@ -89,12 +89,3 @@ theorem HeapPredicate.leOrLeaf_transitive (h₁ : transitive_le le) : le a b →
   cases n <;> simp
   apply h₁ a b _
   exact ⟨h₂, h₃⟩
-
-theorem CompleteTree.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
-  | nn+1 =>
-    unfold get'
-    split
-    case h_2 hx => exact absurd (Fin.mk.inj hx) (Nat.zero_ne_add_one _)
-    case h_1 => trivial