summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Finish CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndexAndreas Grois2024-07-211-1/+105
|
* Heap: Unfinished proof RemoveLastWithIndex returns consistent data.Andreas Grois2024-07-201-0/+34
|
* Minor: Replace some simp by simp only in BinaryHeapAndreas Grois2024-07-201-57/+61
|
* Remove CompleteTree.indexOfLast, add CompleteTree.heapRemoveLastWithIndexAndreas Grois2024-07-201-60/+77
| | | | | indexOfLast was going through the tree the same way as heapRemoveLast did, so heapRemoveLast now can optionally compute the index.
* Heap: Further nomenclature improvements.Andreas Grois2024-07-191-28/+28
|
* Make CompleteTree.heapRemoveLast private.Andreas Grois2024-07-191-40/+38
| | | | | | | It's confusing, because it uses breadth-first indexing, and regular indices are depth-first. Also, it's not needed in the public API, as there is the removeAt function that can do the same.
* Heap: Nomenclature clarified. Push and Pop now do what is expected.Andreas Grois2024-07-191-111/+111
|
* Heap: Exchange return values of the remove/replace functions.Andreas Grois2024-07-191-56/+56
| | | | This makes it easier to extend them, due to the right-associativity of tuples.
* Factor out proofs of CompleteTree.popLast for readabilityAndreas Grois2024-07-191-52/+44
|
* Heap: Minor cleanup. Do a TODO.Andreas Grois2024-07-171-92/+68
|
* Finish BinaryHeap.RemoveAt.Andreas Grois2024-07-161-25/+119
| | | | There is still a helper in this that is very inefficient though...
* Continue on CompleteTree.heapReplaceElementAtIsHeap. Nearly done.Andreas Grois2024-07-151-13/+72
|
* Further work on heapReplaceElementAtIsHeapAndreas Grois2024-07-141-2/+23
|
* Continue at CompleteTree.heapReplaceElementAtIsHeapAndreas Grois2024-07-141-1/+22
|
* BinaryHeap.RemoveRoot added, and some proofs cleaned up a bitAndreas Grois2024-07-141-22/+26
|
* Finish CompleteTree.heapReplaceRootIsHeap.Andreas Grois2024-07-141-9/+42
|
* Continue proof for heapReplaceRootIsHeap (heapReplaceElementAtIsHeap)Andreas Grois2024-07-131-7/+56
|
* Squashed commit of the following:Andreas Grois2024-07-1210-192/+190
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | commit 7aeefe2e761a4892ff2f438e00f3ec7e6d286c5c Author: Andreas Grois <andi@grois.info> Date: Fri Jul 12 21:59:44 2024 +0200 Finish Lean 4.9 update. commit 8a5576ae983203035f6bf0c807b36f1b4d7b63a6 Author: Andreas Grois <andi@grois.info> Date: Fri Jul 12 21:40:21 2024 +0200 Lean 4.9 upgrade, heap is where it was before... commit db34881e21391c96a6a0b939552b0f6f77d05bd8 Author: Andreas Grois <andi@grois.info> Date: Fri Jul 12 00:31:22 2024 +0200 Further Lean 4.9 compat... commit 22444613d58c5bd1a3fcdad0cd6c8d3aee1f3214 Author: Andreas Grois <andi@grois.info> Date: Thu Jul 11 22:15:11 2024 +0200 Further Lean 4.9 porting commit a4ace32cbb02959f9625578b511c2486e0816367 Author: Andreas Grois <andi@grois.info> Date: Wed Jul 10 23:18:29 2024 +0200 Continue porting to Lean 4.9 commit d0f411bcc42b5cb7c72c2ed65ae35875c72e95dd Author: Andreas Grois <andi@grois.info> Date: Wed Jul 10 23:10:34 2024 +0200 Continue port to Lean 4.9 commit 835ce644b97840048de0df40676ff6f3a8b99985 Author: Andreas Grois <andi@grois.info> Date: Wed Jul 10 22:14:59 2024 +0200 Partial port to Lean 4.9. Not compiling yet.
* Continue on CompleteTree.heapReplaceElementAtIsHeapAndreas Grois2024-07-102-9/+217
|
* Finish CompleteTree.get implementation. Not proven to be correct yet.Andreas Grois2024-06-302-6/+15
|
* partial implementation of CompleteTree.getAndreas Grois2024-06-301-0/+18
|
* CompleteTree.replaceElementAt finished - now needs proofAndreas Grois2024-06-301-22/+40
|
* Partial implementation of CompleteTree.removeAtIndexAndreas Grois2024-06-302-3/+66
|
* CompleteTree.popLastIsHeap finished.Andreas Grois2024-06-291-2/+14
|
* Continue on popLast proof. popLastLeavesRoot finished.Andreas Grois2024-06-281-13/+59
|
* Continue on popLast validity proof. Still incomplete.Andreas Grois2024-06-271-5/+57
|
* Heap: Trivial part of popLastIsHeap proof.Andreas Grois2024-03-311-0/+16
|
* Make BinaryTree.PopLast function work with unfoldAndreas Grois2024-01-301-32/+34
| | | | at the cost of making it harder to read.
* Make Find function take a predicate. Simplify PopLast.Andreas Grois2024-01-251-27/+26
|
* Minor, rename wellDefinedLt to wellDefinedLeAndreas Grois2024-01-131-4/+4
|
* Change heap from less-than to less-than-or-equal.Andreas Grois2024-01-131-148/+83
| | | | | This not only simplifies the proofs, it also makes the structure easier to use.
* Fix Heap Insert preserves Heap Proof. Preconditions were wrong.Andreas Grois2024-01-131-18/+59
| | | | | | | | And with wrong I mean "unfulfillable if any elements in the heap should be equal to each other". I'm still not fully happy with this, as it relies on lt being compatible with Eq, but yeah, it works for now.
* Rename not_equal to antisymm, because that's what it is.Andreas Grois2024-01-101-7/+7
|
* (Finally) rename BalancedTree to CompleteTreeAndreas Grois2024-01-101-52/+52
|
* Implement actual BinaryHeap.insert function.Andreas Grois2024-01-101-0/+6
|
* Proof that heap insert preserves a heap is done!Andreas Grois2024-01-101-3/+73
|
* Heap.insert: Insert-Left is proven now.Andreas Grois2024-01-101-7/+45
|
* More progress on heap.insert proofAndreas Grois2024-01-091-8/+25
|
* Further progress on heap insert proof.Andreas Grois2024-01-081-12/+10
|
* Progress on the proof that heap.insert keeps the heap intact.Andreas Grois2024-01-081-0/+17
|
* Unfinished proof that insert keeps heap a heapAndreas Grois2024-01-051-31/+99
|
* Even more cleanup in HeapAndreas Grois2023-12-182-6/+6
|
* More cleanup of code in BinaryHeap.Andreas Grois2023-12-182-55/+61
| | | | | Finally the propositions about even and odd numbers are no longer decidable. Not that I accidentally use them in runtime code!
* Partial cleanup of HeapAndreas Grois2023-12-183-119/+119
|
* Heap now has balancing conditions completeAndreas Grois2023-12-181-18/+174
|
* Heap: At least one subtree needs to be perfect now.Andreas Grois2023-12-151-13/+113
|
* Rename file to BinaryHeap, as it isn't a BTreeAndreas Grois2023-12-132-30/+30
|
* BinTreeHeap: Add condition le m nAndreas Grois2023-12-121-19/+51
|
* Incomplete Heap implementation.Andreas Grois2023-12-115-8/+146
|
* Day9: Simplify proof of terminationAndreas Grois2023-12-091-1/+1
|
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 14:34:49 +0000