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. --- TODO | 31 +++++++++++++++++++------------ 1 file changed, 19 insertions(+), 12 deletions(-) (limited to 'TODO') 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