diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs.lean | 1 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean | 25 | ||||
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 4 | ||||
| -rw-r--r-- | TODO | 2 |
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₃ @@ -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 |