heapUpdateAtOnlyUpdatesAt

4 files changed, 167 insertions, 5 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
index 10364d3..7dbe23d 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateAt.lean
@@ -25,7 +25,7 @@ theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
     case isTrue h => simp only [←hj, beq_iff_eq, Fin.mk.injEq, Nat.add_one_ne_zero] at h --contradiction
     case isFalse =>
       split
-      subst hj
+      subst hj -- and put it back, now that split succeeded.
       simp only [Nat.add_eq, Nat.succ_eq_add_one, Nat.pred_succ]
       split <;> simp only
       case isTrue h₂ =>
@@ -41,3 +41,136 @@ theorem heapUpdateAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
           simp only [Nat.not_le] at h₂
           simp only [leftLen_unfold, gt_iff_lt, h₂]
         apply heapUpdateAtReturnsElementAt
+
+theorem heapUpdatAtRootEqUpdateRoot {α : Type u} {le : α → α → Bool} : CompleteTree.heapUpdateAt le ⟨0, h₁⟩ = CompleteTree.heapUpdateRoot le := by
+  funext
+  unfold heapUpdateAt
+  rfl
+
+theorem heapUpdateAtContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (h₁ : n > 0) (value : α) (index : Fin n) : (heap.heapUpdateAt le index value h₁).fst.contains value := by
+  unfold heapUpdateAt
+  split
+  case isTrue h₂ =>
+    apply heapUpdateRootContainsUpdatedElement
+  case isFalse h₂ =>
+    split
+    rename_i o p v l r _ _ _ index h₁ h₂
+    cases le v value <;> dsimp
+    case false =>
+      split
+      <;> rewrite[contains_as_root_left_right _ _ (Nat.succ_pos _)]
+      <;> left
+      <;> rfl
+    case true =>
+      split
+      <;> rewrite[contains_as_root_left_right _ _ (Nat.succ_pos _)]
+      <;> right
+      case' isTrue =>
+        have : o < o+p+1 := Nat.lt_of_le_of_lt (Nat.le_add_right o p) (Nat.lt_succ_self (o+p)) --term
+        left
+        rewrite[left_unfold]
+      case' isFalse =>
+        have : p < o+p+1 := Nat.lt_of_le_of_lt (Nat.le_add_left p o) (Nat.lt_succ_self (o+p)) --term
+        right
+        rewrite[right_unfold]
+      all_goals
+        apply heapUpdateAtContainsValue
+termination_by n
+
+theorem heapUpdateAtOnlyUpdatesAt {α : Type u} {n : Nat} (le : α → α → Bool) (val : α) (heap : CompleteTree α n) (updateIndex : Fin n) (otherIndex : Fin n) (h₁ : n > 0) (h₂ : updateIndex ≠ otherIndex) : (heap.heapUpdateAt le updateIndex val h₁).fst.contains $ heap.get otherIndex h₁ :=
+  if h₃ : updateIndex = ⟨0, h₁⟩ then
+    have h₄ : otherIndex ≠ ⟨0, h₁⟩ := h₃.subst h₂.symm
+    heapUpdateRootOnlyUpdatesRoot le heap h₁ otherIndex h₄ val
+    |> heapUpdatAtRootEqUpdateRoot.substr (p := λx↦(x val heap h₁).fst.contains (heap.get otherIndex h₁))
+    |> h₃.substr (p := λx↦((heap.heapUpdateAt le x val h₁).fst.contains $ heap.get otherIndex h₁))
+  else if h₄ : otherIndex = ⟨0, h₁⟩ then by
+    subst h₄
+    rw[←get_zero_eq_root]
+    unfold heapUpdateAt
+    --cannot use h₃ here already - it makes split fail. So, splitting twice it is...
+    split
+    case isTrue h => exact absurd ((beq_iff_eq _ _).mp h) h₃
+    split
+    rename_i d1 d2 d3 d4 d5 o p v l r _ _ _ updateIndex _ _
+    clear d1 d2 d3 d4 d5
+    cases le v val <;> dsimp
+    case isFalse.true =>
+      -- v ≤ val -> current root smaller or equal, keep current root, move val down.
+      split
+      <;> simp only [gt_iff_lt, Nat.zero_lt_succ, contains_as_root_left_right]
+      <;> left
+      <;> rewrite[root_unfold]
+      <;> rw[root_unfold]
+    case isFalse.false =>
+      -- v > val -> repace current root by val, move current root down.
+      split
+      <;> simp only [gt_iff_lt, Nat.zero_lt_succ, contains_as_root_left_right]
+      <;> right
+      case' isTrue =>
+        left
+        rewrite[left_unfold]
+      case' isFalse =>
+        right
+        rewrite[right_unfold]
+      all_goals
+        rewrite[root_unfold]
+        apply heapUpdateAtContainsValue
+  else by
+    unfold heapUpdateAt
+    split
+    case isTrue hx => exact absurd ((beq_iff_eq _ _).mp hx) h₃
+    case isFalse =>
+      split
+      rename_i d1 d2 d3 d4 d5 o p v l r olep mhd stc index _ _
+      clear d1 d2 d3 d4 d5
+      cases le v val
+      <;> dsimp
+      -- here we don'treally care if v or val gets handed down. We recurse in any case.
+      -- we do care about the question if we go left or right though.
+      <;> split
+      all_goals
+        have h₄₂ : otherIndex > 0 := Fin.pos_iff_ne_zero.mpr h₄
+        rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
+        right
+      case false.isTrue h₅ | true.isTrue h₅ =>
+        if h₆ : otherIndex ≤ o then
+          have : otherIndex ≤ (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by simp only [leftLen_unfold, h₆]
+          rw[get_left _ _ (Nat.succ_pos _) h₄₂ this]
+          left
+          --rw[left_unfold]
+          have : o < o + p + 1 := Nat.lt_of_le_of_lt (Nat.le_add_right o p) (Nat.lt_succ_self (o+p))
+          apply heapUpdateAtOnlyUpdatesAt
+          simp only [ne_eq, Fin.mk.injEq]
+          exact (Nat.pred_ne_of_ne (Fin.pos_iff_ne_zero.mpr h₃) (Fin.pos_iff_ne_zero.mpr h₄)).mp $ Fin.val_ne_iff.mpr h₂
+        else
+          have : otherIndex > (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by rw[leftLen_unfold]; exact Nat.gt_of_not_le h₆
+          rw[get_right _ _ (Nat.succ_pos _) this]
+          right
+          --rw[right_unfold]
+          --rw[right_unfold]
+          simp only[leftLen_unfold]
+          rw[contains_iff_index_exists]
+          generalize (⟨↑otherIndex - o - 1, _⟩ : Fin _) = solution -- Allows to skip the annoying proof that Lean already has...
+          exists solution --also solves h.h₁ goal? Okay, I don't know why, but I won't complain.
+      case false.isFalse h₅ | true.isFalse h₅ =>
+        if h₆ : otherIndex ≤ o then
+          have : otherIndex ≤ (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by simp only [leftLen_unfold, h₆]
+          rw[get_left _ _ (Nat.succ_pos _) h₄₂ this]
+          left
+          --rw[left_unfold]
+          --rw[left_unfold]
+          rw[contains_iff_index_exists]
+          generalize (⟨↑otherIndex - 1, _⟩ : Fin _) = solution
+          exists solution
+        else
+          have h₆ : otherIndex > (branch v l r olep mhd stc).leftLen (Nat.succ_pos _) := by rw[leftLen_unfold]; exact Nat.gt_of_not_le h₆
+          rw[get_right _ _ (Nat.succ_pos _) h₆]
+          right
+          --rw[right_unfold]
+          have : p < o + p + 1 := Nat.lt_of_le_of_lt (Nat.le_add_left p o) (Nat.lt_succ_self (o+p))
+          apply heapUpdateAtOnlyUpdatesAt
+          simp only [ne_eq, Fin.mk.injEq]
+          --rw[leftLen_unfold]
+          have h₅ : index.val ≥ o + 1 := Nat.gt_of_not_le h₅
+          exact (Nat.sub_ne_of_ne h₅ h₆).mp $ Fin.val_ne_iff.mpr h₂
+termination_by n
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
index b50d8c5..295fcbd 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapUpdateAt.lean
@@ -1,5 +1,6 @@
 import BinaryHeap.CompleteTree.HeapOperations
 import BinaryHeap.CompleteTree.Lemmas
+import BinaryHeap.CompleteTree.NatLemmas
 import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateRoot
 
 namespace BinaryHeap.CompleteTree
diff --git a/BinaryHeap/CompleteTree/NatLemmas.lean b/BinaryHeap/CompleteTree/NatLemmas.lean
index 5733b21..d05fe50 100644
--- a/BinaryHeap/CompleteTree/NatLemmas.lean
+++ b/BinaryHeap/CompleteTree/NatLemmas.lean
@@ -190,3 +190,31 @@ theorem lt_of_add {a b c : Nat} : a + b < c → a < c ∧ b < c := by
     exact lt_of_add_left h₁
   case right =>
     exact lt_of_add_right h₁
+
+theorem pred_ne_of_ne {a b : Nat} (h₁ : a > 0) (h₂ : b > 0) : a ≠ b ↔ a - 1 ≠ b - 1 :=
+  Iff.intro
+    (λh₃ h₄ ↦
+      congrArg Nat.succ h₄
+      |> (Nat.succ_pred (Nat.ne_of_gt h₁)).subst (motive := λx ↦ x = b.pred.succ)
+      |> (Nat.succ_pred (Nat.ne_of_gt h₂)).subst
+      |> flip absurd h₃
+    )
+    (λh₃ h₄ ↦
+      h₄
+      |> (Nat.succ_pred (Nat.ne_of_gt h₁)).substr
+      |> (Nat.succ_pred (Nat.ne_of_gt h₂)).substr
+      |> Nat.succ.inj
+      |> flip absurd h₃
+    )
+
+theorem sub_ne_of_ne {a b c : Nat} (h₁ : a ≥ c) (h₂ : b ≥ c) : a ≠ b ↔ a - c ≠ b - c := by
+  induction c
+  case zero => rfl
+  case succ cc hc =>
+    rw[←Nat.sub_sub]
+    rw[←Nat.sub_sub]
+    have h₃ := (Nat.lt_of_succ_le h₁)
+    have h₄ := (Nat.lt_of_succ_le h₂)
+    have h₅ := hc (Nat.le_of_lt h₃) (Nat.le_of_lt h₄)
+    rw[h₅]
+    apply pred_ne_of_ne (Nat.sub_pos_of_lt h₃) (Nat.sub_pos_of_lt h₄)
diff --git a/TODO b/TODO
index b3fe842..6a07601 100644
--- a/TODO
+++ b/TODO
@@ -15,14 +15,14 @@ This is a rough outline of upcoming tasks:
 [x] Prove that heapPop leaves all values in the tree, except the root.
     - Current proof is not rigorous. Needs more work in the future.
 [x] Prove that heapPop returns the root
-[ ] Prove that CompleteTree.heapUpdateAt returns the element at the given index
-[ ] Prove that CompleteTree.heapUpdateAt indeed updates the value at the given index.
+[x] Prove that CompleteTree.heapUpdateAt returns the element at the given index
+[x] Prove that CompleteTree.heapUpdateAt indeed updates the value at the given index.
     - Use the same approach as heapUpdateRoot
 [ ] Prove that CompleteTree.heapRemoveAt returns the element at the given index
 [ ] Prove that CompleteTree.heapRemoveAt leaves all values in the tree except at the input index.
 
 
-Stuff below is not scheduled to happen any time soon.
+Stuff below is not scheduled to happen any time soon. Feel free to contribute though.
 [ ] Make proofs that currently aren't rigorous rigorous.
-    - For instance by using element counts instead of just contains.
+    - For instance by using element counts instead of contains.
 [ ] Write the performance part of this file.
\ No newline at end of file