Finish left half of heapRemoveLastWithIndexOnlyRemovesOneElement.

1 files changed, 69 insertions, 30 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean
index 8ef5473..442c2d3 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean
@@ -324,7 +324,7 @@ private theorem left_sees_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 =
     assumption
 
 /--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength to allow splitting the goal-/
-private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength2 {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0)
+private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLengthAux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0)
 :
   let o := tree.leftLen'
   let p := tree.rightLen'
@@ -349,11 +349,11 @@ private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength2 {α : T
     rw[leftLen_unfold]
     rfl
 
-private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))
+private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))
 :
   (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.leftLen (Nat.lt_add_right p $ Nat.succ_pos o) = o
 := by
-  apply heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength2 (branch v l r h₁ h₂ h₃) (Nat.lt_add_right p $ Nat.succ_pos o)
+  apply heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLengthAux (branch v l r h₁ h₂ h₃) (Nat.lt_add_right p $ Nat.succ_pos o)
   unfold leftLen' rightLen'
   simp only [leftLen_unfold, rightLen_unfold]
   simp only [decide_eq_true_eq] at h₄
@@ -434,29 +434,43 @@ private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL {α : Type u}
   have h₅ : (branch v l r h₁ h₂ h₃).leftLen' > 0 := Nat.succ_pos o
   heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLAux _ _ h₅ h₄
 
-/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_AuxlIndexNe-/
-private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxlIndexNeAux {α : Type u} {n j : Nat} (tree : CompleteTree α (n+1)) (h₁ : (n+1) > 0) (h₂ : j < tree.leftLen h₁) (h₃ : j.succ < (n+1)) (h₄ : tree.rightLen' < tree.leftLen' ∧ ((tree.rightLen'+1).nextPowerOfTwo = tree.rightLen'+1 : Bool)) (h₅ : ⟨j.succ, h₃⟩ ≠ (Internal.heapRemoveLastWithIndex tree).2.snd) : ⟨j, h₂⟩ ≠ (heapRemoveLastWithIndex' (tree.left h₁) (Nat.zero_lt_of_lt h₂)).snd.snd := by
-  have h₆ := heapRemoveLastWithIndex'_unfold tree.left' $ Nat.zero_lt_of_lt h₂
-  split at h₆
-  rename_i d3 d2 d1 oo l o_gt_0 he1 he2 he3
-  clear d1 d2 d3
-  unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux at h₅
-  split at h₅
-  rename_i o2 p vv ll rr _ _ _
-  unfold left' rightLen' leftLen' at *
-  rw[left_unfold] at *
-  rw[leftLen_unfold, rightLen_unfold] at *
-  subst he1
-  simp at he2
-  subst he2
-  rw[h₆]
-  have : ¬ 0 = oo.succ + p := by omega
-  simp only [this, h₄, and_true, reduceDite] at h₅
-  rw[←Fin.val_ne_iff] at h₅ ⊢
-  simp at h₅
-  unfold Internal.heapRemoveLastWithIndex
+/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength to allow splitting the goal-/
+private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength2Aux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0)
+:
+  let o := tree.leftLen'
+  let p := tree.rightLen'
+  (h₂ : ¬(p < o ∧ ((p+1).nextPowerOfTwo = p+1 : Bool))) → (Internal.heapRemoveLastWithIndex tree).fst.leftLen h₁ = o
+:= by
+  simp only
+  intro h₂
+  unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux
+  split --finally
+  rename_i del1 del2 o p v l r o_le_p max_height_difference subtree_complete
+  clear del2 del1
+  unfold rightLen' leftLen' at h₂
+  simp only [leftLen_unfold, rightLen_unfold] at h₂
+  have h₄ : 0 ≠ o + p := Nat.ne_of_lt h₁
+  simp only [h₄, ↓reduceDite, h₂, decide_True, and_self]
+  cases p
+  case zero =>
+    have : decide ((0 + 1).nextPowerOfTwo = 0 + 1) = true := by simp (config := { ground := true }) only [decide_True, Nat.zero_add]
+    simp only [this, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂
+    exact absurd h₂.symm h₄
+  case succ pp =>
+    unfold leftLen'
+    simp[leftLen_unfold]
+    done
+
+private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength2 {α : Type u} {o p : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : ¬(p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool)))
+:
+  (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).fst.leftLen (Nat.lt_add_right p $ Nat.succ_pos o) = o + 1
+:= by
+  apply heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength2Aux (branch v l r h₁ h₂ h₃) (Nat.lt_add_right p $ Nat.succ_pos o)
+  unfold leftLen' rightLen'
+  simp only [leftLen_unfold, rightLen_unfold]
   assumption
 
+
 private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2Aux {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (h₁ : n > 0)
 :
   let o := tree.leftLen'
@@ -479,10 +493,8 @@ private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2Aux {α : Type
   -- okay, dealing with p.pred.succ is a guarantee for pain. "Stuck at solving universe constraint"
   cases p
   case zero =>
-    have : ((0 + 1).nextPowerOfTwo = 0 + 1) := by simp! (config := {ground := true})
-    have : decide ((0 + 1).nextPowerOfTwo = 0 + 1) = true := by simp[this]
-    simp[this] at h₃
-    simp at h₄
+    have : decide ((0 + 1).nextPowerOfTwo = 0 + 1) = true := by simp (config := { ground := true }) only [decide_True, Nat.zero_add]
+    simp only [this, and_true, Nat.not_lt, Nat.le_zero_eq] at h₃
     exact absurd h₃.symm h₄
   case succ pp =>
     simp at hi --whoa, how easy this gets if one just does cases p...
@@ -498,6 +510,29 @@ private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2 {α : Type u}
 :=
   heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2Aux (branch v l r h₁ h₂ h₃) (by omega) (Nat.succ_pos _) h₄
 
+/--Helper for heapRemoveLastWithIndexOnlyRemovesOneElement_AuxlIndexNe-/
+private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxlIndexNeAux {α : Type u} {n j : Nat} (tree : CompleteTree α (n+1)) (h₁ : (n+1) > 0) (h₂ : j < tree.leftLen h₁) (h₃ : j.succ < (n+1)) (h₄ : tree.rightLen' < tree.leftLen' ∧ ((tree.rightLen'+1).nextPowerOfTwo = tree.rightLen'+1 : Bool)) (h₅ : ⟨j.succ, h₃⟩ ≠ (Internal.heapRemoveLastWithIndex tree).2.snd) : ⟨j, h₂⟩ ≠ (heapRemoveLastWithIndex' (tree.left h₁) (Nat.zero_lt_of_lt h₂)).snd.snd := by
+  have h₆ := heapRemoveLastWithIndex'_unfold tree.left' $ Nat.zero_lt_of_lt h₂
+  split at h₆
+  rename_i d3 d2 d1 oo l o_gt_0 he1 he2 he3
+  clear d1 d2 d3
+  unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux at h₅
+  split at h₅
+  rename_i o2 p vv ll rr _ _ _
+  unfold left' rightLen' leftLen' at *
+  rw[left_unfold] at *
+  rw[leftLen_unfold, rightLen_unfold] at *
+  subst he1
+  simp at he2
+  subst he2
+  rw[h₆]
+  have : ¬ 0 = oo.succ + p := by omega
+  simp only [this, h₄, and_true, reduceDite] at h₅
+  rw[←Fin.val_ne_iff] at h₅ ⊢
+  simp at h₅
+  unfold Internal.heapRemoveLastWithIndex
+  assumption
+
 private theorem heapRemoveLastWithIndexOnlyRemovesOneElement_AuxlIndexNe {α : Type u} {o p j : Nat} (v : α) (l : CompleteTree α (o+1)) (r : CompleteTree α p) (h₁ : p ≤ (o+1)) (h₂ : (o+1) < 2 * (p + 1)) (h₃ : (o + 1 + 1).isPowerOfTwo ∨ (p + 1).isPowerOfTwo) (h₄ : j < o+1) (h₅ : p < (o+1) ∧ ((p+1).nextPowerOfTwo = p+1 : Bool)) (h₆ : ⟨j.succ, (by omega)⟩ ≠ (Internal.heapRemoveLastWithIndex (branch v l r h₁ h₂ h₃)).2.snd) : ⟨j,h₄⟩ ≠ (Internal.heapRemoveLastWithIndex l).snd.snd :=
   --splitting at h₅ does not work. Probably because we have o+1...
   --helper function it is...
@@ -544,14 +579,18 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n
       let rightIsFull : Bool := ((p + 1).nextPowerOfTwo = p + 1)
       if h₅ : p < oo + 1 ∧ rightIsFull then
         have h₆ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL v l r ht1 ht2 ht3 h₅
-        have h₇ := heapRemoveLastWithIndexOnlyRemovesOneElement_Auxllength v l r ht1 ht2 ht3 h₅
+        have h₇ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength v l r ht1 ht2 ht3 h₅
         have h₈ := heqContains h₇ h₆
         rw[h₈]
         have h₉ : ⟨j,j_lt_o⟩ ≠ (Internal.heapRemoveLastWithIndex l).snd.snd := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxlIndexNe v l r ht1 ht2 ht3 j_lt_o h₅ h₁
         exact CompleteTree.AdditionalProofs.heapRemoveLastWithIndexOnlyRemovesOneElement _ _ h₉
       else
         have h₆ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxL2 v l r ht1 ht2 ht3 h₅
-        sorry
+        have h₇ := heapRemoveLastWithIndexOnlyRemovesOneElement_AuxLLength2 v l r ht1 ht2 ht3 h₅
+        have h₈ := heqContains h₇ h₆
+        rw[h₈]
+        rw[contains_iff_index_exists _ _ (Nat.succ_pos oo)]
+        exists ⟨j, j_lt_o⟩
     case isFalse j_ge_o =>
       split
       rename_i p  d1 d2 d3 d4 d5 h₆ pp r _ _ _ h₄ h₅