feat: intermediate tactic info on simpa (#10309)
This PR modifies the `simpa` tactic so that in `simpa ... using e` there is tactic info on the range `simpa ... using` that shows the simplified goal.
This commit is contained in:
Kyle Miller
GitHub
parent
e75e6fbe9e
commit
1a203c7fe5
4 changed files with 114 additions and 75 deletions
|
|
@ -31,84 +31,93 @@ open Lean Parser.Tactic Elab Meta Term Tactic Simp Linter
|
|||
def getLinterUnnecessarySimpa (o : LinterOptions) : Bool :=
|
||||
getLinterValue linter.unnecessarySimpa o
|
||||
|
||||
deriving instance Repr for UseImplicitLambdaResult
|
||||
|
||||
@[builtin_tactic Lean.Parser.Tactic.simpa] def evalSimpa : Tactic := fun stx => do
|
||||
match stx with
|
||||
| `(tactic| simpa%$tk $[?%$squeeze]? $[!%$unfold]? $cfg:optConfig $(disch)? $[only%$only]?
|
||||
$[[$args,*]]? $[using $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
|
||||
$[[$args,*]]? $[using%$usingTk? $usingArg]?) => Elab.Tactic.focus do withSimpDiagnostics do
|
||||
let stx ← `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?)
|
||||
let { ctx, simprocs, dischargeWrapper, .. } ←
|
||||
withMainContext <| mkSimpContext stx (eraseLocal := false)
|
||||
let ctx := if unfold.isSome then ctx.setAutoUnfold else ctx
|
||||
-- TODO: have `simpa` fail if it doesn't use `simp`.
|
||||
let ctx := ctx.setFailIfUnchanged false
|
||||
dischargeWrapper.with fun discharge? => do
|
||||
let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs)
|
||||
(simplifyTarget := true) (discharge? := discharge?)
|
||||
| if getLinterUnnecessarySimpa (← getLinterOptions) then
|
||||
logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
|
||||
return {}
|
||||
g.withContext do
|
||||
let stats ← if let some stx := usingArg then
|
||||
let mvarCounterSaved := (← getMCtx).mvarCounter
|
||||
let e ← Tactic.elabTerm stx none (mayPostpone := true)
|
||||
unless ← occursCheck g e do
|
||||
throwError "Occurs check failed: Expression{indentExpr e}\ncontains the goal {Expr.mvar g}"
|
||||
-- Copy the goal. We want to defer assigning `g := g'` to prevent `MVarId.note` from
|
||||
-- partially assigning the goal in case we need to log unassigned metavariables.
|
||||
-- Without deferring, this can cause `logUnassignedAndAbort` to report that `g` could not
|
||||
-- be synthesized; recall that this function reports that a metavariable could not be
|
||||
-- synthesized if, after mvar instantiation, it contains one of the provided mvars.
|
||||
let gCopy ← mkFreshExprSyntheticOpaqueMVar (← g.getType) (← g.getTag)
|
||||
let (h, g') ← gCopy.mvarId!.note `h e
|
||||
let (result?, stats) ← simpGoal g' ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
|
||||
(simplifyTarget := false) (stats := stats) (discharge? := discharge?)
|
||||
match result? with
|
||||
| some (xs, g') =>
|
||||
let h := xs[0]?.getD h
|
||||
let name ← mkFreshUserName `h
|
||||
let g' ← g'.rename h name
|
||||
setGoals [g']
|
||||
g'.withContext do
|
||||
let gType ← g'.getType
|
||||
let h ← Term.elabTerm (mkIdent name) gType
|
||||
Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let hType ← inferType h
|
||||
unless (← withAssignableSyntheticOpaque <| isDefEq gType hType) do
|
||||
-- `e` still is valid in this new local context
|
||||
Term.throwTypeMismatchError gType hType h
|
||||
(header? := some m!"Type mismatch: After simplification, term{indentExpr e}\n")
|
||||
logUnassignedAndAbort (← filterOldMVars (← getMVars e) mvarCounterSaved)
|
||||
closeMainGoal `simpa (checkUnassigned := false) h
|
||||
| none =>
|
||||
if getLinterUnnecessarySimpa (← getLinterOptions) then
|
||||
if let .fvar h := e then
|
||||
if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
|
||||
logLint linter.unnecessarySimpa (← getRef)
|
||||
m!"Try `simp at {Expr.fvar h}` instead of `simpa using {Expr.fvar h}`"
|
||||
g.assign gCopy
|
||||
pure stats
|
||||
else if let some ldecl := (← getLCtx).findFromUserName? `this then
|
||||
if let (some (_, g), stats) ← simpGoal g ctx (simprocs := simprocs)
|
||||
(fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
|
||||
(discharge? := discharge?) then
|
||||
g.assumption; pure stats
|
||||
else
|
||||
pure stats
|
||||
else
|
||||
g.assumption; pure stats
|
||||
if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
|
||||
let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩)
|
||||
let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with
|
||||
| `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
|
||||
if unfold.isSome then
|
||||
`(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
let stats ← do
|
||||
let { ctx, simprocs, dischargeWrapper, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false)
|
||||
let ctx := if unfold.isSome then ctx.setAutoUnfold else ctx
|
||||
-- TODO: have `simpa` fail if it doesn't use `simp`.
|
||||
let ctx := ctx.setFailIfUnchanged false
|
||||
dischargeWrapper.with fun discharge? => do
|
||||
-- When there is a `using` clause we add tactic info showing the simplified goal.
|
||||
-- The span is `simpa ... using`.
|
||||
let mkInfo ← mkInitialTacticInfo (mkNullNode #[tk, usingTk?.getD .missing])
|
||||
let (some (_, g), stats) ← simpGoal (← getMainGoal) ctx (simprocs := simprocs) (simplifyTarget := true) (discharge? := discharge?)
|
||||
| if getLinterUnnecessarySimpa (← getLinterOptions) then
|
||||
logLint linter.unnecessarySimpa (← getRef) "try 'simp' instead of 'simpa'"
|
||||
return {}
|
||||
-- Replace the goal; captured by `mkInfo` in `using` case below.
|
||||
replaceMainGoal [g]
|
||||
g.withContext do
|
||||
if let some stx := usingArg then
|
||||
if (← getInfoState).enabled then
|
||||
let trees ← getResetInfoTrees
|
||||
withInfoContext (mkInfo := mkInfo) do
|
||||
-- Re-nest info trees so far into tactic info node
|
||||
modifyInfoState fun st => { st with trees }
|
||||
let mvarCounterSaved := (← getMCtx).mvarCounter
|
||||
let e ← Tactic.elabTerm stx none (mayPostpone := true)
|
||||
unless ← occursCheck g e do
|
||||
throwError "Occurs check failed: Expression{indentExpr e}\ncontains the goal {Expr.mvar g}"
|
||||
-- Copy the goal. We want to defer assigning `g := g'` to prevent `MVarId.note` from
|
||||
-- partially assigning the goal in case we need to log unassigned metavariables.
|
||||
-- Without deferring, this can cause `logUnassignedAndAbort` to report that `g` could not
|
||||
-- be synthesized; recall that this function reports that a metavariable could not be
|
||||
-- synthesized if, after mvar instantiation, it contains one of the provided mvars.
|
||||
let gCopy ← mkFreshExprSyntheticOpaqueMVar (← g.getType) (← g.getTag)
|
||||
let (h, g') ← gCopy.mvarId!.note `h e
|
||||
let (result?, stats) ← simpGoal g' ctx (simprocs := simprocs) (fvarIdsToSimp := #[h])
|
||||
(simplifyTarget := false) (stats := stats) (discharge? := discharge?)
|
||||
match result? with
|
||||
| some (xs, g') =>
|
||||
let h := xs[0]?.getD h
|
||||
let name ← mkFreshUserName `h
|
||||
let g' ← g'.rename h name
|
||||
g'.withContext do
|
||||
let gType ← g'.getType
|
||||
let h ← Term.elabTerm (mkIdent name) gType
|
||||
Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let hType ← inferType h
|
||||
unless (← withAssignableSyntheticOpaque <| isDefEq gType hType) do
|
||||
-- `e` still is valid in this new local context
|
||||
Term.throwTypeMismatchError gType hType h
|
||||
(header? := some m!"Type mismatch: After simplification, term{indentExpr e}\n")
|
||||
logUnassignedAndAbort (← filterOldMVars (← getMVars e) mvarCounterSaved)
|
||||
pushGoal g'
|
||||
closeMainGoal `simpa (checkUnassigned := false) h
|
||||
| none =>
|
||||
if getLinterUnnecessarySimpa (← getLinterOptions) then
|
||||
if let .fvar h := e then
|
||||
if (← getLCtx).getRoundtrippingUserName? h |>.isSome then
|
||||
logLint linter.unnecessarySimpa (← getRef)
|
||||
m!"Try `simp at {Expr.fvar h}` instead of `simpa using {Expr.fvar h}`"
|
||||
g.assign gCopy
|
||||
pure stats
|
||||
else if let some ldecl := (← getLCtx).findFromUserName? `this then
|
||||
if let (some (_, g), stats) ← simpGoal g ctx (simprocs := simprocs)
|
||||
(fvarIdsToSimp := #[ldecl.fvarId]) (simplifyTarget := false) (stats := stats)
|
||||
(discharge? := discharge?) then
|
||||
g.assumption
|
||||
pure stats
|
||||
else
|
||||
`(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
| _ => unreachable!
|
||||
TryThis.addSuggestion tk stx (origSpan? := ← getRef)
|
||||
return stats.diag
|
||||
pure stats
|
||||
else
|
||||
g.assumption
|
||||
pure stats
|
||||
if tactic.simp.trace.get (← getOptions) || squeeze.isSome then
|
||||
let usingArg : Option Term := usingArg.map (⟨·.raw.unsetTrailing⟩)
|
||||
let stx ← match ← mkSimpOnly stx.raw.unsetTrailing stats.usedTheorems with
|
||||
| `(tactic| simp $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]?) =>
|
||||
if unfold.isSome then
|
||||
`(tactic| simpa! $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
else
|
||||
`(tactic| simpa $cfg:optConfig $(disch)? $[only%$only]? $[[$args,*]]? $[using $usingArg]?)
|
||||
| _ => unreachable!
|
||||
TryThis.addSuggestion tk stx (origSpan? := ← getRef)
|
||||
return stats.diag
|
||||
| _ => throwUnsupportedSyntax
|
||||
|
||||
end Lean.Elab.Tactic.Simpa
|
||||
|
|
|
|||
|
|
@ -148,3 +148,14 @@ example : True := by induction 1 with done
|
|||
--^ $/lean/plainGoal
|
||||
|
||||
end
|
||||
|
||||
section
|
||||
|
||||
example (f : Nat → Nat) (n : Nat) (hf : ∀ x, f x = x + 0 + 1) : f n + 0 = 1 + n := by
|
||||
simpa [Nat.add_zero, Nat.add_comm] using hf n
|
||||
--^ $/lean/plainGoal
|
||||
--^ $/lean/plainGoal
|
||||
--^ $/lean/plainGoal
|
||||
--^ $/lean/plainGoal
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -185,3 +185,24 @@ null
|
|||
{"textDocument": {"uri": "file:///plainGoal.lean"},
|
||||
"position": {"line": 146, "character": 34}}
|
||||
{"rendered": "```lean\nx✝ : Nat\n⊢ True\n```", "goals": ["x✝ : Nat\n⊢ True"]}
|
||||
{"textDocument": {"uri": "file:///plainGoal.lean"},
|
||||
"position": {"line": 154, "character": 2}}
|
||||
{"rendered":
|
||||
"```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n + 0 = 1 + n\n```",
|
||||
"goals":
|
||||
["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n + 0 = 1 + n"]}
|
||||
{"textDocument": {"uri": "file:///plainGoal.lean"},
|
||||
"position": {"line": 154, "character": 3}}
|
||||
{"rendered":
|
||||
"```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1\n```",
|
||||
"goals":
|
||||
["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1"]}
|
||||
{"textDocument": {"uri": "file:///plainGoal.lean"},
|
||||
"position": {"line": 154, "character": 41}}
|
||||
{"rendered":
|
||||
"```lean\nf : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1\n```",
|
||||
"goals":
|
||||
["f : Nat → Nat\nn : Nat\nhf : ∀ (x : Nat), f x = x + 0 + 1\n⊢ f n = n + 1"]}
|
||||
{"textDocument": {"uri": "file:///plainGoal.lean"},
|
||||
"position": {"line": 154, "character": 43}}
|
||||
{"rendered": "no goals", "goals": []}
|
||||
|
|
|
|||
|
|
@ -18,7 +18,6 @@ htrue : True
|
|||
---
|
||||
error: unsolved goals
|
||||
htrue : True
|
||||
h✝ : False
|
||||
⊢ False
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
@ -35,7 +34,6 @@ context:
|
|||
⊢ False
|
||||
---
|
||||
error: unsolved goals
|
||||
h✝ : False
|
||||
⊢ False
|
||||
-/
|
||||
#guard_msgs in
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue