summaryrefslogtreecommitdiff
path: root/Common
Commit message (Collapse)AuthorAgeFilesLines
* Day 13, Part 1Andreas Grois2024-11-251-0/+5
|
* Day 12 Part 1.Andreas Grois2024-09-241-0/+16
| | | | | God, I fell into the premature optimization trap here... But I'm glad I did, that should make part 2 way easier.
* Continue Day12Andreas Grois2024-09-233-0/+60
|
* Continue a bit with Day 11 Part 1Andreas Grois2024-09-191-3/+6
|
* Day 11 ParsingAndreas Grois2024-09-192-24/+99
|
* Continue Day11/ParsingAndreas Grois2024-09-182-0/+37
|
* Begin Day 11.Andreas Grois2024-09-181-0/+46
|
* Day 10, Part 2Andreas Grois2024-09-161-0/+9
|
* Continue Day10 Part2Andreas Grois2024-09-091-0/+11
|
* Begin implementing Day10 Part1Andreas Grois2024-09-081-0/+7
|
* Move BinaryHeap to its own Github project.Andreas Grois2024-09-012-1423/+0
|
* Heap: Nomenclature and namespace changes.Andreas Grois2024-07-211-25/+25
|
* Simplify CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndexAndreas Grois2024-07-211-78/+32
|
* 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-126-187/+183
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
|
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 17:36:53 +0000