summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Continue a bit on Day10 Part2Andreas Grois2024-09-101-17/+61
|
* Continue Day10 Part2Andreas Grois2024-09-093-6/+66
|
* Begin Day 10 Part 2Andreas Grois2024-09-081-11/+38
|
* Fix issue in Day10 Part1 end condition.Andreas Grois2024-09-081-1/+1
|
* Day 10 Part 1Andreas Grois2024-09-082-52/+76
|
* Begin implementing Day10 Part1Andreas Grois2024-09-082-34/+351
|
* Day 10 Parsing. If I don' want to prove the inverse, it's done.Andreas Grois2024-09-071-6/+100
|
* Parser for Day10, maybe done.Andreas Grois2024-09-053-14/+138
|
* Continue day10 input parsing proofsAndreas Grois2024-09-051-4/+80
|
* Contineu Area.ParseRaw_start_positionAndreas Grois2024-09-041-3/+19
|
* Unfinished rewrite of Area.parseAndreas Grois2024-09-041-45/+299
|
* First draft of input-parsing function for Day 10.Andreas Grois2024-09-022-1/+251
| | | | Fail to prove anything for it...
* Move BinaryHeap to its own Github project.Andreas Grois2024-09-015-1426/+4
|
* 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-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
|
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 15:46:10 +0000