From 7763a8ef8d5190fad39e9e677c5f44c536973655 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 12 Jun 2024 14:45:58 +0200 Subject: Add the Simp.Config to the simp wrappers --- backends/lean/Base/Arith/Int.lean | 6 ++-- backends/lean/Base/Arith/Scalar.lean | 47 +++++++++++++++---------------- backends/lean/Base/Progress/Progress.lean | 4 +-- backends/lean/Base/Utils.lean | 16 +++++------ 4 files changed, 36 insertions(+), 37 deletions(-) (limited to 'backends/lean') diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index 4a3db5f8..59cdca25 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -180,7 +180,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 +214,7 @@ 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) + Tactic.allGoals do tryTac (dsimpAt false {} [] [] [] Tactic.Location.wildcard) elab "int_tac_preprocess" : tactic => intTacPreprocess (do pure ()) @@ -231,7 +231,7 @@ def intTac (tacName : String) (splitGoalConjs : Bool) (extraPreprocess : Tactic -- 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)) + 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 linarith diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean index 86b2e216..c2e4e24e 100644 --- a/backends/lean/Base/Arith/Scalar.lean +++ b/backends/lean/Base/Arith/Scalar.lean @@ -8,30 +8,29 @@ open Lean Lean.Elab Lean.Meta open Primitives def scalarTacExtraPreprocess : Tactic.TacticM Unit := do - Tactic.withMainContext do - -- Inroduce the bounds for the isize/usize types - let add (e : Expr) : Tactic.TacticM Unit := do - let ty ← inferType e - let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false) - add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []]) - add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) - add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) - -- Reveal the concrete bounds, simplify calls to [ofInt] - Utils.simpAt true - -- Unfoldings - [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, - ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min, - ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max, - ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min, - ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max, - ``Usize.min - ] - -- Simp lemmas - [``Scalar.ofInt_val_eq, ``Scalar.neq_to_neq_val, - ``Scalar.lt_equiv, ``Scalar.le_equiv, ``Scalar.eq_equiv] - -- Hypotheses - [] .wildcard - + Tactic.withMainContext do + -- Inroduce the bounds for the isize/usize types + let add (e : Expr) : Tactic.TacticM Unit := do + let ty ← inferType e + let _ ← Utils.addDeclTac (← Utils.mkFreshAnonPropUserName) e ty (asLet := false) + add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []]) + add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) + add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) + -- Reveal the concrete bounds, simplify calls to [ofInt] + Utils.simpAt true {} + -- Unfoldings + [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, + ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min, + ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max, + ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min, + ``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max, + ``Usize.min + ] + -- Simp lemmas + [``Scalar.ofInt_val_eq, ``Scalar.neq_to_neq_val, + ``Scalar.lt_equiv, ``Scalar.le_equiv, ``Scalar.eq_equiv] + -- Hypotheses + [] .wildcard elab "scalar_tac_preprocess" : tactic => intTacPreprocess scalarTacExtraPreprocess diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index f2a56e50..39a48044 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -135,7 +135,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) Tactic.focus do let _ ← tryTac - (simpAt true [] + (simpAt true {} [] [``Primitives.bind_tc_ok, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div] [hEq.fvarId!] (.targets #[] true)) -- It may happen that at this point the goal is already solved (though this is rare) @@ -144,7 +144,7 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) else trace[Progress] "goal after applying the eq and simplifying the binds: {← getMainGoal}" -- TODO: remove this (some types get unfolded too much: we "fold" them back) - let _ ← tryTac (simpAt true [] scalar_eqs [] .wildcard_dep) + let _ ← tryTac (simpAt true {} [] scalar_eqs [] .wildcard_dep) trace[Progress] "goal after folding back scalar types: {← getMainGoal}" -- Clear the equality, unless the user requests not to do so let mgoal ← do diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 7ae5a832..6ee854cc 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -664,7 +664,7 @@ example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by Something very annoying is that there is no function which allows to initialize a simp context without doing an elaboration - as a consequence we write our own here. -/ -def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) : +def mkSimpCtx (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) : Tactic.TacticM Simp.Context := do -- Initialize either with the builtin simp theorems or with all the simp theorems let simpThms ← @@ -693,7 +693,7 @@ def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) ( throwError "Not a proposition: {thmName}" ) simpThms let congrTheorems ← getSimpCongrTheorems - pure { simpTheorems := #[simpThms], congrTheorems } + pure { config, simpTheorems := #[simpThms], congrTheorems } inductive Location where /-- Apply the tactic everywhere. Same as `Tactic.Location.wildcard` -/ @@ -731,28 +731,28 @@ where return usedSimps /- Call the simp tactic. -/ -def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) +def simpAt (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) (loc : Location) : Tactic.TacticM Unit := do -- Initialize the simp context - let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse + let ctx ← mkSimpCtx simpOnly config declsToUnfold thms hypsToUse -- Apply the simplifier let _ ← customSimpLocation ctx (discharge? := .none) loc /- Call the dsimp tactic. -/ -def dsimpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) +def dsimpAt (simpOnly : Bool) (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) (loc : Tactic.Location) : Tactic.TacticM Unit := do -- Initialize the simp context - let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse + let ctx ← mkSimpCtx simpOnly config declsToUnfold thms hypsToUse -- Apply the simplifier dsimpLocation ctx loc -- Call the simpAll tactic -def simpAll (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) : +def simpAll (config : Simp.Config) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) : Tactic.TacticM Unit := do -- Initialize the simp context - let ctx ← mkSimpCtx false declsToUnfold thms hypsToUse + let ctx ← mkSimpCtx false config declsToUnfold thms hypsToUse -- Apply the simplifier let _ ← Lean.Meta.simpAll (← getMainGoal) ctx -- cgit v1.2.3