From a4734cad1ef5f69cf9505c923eb2990c5403616c Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Mon, 22 Jul 2024 23:53:26 +0200 Subject: Add GetElem instances. --- BinaryHeap.lean | 26 ++++++++++++++++++++++++-- TODO | 31 +++++++++++++++++++------------ 2 files changed, 43 insertions(+), 14 deletions(-) diff --git a/BinaryHeap.lean b/BinaryHeap.lean index d61c4fe..cd0e63f 100644 --- a/BinaryHeap.lean +++ b/BinaryHeap.lean @@ -17,10 +17,10 @@ def new (α : Type u) {le : α → α → Bool} (h₁ : BinaryHeap.transitive_le } /-- Adds an element into a heap. O(log(n)) -/ -def push {α : Type u} {lt : α → α → Bool} {n : Nat} : α → BinaryHeap α lt n → BinaryHeap α lt (n+1) +def push {α : Type u} {le : α → α → Bool} {n : Nat} : α → BinaryHeap α le n → BinaryHeap α le (n+1) | elem, .mk tree valid wellDefinedLe => let valid := tree.heapPushIsHeap valid wellDefinedLe.left wellDefinedLe.right - let tree := tree.heapPush lt elem + let tree := tree.heapPush le elem {tree, valid, wellDefinedLe} /-- Removes the smallest element from the heap and returns it. O(log(n)) -/ @@ -48,3 +48,25 @@ def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le (n+1) → (pred : α → Bool) → Option (Fin (n+1)) | {tree, valid := _, wellDefinedLe := _}, pred => tree.indexOf pred + +instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index > 0 ∧ index < n) where + getElem := λ heap index h₁ ↦ match n, heap, index with + | (_+1), {tree, ..}, index => tree.get ⟨index, h₁.right⟩ + +instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ n > 0) where + getElem := λ heap index _ ↦ match n, heap, index with + | (_+1), {tree, ..}, index => tree.get index + +/--Helper for the common case of using natural numbers for sorting.-/ +theorem nat_ble_to_heap_le_total : total_le Nat.ble := by + unfold total_le + simp only [Nat.ble_eq] + exact Nat.le_total + +/--Helper for the common case of using natural numbers for sorting.-/ +theorem nat_ble_to_heap_transitive_le : transitive_le Nat.ble := by + unfold transitive_le + intros a b c + repeat rw[Nat.ble_eq] + rw[and_imp] + exact Nat.le_trans diff --git a/TODO b/TODO index 3f2db67..382afc6 100644 --- a/TODO +++ b/TODO @@ -1,5 +1,7 @@ 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 + CompleteTree.get [ ] Prove that CompleteTree.heapUpdateAt returns the element at the given index [ ] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same tree [ ] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same element @@ -9,19 +11,24 @@ This is a rough outline of upcoming tasks: - A potential approach is to show that any index in the resulting tree can be converted into an index in the original tree (by adding one if it's >= the returned index of heapRemoveLastWithIndex), and getting elements from both trees. - - **EASIER**: Or just show that except for the n=1 case the value is unchanged. - The type signature proves the rest. + - Maybe easier: Or show that except for the n=1 case the value is unchanged. + The type signature proves the rest, so try, like induction maybe? [ ] Prove that if CompleteTree.indexOf returns some, CompleteTree.get with that result fulfills the predicate. -[ ] Prove that CompleteTree.heapUpdateRoot indeed removes the value at the root. - [x] A part of this is to show that the new root is not the old root, but rather the passed in value or - the root of one of the sub-trees. - [ ] The second part is to show that the recursion (if there is one) does not pass on the old root. - - Basically that heapUpdateRoot either does not recurse, or recurses with the value it started out with. - - This should be relatively straightforward. (left unchanged or left.heapUpdateRoot value and right - unchanged or right.heapUpdateRoot value) - [x] The last part would be to show that only one element gets removed - - Enforced by type signature. -[ ] Prove that CompleteTree.heapUpdateAt indeed removes the value at the given index. +[ ] Prove that CompleteTree.heapUpdateRoot indeed exchanges the value at the root. + - Straightforward, but hard to prove: + [ ] Show that for each index in the original heap (except 0) the element is now either the new root, or + in the left or in the right subtree. + - Maybe a new predicate? CompleteTree.contains x => root = x OR left.contains x OR right.contains x + - Try unfolding both functions like in heapRemoveLastWithIndexReturnsItemAtIndex. + - Alternative approach, but less convincing + [x] A part of this is to show that the new root is not the old root, but rather the passed in value or + the root of one of the sub-trees. + [ ] The second part is to show that the recursion (if there is one) does not pass on the old root. + - Basically that heapUpdateRoot either does not recurse, or recurses with the value it started out with. + - This should be relatively straightforward. (left unchanged or left.heapUpdateRoot value and right + unchanged or right.heapUpdateRoot value) +[ ] Prove that CompleteTree.heapUpdateAt indeed updates the value at the given index. + - Use contains again (if that works), or - Basically making sure that if index != 0 the recursion does either pass on the passed-in value, or the current node's value. - This sounds so trivial, that I am not sure if it's even worth the effort. -- cgit v1.2.3