Finish contains_iff_index_exists

2 files changed, 92 insertions, 10 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean
index 1b3ef50..43927f5 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean
@@ -91,6 +91,53 @@ private theorem if_contains_get_eq_auxl {α : Type u} {o : Nat} (tree : Complete
     rw[heq]
     assumption
 
+private theorem if_contains_get_eq_auxr {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : tree.rightLen (Nat.succ_pos o) > 0) :
+  ∀(indexl : Fin (tree.rightLen (Nat.succ_pos o))), (tree.right _).get indexl h₁ = element → ∃(index : Fin (o+1)), tree.get index (Nat.succ_pos o) = element
+:= by
+  intro indexr
+  let index : Fin (o+1) := ⟨(tree.leftLen (Nat.succ_pos o) + indexr.val + 1), by
+    have h₂ : tree.leftLen (Nat.succ_pos _) + tree.rightLen _ + 1 = tree.length := Eq.symm $ lengthEqLeftRightLenSucc tree _
+    rw[length] at h₂
+    have h₃ : tree.leftLen (Nat.succ_pos o) + indexr.val + 1 < tree.leftLen (Nat.succ_pos o) + tree.rightLen (Nat.succ_pos o) + 1 := by
+      apply Nat.succ_lt_succ
+      apply Nat.add_lt_add_left
+      exact indexr.isLt
+    exact Nat.lt_of_lt_of_eq h₃ h₂
+  ⟩
+  intro prereq
+  exists index
+  unfold get
+  simp
+  unfold get'
+  generalize hindex : index = i
+  split
+  case h_1 =>
+    have : index.val = 0 := Fin.val_eq_of_eq hindex
+    contradiction
+  case h_2 j p q v l r ht1 ht2 ht3 _ _ =>
+    have h₂ : index.val = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) + indexr.val + 1 := rfl
+    have h₃ : index.val = j.succ := Fin.val_eq_of_eq hindex
+    have h₄ : j = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) + indexr.val := by
+      rw[h₃] at h₂
+      exact Nat.succ.inj h₂
+    have : p = (branch v l r ht1 ht2 ht3).leftLen (Nat.succ_pos _) := rfl
+    have h₅ : ¬(j < p) := by simp_arith [this, h₄]
+    simp only [h₅, ↓reduceDite, Nat.add_eq]
+    unfold get at prereq
+    split at prereq
+    rename_i pp ii rr _ hel hei heq _
+    split
+    rename_i ppp rrr _ _ _ _ _ _ _ _
+    have : pp = ppp := by rw[rightLen_unfold] at hel; exact Nat.succ.inj hel.symm
+    subst pp
+    simp only [gt_iff_lt, ne_eq, Nat.succ_eq_add_one, Nat.add_eq, Nat.reduceEqDiff, heq_eq_eq, Nat.zero_lt_succ] at *
+    have : j = ii.val + p := by omega
+    subst this
+    simp
+    rw[right_unfold] at heq
+    rw[heq]
+    assumption
+
 private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree α (o+1)) (element : α) (h₁ : tree.contains element) : ∃(index : Fin (o+1)), tree.get' index = element := by
     revert h₁
     unfold contains
@@ -113,22 +160,42 @@ private theorem if_contains_get_eq {α : Type u} {o : Nat} (tree : CompleteTree
       match hn : n, hl: l with
       | 0, .leaf => by contradiction
       | (nn+1), l => by
-        have nn_lt_o : nn < o := by have : o = nn + 1 + m := Nat.succ.inj he; omega
-        have blah := if_contains_get_eq l element h₂
-        have blupp := if_contains_get_eq_auxl tree element $ Nat.zero_lt_of_lt nn_lt_o
-        simp at blupp
-        simp[get_eq_get'] at blah ⊢
-        apply blah.elim
+        have nn_lt_o : nn < o := by have : o = nn + 1 + m := Nat.succ.inj he; omega --also for termination
+        have h₃ := if_contains_get_eq l element h₂
+        have h₄ := if_contains_get_eq_auxl tree element $ Nat.zero_lt_of_lt nn_lt_o
+        simp only at h₄
+        simp[get_eq_get'] at h₃ ⊢
+        apply h₃.elim
         match o, tree with
         | (yy+_), .branch _ ll _ _ _ _ =>
           simp_all[left_unfold, leftLen_unfold]
           have : yy = nn+1 := heqSameLeftLen (by omega) (Nat.succ_pos _) heq
-          subst yy
           have : _ = m := heqSameRightLen (by omega) (Nat.succ_pos _) heq
-          subst m
+          subst yy m
+          simp_all
+          exact h₄
+    case h_2.inr.inr h₂ => exact
+      match hm : m, hr: r with
+      | 0, .leaf => by contradiction
+      | (mm+1), r => by
+        have mm_lt_o : mm < o := by have : o = n + (mm + 1) := Nat.succ.inj he; omega --termination
+        have h₃ := if_contains_get_eq r element h₂
+        have : tree.rightLen (Nat.succ_pos o) > 0 := by
+          have := heqSameRightLen (he) (Nat.succ_pos o) heq
+          simp[rightLen_unfold] at this
+          rw[this]
+          exact Nat.succ_pos mm
+        have h₄ := if_contains_get_eq_auxr tree element this
+        simp[get_eq_get'] at h₃ ⊢
+        apply h₃.elim
+        match o, tree with
+        | (_+zz), .branch _ _ rr _ _ _ =>
+          simp_all[right_unfold, rightLen_unfold]
+          have : _ = n := heqSameLeftLen (by omega) (Nat.succ_pos _) heq
+          have : zz = mm+1 := heqSameRightLen (by omega) (Nat.succ_pos _) heq
+          subst n zz
           simp_all
-          exact blupp
-    case h_2.inr.inr h₂ => sorry
+          exact h₄
   termination_by o
 
 
diff --git a/BinaryHeap/CompleteTree/Lemmas.lean b/BinaryHeap/CompleteTree/Lemmas.lean
index dc26dd5..1841111 100644
--- a/BinaryHeap/CompleteTree/Lemmas.lean
+++ b/BinaryHeap/CompleteTree/Lemmas.lean
@@ -24,6 +24,8 @@ theorem CompleteTree.left_unfold {α : Type u} {o p : Nat} (v : α) (l : Complet
 
 theorem CompleteTree.leftLen_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).leftLen h₄ = o := rfl
 
+theorem CompleteTree.rightLen_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).rightLen h₄ = p := rfl
+
 /-- Helper to rw away right, because Lean 4.9 makes it unnecessarily hard to deal with match in tactics mode... -/
 theorem CompleteTree.right_unfold {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α o) (r : CompleteTree α p) (h₁ : p ≤ o) (h₂ : o < 2 * (p + 1)) (h₃ : (o + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : o + p + 1 > 0): (CompleteTree.branch v l r h₁ h₂ h₃).right h₄ = r := rfl
 
@@ -50,3 +52,16 @@ theorem CompleteTree.leftLenLtN {α : Type u} {n : Nat} (tree : CompleteTree α
   rw[length]
   rename_i o p _ _ _ _ _ _ _
   exact Nat.lt_of_le_of_lt (Nat.le_add_right o p) (Nat.lt_succ_self (o+p))
+
+theorem CompleteTree.rightLenLtN {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n>0) : tree.rightLen h₁ < n := by
+  unfold rightLen
+  split
+  rw[length]
+  rename_i o p _ _ _ _ _ _ _
+  exact Nat.lt_of_le_of_lt (Nat.le_add_left p o) (Nat.lt_succ_self (o+p))
+
+theorem CompleteTree.lengthEqLeftRightLenSucc {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n>0) : tree.length = tree.leftLen h₁ + tree.rightLen h₁ + 1 := by
+  unfold leftLen rightLen
+  split
+  unfold length
+  rfl