diff options
author | Son HO | 2024-05-24 07:44:03 +0200 |
---|---|---|
committer | GitHub | 2024-05-24 07:44:03 +0200 |
commit | e713c3477f85cfe0eb691ac823b2702f58c8df16 (patch) | |
tree | 006d4fd760a13b49defbbfa698b8a37402f46219 /backends/lean/Base/Utils.lean | |
parent | 239435fc667fa0d18979e603ce3fd4caa128cd54 (diff) | |
parent | 721fbdd3eaf50f74e9c6dbc94b6811faa700127c (diff) |
Merge pull request #198 from AeneasVerif/son/omega
Update scalar_tac to use omega instead of linarith
Diffstat (limited to 'backends/lean/Base/Utils.lean')
-rw-r--r-- | backends/lean/Base/Utils.lean | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index eacfe72b..7ae5a832 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -658,6 +658,12 @@ example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by rename_i x y z exists x + y + z +/- Initialize a context for the `simp` function. + + The initialization of the context is adapted from `Tactic.elabSimpArgs`. + 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) : Tactic.TacticM Simp.Context := do -- Initialize either with the builtin simp theorems or with all the simp theorems @@ -689,7 +695,6 @@ def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) ( let congrTheorems ← getSimpCongrTheorems pure { simpTheorems := #[simpThms], congrTheorems } - inductive Location where /-- Apply the tactic everywhere. Same as `Tactic.Location.wildcard` -/ | wildcard @@ -725,11 +730,7 @@ where | some (_, mvarId) => replaceMainGoal [mvarId] return usedSimps -/- Call the simp tactic. - The initialization of the context is adapted from Tactic.elabSimpArgs. - 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. -/ +/- Call the simp tactic. -/ def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) (loc : Location) : Tactic.TacticM Unit := do @@ -738,6 +739,15 @@ def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hyp -- 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) + (loc : Tactic.Location) : + Tactic.TacticM Unit := do + -- Initialize the simp context + let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse + -- Apply the simplifier + dsimpLocation ctx loc + -- Call the simpAll tactic def simpAll (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) : Tactic.TacticM Unit := do |