Continue heapRemoveLastWithIndexRelationGt

2 files changed, 84 insertions, 23 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
index 8922b76..50d1ece 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/Get.lean
@@ -74,3 +74,36 @@ theorem get_right' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r
   (branch v l r m_le_n max_height_diff subtree_complete).get index (Nat.succ_pos _) = r.get ⟨index.val - n - 1, h₂⟩  (Nat.zero_lt_of_lt h₂)
 :=
   get_right (branch v l r m_le_n max_height_diff subtree_complete) index (Nat.succ_pos _) h₁
+
+theorem get_left {α : Type u} {n : Nat} (tree : CompleteTree α n) (index : Fin n) (h₁ : n > 0) (h₂ : index > ⟨0, h₁⟩) (h₃ : index ≤ tree.leftLen h₁) :
+  have h₃ : ↑index - 1 < tree.leftLen h₁ := Nat.lt_of_lt_of_le (Nat.pred_lt_self h₂) h₃
+  have h₄ : tree.leftLen h₁ > 0 := Nat.zero_lt_of_lt h₃
+  tree.get index h₁ = (tree.left h₁).get ⟨index.val - 1, h₃⟩ h₄
+:=
+  match n, tree with
+  | (o+p+1), .branch v l r _ _ _ => by
+    simp[left_unfold]
+    generalize hnew : get ⟨↑index - 1, _⟩ l _ = new
+    unfold get get'
+    split
+    case h_1 => contradiction
+    case h_2 j h₃ o2 p2 v2 l2 r2 _ _ _ d1 he₁ he₂ =>
+      clear d1
+      have : o = o2 := heqSameLeftLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂
+      have : p = p2 := heqSameRightLen (congrArg Nat.succ he₁) (Nat.succ_pos _) he₂
+      subst o2 p2
+      simp[leftLen_unfold] at h₃
+      have h₄ : j < o :=Nat.lt_of_succ_le h₃
+      simp[h₄]
+      cases o ; contradiction
+      case succ oo =>
+        simp at hnew he₂ ⊢
+        have := he₂.right.left
+        subst l2
+        assumption
+
+theorem get_left' {α : Type u} {n m : Nat} {v : α} {l : CompleteTree α n} {r : CompleteTree α m} {m_le_n : m ≤ n} {max_height_diff : n < 2 * (m + 1)} {subtree_complete : (n + 1).isPowerOfTwo ∨ (m + 1).isPowerOfTwo} (index : Fin (n + m + 1)) (h₁ : index > ⟨0, Nat.succ_pos _⟩) (h₂ : index ≤ n) :
+  have h₃ : ↑index - 1 < n := Nat.lt_of_lt_of_le (Nat.pred_lt_self h₁) h₂
+  (branch v l r m_le_n max_height_diff subtree_complete).get index (Nat.succ_pos _) = l.get ⟨index.val - 1, h₃⟩  (Nat.zero_lt_of_lt h₃)
+:=
+  get_left (branch v l r m_le_n max_height_diff subtree_complete) index (Nat.succ_pos _) h₁ h₂
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index 405b5ee..364cbf3 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -766,51 +766,62 @@ private theorem heapRemoveLastWithIndexRelationGt_Aux {α : Type u} {o p q : Nat
     simp at hp₅
     assumption
 
+private theorem heapRemoveLastWithIndexRelationGt_Aux2 {α : Type u} {oo p : Nat} (index : Fin (oo + 1 + p)) (tree : CompleteTree α (oo + p + 1)) (h₁ :  oo + p + 1 = oo + 1 + p) (h₂ : oo + 1 + p > 0) (h₃ : oo + p + 1 > 0) (h₄ : index.val < oo + p + 1) : get index (h₁▸tree) h₂ = get ⟨index.val,h₄⟩ tree h₃ := by
+  induction p generalizing oo
+  case zero =>
+    simp
+  case succ pp hp =>
+    have hp₂ := hp (oo := oo+1)
+    have hp₃ : (oo + 1 + pp + 1) = oo + (pp + 1) + 1 := by simp_arith
+    have hp₄ : (oo + 1 + 1 + pp) = oo + 1 + (pp + 1) := by simp_arith
+    rw[hp₃, hp₄] at hp₂
+    exact hp₂ index tree h₁ h₂ h₃ h₄
+
 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
-  (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get (index.pred $ Fin.ne_of_gt this) (by omega) = heap.get index (by omega)
+  have : n > 0 := Nat.lt_of_lt_of_le (Fin.pos_iff_ne_zero.mpr $ Fin.ne_zero_of_gt h₁) (Nat.le_of_lt_succ index.isLt)
+  (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get (index.pred $ Fin.ne_zero_of_gt h₁) this = heap.get index (Nat.succ_pos _)
 := by
-have h₂ : 0 ≠ n := by omega
+have h₂ : 0 ≠ n := Ne.symm $ Nat.ne_zero_iff_zero_lt.mpr $ Nat.lt_of_lt_of_le (Fin.pos_iff_ne_zero.mpr $ Fin.ne_zero_of_gt h₁) (Nat.le_of_lt_succ index.isLt)
 revert h₁
 unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux
 intro h₁
 split at h₁
 rename_i o p v l r _ _ _ _
-simp at h₂
-simp[h₂] at h₁ ⊢
+simp only [Nat.add_eq, ne_eq] at h₂
+simp only [Nat.add_eq, h₂, ↓reduceDite, decide_eq_true_eq, Fin.zero_eta, Fin.isValue,
+  Nat.succ_eq_add_one, Fin.castLE_succ, Nat.pred_eq_sub_one, gt_iff_lt] at h₁ ⊢
 split
 case isFalse h₃ =>
   --removed right
-  simp[h₃] at h₁ ⊢
-  cases p <;> simp at h₁ ⊢
+  simp only [h₃, ↓reduceDite, Fin.isValue] at h₁ ⊢
+  cases p <;> simp only [Nat.add_zero, Nat.reduceSub, Nat.reduceAdd, Fin.isValue] at h₁ ⊢
   case zero =>
-    simp (config := {ground := true}) at h₃
+    simp (config := { ground := true }) only [Nat.zero_add, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃
     subst o
     contradiction
   case succ pp _ _ _ _ =>
     generalize hold : get index (branch v l r _ _ _) _ = oldValue
     have h₄ : index ≠ 0 := Fin.ne_zero_of_gt h₁
     have h₅ : index.pred h₄ > o := by
-      simp
+      simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt]
       rw[Fin.lt_iff_val_lt_val] at h₁
-      simp at h₁
+      simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁
       omega
     have h₆ : index > o := by
-      simp at h₅
+      simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt] at h₅
       omega
     have h₇ : ↑index - o - 1 < pp + 1 := by
       have : ↑index < o.add (pp + 1) + 1 := index.isLt
       unfold Fin.pred Fin.subNat at h₅
-      simp at h₅
+      simp only [Nat.add_eq, gt_iff_lt] at h₅
       generalize index.val = i at h₅ h₆ this ⊢
-      simp at this
+      simp only [Nat.add_eq] at this
       omega
     have h₈ : ⟨↑index - o - 1, h₇⟩ > (Internal.heapRemoveLastWithIndex r).snd.snd := by
       unfold Internal.heapRemoveLastWithIndex
-      simp
+      simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one, gt_iff_lt]
       rw[Fin.lt_iff_val_lt_val] at h₁ ⊢
-      simp at h₁ ⊢
+      simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁ ⊢
       generalize Fin.val (Internal.heapRemoveLastAux (β := λn ↦ α × Fin n) r _ _ _).2.snd = indexInR at h₁ ⊢
       omega
     rw[get_right' _ h₅]
@@ -819,17 +830,17 @@ case isFalse h₃ =>
     have h₉ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt r ⟨↑index - o - 1, h₇⟩ h₈
     unfold Internal.heapRemoveLastWithIndex at h₉
     unfold Fin.pred Fin.subNat at h₉
-    simp at h₉
-    simp
+    simp only [Nat.add_eq, Fin.zero_eta, Fin.isValue, Nat.succ_eq_add_one] at h₉
+    simp only [Nat.add_eq, Fin.coe_pred, Fin.isValue]
     have : ↑index - 1 - o - 1 = ↑index - o - 1 - 1 := by omega
-    simp[this, h₉]
+    simp only [this, Nat.add_eq, Fin.isValue, h₉]
 case isTrue h₃ =>
   --removed left
-  simp[h₃] at h₁ ⊢
+  simp only [h₃, and_self, ↓reduceDite, Fin.isValue] at h₁ ⊢
   cases o
   case zero => exact absurd h₃.left $ Nat.not_lt_zero p
   case succ oo _ _ _ _ =>
-    simp at h₁ ⊢
+    simp only [Fin.isValue] at h₁ ⊢
     if h₄ : index > oo + 1 then
       -- get goes into the right branch
       rw[get_right' _ h₄]
@@ -840,13 +851,30 @@ case isTrue 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 [Nat.add_eq, ne_eq, Fin.zero_eta, Nat.succ_eq_add_one, Nat.pred_eq_sub_one,
+        Fin.coe_pred, Fin.isValue, ← lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
       simp only[leftLen_unfold]
       apply heapRemoveLastWithIndexRelationGt_Aux
-      case h₁ => simp_arith
+      case h₁ => simp_arith only
       case h₅ => exact Nat.succ_pos _
     else
       -- get goes into the left branch
+      rw[heapRemoveLastWithIndexRelationGt_Aux2]
+      case h₃ => exact Nat.succ_pos _
+      case h₄ => omega
+      generalize hold :  get index (branch v l r _ _ _) _ = old
+      have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁
+      have h₆ : index.pred h₅ ≤ oo := by
+        simp only [Nat.add_eq, Fin.coe_pred]
+        rw[Fin.lt_iff_val_lt_val] at h₁
+        simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE] at h₁
+        omega
+      have h₇ : ↑index - 1 < oo + p + 1 :=
+        Nat.lt_of_le_of_lt ((Fin.coe_pred index h₅).subst (motive := λx ↦ x ≤ oo) h₆) (Nat.lt_succ_of_le (Nat.le_add_right oo p))
+      rw[get_left']
+      <;> simp
+      case h₁ => sorry
+      case h₂ => exact h₆
       sorry
 
 protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)):