Continue HeapUpdateRootOnlyUpdatesRoot. Left side finished.

2 files changed, 79 insertions, 6 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
index cbe36b5..3333f1f 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
@@ -1,12 +1,13 @@
 import BinaryHeap.CompleteTree.HeapOperations
 import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateRoot
 import BinaryHeap.CompleteTree.Lemmas
+import BinaryHeap.CompleteTree.AdditionalProofs.Contains
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
 -- That heapUpdateRootReturnsRoot is already proven in HeapProofs.HeapUpdateRoot
 
-theorem HeapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α → Bool) (tree : CompleteTree α n) (h₁ : n > 0) (index : Fin n) (h₂ : index ≠ ⟨0, h₁⟩) (value : α) : (tree.heapUpdateRoot le value h₁).fst.contains $ tree.get index h₁ := by
+theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α → Bool) (tree : CompleteTree α n) (h₁ : n > 0) (index : Fin n) (h₂ : index ≠ ⟨0, h₁⟩) (value : α) : (tree.heapUpdateRoot le value h₁).fst.contains $ tree.get index h₁ := by
   generalize h₃ : (get index tree h₁) = oldVal
   unfold get at h₃
   unfold heapUpdateRoot
@@ -40,9 +41,72 @@ theorem HeapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α �
         simp[this] at h₃ ⊢
         cases le value (l.root _) <;> simp
         case false =>
-
-          sorry
-        case true =>
-          --rewrite h₃ into l.contains oldVal somehow.
+          cases j
+          case zero =>
+            rw[heapUpdateRootReturnsRoot]
+            rw[get_zero_eq_root]
+            unfold get; simp only
+            rw[h₃, contains_as_root_left_right _ _ (Nat.succ_pos _)]
+            left
+            rw[root_unfold]
+          case succ jj h₄ =>
+            have h₅ : oo = 0 := by omega
+            have h₆ : jj < oo := Nat.lt_of_succ_lt_succ this
+            have h₆ : jj < 0 := h₅.subst h₆
+            exact absurd h₆ $ Nat.not_lt_zero jj
+        case true h₄ _ _ _ _ _=>
+          rw[contains_as_root_left_right _ _ h₄]
+          right
+          left
+          rewrite[contains_iff_index_exists']
+          exists ⟨j,this⟩
+      case succ pp _ _ _ _ _ _ _ _ =>
+        simp
+        if h : j < oo + 1 then
+          -- index was in l
+          simp only [h, ↓reduceDite] at h₃
+          split
+          case isTrue =>
+            simp
+            rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
+            right
+            left
+            rw[←h₃, contains_iff_index_exists', left_unfold]
+            exists ⟨j,h⟩
+          case isFalse =>
+            split
+            <;> rw[heapUpdateRootReturnsRoot]
+            case isTrue =>
+              -- l.root gets moved up
+              simp only
+              cases j
+              case zero =>
+                rw[get_zero_eq_root]
+                unfold get
+                simp only
+                rw[h₃, contains_as_root_left_right _ _ (Nat.succ_pos _)]
+                left
+                rw[root_unfold]
+              case succ jj _ =>
+                --recursion
+                rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
+                right
+                left
+                rw[←h₃, left_unfold]
+                have : oo + 1 < oo + 1 + pp + 1 + 1 := by simp_arith --termination
+                apply heapUpdateRootOnlyUpdatesRoot
+                apply Fin.ne_of_val_ne
+                simp only [Nat.add_one_ne_zero, not_false_eq_true]
+            case isFalse =>
+              -- r.root gets moved up
+              rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
+              right
+              left
+              simp only [left_unfold]
+              rw[←h₃, contains_iff_index_exists']
+              exists ⟨j, h⟩
+        else
+          -- index was in r
+          simp only [h, ↓reduceDite] at h₃
           sorry
-      case succ pp => sorry
+termination_by n
diff --git a/BinaryHeap/CompleteTree/Lemmas.lean b/BinaryHeap/CompleteTree/Lemmas.lean
index e7a7e7b..b37dda1 100644
--- a/BinaryHeap/CompleteTree/Lemmas.lean
+++ b/BinaryHeap/CompleteTree/Lemmas.lean
@@ -89,3 +89,12 @@ theorem HeapPredicate.leOrLeaf_transitive (h₁ : transitive_le le) : le a b →
   cases n <;> simp
   apply h₁ a b _
   exact ⟨h₂, h₃⟩
+
+theorem CompleteTree.get_zero_eq_root {α : Type u} {n : Nat} (tree : CompleteTree α n) (h₁ : n > 0): tree.root h₁ = tree.get ⟨0,h₁⟩ h₁ := by
+  unfold get
+  match n with
+  | nn+1 =>
+    unfold get'
+    split
+    case h_2 hx => exact absurd (Fin.mk.inj hx) (Nat.zero_ne_add_one _)
+    case h_1 => trivial