| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | partial implementation of CompleteTree.get | Andreas Grois | 2024-06-30 | 1 | -0/+18 |
| | | |||||
| * | CompleteTree.replaceElementAt finished - now needs proof | Andreas Grois | 2024-06-30 | 1 | -22/+40 |
| | | |||||
| * | Partial implementation of CompleteTree.removeAtIndex | Andreas Grois | 2024-06-30 | 2 | -3/+66 |
| | | |||||
| * | CompleteTree.popLastIsHeap finished. | Andreas Grois | 2024-06-29 | 1 | -2/+14 |
| | | |||||
| * | Continue on popLast proof. popLastLeavesRoot finished. | Andreas Grois | 2024-06-28 | 1 | -13/+59 |
| | | |||||
| * | Continue on popLast validity proof. Still incomplete. | Andreas Grois | 2024-06-27 | 1 | -5/+57 |
| | | |||||
| * | Heap: Trivial part of popLastIsHeap proof. | Andreas Grois | 2024-03-31 | 1 | -0/+16 |
| | | |||||
| * | Make BinaryTree.PopLast function work with unfold | Andreas Grois | 2024-01-30 | 1 | -32/+34 |
| | | | | | at the cost of making it harder to read. | ||||
| * | Make Find function take a predicate. Simplify PopLast. | Andreas Grois | 2024-01-25 | 1 | -27/+26 |
| | | |||||
| * | Minor, rename wellDefinedLt to wellDefinedLe | Andreas Grois | 2024-01-13 | 1 | -4/+4 |
| | | |||||
| * | Change heap from less-than to less-than-or-equal. | Andreas Grois | 2024-01-13 | 1 | -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 Grois | 2024-01-13 | 1 | -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 Grois | 2024-01-10 | 1 | -7/+7 |
| | | |||||
| * | (Finally) rename BalancedTree to CompleteTree | Andreas Grois | 2024-01-10 | 1 | -52/+52 |
| | | |||||
| * | Implement actual BinaryHeap.insert function. | Andreas Grois | 2024-01-10 | 1 | -0/+6 |
| | | |||||
| * | Proof that heap insert preserves a heap is done! | Andreas Grois | 2024-01-10 | 1 | -3/+73 |
| | | |||||
| * | Heap.insert: Insert-Left is proven now. | Andreas Grois | 2024-01-10 | 1 | -7/+45 |
| | | |||||
| * | More progress on heap.insert proof | Andreas Grois | 2024-01-09 | 1 | -8/+25 |
| | | |||||
| * | Further progress on heap insert proof. | Andreas Grois | 2024-01-08 | 1 | -12/+10 |
| | | |||||
| * | Progress on the proof that heap.insert keeps the heap intact. | Andreas Grois | 2024-01-08 | 1 | -0/+17 |
| | | |||||
| * | Unfinished proof that insert keeps heap a heap | Andreas Grois | 2024-01-05 | 1 | -31/+99 |
| | | |||||
| * | Even more cleanup in Heap | Andreas Grois | 2023-12-18 | 2 | -6/+6 |
| | | |||||
| * | More cleanup of code in BinaryHeap. | Andreas Grois | 2023-12-18 | 2 | -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 Heap | Andreas Grois | 2023-12-18 | 3 | -119/+119 |
| | | |||||
| * | Heap now has balancing conditions complete | Andreas Grois | 2023-12-18 | 1 | -18/+174 |
| | | |||||
| * | Heap: At least one subtree needs to be perfect now. | Andreas Grois | 2023-12-15 | 1 | -13/+113 |
| | | |||||
| * | Rename file to BinaryHeap, as it isn't a BTree | Andreas Grois | 2023-12-13 | 2 | -30/+30 |
| | | |||||
| * | BinTreeHeap: Add condition le m n | Andreas Grois | 2023-12-12 | 1 | -19/+51 |
| | | |||||
| * | Incomplete Heap implementation. | Andreas Grois | 2023-12-11 | 5 | -8/+146 |
| | | |||||
| * | Day9: Simplify proof of termination | Andreas Grois | 2023-12-09 | 1 | -1/+1 |
| | | |||||
| * | Day 9 | Andreas Grois | 2023-12-09 | 4 | -18/+284 |
| | | |||||
| * | Fix Day 8 Part 2: Forgot to un-comment something. | Andreas Grois | 2023-12-09 | 1 | -2/+2 |
| | | | | | While it doesn't change the result, it was technically wrong. | ||||
| * | Day 8 Part 2 | Andreas Grois | 2023-12-09 | 5 | -17/+156 |
| | | |||||
| * | Not working Day8 Part 2. | Andreas Grois | 2023-12-08 | 2 | -21/+52 |
| | | | | | Seems we need to be smarter. | ||||
| * | Day 8 Part 1 | Andreas Grois | 2023-12-08 | 4 | -2/+893 |
| | | |||||
| * | Day 7 | Andreas Grois | 2023-12-08 | 8 | -0/+1243 |
| | | |||||
| * | Day 6 | Andreas Grois | 2023-12-07 | 3 | -9/+82 |
| | | |||||
| * | Allow error messages in parsing (for debugging) | Andreas Grois | 2023-12-07 | 10 | -33/+62 |
| | | | | | And fix an off-by-one in day 5 | ||||
| * | Part 2, finally | Andreas Grois | 2023-12-06 | 2 | -17/+66 |
| | | |||||
| * | Part of Day5 Part 2 | Andreas Grois | 2023-12-06 | 1 | -54/+105 |
| | | |||||
| * | Day5, part 1 | Andreas Grois | 2023-12-06 | 5 | -5/+475 |
| | | |||||
| * | Day 4 | Andreas Grois | 2023-12-04 | 4 | -0/+277 |
| | | | | | I'm particularly proud of part 2. | ||||
| * | Day 3: Fix swapped adjacents. | Andreas Grois | 2023-12-03 | 1 | -11/+11 |
| | | |||||
| * | Day 3, minor cleanup | Andreas Grois | 2023-12-03 | 1 | -31/+12 |
| | | |||||
| * | Day 3 | Andreas Grois | 2023-12-03 | 8 | -1/+319 |
| | | |||||
| * | Quicksort. Might be useful later. | Andreas Grois | 2023-12-03 | 2 | -0/+25 |
| | | |||||
| * | Day 2 | Andreas Grois | 2023-12-02 | 7 | -3/+208 |
| | | |||||
| * | Day 1 | Andreas Grois | 2023-12-01 | 10 | -0/+1165 |
 |
index : aoc-2023 | |
| Advent of Code 2023 - I'm still learning Lean4, so please don't judge. | Andreas Grois |
| summaryrefslogtreecommitdiff |