From 084ae8e9fea7b92c72d0cee83590d32d98038f45 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Tue, 30 Jul 2024 22:39:00 +0200 Subject: Update TODO file --- TODO | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'TODO') diff --git a/TODO b/TODO index 5f8f446..c4ed7da 100644 --- a/TODO +++ b/TODO @@ -5,14 +5,11 @@ This is a rough outline of upcoming tasks: [ ] 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 only removes one element and leaves the rest unchanged +[x] Prove that CompleteTree.heapRemoveLastWithIndex only removes one element and leaves the rest unchanged - 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? + - Done by showing that each element of the input tree is in the output tree, except for the one at the + returned index. [ ] 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: -- cgit v1.2.3