TODO


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

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
[ ] Prove that CompleteTree.heapRemoveLastWithIndex indeed removes the last element
    - This automatically serves as a proof for CompleteTree.heapRemoveLast, once it is shown that they
      yield the same tree
    - 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.
    - 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 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.
    - The Heap Property that has already been proven shows the rest.


[ ] Write the performance part of this file.