aoc-2023/Common/BinaryHeap.lean, branch main Advent of Code 2023 - I'm still learning Lean4, so please don't judge. https://git.grois.info/aoc-2023/atom/Common/BinaryHeap.lean?h=main 2024-08-31T22:03:28Z Move BinaryHeap to its own Github project. 2024-08-31T22:03:28Z Andreas Grois andi@grois.info 2024-08-31T22:03:28Z urn:sha1:539545228c4d78cc3fdbf369c3934ad27fd17b32 Heap: Nomenclature and namespace changes. 2024-07-21T17:21:02Z Andreas Grois andi@grois.info 2024-07-21T17:21:02Z urn:sha1:2b6a25a248d7e588cdef266d8d62f50568c5de10 Simplify CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex 2024-07-21T16:52:02Z Andreas Grois andi@grois.info 2024-07-21T16:52:02Z urn:sha1:feb2542732913a57aad8ce06d7923cb8d6d546b4 Finish CompleteTree.heapRemoveLastWithIndexReturnsItemAtIndex 2024-07-21T13:34:01Z Andreas Grois andi@grois.info 2024-07-21T13:34:01Z urn:sha1:0f19f8ee7578cded305dd309baa63c6de1f80f8e Heap: Unfinished proof RemoveLastWithIndex returns consistent data. 2024-07-20T17:45:13Z Andreas Grois andi@grois.info 2024-07-20T17:45:13Z urn:sha1:7b10e3e65abc1ed509872f64a8c1dcd890775f06 Minor: Replace some simp by simp only in BinaryHeap 2024-07-20T15:32:44Z Andreas Grois andi@grois.info 2024-07-20T15:32:44Z urn:sha1:e0faf20f446cbdb7723f2cc647c25590651815d6 Remove CompleteTree.indexOfLast, add CompleteTree.heapRemoveLastWithIndex 2024-07-19T22:10:13Z Andreas Grois andi@grois.info 2024-07-19T22:10:13Z urn:sha1:8659efb6bf0f3e21f0ab8d78e657739bc2238142 indexOfLast was going through the tree the same way as heapRemoveLast did, so heapRemoveLast now can optionally compute the index. Heap: Further nomenclature improvements. 2024-07-19T15:06:50Z Andreas Grois andi@grois.info 2024-07-19T15:06:50Z urn:sha1:b22f0f04c6fdf378a4c586cab657975f7d49f992 Make CompleteTree.heapRemoveLast private. 2024-07-19T15:03:45Z Andreas Grois andi@grois.info 2024-07-19T15:03:45Z urn:sha1:4d67d2e1597d1ed976fb4d1eb0062171925a45cb 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. 2024-07-19T14:45:09Z Andreas Grois andi@grois.info 2024-07-19T14:45:09Z urn:sha1:fa9074b17a6afc73cdf1854da222ba961fc1cc5c