heapPopReturnsRoot

4 files changed, 29 insertions, 3 deletions

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs.lean b/BinaryHeap/CompleteTree/AdditionalProofs.lean
index 1050dba..75d40fc 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs.lean
@@ -1,3 +1,4 @@
 import BinaryHeap.CompleteTree.AdditionalProofs.Contains
 import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast
 import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateRoot
+import BinaryHeap.CompleteTree.AdditionalProofs.HeapPop
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
new file mode 100644
index 0000000..521b598
--- /dev/null
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
@@ -0,0 +1,25 @@
+import BinaryHeap.CompleteTree.HeapOperations
+import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast
+import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateRoot
+
+namespace BinaryHeap.CompleteTree.AdditionalProofs
+
+theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le : α → α → Bool) : (tree.heapPop le).snd = tree.root (Nat.succ_pos n) := by
+  unfold heapPop
+  split
+  <;> simp only
+  case isFalse h₁ =>
+    unfold Internal.heapRemoveLast Internal.heapRemoveLastAux
+    split
+    rename_i n m v l r _ _ _
+    have h₂ : 0 = n + m := Eq.symm $  Nat.eq_zero_of_le_zero $ Nat.le_of_not_gt h₁
+    simp only [h₂, ↓reduceDite, id_eq, root_unfold]
+    have : n = 0 := And.left $ Nat.add_eq_zero.mp h₂.symm
+    subst n
+    have : m = 0 := And.right $ Nat.add_eq_zero.mp h₂.symm
+    subst m
+    rfl
+  case isTrue h₁ =>
+    have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexLeavesRoot tree h₁
+    have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree tree
+    simp only [h₃, heapUpdateRootReturnsRoot, h₂]
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index 5396d7f..375907a 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -84,7 +84,7 @@ protected theorem heapRemoveLastWithIndexReturnsItemAtIndex {α : Type u} {o : N
         apply AdditionalProofs.heapRemoveLastWithIndexReturnsItemAtIndex
         done
 
-private theorem heapRemoveLastWithIndexLeavesRoot {α : Type u} {n: Nat} (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.succ_pos n) = (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.root h₁ :=
+protected theorem heapRemoveLastWithIndexLeavesRoot {α : Type u} {n: Nat} (heap : CompleteTree α (n+1)) (h₁ : n > 0) : heap.root (Nat.succ_pos n) = (CompleteTree.Internal.heapRemoveLastWithIndex heap).fst.root h₁ :=
   CompleteTree.heapRemoveLastAuxLeavesRoot heap _ _ _ h₁
 
 private theorem lens_see_through_cast {α : Type u} {p q : Nat} (h₁ : q+p+1 = q+1+p) (len : {n : Nat} → CompleteTree α n → (n > 0) → Nat) (heap : CompleteTree α (q+p+1)) (ha : q+p+1 > 0) (hb : q+1+p > 0): len heap ha = len (h₁▸heap) hb:= by
@@ -553,7 +553,7 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n
       clear del1 del2
       left
       have h₃ := heqSameRoot he h₂ heq
-      have h₄ := heapRemoveLastWithIndexLeavesRoot ((branch v l r m_le_n max_height_difference subtree_complete)) h₂
+      have h₄ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexLeavesRoot ((branch v l r m_le_n max_height_difference subtree_complete)) h₂
       rw[←h₄] at h₃
       rw[root_unfold] at h₃
       rw[root_unfold] at h₃
diff --git a/TODO b/TODO
index 3f08bcd..b5e7d4f 100644
--- a/TODO
+++ b/TODO
@@ -14,7 +14,7 @@ This is a rough outline of upcoming tasks:
 [x] Prove that CompleteTree.heapUpdateRoot indeed exchanges the value at the root.
     - Done by showing that the new tree contains all elements except the root, and the updated value.
 [ ] Prove that heapPop leaves all values in the tree, except the root.
-[ ] Prove that heapPop returns the root
+[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.
     - Use the same approach as heapUpdateRoot