From 9769ad65723866093b35cd2c8875cc45e65d477a Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 27 Nov 2023 04:02:38 -0800 Subject: [PATCH] fix: missing withContext in simp trace (#2053) As [reported on Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/simp.3F.20.5B*.5D/near/322724789). --------- Co-authored-by: Scott Morrison --- src/Lean/Elab/Tactic/Simp.lean | 10 +++++----- tests/lean/simp_trace.lean | 4 ++++ tests/lean/simp_trace.lean.expected.out | 4 ++++ 3 files changed, 13 insertions(+), 5 deletions(-) diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index d6d6daf6a3..b87e90afab 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -283,7 +283,7 @@ def traceSimpCall (stx : Syntax) (usedSimps : UsedSimps) : MetaM Unit := do | .fvar fvarId => -- local hypotheses in the context if let some ldecl := lctx.find? fvarId then localsOrStar := localsOrStar.bind fun locals => - if !ldecl.userName.isInaccessibleUserName && + if !ldecl.userName.isInaccessibleUserName && !ldecl.userName.hasMacroScopes && (lctx.findFromUserName? ldecl.userName).get!.fvarId == ldecl.fvarId then some (locals.push ldecl.userName) else @@ -337,14 +337,14 @@ where /- "simp " (config)? (discharger)? ("only ")? ("[" simpLemma,* "]")? (location)? -/ -@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => do - let { ctx, dischargeWrapper } ← withMainContext <| mkSimpContext stx (eraseLocal := false) +@[builtin_tactic Lean.Parser.Tactic.simp] def evalSimp : Tactic := fun stx => withMainContext do + let { ctx, dischargeWrapper } ← mkSimpContext stx (eraseLocal := false) let usedSimps ← dischargeWrapper.with fun discharge? => simpLocation ctx discharge? (expandOptLocation stx[5]) if tactic.simp.trace.get (← getOptions) then traceSimpCall stx usedSimps -@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => do +@[builtin_tactic Lean.Parser.Tactic.simpAll] def evalSimpAll : Tactic := fun stx => withMainContext do let { ctx, .. } ← mkSimpContext stx (eraseLocal := true) (kind := .simpAll) (ignoreStarArg := true) let (result?, usedSimps) ← simpAll (← getMainGoal) ctx match result? with @@ -370,7 +370,7 @@ where | none => replaceMainGoal [] | some mvarId => replaceMainGoal [mvarId] if tactic.simp.trace.get (← getOptions) then - traceSimpCall (← getRef) usedSimps + mvarId.withContext <| traceSimpCall (← getRef) usedSimps @[builtin_tactic Lean.Parser.Tactic.dsimp] def evalDSimp : Tactic := fun stx => do let { ctx, .. } ← withMainContext <| mkSimpContext stx (eraseLocal := false) (kind := .dsimp) diff --git a/tests/lean/simp_trace.lean b/tests/lean/simp_trace.lean index f879cfa0ce..08a83258c0 100644 --- a/tests/lean/simp_trace.lean +++ b/tests/lean/simp_trace.lean @@ -134,3 +134,7 @@ example (P Q : Prop) (h : P ↔ Q) (p : P) : Q := by theorem my_thm' : a ↔ a ∧ a := my_thm.symm example (P : Prop) : P ∧ P ↔ P := by simp only [← my_thm'] + +example {P : Prop} : P → P := by intro h; simp [*] + +example {P : Prop} : P → P := by intro; simp [*] diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out index febf277f79..b5fbba577b 100644 --- a/tests/lean/simp_trace.lean.expected.out +++ b/tests/lean/simp_trace.lean.expected.out @@ -120,3 +120,7 @@ Try this: simp only [← h] Try this: simp only [← my_thm'] [Meta.Tactic.simp.rewrite] ← @my_thm':1000, P ∧ P ==> P [Meta.Tactic.simp.rewrite] iff_self:1000, P ↔ P ==> True +Try this: simp only [h] +[Meta.Tactic.simp.rewrite] h:1000, P ==> True +Try this: simp only [*] +[Meta.Tactic.simp.rewrite] a✝:1000, P ==> True