aeneas/backends/lean/Base/Arith, branch isabelle

Improve `scalar_tac` and `scalar_decr_tac` (#256)

2024-06-22T11:22:32Z

* 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)

2024-06-21T21:24:01Z

* 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 Co-authored-by: Son Ho

Make a minor cleanup

2024-06-17T04:26:43Z

Merge branch 'son/update-lean' into has-int-pred

2024-06-17T04:16:43Z

Update Lean to v4.9.0-rc1

2024-06-13T20:04:13Z

Merge branch 'main' into prop-has-imp-sort

2024-06-12T16:46:36Z

Deactivate the coercion from Nat to Scalar

2024-06-12T12:46:52Z

Add the Simp.Config to the simp wrappers

2024-06-12T12:45:58Z

backends/lean: introduce `HasIntPred` automation

2024-06-12T12:27:11Z

`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

feat: `PropHasImp` can have `Sort u` as premisses

2024-06-11T14:04:19Z

This makes it possible to have `InBounds ... : Type 1` for example as `x`. Signed-off-by: Ryan Lahfa