fix

Author: lua-vr

Mathlib/Tactic/Setm.lean

@@ -6,6 +6,7 @@ Authors: Lua Viana Reis, Kyle Miller, Gareth Ma
 module
 
 public meta import Mathlib.Tactic.Set
+public meta import Mathlib.Tactic.Core
 public meta import Lean.Elab.BuiltinTerm
 public meta import Batteries.Tactic.Exact
 
@@ -17,26 +18,26 @@ This module defines the `setm` tactic.
 
 meta section
 
-open Lean Elab Tactic Meta Term Syntax
+open Lean Mathlib Elab Tactic Meta Term Syntax
 
-abbrev SetMReplaceM := StateT (AssocList Name MVarId) TermElabM
+abbrev SetMReplaceM := StateT (List (Name × MVarId)) TermElabM
 
 /-- 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
+    let pair ←
+      if let `(?$n:ident) := stx then
+        (← get).find? (·.1 == n.getId) |>.getDM do
+          let name ← mkFreshUserName n.getId
+          let mvar ← mkFreshExprMVar none (userName := name)
+          pure (n.getId, mvar.mvarId!)
+      else if let `(?_) := stx then
+        let name ← mkFreshUserName `x
+        let mvar ← mkFreshExprMVar none (userName := name)
+        pure (name, mvar.mvarId!)
+      else return none
+    modify (.cons pair)
+    return ← withRef stx <| `(? $(mkIdent (← pair.2.getTag)))
   return ⟨stx⟩
 
 /--
@@ -45,41 +46,41 @@ local declaration (using the `at h` syntax) or the main goal, and introduces `le
 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
+syntax (name := setM) "setm " term ("using" ident)? (Parser.Tactic.location)? : tactic
 
-@[tactic setM]
-public def evalSetM : Tactic
-  | `(tactic| setm $pat:term $[$loc:location]?) => withReducibleAndInstances do
-    let locations := expandOptLocation (Lean.mkOptionalNode loc)
-    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 := 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
-    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}"
+def 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}"
+
+elab_rules : tactic
+| `(tactic| setm $pat:term $[using $usingArg]? $[$loc:location]?) =>
+  withMainContext do
+    let (pat, mvars) ← (replaceWithMVars pat).run {}
+    let pat ← Term.elabTerm pat none
+    let mut g ← getMainGoal
+    for (name, mvar) in mvars.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]
+    withMainContext <| withReducibleAndInstances do
+      if let some place := usingArg.map getId then
+        let loc := (← getLocalDeclFromUserName place).fvarId
+        if ← isDefEq pat (← loc.getType) then
+          replaceMainGoal [← g.changeLocalDecl loc pat false]
+        else
+          defeqError pat (← loc.getType)
+      else
+        if ← isDefEq pat (← g.getType) then
+          replaceMainGoal [← g.replaceTargetDefEq pat]
+        else
+          defeqError pat (← g.getType)
+      if let some loc := loc then
+        for (name, _) in mvars do
+        let expr := (← getLocalDeclFromUserName name).value
+        evalTactic (← `(tactic| try
+          rewrite [show $(← Term.exprToSyntax expr) = $(mkIdent name) from rfl] $loc))

MathlibTest/Tactic/Setm.lean

@@ -16,10 +16,10 @@ example : 1 + 2 = 3 := by
 
 /- Usage with `at` keywords -/
 example (h1 : 1 + 1 = 5) (h2 : 1 + 3 = 5) (h3 : 1 + 2 = 5) : True := by
-  setm ?A + _ = ?B at h1 h2 h3
+  setm ?A + _ = ?B using h1 at *
   guard_hyp A :=ₛ 1
   guard_hyp B :=ₛ 5
-  guard_hyp h1 :ₛ A + 1 = B
+  guard_hyp h1 :ₛ A + A = B
   guard_hyp h2 :ₛ A + 3 = B
   guard_hyp h3 :ₛ A + 2 = B
   trivial
@@ -35,16 +35,17 @@ example (h : b + a = c) : a + b = c := by
   clear A B
   /- setm 2 -/
   rewrite [Nat.add_comm]
-  setm ?A + ?B = _ at h ⊢
+  setm ?A + ?B = _ at h
   guard_hyp A :=ₛ b
   guard_hyp B :=ₛ a
+  guard_hyp h :ₛ A + B = c
   exact h
 
 /- Strange problem -/
 
 example (n : Bool) : 1 + 2 = 3 := by
   cases n
-  · setm ?A + ?B = _
+  · setm ?A + ?B = ?_
     guard_hyp A :=ₛ 1
     guard_hyp B :=ₛ 2
     trivial
@@ -59,7 +60,7 @@ instance : HAdd NotQuiteNat NotQuiteNat NotQuiteNat := inferInstanceAs (HAdd Nat
 
 example {a b c : NotQuiteNat} (h : a + b = c) : True := by
   /- setm 1-/
-  setm ?A + ?B = _ at h
+  setm ?A + ?B = _ using h
   guard_hyp A := a
   guard_hyp B := b
   trivial
@@ -73,7 +74,7 @@ is not definitionally equal to the target
 #guard_msgs in
 example {a b c : NotQuiteNat} (h : a + b = c) : True := by
   /- setm 1-/
-  setm (?A : Nat) + ?B = _ at h
+  setm (?A : Nat) + ?B = _ using h
 
 /- Test conflicts with goal metavariables (thanks to Niklas Halonen for this example!) -/