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>

1 files changed, 41 insertions, 7 deletions

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 068d6f2f..b1927cfd 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -3,6 +3,7 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
+import Mathlib.Tactic.Ring.RingNF
 import Base.Utils
 import Base.Arith.Base
 
@@ -111,7 +112,7 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact
   let hs := HashSet.empty
   -- Explore the declarations
   let decls ← ctx.getDecls
-  let hs ← decls.foldlM (fun hs d => do 
+  let hs ← decls.foldlM (fun hs d => do
     -- Collect instances over all subexpressions in the context.
     -- Note that we explore the *type* of the local declarations: if we have
     -- for instance `h : A ∧ B` in the context, the expression itself is simply
@@ -154,7 +155,7 @@ def lookupHasIntPred (e : Expr) : MetaM (Option Expr) :=
   lookupProp "lookupHasIntPred" ``HasIntPred e (fun term => pure #[term]) (fun _ => pure #[])
 
 -- Collect the instances of `HasIntPred` for the subexpressions in the context
-def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do 
+def collectHasIntPredInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do
   collectInstancesFromMainCtx lookupHasIntPred
 
 -- Return an instance of `PropHasImp` for `e` if it has some
@@ -201,7 +202,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
     -- Add a declaration
     let nval ← Utils.addDeclTac name e type (asLet := false)
     -- Simplify to unfold the declaration to unfold (i.e., the projector)
-    Utils.simpAt true {} #[] [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
+    Utils.simpAt true {} [] [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
     -- Return the new value
     pure nval
 
@@ -214,7 +215,7 @@ def introHasIntPropInstances : Tactic.TacticM (Array Expr) := do
 elab "intro_has_int_prop_instances" : tactic => do
   let _ ← introHasIntPropInstances
 
-def introHasIntPredInstances : Tactic.TacticM (Array Expr) := do 
+def introHasIntPredInstances : Tactic.TacticM (Array Expr) := do
   trace[Arith] "Introducing the HasIntPred instances"
   introInstances ``HasIntPred.concl lookupHasIntPred
 
@@ -230,6 +231,8 @@ def introPropHasImpInstances : Tactic.TacticM (Array Expr) := do
 elab "intro_prop_has_imp_instances" : tactic => do
   let _ ← introPropHasImpInstances
 
+def intTacSimpRocs : List Name := [``Int.reduceNegSucc, ``Int.reduceNeg]
+
 /- Boosting a bit the `omega` tac.
  -/
 def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM Unit := do
@@ -244,7 +247,33 @@ def intTacPreprocess (extraPreprocess :  Tactic.TacticM Unit) : Tactic.TacticM U
   extraPreprocess
   -- Reduce all the terms in the goal - note that the extra preprocessing step
   -- might have proven the goal, hence the `Tactic.allGoals`
-  Tactic.allGoals do tryTac (dsimpAt false {} #[] [] [] [] Tactic.Location.wildcard)
+  let dsimp :=
+    Tactic.allGoals do tryTac (
+      -- We set `simpOnly` at false on purpose
+      dsimpAt false {} intTacSimpRocs
+        -- Declarations to unfold
+        []
+        -- Theorems
+        []
+        [] Tactic.Location.wildcard)
+  dsimp
+  -- More preprocessing: apply norm_cast to the whole context
+  Tactic.allGoals (Utils.tryTac (Utils.normCastAtAll))
+  -- norm_cast does weird things with negative numbers so we reapply simp
+  dsimp
+  -- We also need this, in case the goal is: ¬ False
+  Tactic.allGoals do tryTac (
+    Utils.simpAt true {}
+               -- Simprocs
+               intTacSimpRocs
+               -- Unfoldings
+               []
+                -- Simp lemmas
+                [``not_false_eq_true]
+                -- Hypotheses
+                []
+                (.targets #[] true)
+  )
 
 elab "int_tac_preprocess" : tactic =>
   intTacPreprocess (do pure ())
@@ -260,8 +289,6 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess :  Tactic
   -- Preprocess - wondering if we should do this before or after splitting
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
-  -- More preprocessing
-  Tactic.allGoals (Utils.tryTac (Utils.simpAt true {} #[] [] [``nat_zero_eq_int_zero] [] .wildcard))
   -- Split the conjunctions in the goal
   if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call omega
@@ -298,4 +325,11 @@ example (x y : Int) (h0: 0 ≤ x) (h1: x ≠ 0) (h2 : 0 ≤ y) (h3 : y ≠ 0) :
 example (a : Prop) (x : Int) (h0: 0 < x) (h1: x < 0) : a := by
   int_tac
 
+-- Intermediate cast through natural numbers
+example (a : Prop) (x : Int) (h0: (0 : Nat) < x) (h1: x < 0) : a := by
+  int_tac
+
+example (x : Int) (h : x ≤ -3) : x ≤ -2 := by
+  int_tac
+
 end Arith