Skip to content

[Merged by Bors] - chore(AtLocation): clean up backtick handling #37999

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
grunweg wants to merge 4 commits into from
Closed

[Merged by Bors] - chore(AtLocation): clean up backtick handling #37999

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
6cc7c33
chore(AtLocation): clean up backtick handling
grunweg Apr 13, 2026
cda45b6
Update test error messages
grunweg Apr 13, 2026
530feb6
Apply suggestions from code review
grunweg Apr 14, 2026
d361f98
[pre-commit.ci lite] apply automatic fixes
pre-commit-ci-lite[bot] Apr 14, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Abel.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -506,7 +506,7 @@ elab (name := abelNF) "abel_nf" tk:"!"? cfg:optConfig loc:(location)? : tactic =
let loc := (loc.map expandLocation).getD (.targets #[] true)
let s ← IO.mkRef {}
let m := AtomM.recurse s cfg.toConfig (wellBehavedDischarge := true) evalExpr (cleanup cfg)
transformAtLocation (m ·) "`abel_nf`" loc (failIfUnchanged := true) false
transformAtLocation (m ·) "abel_nf" loc (failIfUnchanged := true) false

@[tactic_alt abel]
macro "abel_nf!" cfg:optConfig loc:(location)? : tactic =>
Expand Down
3 changes: 1 addition & 2 deletions Mathlib/Tactic/FieldSimp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -711,8 +711,7 @@ elab (name := fieldSimp) "field_simp" d:(discharger)? args:(simpArgs)? loc:(loca
let m := AtomM.recurse s { contextual := true } (wellBehavedDischarge := false)
(fun e ↦ reduceProp disch e <|> reduceExpr disch e) cleanup
let loc := (loc.map expandLocation).getD (.targets #[] true)
transformAtLocation
(m ·) "`field_simp`" (failIfUnchanged := true) (mayCloseGoalFromHyp := true) loc
transformAtLocation (m ·) "field_simp" (failIfUnchanged := true) (mayCloseGoalFromHyp := true) loc

/--
`field_simp` normalizes an expression in a (semi-)field by rewriting it to a common denominator,
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Tactic/Push.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -211,7 +211,7 @@ def elabDischarger (stx : TSyntax ``discharger) : TacticM Simp.Discharge :=
def push (cfg : Config) (disch? : Option Simp.Discharge) (head : Head) (loc : Location)
(failIfUnchanged : Bool := true) : TacticM Unit := do
let cfg := { distrib := cfg.distrib || (← getBoolOption `push_neg.use_distrib) }
transformAtLocation (pushCore head cfg disch? ·) "`push`" loc failIfUnchanged
transformAtLocation (pushCore head cfg disch? ·) "push" loc failIfUnchanged

/--
`push c` rewrites the goal by pushing the constant `c` deeper into an expression.
Expand Down Expand Up @@ -318,7 +318,7 @@ elab (name := pull) "pull" disch?:(discharger)? head:(ppSpace colGt term) loc:(l
let disch? ← disch?.mapM elabDischarger
let head ← elabHead head
let loc := (loc.map expandLocation).getD (.targets #[] true)
transformAtLocation (pullCore head · disch?) "`pull`" loc (failIfUnchanged := true) false
transformAtLocation (pullCore head · disch?) "pull" loc (failIfUnchanged := true) false

/-- A simproc variant of `push fun _ ↦ _`, to be used as `simp [↓pushFun]`. -/
simproc_decl _root_.pushFun (fun _ ↦ ?_) := pushStep .lambda {}
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Ring/RingNF.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -138,7 +138,7 @@ elab (name := ringNF) "ring_nf" tk:"!"? cfg:optConfig loc:(location)? : tactic =
let loc := (loc.map expandLocation).getD (.targets #[] true)
let s ← IO.mkRef {}
let m := AtomM.recurse s cfg.toConfig (wellBehavedDischarge := true) evalExpr (cleanup cfg)
transformAtLocation (m ·) "`ring_nf`" loc cfg.failIfUnchanged false
transformAtLocation (m ·) "ring_nf" loc cfg.failIfUnchanged false

@[tactic_alt ringNF] macro "ring_nf!" cfg:optConfig loc:(location)? : tactic =>
`(tactic| ring_nf ! $cfg:optConfig $(loc)?)
Expand Down
14 changes: 9 additions & 5 deletions Mathlib/Util/AtLocation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ namespace Mathlib.Tactic
open Lean Meta Elab.Tactic

/-- Use the procedure `m` to rewrite the provided goal. -/
-- Assumes `proc` is not surrounded by backticks itself.
Comment thread
grunweg marked this conversation as resolved.
Outdated
def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
(failIfUnchanged : Bool) (goal : MVarId) :
ReaderT Simp.Context MetaM (Option MVarId) := do
Expand All @@ -56,7 +57,7 @@ def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (pro
-- we use expression equality here (rather than defeq) to be consistent with, e.g.,
-- `applySimpResultToTarget`
let unchanged := tgt.cleanupAnnotations == r.expr.cleanupAnnotations
if failIfUnchanged && unchanged then throwError "{proc} made no progress on the goal"
if failIfUnchanged && unchanged then throwError "`{proc}` made no progress on the goal"
if r.expr.isTrue then
goal.assign (← mkOfEqTrue (← r.getProof))
pure none
Expand All @@ -71,23 +72,25 @@ def transformAtTarget (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (pro
The `simpTheorems` of the simp-context carried with `m` will be modified to remove `fvarId`;
this ensures that if the procedure `m` involves rewriting by this `SimpTheoremsArray`, then, e.g.,
`h : x = y` is not transformed (by rewriting `h`) to `True`. -/
-- Assumes `proc` is not surrounded by backticks itself.
Comment thread
grunweg marked this conversation as resolved.
Outdated
def transformAtLocalDecl (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
(failIfUnchanged : Bool) (mayCloseGoal : Bool) (fvarId : FVarId) (goal : MVarId) :
ReaderT Simp.Context MetaM (Option MVarId) := do
let ldecl ← fvarId.getDecl
if ldecl.isImplementationDetail then
throwError "Cannot run {proc} at {ldecl.userName}, it is an implementation detail"
throwError "Cannot run `{proc}` at `{ldecl.userName}`, it is an implementation detail"
let tgt ← instantiateMVars (← fvarId.getType)
let eraseFVarId (ctx : Simp.Context) :=
ctx.setSimpTheorems <| ctx.simpTheorems.eraseTheorem (.fvar fvarId)
let r ← withReader eraseFVarId <| m tgt
-- we use expression equality here (rather than defeq) to be consistent with, e.g.,
-- `applySimpResultToLocalDeclCore`
if failIfUnchanged && tgt.cleanupAnnotations == r.expr.cleanupAnnotations then
throwError "{proc} made no progress at {ldecl.userName}"
throwError "`{proc}` made no progress at `{ldecl.userName}`"
return (← applySimpResultToLocalDecl goal fvarId r mayCloseGoal).map Prod.snd

/-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal). -/
-- Assumes `proc` is not surrounded by backticks itself.
Comment thread
grunweg marked this conversation as resolved.
Outdated
def transformAtLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (proc : String)
(loc : Location) (failIfUnchanged : Bool := true) (mayCloseGoalFromHyp : Bool := false)
-- streamline the most common use case, in which the procedure `m`'s implementation is not
Expand All @@ -97,11 +100,12 @@ def transformAtLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result) (p
withLocation loc
(liftMetaTactic1 ∘ (transformAtLocalDecl m proc failIfUnchanged mayCloseGoalFromHyp · · ctx))
(liftMetaTactic1 (transformAtTarget m proc failIfUnchanged · ctx))
fun _ ↦ throwError "{proc} made no progress anywhere"
fun _ ↦ throwError "`{proc}` made no progress anywhere"

/-- Use the procedure `m` to transform at specified locations (hypotheses and/or goal).

In the wildcard case (`*`), filter out all dependent and/or non-Prop hypotheses. -/
-- Assumes `proc` is not surrounded by backticks itself.
Comment thread
grunweg marked this conversation as resolved.
Outdated
def transformAtNondepPropLocation (m : Expr → ReaderT Simp.Context MetaM Simp.Result)
(proc : String) (loc : Location) (failIfUnchanged : Bool := true)
(mayCloseGoalFromHyp : Bool := false)
Expand All @@ -112,6 +116,6 @@ def transformAtNondepPropLocation (m : Expr → ReaderT Simp.Context MetaM Simp.
withNondepPropLocation loc
(liftMetaTactic1 ∘ (transformAtLocalDecl m proc failIfUnchanged mayCloseGoalFromHyp · · ctx))
(liftMetaTactic1 (transformAtTarget m proc failIfUnchanged · ctx))
fun _ ↦ throwError "{proc} made no progress anywhere"
fun _ ↦ throwError "`{proc}` made no progress anywhere"

end Mathlib.Tactic
8 changes: 2 additions & 6 deletions MathlibTest/abel.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -99,9 +99,7 @@ error: `abel_nf` made no progress on the goal
#guard_msgs in
example : False := by abel_nf

/--
error: `abel_nf` made no progress at w
-/
/-- error: `abel_nf` made no progress at `w` -/
#guard_msgs in
example [AddCommGroup α] (x y z : α) (w : x = y + z) : False := by
abel_nf at w
Expand Down Expand Up @@ -141,9 +139,7 @@ example [AddCommGroup α] (x y z : α) (_w : x = y + z) : False := by
example [AddCommGroup α] (x y z : α) (_w : x = y + z) : x - x = 0 := by
abel_nf at *

/--
error: `abel_nf` made no progress at w
-/
/-- error: `abel_nf` made no progress at `w` -/
#guard_msgs in
example [AddCommGroup α] (x y z : α) (w : x = y + z) : x - x = 0 := by
abel_nf at w ⊢
Expand Down
4 changes: 2 additions & 2 deletions MathlibTest/push_neg.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,14 +151,14 @@ example {P : Prop} (h : P) : P := by push Not at *

-- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562
-- (Previously, because of a metavariable instantiation issue, the tactic succeeded as a no-op.)
/-- error: `push` made no progress at h -/
/-- error: `push` made no progress at `h` -/
#guard_msgs in
example {x y : ℕ} : True := by
have h : x ≤ y := test_sorry
push Not at h

-- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562 (previously the tactic succeeded as a no-op)
/-- error: Cannot run `push` at inductive_proof, it is an implementation detail -/
/-- error: Cannot run `push` at `inductive_proof`, it is an implementation detail -/
#guard_msgs in
def inductive_proof : True := by
push Not at inductive_proof
Expand Down
2 changes: 1 addition & 1 deletion MathlibTest/ring.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,7 +243,7 @@ example (n : ℤ) (r : ℝ) : n • r = n * r := by

-- new behaviour as of https://github.com/leanprover-community/mathlib4/issues/27562
-- (Previously, because of a metavariable instantiation issue, the tactic succeeded as a no-op.)
/-- error: `ring_nf` made no progress at h -/
/-- error: `ring_nf` made no progress at `h` -/
#guard_msgs in
example {R : Type*} [CommSemiring R] {x y : R} : True := by
have h : x + y = 3 := test_sorry
Expand Down
Loading