From 4d30546c809cb2c512e0c3fd8ee540fff1330eab Mon Sep 17 00:00:00 2001
From: Son HO
Date: Fri, 21 Jun 2024 23:24:01 +0200
Subject: 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>---
 backends/lean/Base/Arith/Base.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'backends/lean/Base/Arith/Base.lean')

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
-- 
cgit v1.2.3

