Add GetElem instances.

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.