aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAgeFilesLines
* Fix compilation with Lean 4.10.Andreas Grois2024-08-139-102/+92
|
* heapPopOnlyRemovesRoot is finally doneAndreas Grois2024-08-133-566/+83
|
* Finish heapRemoveLastWithIndexRelation. That was a piece of work...Andreas Grois2024-08-121-22/+62
|
* Start heapRemoveLastWithIndexRelationLtAndreas Grois2024-08-121-1/+51
|
* Continue heapRemoveLastWithIndexRelation.Andreas Grois2024-08-114-6/+19
| | | | Case for index equal removed index.
* Finish heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-112-52/+84
| | | | | | and optimize it a bit. All that omega and simp was really increasing compilation time... So, a lot of smaller proofs in that function are now done by hand instead.
* Continue heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-102-23/+84
|
* continue heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-101-10/+23
|
* Continue on heapRemoveLastWithIndexRelationAndreas Grois2024-08-094-12/+40
|
* First branch of heapRemoveLastWithIndexRelationGtAndreas Grois2024-08-091-5/+19
|
* heapRemoveLastWithIndexRelation - continuedAndreas Grois2024-08-082-54/+89
|
* MinorAndreas Grois2024-08-081-0/+6
|
* Unfinished heapPop proof workAndreas Grois2024-08-082-0/+177
|
* heapPopReturnsRootAndreas Grois2024-08-044-3/+29
|
* Update TODOAndreas Grois2024-08-041-19/+9
|
* heapUpdateRootContainsUpdatedElementAndreas Grois2024-08-041-0/+38
|
* Finish heapUpdateRootOnlyUpdtesRoot.Andreas Grois2024-08-041-5/+37
|
* Continue heapUpdateRootOnlyUpdatesRootAndreas Grois2024-08-041-1/+12
|
* Continue HeapUpdateRootOnlyUpdatesRoot. Left side finished.Andreas Grois2024-08-042-6/+79
|
* OopsAndreas Grois2024-08-031-0/+48
|
* Partial proof that HeapUpdateRoot only changes the root.Andreas Grois2024-08-032-1/+2
|
* Proves about heapRemoveLast.Andreas Grois2024-08-022-3/+93
|
* Split AdditionalProofs into several files.Andreas Grois2024-08-013-827/+826
|
* Split HeapProofs into several smaller files.Andreas Grois2024-07-319-687/+702
|
* Update TODO fileAndreas Grois2024-07-301-6/+3
|
* Finish heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-301-8/+130
| | | | | It could use some cleanup though. Compiling it takes quite long already...
* Minor progress on heapRemoveLastWithIndexOnlyRemovesOneElementAndreas Grois2024-07-301-5/+109
|
* Finish left half of heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-281-30/+69
|
* Continue heapRemoveLastWithIndexOnlyRemovesOneElement. Progress!Andreas Grois2024-07-282-28/+19
|
* Minor, some trial and error.Andreas Grois2024-07-282-8/+59
|
* Continue heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-281-11/+35
| | | | One of 4 branches done.
* Continue on heapRemoveLastWithIndexOnlyRemovesOneElement.Andreas Grois2024-07-281-22/+53
|
* Progress?Andreas Grois2024-07-271-3/+34
|
* Continue heapRemoveLastWithIndexOnlyRemovesOneElementAndreas Grois2024-07-272-14/+109
|
* Partial implementation of heapRemoveLastWithIndexOnlyRemovesOneElementAndreas Grois2024-07-265-12/+79
|
* Finish contains_iff_index_existsAndreas Grois2024-07-252-10/+92
|
* Start contains_iff_index_exists implementation. Unfinished.Andreas Grois2024-07-246-35/+190
|
* Fix performance issue in CompleteTree.contains.Andreas Grois2024-07-241-6/+7
|
* Minor: Fix indentation. Sorry.Andreas Grois2024-07-241-12/+12
|
* Add CompleteTree.contains. Decidable Predicate.Andreas Grois2024-07-241-0/+28
| | | | This is a preparation step for additional proofs.
* Add CompleteTree/AdditionalOperations.lean for non-heap operations.Andreas Grois2024-07-234-48/+53
|
* Split code in multiple source files. Separate proofs and logic.Andreas Grois2024-07-239-1148/+1220
|
* Add GetElem instances.Andreas Grois2024-07-222-14/+43
|
* Initial commit.Andreas Grois2024-07-2211-0/+1543
generated by cgit v1.2.3 (git 2.46.0) at 2025-11-04 20:15:34 +0000