summaryrefslogtreecommitdiff
path: root/Common
Commit message (Collapse)AuthorAgeFilesLines
* Day 17, part 1 (hopefully)Andreas Grois2024-12-224-11/+209
|
* Continue Day17Andreas Grois2024-12-214-0/+153
|
* Remove useless simp_wf tactic callsHEADmainAndreas Grois2024-12-171-1/+0
|
* Day 16 Part 2Andreas Grois2024-12-161-0/+42
|
* Begin Day16Andreas Grois2024-12-143-0/+20
|
* Day 14, Part 1.Andreas Grois2024-11-282-0/+14
|
* 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.
generated by cgit v1.2.3 (git 2.46.0) at 2026-05-06 15:09:49 +0000