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 Co-authored-by: Son Ho --- backends/lean/Base/Arith/Int.lean | 48 +++++++++++++++++++++++++++++++++------ 1 file changed, 41 insertions(+), 7 deletions(-) (limited to 'backends/lean/Base/Arith/Int.lean') 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 -- cgit v1.2.3