diff options
| author | Son HO | 2024-06-21 23:24:01 +0200 |
|---|---|---|
| committer | GitHub | 2024-06-21 23:24:01 +0200 |
| commit | 4d30546c809cb2c512e0c3fd8ee540fff1330eab (patch) | |
| tree | d83926c9aa30f7bfb2a1c6db0e776003bca63355 /backends/lean/Base/Arith/Base.lean | |
| parent | f264b9dcc6331eb9149d951f308cdc61c8c02801 (diff) | |
Add some proofs for the Lean backend (#255)
* 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>
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Arith/Base.lean | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean index fb6b12e5..320b4b53 100644 --- a/backends/lean/Base/Arith/Base.lean +++ b/backends/lean/Base/Arith/Base.lean @@ -52,10 +52,6 @@ theorem int_pos_ind (p : Int → Prop) : rename_i m cases m <;> simp_all --- We sometimes need this to make sure no natural numbers appear in the goals --- TODO: there is probably something more general to do -theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp - -- This is mostly used in termination proofs theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) : ↑(x.toNat) < y := by @@ -68,4 +64,8 @@ theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ) have : 0 ≤ x := by omega simp [Int.toNat_sub_of_le, *] +-- WARNING: do not use this with `simp` as it might loop. The left-hand side indeed reduces to the +-- righ-hand side, meaning the rewriting can be applied to `n` itself. +theorem ofNat_instOfNatNat_eq (n : Nat) : @OfNat.ofNat Nat n (instOfNatNat n) = n := by rfl + end Arith |