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

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.heapPush leaves all elements that were already in the heap in the heap.
[x] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same tree
[x] Prove that CompleteTree.heapRemoveLastWithIndex and CompleteTree.heapRemoveLast yield the same element
[x] Prove that CompleteTree.heapRemoveLastWithIndex only removes one element and leaves the rest unchanged
    [x] This automatically serves as a proof for CompleteTree.heapRemoveLast, once it is shown that they
      yield the same tree
    - Done by showing how indices relate between both trees.
[ ] Prove that if CompleteTree.indexOf returns some, CompleteTree.get with that result fulfills the predicate.
[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.
[x] Prove that heapPop leaves all values in the tree, except the root.
    - Current proof is not rigorous. Needs more work in the future.
[x] Prove that heapPop returns the root
[x] Prove that CompleteTree.heapUpdateAt returns the element at the given index
[x] Prove that CompleteTree.heapUpdateAt indeed updates the value at the given index.
    - Use the same approach as heapUpdateRoot
[x] Prove that CompleteTree.heapRemoveAt returns the element at the given index
[ ] Prove that CompleteTree.heapRemoveAt leaves all values in the tree except at the input index.


Stuff below is not scheduled to happen any time soon. Feel free to contribute though.
[ ] Make proofs that currently aren't rigorous rigorous.
    - For instance by using element counts instead of contains.
[ ] Write the performance part of this file.