Unfinished heapPop proof work

2 files changed, 177 insertions, 0 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
index 521b598..af03076 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
@@ -23,3 +23,41 @@ theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)
     have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexLeavesRoot tree h₁
     have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree tree
     simp only [h₃, heapUpdateRootReturnsRoot, h₂]
+
+theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index (Nat.succ_pos _) := by
+  unfold heapPop
+  split <;> simp
+  case isFalse h₃ => omega --contradiction. if n == 0 then index cannot be ≠ 0
+  case isTrue h₃ =>
+    if h₂ : index = (Internal.heapRemoveLastWithIndex tree).snd.snd then
+      have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex tree
+      rw[←h₂] at h₃
+      unfold get
+      simp only
+      have := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement tree
+      rw[←this] at h₃
+      simp[h₃, heapUpdateRootContainsUpdatedElement]
+    else
+      sorry
+
+
+theorem heapPopOnlyRemovesRoot2 {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index (Nat.succ_pos _) := by
+  unfold heapPop
+  have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastEitherContainsOrReturnsElement tree index
+  simp only at h₂
+  split <;> simp
+  case isFalse h₃ => omega --contradiction. if n == 0 then index cannot be ≠ 0
+  case isTrue h₃ =>
+    cases h₂
+    case inr h₂ =>
+      rw[h₂]
+      exact heapUpdateRootContainsUpdatedElement (Internal.heapRemoveLast tree).fst le (get index tree (Nat.succ_pos _)) h₃
+    case inl h₂ =>
+      generalize h₄ : (Internal.heapRemoveLast tree).fst = withoutLast
+      have h₅ := CompleteTree.AdditionalProofs.heapRemoveLastLeavesRoot tree h₃
+      rw[h₄] at h₂ h₅
+      have := heapUpdateRootOnlyUpdatesRoot le withoutLast h₃
+      rw[contains_iff_index_exists _ _ h₃] at h₂
+      -- to use h₂.elim we need to rewrite this into
+      -- ∀ (a : Fin n), get a withoutLast h₃ = get index tree ⋯ → something
+      sorry
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index 375907a..a505c91 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -701,3 +701,142 @@ protected theorem heapRemoveLastEitherContainsOrReturnsElement {α : Type u} {n
   rewrite[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement]
   rewrite[CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree]
   assumption
+
+protected theorem heapRemoveLastLeavesRoot {α : Type u} {n: Nat} (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.succ_pos n) = (CompleteTree.Internal.heapRemoveLast heap).fst.root h₁ :=
+  CompleteTree.heapRemoveLastAuxLeavesRoot heap _ _ _ h₁
+
+private theorem heapRemoveLastWithIndexIndexNeZeroForNGt1 {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) : (CompleteTree.Internal.heapRemoveLastWithIndex heap).snd.snd = 0 ↔ n = 0 := by
+  constructor
+  case mp =>
+    unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux
+    split
+    rename_i o p v l r _ _ _
+    split
+    case isTrue =>
+      intro
+      rename 0 = o + p => h₁
+      exact h₁.symm
+    case isFalse =>
+      intro h₁
+      simp at h₁
+      split at h₁
+      case isTrue =>
+        cases o; omega
+        case succ oo _ _ _ _ _ =>
+          simp at h₁
+          exact absurd h₁ $ Fin.succ_ne_zero _
+      case isFalse =>
+        simp at h₁
+        exact absurd h₁ $ Fin.succ_ne_zero _
+  case mpr =>
+    intro h₁
+    unfold Internal.heapRemoveLastWithIndex Internal.heapRemoveLastAux
+    split
+    rename_i o p v l r _ _ _
+    simp at h₁
+    simp[h₁]
+    have : o = 0 := And.left $ Nat.add_eq_zero_iff.mp h₁
+    subst o
+    have : p = 0 := And.right $ Nat.add_eq_zero_iff.mp h₁
+    subst p
+    rfl
+
+
+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)
+:= by
+have h₂ : 0 ≠ n := by omega
+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₁ ⊢
+split
+case isFalse h₃ =>
+  --removed right
+  simp[h₃] at h₁ ⊢
+  cases p <;> simp at h₁ ⊢
+  case zero =>
+    simp (config := {ground := true}) at h₃
+    subst o
+    contradiction
+  case succ pp _ _ _ _ =>
+    generalize hold : get index (branch v l r _ _ _) _ = oldValue
+    unfold get at hold ⊢
+    simp at hold ⊢
+    unfold get' at hold ⊢
+    split
+    <;> split at hold
+    case h_1.h_1 =>
+      exact absurd h₁ $ Fin.not_lt_zero _
+    case h_1.h_2 j _ _ _ _ _ _ _ _ _ _ _ _ _ hj =>
+      have h₃ : j = 0 := by simp at hj; exact Fin.val_eq_of_eq hj
+      subst j
+      simp at h₁
+      have := Fin.lt_iff_val_lt_val.mp h₁
+      simp_arith at this
+    case h_2.h_1 hx =>
+      contradiction
+    case h_2.h_2 j2 h₃2 or pr vr lr rr _ _ _ d3 he3 he4 j h₃ o2 p2 v2 l2 r2 _ _ _ d2 he1 he2 d1 hje =>
+      clear d2 d3
+      have : j = j2 + 1 := by simp at hje; assumption
+      subst j
+      have : o = o2 := heqSameLeftLen (congrArg Nat.succ he1) (by omega) he2
+      have : (pp+1) = p2 := heqSameRightLen (congrArg Nat.succ he1) (by omega) he2
+      subst o2 p2
+      simp at he2
+      have := he2.left
+      have := he2.right.left
+      have := he2.right.right
+      subst v2 l2 r2
+      have : o = or := heqSameLeftLen (congrArg Nat.succ he3) (by omega) he4
+      have : (pp + 1 - 1) = pr := heqSameRightLen (congrArg Nat.succ he3) (by omega) he4
+      subst or pr
+      simp at he4
+      have := he4.left
+      have := he4.right.left
+      subst lr vr
+      simp at he4
+      have : ¬j2 + 1 < o := by simp_arith[Fin.lt_iff_val_lt_val] at h₁; omega
+      simp[this] at hold
+      have : ¬j2 < o := by simp_arith[Fin.lt_iff_val_lt_val] at h₁; omega
+      simp[this]
+      --cases pp
+      --omega
+      split
+      rename_i d2 d3 d4 d5 d6 d7 d8
+      clear d2 d3 d4 d5 d6 d7 d8 hje d1
+      rename_i d2 d3 d4 d5 d6 d7 d8 d9 h₆2 pp2 rr2 _ _ _ h₂ h₅ d1 h₆ he6 he5
+      clear d1 d2 d3 d4 d5 d6 d7 d8 d9 h₆2
+      simp at he6
+      subst he6
+      simp at he5
+      subst rr2
+      sorry
+case isTrue h₃ =>
+  --removed left
+  sorry
+
+protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)):
+  let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap
+  if h₁ : index > oldIndex then
+    have : oldIndex ≥ 0 := Fin.zero_le oldIndex
+    have : index > 0 := by omega
+    result.get (index.pred $ Fin.ne_of_gt this) (by omega) = heap.get index (by omega)
+  else if h₂ : index < oldIndex then
+    result.get (index.castLT (by omega)) (by omega) = heap.get index (by omega)
+  else
+    removedElement = heap.get index (Nat.succ_pos _)
+:= by
+  simp
+  split
+  case isTrue h₁ =>
+    apply CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt
+    assumption
+  split
+  case isFalse.isTrue h₁ h₂ => sorry
+  case isFalse.isFalse h₁ h₂ => sorry