new version based on Kyle's

Author: lua-vr

Mathlib/Tactic/Setm.lean

@@ -1,12 +1,13 @@
 /-
 Copyright (c) 2026 Lua Viana Reis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Lua Viana Reis
+Authors: Lua Viana Reis, Kyle Miller, Gareth Ma
 -/
 module
 
 public meta import Mathlib.Tactic.Set
 public meta import Lean.Elab.BuiltinTerm
+public meta import Batteries.Tactic.Exact
 
 /-!
 # The `setm` tactic
@@ -18,90 +19,67 @@ meta section
 
 open Lean Elab Tactic Meta Term Syntax
 
-namespace Mathlib.Tactic.SetM
+abbrev SetMReplaceM := StateT (AssocList Name MVarId) TermElabM
 
-partial def wrapSyntheticHoles : Syntax → StateT (NameMap MVarId) TacticM Syntax :=
-  fun stx => do
-    if stx.isOfKind ``Lean.Parser.Term.syntheticHole && stx[1].isIdent then
-      let mvar ←
-        if let .some old := (← get).get? stx[1].getId then
-          pure old
-        else
-          let name ← mkFreshUserName stx[1].getId
-          let mvar := (← mkFreshExprMVar .none (userName := name)).mvarId!
-          modify (.insert · stx[1].getId mvar)
-          pure mvar
-      let ident : Ident := mkIdent (← mvar.getTag)
-      return ← withRef stx <| `(? $ident)
-    match stx with
-    | .node info kind args => return .node info kind (← args.mapM wrapSyntheticHoles)
-    | _ => return stx
+/-- Collect all synthetic holes and replace them with fresh metavariables. -/
+partial def replaceWithMVars (stx : Term) : SetMReplaceM Term := do
+  let stx ← stx.raw.replaceM fun stx ↦ do
+    if let `(?$n:ident) := stx then
+      let mvar ← ((← get).find? n.getId).getDM do
+        let name ← mkFreshUserName n.getId
+        let mvar := (← mkFreshExprMVar none (userName := name)).mvarId!
+        modify (.cons n.getId mvar)
+        pure mvar
+      return ← withRef stx <| `(? $(mkIdent (← mvar.getTag)))
+    else if let `(?_) := stx then
+      let mvar ← mkFreshExprMVar none
+      let name ← mkFreshUserName .anonymous
+      modify (.cons name mvar.mvarId!)
+      return ← withRef stx <| `(? $(mkIdent name))
+    else pure none
+  return ⟨stx⟩
 
-syntax (name := setMStx) "setm " term (Parser.Tactic.location)? : tactic
-
--- This code was copied from the `change` tactic in core. I am not sure if in our context,
--- all of it is necessary (could there be other synthetic opaque MVars that were not holes?).
-def elabSetM (e : Expr) (p : Syntax) : TacticM Expr := do
-  let p ← runTermElab do
-    let p ← Term.elabTermEnsuringType p (← inferType e)
-    unless ← isDefEq p e do
-      Term.synthesizeSyntheticMVars (postpone := .partial)
-      discard <| isDefEq p e
-    pure p
-  withAssignableSyntheticOpaque do
-    unless ← isDefEq p e do
-      throwError MessageData.ofLazyM (es := #[p, e]) do
-        let (p, tgt) ← addPPExplicitToExposeDiff p e
-        return m!"setm: pattern{indentExpr p}\nis not defeq to goal{indentExpr tgt}"
-    return ← instantiateMVars p
+/--
+The `setm` tactic ("`set` with matching") matches a pattern containing named holes the type of a
+local declaration (using the `at h` syntax) or the main goal, and introduces `let` bound variables
+representing subexpressions whose location corresponds to the given named hole. These variables are
+also substituted into the type of declaration (or main goal).
+-/
+syntax (name := setM) "setm " term (Parser.Tactic.location)? : tactic
 
-@[tactic setMStx]
+@[tactic setM]
 public def evalSetM : Tactic
   | `(tactic| setm $pat:term $[$loc:location]?) => withReducibleAndInstances do
-    let (pat, mvars) ← StateT.run (wrapSyntheticHoles pat) .empty
     let locations := expandOptLocation (Lean.mkOptionalNode loc)
-    -- First, unify the pattern with the target of each location.
-    withLocation locations
-      (atLocal := unify pat ∘ .some)
-      (atTarget := unify pat .none)
-      (failed := fun _ ↦ throwError "'setm' tactic failed")
-    -- The, for each metavariable...
-    for (n, m) in mvars do
-      -- ... instantiate it and introduce a let into the context...
-      let val ← instantiateMVars (.mvar m)
-      let ty ← m.getType'
-      let fvar ← liftMetaTacticAux fun goal ↦ do
-        let (fvar, goal) ← (← goal.define n ty val).intro1P
-        return (fvar, [goal])
-      -- ... and rewrite the introduced decl in each one of the locations.
+    withMainContext do
+      let (pat, mvars) ← (replaceWithMVars pat).run {}
+      let pat ← Term.elabTerm pat none
+      let mut g ← getMainGoal
+      for (name, mvar) in mvars.toList.reverse do
+        let mvar' ← mkFreshExprMVar none
+        g ← g.define name (← mvar'.mvarId!.getType) mvar'
+        let (fvar, g') ← g.intro1P
+        mvar.assign (.fvar fvar)
+        g := g'
+      replaceMainGoal [g]
       withLocation locations
-        (atLocal := rewrite fvar val ∘ .some)
-        (atTarget := rewrite fvar val .none)
-        (failed := fun _ ↦ throwError "'setm' tactic failed")
+        (atLocal := fun loc ↦ do
+          if ← isDefEq pat (← loc.getType) then
+            liftMetaTactic fun g ↦ do
+              return [← g.replaceLocalDeclDefEq loc pat]
+          else
+            defeqError pat (← loc.getType))
+        (atTarget := do
+          liftMetaTactic fun g ↦ do
+            if ← isDefEq pat (← g.getType) then
+              return [← g.replaceTargetDefEq pat]
+            else
+              defeqError pat (← g.getType))
+        (failed := fun _ ↦ throwError "tactic `setm` failed")
   | _ => throwUnsupportedSyntax
   where
-    unify (pat : Syntax) (lvar : Option FVarId) : TacticM Unit := do
-      let e ← if let .some l := lvar
-        then l.getType
-        else getMainTarget
-      let tgt ← elabSetM e pat
-      liftMetaTactic fun goal => do
-        return [← changeDecl goal tgt lvar]
-    rewrite (fvar : FVarId) (val : Expr) (lvar : Option FVarId) : TacticM Unit := do
-      liftMetaTactic fun goal ↦ do
-        let tgt ← instantiateMVars (← lvar.elim goal.getType (·.getType))
-        let absTgt ← kabstract tgt val
-        let goal ← if absTgt.hasLooseBVars
-          then changeDecl goal (absTgt.instantiate1 (.fvar fvar)) lvar
-          else pure goal
-        return [goal]
-    changeDecl (goal : MVarId) (tgt : Expr) (l? : Option FVarId := .none) : MetaM MVarId :=
-      match l? with
-      | .some fvar => do
-        let lctx := (← goal.getDecl).lctx.modifyLocalDecl fvar
-          fun d ↦ d.setType tgt
-        goal.modifyLCtx (fun _ ↦ lctx)
-        return goal
-      | .none => goal.replaceTargetDefEq tgt
-
-end Mathlib.Tactic.SetM
+    defeqError {α} (p e : Expr) : MetaM α :=
+      throwError MessageData.ofLazyM (es := #[p, e]) do
+        let (p, tgt) ← addPPExplicitToExposeDiff p e
+        return m!"setm pattern{indentExpr p}\nis not definitionally equal {
+          ""}to the target{indentExpr tgt}"

MathlibTest/Tactic/Setm.lean

@@ -19,7 +19,7 @@ example (h1 : 1 + 1 = 5) (h2 : 1 + 3 = 5) (h3 : 1 + 2 = 5) : True := by
   setm ?A + _ = ?B at h1 h2 h3
   guard_hyp A :=ₛ 1
   guard_hyp B :=ₛ 5
-  guard_hyp h1 :ₛ A + A = B
+  guard_hyp h1 :ₛ A + 1 = B
   guard_hyp h2 :ₛ A + 3 = B
   guard_hyp h3 :ₛ A + 2 = B
   trivial
@@ -40,6 +40,17 @@ example (h : b + a = c) : a + b = c := by
   guard_hyp B :=ₛ a
   exact h
 
+/- Strange problem -/
+
+example (n : Bool) : 1 + 2 = 3 := by
+  cases n
+  · setm ?A + ?B = _
+    guard_hyp A :=ₛ 1
+    guard_hyp B :=ₛ 2
+    trivial
+  setm ?A + ?B = _
+  trivial
+
 /- Test reducible + instances transparency -/
 
 def NotQuiteNat : Type := Nat
@@ -54,9 +65,9 @@ example {a b c : NotQuiteNat} (h : a + b = c) : True := by
   trivial
 
 /--
-error: setm: pattern
-  @Eq Nat (?A✝ + ?B✝) ?m.12
-is not defeq to goal
+error: setm pattern
+  @Eq Nat (A + B) ?m.12
+is not definitionally equal to the target
   @Eq NotQuiteNat (a + b) c
 -/
 #guard_msgs in