summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO2024-06-222-17/+13
| | | | | | | * Fix an issue in a proof of the hashmap * Improve scalar_decr_tac * Improve the error message of scalar_tac and add the missing Termination.lean
* Add some proofs for the Lean backend (#255)Son HO2024-06-213-14/+54
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Make progress on the proofs of the hashmap * Make a minor modification to the hashmap * Make progress on the hashmap * Make progress on the proofs * Make progress on the proofs * Make progress on the proof of the hashmap * Progress on the proofs of the hashmap * Update a proof * Update the Charon pin * Make minor modifications to the hashmap * Regenerate the tests * Regenerate the hashmap * Add lemmas to the Lean backend * Make progress on the proofs of the hashmap * Make a minor fix * Finish the proof about the hashmap * Update scalar_tac * Make a minor modification in the hashmap * Update the proofs of the hashmap --------- Co-authored-by: Son Ho <sonho@Sons-MacBook-Pro.local> Co-authored-by: Son Ho <sonho@Sons-MBP.lan>
* Make a minor cleanupSon Ho2024-06-171-9/+11
|
* Merge branch 'son/update-lean' into has-int-predSon Ho2024-06-173-35/+45
|\
| * Update Lean to v4.9.0-rc1Son Ho2024-06-133-10/+11
| |
| * Merge branch 'main' into prop-has-imp-sortSon HO2024-06-122-27/+36
| |\
| | * Deactivate the coercion from Nat to ScalarSon Ho2024-06-121-0/+10
| | |
| | * Add the Simp.Config to the simp wrappersSon Ho2024-06-122-27/+26
| | |
| * | feat: `PropHasImp` can have `Sort u` as premissesRyan Lahfa2024-06-111-1/+1
| |/ | | | | | | | | | | | | This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* / backends/lean: introduce `HasIntPred` automationRyan Lahfa2024-06-121-5/+33
|/ | | | | | | | | | | | | `HasIntPred` enable generation of facts based on specific terms in the context rather than their types, e.g. if the "length of a list" occurs in the context, generate the fact 0 ≤ length of that list, which can be further used for `scalar_tac` automation to discharge bounds goals. The aim is to use it to simplify various height related computations, e.g. whenever "height of a (left ; right) tree" is encountered, generate "height left < height of a (left ; right) tree", etc. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
* Update scalar_tac to use omega instead of linarithSon Ho2024-05-243-98/+66
|
* Update the lean toolchain and fix the proofsSon Ho2024-04-051-1/+0
|
* Update the handling of notations like #u32 or #isizeSon Ho2024-03-081-1/+1
|
* Improve the Lean backendSon Ho2024-01-261-2/+9
|
* Refold the scalar types when applying progressSon Ho2023-10-172-3/+3
|
* Implement tactics for termination proofs which involve arithmeticSon Ho2023-10-173-0/+34
|
* Improve scalar_tacSon Ho2023-09-182-5/+20
|
* Update to Lean 4.0.0 and fix some broken proofsSon Ho2023-09-141-1/+1
|
* Start adding support for Arrays/Slices in the Lean librarySon Ho2023-08-042-10/+25
|
* Update the syntax of the progress tacticSon Ho2023-07-262-2/+2
|
* Make progress on the proofs of the hashmapSon Ho2023-07-251-0/+1
|
* Make progress on the hashmap propertiesSon Ho2023-07-253-1/+8
|
* Improve int_tac and scalar_tacSon Ho2023-07-252-10/+59
|
* Make some proofs in Hashmap/Properties.lean and improve progressSon Ho2023-07-201-1/+1
|
* Improve progressSon Ho2023-07-191-8/+0
|
* Move an arithmetic lemmaSon Ho2023-07-181-0/+6
|
* Reorganize the Lean backendSon Ho2023-07-173-329/+284
|
* Move a definitionSon Ho2023-07-171-3/+0
|
* Update a commentSon Ho2023-07-131-2/+1
|
* Add IList.leanSon Ho2023-07-132-64/+112
|
* Improve progress to use assumptions and start working on a nice syntaxSon Ho2023-07-121-41/+1
|
* Improve the handling of arithmetic boundsSon Ho2023-07-121-2/+6
|
* Finish a first version of the progress tacticSon Ho2023-07-121-93/+29
|
* Work on the progress tacticSon Ho2023-07-111-13/+29
|
* Start working on the progress tacticSon Ho2023-07-102-0/+419
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 08:04:36 +0000