Finish heapRemoveLastWithIndexRelation. That was a piece of work...

1 files changed, 62 insertions, 22 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index 02f985c..0aa9481 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -804,7 +804,7 @@ case isFalse h₃ =>
     have h₄ : index ≠ 0 := Fin.ne_zero_of_gt h₁
     have h₅ : index.pred h₄ > o := by
       simp only [Nat.add_eq, Fin.coe_pred, gt_iff_lt]
-      rw[Fin.lt_iff_val_lt_val] at h₁
+      rewrite[Fin.lt_iff_val_lt_val] at h₁
       simp only [Nat.succ_eq_add_one, Fin.isValue, Fin.val_succ, Fin.coe_castLE, Fin.coe_addNat] at h₁
       exact Nat.lt_of_add_right $ Nat.lt_pred_of_succ_lt h₁
     have h₆ : index > o :=  Nat.lt_of_add_left $ Nat.succ_lt_of_lt_pred h₅
@@ -814,9 +814,9 @@ case isFalse h₃ =>
       (Nat.sub_lt_of_lt_add this (Nat.succ_le_of_lt h₆) : ↑index - (o + 1) < pp + 1)
     have h₈ : ⟨↑index - o - 1, h₇⟩ > (Internal.heapRemoveLastWithIndex r).snd.snd :=
       Nat.lt_sub_of_add_lt (b := o+1) h₁
-    rw[get_right' _ h₅]
-    rw[get_right' _ h₆] at hold
-    rw[←hold]
+    rewrite[get_right' _ h₅]
+    rewrite[get_right' _ h₆] at hold
+    rewrite[←hold]
     have h₉ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt r ⟨↑index - o - 1, h₇⟩ h₈
     unfold Internal.heapRemoveLastWithIndex at h₉
     unfold Fin.pred Fin.subNat at h₉
@@ -837,13 +837,13 @@ case isTrue h₃ =>
     simp only [Fin.isValue] at h₁ ⊢
     if h₄ : index > oo + 1 then
       -- get goes into the right branch
-      rw[get_right' _ h₄]
+      rewrite[get_right' _ h₄]
       have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁
       have h₆ : index.pred h₅ > oo := Nat.lt_pred_iff_succ_lt.mpr h₄
-      rw[get_right]
+      rewrite[get_right]
       case h₂ =>
-        rw[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
-        rw[leftLen_unfold]
+        rewrite[←lens_see_through_cast _ leftLen _ (Nat.succ_pos _) _]
+        rewrite[leftLen_unfold]
         assumption
       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 _) _]
@@ -854,7 +854,7 @@ case isTrue h₃ =>
     else
       -- get goes into the left branch
       have h₅ : index ≠ 0 := Fin.ne_zero_of_gt h₁
-      rw[heapRemoveLastWithIndexRelationGt_Aux2]
+      rewrite[heapRemoveLastWithIndexRelationGt_Aux2]
       case h₃ => exact Nat.succ_pos _
       case h₄ => exact
         Nat.le_of_not_gt h₄
@@ -866,11 +866,11 @@ case isTrue h₃ =>
       have h₆ : index.pred h₅ ≤ oo := Nat.pred_le_iff_le_succ.mpr $ Nat.le_of_not_gt h₄
       have h₇ : ↑index - 1 ≤ oo := (Fin.coe_pred index h₅).subst (motive := λx↦x ≤ oo) h₆
       have h₈ : ↑index ≤ oo + 1 := Nat.le_succ_of_pred_le h₇
-      rw[get_left']
+      rewrite[get_left']
       case h₁ => exact Nat.zero_lt_of_lt $ Nat.lt_sub_of_add_lt h₁
       case h₂ => exact h₆
       simp only [Fin.coe_pred, Fin.isValue]
-      rw[get_left'] at hold
+      rewrite[get_left'] at hold
       case h₁ => exact Fin.pos_iff_ne_zero.mpr h₅
       case h₂ => exact h₈
       subst hold
@@ -884,13 +884,14 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea
   (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.get ⟨index.val, this⟩ hn = heap.get index (Nat.succ_pos _)
 :=
   have hn : 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 (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt)
+  have hi : index.val < n := Nat.lt_of_lt_of_le h₁ $ Nat.lt_succ.mp (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd.isLt
   if h₂ : index = 0 then by
     subst index
-    simp
+    simp only [Fin.val_zero]
     have := Fin.zero_eta.subst (motive := λx ↦ heap.root _ = get x heap _) $ get_zero_eq_root heap (Nat.succ_pos _)
-    rw[←this]
+    rewrite[←this]
     have :=  get_zero_eq_root (Internal.heapRemoveLastWithIndex heap).fst hn
-    rw[←this]
+    rewrite[←this]
     apply Eq.symm
     apply CompleteTree.AdditionalProofs.heapRemoveLastWithIndexLeavesRoot
   else by
@@ -906,25 +907,64 @@ protected theorem heapRemoveLastWithIndexRelationLt {α : Type u} {n : Nat} (hea
     split
     case isFalse h₄ =>
       --removed right
-      simp [h₄] at h₁ ⊢
+      simp only [h₄, ↓reduceDite, Fin.isValue] at h₁ ⊢
       cases p
       case zero =>
         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 =>
-        simp only [Fin.isValue] at h₁ ⊢
+      case succ pp _ _ _ _ =>
         if h₄ : index > o then
           --get goes into right branch -> recursion
-          rw[get_right' _ h₄]
-          sorry
+          rewrite[get_right' _ h₄]
+          have h₅ : (⟨index.val, hi⟩ : Fin (o + (pp+1))) > o := h₄
+          rewrite[get_right' _ h₅]
+          simp only [Nat.add_eq, Fin.isValue]
+          rewrite[Fin.lt_iff_val_lt_val] at h₁
+          have : ↑index - o - 1 < pp + 1 :=
+            hi
+            |> Nat.sub_lt_left_of_lt_add (n := o) (Nat.le_of_lt h₄)
+            |> (flip (Nat.sub_lt_of_lt_add)) (Nat.zero_lt_sub_of_lt h₄)
+            |> Nat.lt_succ_of_lt
+          have h₈ : ⟨↑index - o - 1, this⟩ < (Internal.heapRemoveLastWithIndex r).snd.snd :=
+            Nat.sub_lt_of_lt_add (b := o+1) h₁ h₅
+          exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt r  ⟨↑index - o - 1, this⟩ h₈
         else
           --get goes into left branch
-          sorry
+          have h₄₂ : index ≤ o := Nat.le_of_not_gt h₄
+          have h₂₂ : index > 0 := Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂
+          rewrite[get_left' _ h₂₂ h₄₂]
+          have h₅ : (⟨index.val, hi⟩ : Fin (o + (pp+1))) ≤ o := h₄₂
+          have h₆ : (⟨index.val, hi⟩ : Fin (o + (pp+1))) > ⟨0,Nat.succ_pos _⟩ := h₂₂
+          rw[get_left' _ h₆ h₅]
     case isTrue h₄ =>
       --removed left
-      simp [h₄] at h₁ ⊢
-      sorry
+      --get has to go into the square hole - erm, left branch too
+      cases o
+      case zero =>
+        exact absurd h₄.left $ Nat.not_lt_zero _
+      case succ oo _ _ _ _ =>
+        rewrite[Fin.lt_iff_val_lt_val] at h₁
+        simp only [Nat.add_eq, h₄, and_self, ↓reduceDite, Fin.isValue, Fin.val_succ,
+          Fin.coe_castLE] at h₁ ⊢
+        have h₂₂ : index > 0 := Nat.zero_lt_of_ne_zero $ Fin.val_ne_iff.mpr h₂
+        have h₆ := (Nat.add_comm_right oo 1 p).subst hi
+        have h₈ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) > ⟨0,Nat.succ_pos _⟩ := h₂₂
+        have h₇ : (⟨index.val, h₆⟩ : Fin (oo + p + 1)) ≤ oo := by
+          generalize (Internal.heapRemoveLastAux l (β := λn ↦ α × Fin n) _ _ _).2.snd = i at h₁
+          have a : i.val ≤ oo := Nat.le_of_lt_succ i.isLt
+          have b : index.val ≤ i.val := Nat.le_of_lt_succ h₁
+          exact Nat.le_trans b a
+        have h₅ : index ≤ oo+1 := Nat.le_succ_of_le h₇
+        rewrite[get_left' _ h₂₂ h₅]
+        rewrite[heapRemoveLastWithIndexRelationGt_Aux2]
+        case h₃ => exact Nat.succ_pos _
+        case h₄ => exact h₆
+        rewrite[get_left' _ h₈ h₇]
+        have : index.val - 1 < oo + 1 := Nat.sub_one_lt_of_le h₂₂ h₅
+        have h₉ : ⟨↑index - 1, this⟩ < (Internal.heapRemoveLastWithIndex l).snd.snd :=
+            Nat.sub_lt_of_lt_add h₁ h₂₂
+        exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationLt l ⟨↑index - 1, _⟩ h₉
 
 protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)):
   let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap