heapPushContainsValue

3 files changed, 49 insertions, 1 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean
index 4ab43f0..4643be9 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean
@@ -4,3 +4,4 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateRoot
 import BinaryHeap.CompleteTree.AdditionalProofs.HeapPop
 import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateAt
 import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveAt
+import BinaryHeap.CompleteTree.AdditionalProofs.HeapPush
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
new file mode 100644
index 0000000..89557c1
--- /dev/null
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPush.lean
@@ -0,0 +1,47 @@
+import BinaryHeap.CompleteTree.HeapOperations
+import BinaryHeap.CompleteTree.AdditionalOperations
+import BinaryHeap.CompleteTree.AdditionalProofs.Contains
+
+namespace BinaryHeap.CompleteTree.AdditionalProofs
+
+private theorem containsSeesThroughCast {α : Type u} {o p : Nat} (heap : CompleteTree α (o + 1 + p + 1)) (h₁ : o + 1 + p + 1 = o + p + 2) : heap.contains = (h₁▸heap).contains := by
+  induction p generalizing o
+  case zero => rfl
+  case succ pp hp =>
+    have hp := hp (o := o + 1)
+    have : o + 1 + 1 + pp + 1 = o + 1 + (pp + 1) + 1 := by omega
+    rw[this] at hp
+    have : o + 1 + pp + 2 = o + (pp + 1) + 2 := by omega
+    rw[this] at hp
+    have hp := hp heap h₁
+    assumption
+
+theorem heapPushContainsValue {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α n) (val : α) : (heap.heapPush le val).contains val := by
+  unfold heapPush
+  split
+  case h_1 =>
+    rw[contains_as_root_left_right _ _ (Nat.succ_pos _),root_unfold]
+    left
+    rfl
+  case h_2 =>
+    rename_i o p v l r p_le_o max_height_difference subtree_complete
+    cases le val v
+    <;> dsimp
+    <;> split
+    case' true.isFalse | false.isFalse =>
+      rw[←containsSeesThroughCast]
+    case true.isTrue | true.isFalse =>
+      rw[contains_as_root_left_right _ _ (Nat.succ_pos _), root_unfold]
+      left
+      rfl
+    case' false.isTrue | false.isFalse =>
+      rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
+      right
+    case false.isTrue =>
+      right
+      rw[right_unfold]
+      exact heapPushContainsValue le r val
+    case false.isFalse =>
+      left
+      rw[left_unfold]
+      exact heapPushContainsValue le l val
diff --git a/TODO b/TODO
index 99bb92e..0d18880 100644
--- a/TODO
+++ b/TODO
@@ -1,6 +1,6 @@
 This is a rough outline of upcoming tasks:
 
-[ ] Prove that an index exists such that after CompleteTree.heapPush the pushed element can be obtained by
+[x] Prove that an index exists such that after CompleteTree.heapPush the pushed element can be obtained by
     CompleteTree.get
 [ ] Prove that CompleteTree.heapPush leaves all elements that were already in the heap in the heap.
 [x] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same tree