summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith (unfollow)
Commit message (Collapse)AuthorFilesLines
2024-06-22Improve `scalar_tac` and `scalar_decr_tac` (#256)Son HO2-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
2024-06-21Add some proofs for the Lean backend (#255)Son HO3-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>
2024-06-17Make a minor cleanupSon Ho1-9/+11
2024-06-13Update Lean to v4.9.0-rc1Son Ho3-10/+11
2024-06-12Deactivate the coercion from Nat to ScalarSon Ho1-0/+10
2024-06-12Add the Simp.Config to the simp wrappersSon Ho2-27/+26
2024-06-12backends/lean: introduce `HasIntPred` automationRyan Lahfa1-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>
2024-06-11feat: `PropHasImp` can have `Sort u` as premissesRyan Lahfa1-1/+1
This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
2024-05-24Update scalar_tac to use omega instead of linarithSon Ho3-98/+66
2024-04-05Update the lean toolchain and fix the proofsSon Ho1-1/+0
2024-03-08Update the handling of notations like #u32 or #isizeSon Ho1-1/+1
2024-01-26Improve the Lean backendSon Ho1-2/+9
2023-10-17Refold the scalar types when applying progressSon Ho2-3/+3
2023-10-17Implement tactics for termination proofs which involve arithmeticSon Ho3-0/+34
2023-09-18Improve scalar_tacSon Ho2-5/+20
2023-09-14Update to Lean 4.0.0 and fix some broken proofsSon Ho1-1/+1
2023-08-04Start adding support for Arrays/Slices in the Lean librarySon Ho2-10/+25
2023-07-26Update the syntax of the progress tacticSon Ho2-2/+2
2023-07-25Make progress on the proofs of the hashmapSon Ho1-0/+1
2023-07-25Make progress on the hashmap propertiesSon Ho3-1/+8
2023-07-25Improve int_tac and scalar_tacSon Ho2-10/+59
2023-07-20Make some proofs in Hashmap/Properties.lean and improve progressSon Ho1-1/+1
2023-07-19Improve progressSon Ho1-8/+0
2023-07-18Move an arithmetic lemmaSon Ho1-0/+6
2023-07-17Reorganize the Lean backendSon Ho3-329/+284
2023-07-17Move a definitionSon Ho1-3/+0
2023-07-13Update a commentSon Ho1-2/+1
2023-07-13Add IList.leanSon Ho2-64/+112
2023-07-12Improve progress to use assumptions and start working on a nice syntaxSon Ho1-41/+1
2023-07-12Improve the handling of arithmetic boundsSon Ho1-2/+6
2023-07-12Finish a first version of the progress tacticSon Ho1-93/+29
2023-07-11Work on the progress tacticSon Ho1-13/+29
2023-07-10Start working on the progress tacticSon Ho2-0/+419
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 09:45:11 +0000