Help with writing tactic

Stream: metaprogramming / tactics

[Gareth Ma]

Hi, I need some guidance on writing tactics. The goal is to have a simple way to replace expressions in the goal with variables. Here's what I want:

example : 1 + 2 = 3 := by
  introNames (?A : ℕ) + ?B = ?C
  /-
  This should introduce the following into the context:
    A : ℕ := 1
    B : ℕ := 2
    C : ℕ := 3
  -/
  done

And it should be functionally the same as

example : 1 + 2 = 3 := by
  /- The obstacle? is how to find what A B C should be in the tactic -/
  set A : ℕ := 1 with hA
  set B : ℕ := 2 with hB
  set C : ℕ := 3 with hC
  change A + B = C
  done

It feels like some combination of change (of course) and refine, but I don't know how to implement it. The source code of the two tactics are huge...

[Damiano Testa]

Is using set instead of let closer to what you want?

[Gareth Ma]

Oh yeah forgot about that

[Gareth Ma]

Sorry I’m on phone right now but I will edit it when I get back.

[Gareth Ma]

After hours of struggling I at least learned how to make the hypotheses I want. Now I need to do the parsing step with A B C...
It seems that all the work has been done already, since it's how IsDefEq work, but I don't know how to use it. Any help would be great.

/-
Usage: introNames ?A
It adds `A : Prop := <target>` and `hA : A = <target>` into the local context
Then replaces the entire goal with just `A` lmao
-/
syntax "introNames" (ppSpace colGt term) : tactic
elab_rules : tactic
| `(tactic|introNames $e:term) =>
  withMainContext do
    let te ← elabTerm (mayPostpone := true) e none
    match te with
    | Expr.mvar mvarId => do
      let name := ((←getMCtx).decls.find! mvarId).userName
      let a : Ident := mkIdent name
      let ha : Ident := mkIdent $ name.appendBefore "h"
      let goal ← getMainGoal
      let val ← getMainTarget
      let (fvar, goal) ← (←goal.define "A" (←inferType val) val).intro1P
      replaceMainGoal [goal]
      evalTactic (← `(tactic| try rewrite [show $(←Term.exprToSyntax val) = $a from rfl] at *))
      evalTactic (← `(tactic| have $ha : $a = $(←Term.exprToSyntax val) := rfl))
      dbg_trace f!"POGGERS!"
    | _ => throwError "RHS is not a hole"

example : (1 + 1) + (2 + 2) + (3 + 3) = 12 := by
  introNames ?A
  /-
  ▶ 1 goal
  A : Prop := 1 + 1 + (2 + 2) + (3 + 3) = 12
  hA : A = (1 + 1 + (2 + 2) + (3 + 3) = 12)
  ⊢ A
  -/
  done

[Thomas Murrills]

Nice! You’re right to identify isDefEq as doing the important work!

Broadly, the way I’d approach this is

1. elabTermWithHoles on the argument to collect the new metavariables.
2. isDefEq to unify with the goal type and assign them, figuring out what they have to be.
3. Use the values of these assignments (but not the mvars themselves) to generate the local declarations, and add them to the original goal’s local context.
4. Replace the metavariables in the expression we got with elabTermWithHoles not with their assignments, but with these new hypotheses
5. change the goal target to this new goal

But you might notice something tricky here: we assign the metavariables to figure out what they should be, but then go through and replace them with something that isn’t their assignment! What gives?

One way to solve this is by abstracting the new metavariables as the arguments of a function first (iirc stuff surrounding elimMVar might be relevant), then creating temporary metavariables that exist just for the unification step to extract the necessary values, then adding the hypotheses and applying this function to the hypotheses we’ve made (and reducing).

Another way is to assign them by isDefEq, backtrack the state so that they’re now unassigned (while keeping the assignments we found), then eventually assign them to the hypotheses we make!

This is kind of a cheeky strategy but involves fewer manual transformations of the expressions in question into functions and back. However, the former involves less fiddling with the MetaM state (which tracks assignments). Which is preferable is, to my mind, a matter of taste. Maybe there’s an answer in terms of performance, though, I’m not sure.

Now, if you want to rename these everywhere, you might want to rewrite the hypothesis types as well, but that’s fairly straightforward compared to the rest. :)

I’d be happy to write up this code later, but if this is a “learning how to do it” situation instead of a “having it written” situation I’m also happy to refrain from doing so. :)

Also I think @Shreyas Srinivas is working on something similar.

[Gareth Ma]

Thanks a lot for your answer, I will read and try out what you said when I wake :) It's probably best for me to try it myself rather than having someone write it for me <3

[Gareth Ma]

What am I doing wrong here? In the Lean book on isDefEq, it gives this code:

#eval show MetaM Unit from do
  let a ← Lean.Meta.mkFreshExprMVar (Expr.const `Nat []) (userName := `a)
  let expr1 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, a]
  let expr2 := Lean.mkAppN (Expr.const `Nat.add []) #[Lean.mkNatLit 2, Lean.mkNatLit 1]
  let isEqual ← Lean.Meta.isDefEq expr1 expr2
  IO.println isEqual -- true

However, my version with a tactic doesn't work:

syntax "testDefEq" (ppSpace colGt term) : tactic
elab_rules : tactic
| `(tactic|testDefEq $e:term $f:term) => do
  let (ee, _) ← elabTermWithHoles e none "suffix" (allowNaturalHoles := true)
  let (ff, _) ← elabTermWithHoles f none "suffix" (allowNaturalHoles := true)
  dbg_trace f!"defeq : {←isDefEq ee ff}"

example : 1 + 2 = 3 := by
  testDefEq (2 + ?A) (2 + 1) -- false

[Gareth Ma]

Here's the ee and ff in my version:

ee : Eq.{1} Nat (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))
ff : Eq.{1} Nat (HAdd.hAdd.{0, 0, 0} Nat Nat Nat (instHAdd.{0} Nat instAddNat) (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) ?_uniq.47755) (OfNat.ofNat.{0} Nat 3 (instOfNatNat 3))
defeq : false

which should unify right? I can literally replace ?_uniq.47755 (as a string) with that OfNat.ofNat.{0} Nat 2 (instOfNatNat 2) and it is an exact match :/

[Gareth Ma]

Perhaps this is a bit clearer
Screenshot-2023-10-23-at-11.38.57.png

[Damiano Testa]

I have never used the termWithHoles but it seems to create opaque holes. I wonder if that is the issue: Lean may not be able to assign those. Did you try with a plain elabTerm?

[Gareth Ma]

I will try that. I used elabTermWithHoles since Thomas mentioned it up there :)

[Gareth Ma]

No, the isDefEq still doesn't work

[Damiano Testa]

I'm on mobile, but try to look at the move_add tactic: I have certainly unified similar terms with holes and it worked for my purpose.

[Gareth Ma]

Okay! Thanks

[Jannis Limperg]

The ?A [unassignable] in the defeq trace indicates that something is indeed creating opaque metavariables.

[Damiano Testa]

Here

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/MoveAdd.lean#L407

Is the parsing, I think, earlier in the file there is an isDefEq check. I hope that this helps!

[Gareth Ma]

Okay I understand (not really) what you two mean for "opaque metavariables" now, which led to a terrible solution

[Gareth Ma]

-     dbg_trace f!"defeq : {←isDefEq ee ff}"
+     dbg_trace f!"defeq : {←withAssignableSyntheticOpaque <| isDefEq ee ff}"

[Damiano Testa]

My vague understanding of this is that mvars are very willing to unify, which is sometimes desirable, sometimes not. With elabTermsWithHoles you explicitly try to avoid "random unification". With elabTerm, the holes should be more receptive.

Having said that, I do not know if using ?A instead of _ for a hole has further implications.

[Damiano Testa]

Looking at this again, I think that

• elabTermWithHoles will create an opaque metavariable that will not get unified in the isDefEq call
• elabTerm produces live metavariables, but not if they are "named".

So, using elabTerm, this

  testDefEq (2 + _) (2 + 1)

gives true, but passing

  testDefEq (2 + ?A) (2 + 1)

gives false. With elabTermWithHoles it is false regardless.

I do not know if your solution using withAssignableSyntheticOpaque is "standard", but seems a good way to proceed, given the constraints.

[Gareth Ma]

I think the easiest solution here, though maybe not the "cleanest", is to set every hole to .natural instead of the opaque hole right now. However, this is giving me error...

/- MRC -/
import Lean
open Lean.Elab.Tactic
syntax "testDefEq" (ppSpace colGt term) : tactic
elab_rules : tactic
| `(tactic|testDefEq $e:term $f:term) => do
  withMainContext do
    let (ff, mvarIds) ← elabTermWithHoles f none "suffix" (allowNaturalHoles := true)
    mvarIds.mapM fun mvarId => mvarId.setKind .natural


/-
▶ 214:5-214:55: error:
type mismatch
  mapM (fun mvarId => ?m.44983 mvarId) mvarIds
has type
  ReaderT Tactic.Context (StateRefT' IO.RealWorld Tactic.State TermElabM) (List ?m.44934) : Type
but is expected to have type
  TacticM PUnit.{1} : Type
-/

[Gareth Ma]

Oh oops, we were typing at the same minute

[Damiano Testa]

I think that the error is telling you that you should be returning a unit, while you are returning a list of units: try

    let _ ← mvarIds.mapM fun mvarId => mvarId.setKind .natural

[Gareth Ma]

Oh, that works, thanks

[Gareth Ma]

What does the ReaderT Tactic.Context (StatRefT' IO.RealWorld Tactic.State TermElabM) part mean?

[Jannis Limperg]

See the comment at the top of Lean.MetavarContext for precise info about opaque mvars (and many other things besides).

Usually Lean syntax uses ?A for opaque metavariables and ?_A for non-opaque mvars (I think), but if you only want non-opaque mvars, then it makes sense to collect the opaque mvars and turn them into non-opaque ones, either via an option for elabTerm* if available or via your mapM hack. The withAssignableSyntheticOpaque may affect other mvars present in the goal, so it's probably less correct.

[Jannis Limperg]

Gareth Ma said:

What does the ReaderT Tactic.Context (StatRefT' IO.RealWorld Tactic.State TermElabM) part mean?

This is the definition of TacticM, which apparently got unfolded somewhere during typechecking.

[Jannis Limperg]

Damiano Testa said:

I think that the error is telling you that you should be returning a unit, while you are returning a list of units: try

    let _ ← mvarIds.mapM fun mvarId => mvarId.setKind .natural

Even better: mvarIds.forM ..., which avoids constructing the list entirely.

[Gareth Ma]

Sorry for the many questions :/ but why is ?A a bound variable

import Lean

open Lean Meta Elab.Tactic

syntax "testDefEq" (ppSpace colGt term) : tactic
elab_rules : tactic
| `(tactic|testDefEq $f:term) => do
  withMainContext do
    let target ← getMainTarget
    let (ff, mvarIds) ← elabTermWithHoles f none "suffix" (allowNaturalHoles := true)
    mvarIds.forM fun mvarId => mvarId.setKind .natural
    let mvar := mvarIds[0]!
    let mctx ← getMCtx
    /- mvar should be the `?A` -/
    assert! (mctx.decls.find! mvar).userName = "A"
    if ←isDefEq target ff then
      /- Now mvar should be set to 2 because of the isDefEq? -/
      assert! ←mvar.isAssigned
      let mvarVal := mctx.eAssignment.find! mvar
      /- Why is it a bound variable? -/
      /- kind : Lean.Expr.bvar 0 -/
      dbg_trace f!"kind : {repr mvarVal}"
    else
      throwError "Not isDefEq"

example : 1 + 2 = 3 := by
  testDefEq 1 + ?A = 3

I don't understand how isDefEq works and how to use it

[Gareth Ma]

I tried to clean my code up so it's easier to read

[Damiano Testa]

mvar is a metavariable corresponding to the goal that ?A represents, that is, a natural number. If you use

      logInfo m!"ff after: {ff}\nmvar: {mvar}"

you can see that ff is assigned to the right sum, and that mvar is a single goal with type Nat. So Lean deduced that your ?A represents a natural number. If you place a

    logInfo m!"ff before: {ff}"

just before the if isDefEq you will see that ff contains an mvar.

[Damiano Testa]

Btw, if I remember correctly, in Lean 3 ff was what is now called false, so seeing it in your code always makes me a little anxious...

[Gareth Ma]

Aha I see, so the entire ff becomes the sum

[Gareth Ma]

But how should I extract "what should ?A be replaced with"? Since my tactic's goal is to eventually create a let A := <what A should be>

[Gareth Ma]

I think this is where I should go back to Thomas' original reply and read the "... you might notice something tricky here:" part :P
Thanks everyone for the help so far

[Gareth Ma]

Ohh I should use getExprMVarAssignment?!!

[Gareth Ma]

Wait, then from here it seems quite straightforward (I will regret saying this)

[Gareth Ma]

syntax "testDefEq" (ppSpace colGt term) : tactic
elab_rules : tactic
| `(tactic|testDefEq $f:term) => do
  withMainContext do
    let goal ← getMainGoal
    let target ← getMainTarget
    let (ff, mvarIds) ← elabTermWithHoles f none "suffix" (allowNaturalHoles := true)
    mvarIds.forM fun mvarId => mvarId.setKind .natural
    let mvarId := mvarIds[0]!
    let mctx ← getMCtx
    /- mvar should be the `?A` -/
    let name := ((←getMCtx).decls.find! mvarId).userName
    let a : Ident := mkIdent name
    let ha : Ident := mkIdent $ name.appendBefore "h"
    assert! name = "A"

    if ←isDefEq target ff then
      /- Now mvar should be set to 2 because of the isDefEq? -/
      assert! ←mvarId.isAssigned
      let mvarVal := mctx.eAssignment.find! mvarId
      /- Why is it a bound variable? -/
      /- kind : Lean.Expr.bvar 0 -/
      logInfo f!"ff : {ff}"
      logInfo m!"mvar : {mvarId}"
      logInfo f!"kind : {repr mvarVal}"

      match (←getExprMVarAssignment? mvarId) with
      | some mvarAss =>
        logInfo m!"ass : {mvarAss}"
        let mvarType ← inferType mvarAss
        let (fvar, goal) ← (←goal.define "A" mvarType mvarAss).intro1P
        replaceMainGoal [goal]
        logInfo m!"syn : {←delabToRefinableSyntax mvarAss}"
        evalTactic (← `(tactic| rewrite [show $(←Term.exprToSyntax mvarAss) = $a from rfl]))
        evalTactic (← `(tactic| have $ha : $a = $(←Term.exprToSyntax mvarAss) := rfl))
      | none => throwError "what"
    else
      throwError "Not isDefEq"

example : 1 + (2 * (5 - 3)) = 3 := by
  testDefEq 1 + ?A = 3
  /-
  ▶ 1 goal
  A : ℕ := 2 * (5 - 3)
  hA : A = 2 * (5 - 3)
  ⊢ 1 + A = 3
  -/
  done

Very proud of myself for this :) All that remains is to do it for all the variables, but that's easy.
Thanks everyone for the help once again!!!

[Gareth Ma]

Exactly what I want (I think)

[Gareth Ma]

Final code:

syntax "testDefEq" (ppSpace colGt term) : tactic
elab_rules : tactic
| `(tactic|testDefEq $f:term) => do
  withMainContext do
    let target ← getMainTarget
    let (ff, mvarIds) ← elabTermWithHoles f none "suffix" (allowNaturalHoles := true)
    let mctx ← getMCtx
    mvarIds.forM fun mvarId => mvarId.setKind .natural
    if ←isDefEq target ff then
      mvarIds.forM fun mvarId => do
        let goal ← getMainGoal
        let name := (mctx.decls.find! mvarId).userName
        let a : Ident := mkIdent name
        let ha : Ident := mkIdent $ name.appendBefore "h"
        assert! ←mvarId.isAssigned
        match (←getExprMVarAssignment? mvarId) with
        | some mvarAss =>
          let mvarType ← inferType mvarAss
          let (_, goal) ← (←goal.define name mvarType mvarAss).intro1P
          replaceMainGoal [goal]
          /- Copied from `set ... with ...` -/
          evalTactic (← `(tactic| rewrite [show $(←Term.exprToSyntax mvarAss) = $a from rfl]))
          evalTactic (← `(tactic| have $ha : $a = $(←Term.exprToSyntax mvarAss) := rfl))
        | none => throwError "what"
    else
      throwError "Not isDefEq"

example : 1 + (2 * (5 - 3)) = 3 := by
  testDefEq ?A + ?B = 3
  /-
  ▶ 1 goal
  A : ℕ := 1
  hA : A = 1
  B : ℕ := 2 * (5 - 3)
  hB : B = 2 * (5 - 3)
  ⊢ A + B = 3
  -/
  done

[Gareth Ma]

Thomas Murrills said:

...

But you might notice something tricky here: we assign the metavariables to figure out what they should be, but then go through and replace them with something that isn’t their assignment! What gives?

...

Another way is to assign them by isDefEq, backtrack the state so that they’re now unassigned (while keeping the assignments we found), then eventually assign them to the hypotheses we make!

This is kind of a cheeky strategy but involves fewer manual transformations of the expressions in question into functions and back. However, the former involves less fiddling with the MetaM state (which tracks assignments). Which is preferable is, to my mind, a matter of taste. Maybe there’s an answer in terms of performance, though, I’m not sure.

Now, if you want to rename these everywhere, you might want to rewrite the hypothesis types as well, but that’s fairly straightforward compared to the rest. :)

Also, I don't think the backtracking part is necessary. Or at least my code seems to work without doing any backtracking. I just get the assignments, make local hypotheses, then use rewrite and have (like how set ... with ... works)

[Damiano Testa]

Following some precedents in mathlib, this could be called setm, for set with match, similar to congrm.

[Gareth Ma]

Great! I will polish it and add some more features then make a PR :)

[Jireh Loreaux]

@Gareth Ma it would be great if you could modify this to accept a location with the at syntax, so that you could do this for hypotheses too instead of just the main goal.

[Jireh Loreaux]

Also, I expect that once Scott answers my question here that the inclusion of hA and hB should be unnecessary, which currently clutters the tactic state.

[Gareth Ma]

Seems like it. It's easily fixable though after your question is fixed. I will add a note.

[Thomas Murrills]

Very nice! :D However, there is a subtle reason I didn't suggest using rewrite in this case: a situation in which someone might not have their subexpressions named the way they want after using rewrite. Can you spot it?

[Gareth Ma]

(I am trying to come up with an example where ?A=1+1 and ?B=1+1+1 (which doesn't rewrite) but my tactic is working too well)

[Gareth Ma]

example : (4 + 0) - (3 + 1) = 0 := by
  setm ?A - ?B = (_ : Nat)
/-
A : ℕ := 4 + 0
B : ℕ := 3 + 1
hA : A = B
hB : B = 3 + 1
⊢ A - A = 0
-/

Is this what you mean?

[Gareth Ma]

If so, can I just do a stupid change at the end to make it precisely what the user wants? As in here, I will add a change A - B = _

[Thomas Murrills]

Yep, that! When one is reducibly defeq to another, that’ll happen; and likewise when one is a subexpression of an expression which is reducibly defeq to another.

Hmm, how do you know where A and B should be? And if we do know, why not just change and avoid the rewrite? (Well, we still might want to rewrite hypotheses, but at least avoid it on the goal)

[Gareth Ma]

Ah wait, the version above isn't the newest one, I made some modifications

[Gareth Ma]

Give me a second

[Gareth Ma]

/- todo: handle loc -/
syntax (name := setM) "setm " term (location)?: tactic
elab_rules : tactic
| `(tactic| setm $expr:term) => do
  withMainContext do
    /- dbg_trace f!"at : {loc}" -/
    let (pattern, mvarIds) ← elabTermWithHoles expr none (←getMainTag) (allowNaturalHoles := true)
    dbg_trace f!"{pattern}"
    /- Named holes are by default syntheticOpaque and not assignable, so we change that -/
    mvarIds.forM fun mvarId => mvarId.setKind .natural
    trace[Tactic.setm] "pattern : {pattern}"
    /- We let isDefEq match the given pattern with the target specified (default: main goal) -/
    let mctx ← getMCtx
    let mdecls := mctx.decls
    /- TODO : Handle loc -/
    if ←isDefEq (←getMainTarget) pattern then
      mvarIds.forM fun mvarId => do
        match (mdecls.find! mvarId).userName with
        | Name.anonymous => return ()
        | name =>
          let a := mkIdent name
          let ha := mkIdent $ name.appendBefore "h"
          match (←getExprMVarAssignment? mvarId) with
          | some mvarAss => evalTactic (←`(tactic| set $a := $(←Term.exprToSyntax mvarAss) with $ha))
          | none => throwError "File a bug report!"
        logInfo m!"{←getMainGoal}\n"
    else
      throwError f!"setm: pattern is not definitionally equal to the goal."

[Gareth Ma]

I use a set instead, but it runs into the same problem

[Gareth Ma]

I will be back in an hour or so

[Jireh Loreaux]

I think the process should look something like this:

1. Take a some stx representing a term and traverse it with docs#Lean.TSyntax.replaceM. Whenever you come across the relevant piece of named syntax (e.g., a named hole ?a), check if there is already a declaration in the context with that name (this is for when you have something repeated), if so, replace it with an atom of the same name. If not, create a new metavariable, and a local let declaration with the provided name, and replace it with an atom for that name.
2. Call change on the modified stx, which should assign all the metavariables which were created.

[Gareth Ma]

Okay, I will try it... replaceM is used once in the entire codebase and without docs :tear: Not ideal...

[Jireh Loreaux]

(Also, take everything I say with a grain of salt, I'm pretty new to metaprogamming :laughing:)

[Gareth Ma]

You can't be newer than me, I started around 24 hours ago :P

[Jireh Loreaux]

~2 weeks isn't that much more!

[Gareth Ma]

I think it's easier to work with Expr instead of Syntax, so I probably need docs#Lean.Expr.replace instead :D

[Jireh Loreaux]

Hmm... I don't think that's what you want, because you are dealing with actual syntax coming in.

[Jireh Loreaux]

Once you do ElabTermWithHoles, you have metavariables all throughout your resulting expression. You need to make local let declarations for all of them and then substitute back. Hmmm...., nevermind, I think you may be right.

[Gareth Ma]

I spent almost an hour debugging nothing... I thought getMCtx returns a pointer to the context (which should be "global"), but of course it doesn't

[Gareth Ma]

Anyways I am close, here is what I have

[Thomas Murrills]

I agree that syntax should not be present here. :) Here's one way to do it, using the first option I presented (abstract the mvars) which might introduce you to some useful metaprogramming functions.

1. after elabTermWithHoles, abstract the mvars you've collected using (I believe) mkLambdaFVars. Despite referring to fvars, I think it also works for mvars. This gets you an Expr which is a lambda.
2. Use lambdaMetaTelescope on the resulting lambda to introduce these back as new metavariables.
3. Use isDefEq to unify the result with the goal, assigning those new metavariables.
4. Create local hypotheses using the new metavariables as the body and the names of the original metavariables. Collect the resulting expressions/fvars as you go.
5. Assign your original metavariables to these resulting fvars.
6. change the goal to the original expression you got from elaboration, which now includes assigned mvars. (You don't need syntax; use the MetaM version.)

Also, stylistic note: you should never really need to get the mctx. For most things, there's a function that does it, e.g. getUsername. :)

[Thomas Murrills]

Oops, sorry, race condition :)

[Gareth Ma]

I am very close on mine, so I will finish it first :D

[Jireh Loreaux]

That's a neat trick I wouldn't have thought of: duplicating the expression with new mvars; nice.

[Gareth Ma]

That's what I am doing

[Shreyas Srinivas]

@Thomas Murrills : just read the tag and the thread properly . @Gareth Ma , the tactic is pretty cool. Fwiw, I will continue working on my version in the coming weekend, since I see it as a learning exercise. I want to learn what I can get out of conv and working maximally within macros anyway.

[Gareth Ma]

Damn it's looking great

▶ 97:3-97:7: error:
[error when printing message: unknown goal [anonymous]]

▶ 97:3-97:7: error:
unknown metavariable '?[anonymous]'

My code is so messed up now that I am not sure it's worth anyone's time reading it :(

[Gareth Ma]

If anyone has some spare time to help debug and explain what went wrong I will greatly appreciate it :(

syntax (name := setM) "setm " term : tactic
elab_rules : tactic
| `(tactic| setm $expr:term) => do
  withMainContext do
    let (origPattern, mvarIds) ← elabTermWithHoles expr none (←getMainTag) (allowNaturalHoles := true)
    /- Named holes are by default syntheticOpaque and not assignable, so we change that -/
    mvarIds.forM fun mvarId => mvarId.setKind .natural
    trace[Tactic.setm] "origPattern : {origPattern}"

    /- Create new placeholder mvars -/
    let name (x : MVarId) := do return (←x.getDecl).userName
    let mvarIdsPairs ← mvarIds.mapM
      (fun x => return (x, ←mkFreshExprMVar none (userName := ←name x)))
    let mvarIdsMap := @HashMap.ofList _ _ instBEqMVarId instHashableMVarId mvarIdsPairs

    /- newPattern is the placeholder pattern with a bunch of placeholder mvars -/
    let newPattern := origPattern.replace (fun x =>
      match x with
      | .mvar x => mvarIdsMap.find? x
      | _ => none
    )

    /- We let isDefEq match the given pattern -/
    let mctx ← getMCtx
    let mdecls := mctx.decls
    if ←isDefEq (←getMainTarget) newPattern then
      /- We iterate over the (old, new) vars -/
      mvarIdsPairs.forM fun (mvarIdOld, mvarExprNew) => do
        let mvarIdNew := mvarExprNew.mvarId!
        match (mdecls.find! mvarIdNew).userName with
        | Name.anonymous => return ()
        | name =>
          let a := mkIdent name
          let ha := mkIdent $ name.appendBefore "h"
          let goal ← getMainGoal
          match (←getExprMVarAssignment? mvarIdNew) with
          | some mvarAss =>
            /-
            Here mvarIdNew is assigned to mvarAss, and mvarIdOld <-> mvarIdNew, so I
              (1) let $a := mvarAss -- Here fvarId stores $a (?)
              (2) have $ha : $a = mvarAss := rfl
              (3) assign $a to mvarIdOld
            -/
            /- (1) -/
            let mvarType ← inferType mvarAss
            let (fvarId, goal) ← (←goal.define a.getId mvarType mvarAss).intro1P
            replaceMainGoal [goal]
            /- (2) -/
            evalTactic (←`(tactic| have $ha : $a = $(←Term.exprToSyntax mvarAss) := rfl))
            /- (3) -/
            mvarIdOld.assign (.fvar fvarId)
          | none => throwError "File a bug report!"
    else
      throwError f!"setm: pattern is not definitionally equal to the goal."

    /- At the end, all the original mvars are replaced with the new fvars -/
    replaceMainGoal [origPattern.mvarId!]

example : (4 + 0) - (3 + 1) = 2 := by
  setm ?A - ?B = (_ : Nat)
  done

[Gareth Ma]

Ah I know, the fvar are bound variables, but origPattern doesn't include those uh bounds

[Gareth Ma]

-     replaceMainGoal [origPattern.mvarId!]
+     evalTactic (←`(tactic| change $(←Term.exprToSyntax origPattern)))

Done!

[Gareth Ma]

Screenshot-2023-10-24-at-01.27.17.png

Sorry for the spam, though I don't think anyone receives any notifications anyways... but it works now

[Gareth Ma]

@Thomas Murrills About your first two points using mkLambdaFVars and lambdaMetaTelescope, it seems I used a completely different method:

    /- Create new placeholder mvars -/
    let name (x : MVarId) := do return (←x.getDecl).userName
    let mvarIdsPairs ← mvarIds.mapM
      (fun x => return (x, ←mkFreshExprMVar none (userName := ←name x)))
    let mvarIdsMap := @HashMap.ofList _ _ instBEqMVarId instHashableMVarId mvarIdsPairs

    /- newPattern is the placeholder pattern with a bunch of placeholder mvars -/
    let newPattern := origPattern.replace (fun x =>
      match x with
      | .mvar x => mvarIdsMap.find? x
      | _ => none
    )

Is it doing the same thing as what you are saying? (the mvarIdsMap isn't really necessary, but speeds up newPattern a bit I guess)

[Thomas Murrills]

Oh, very nice! :tada: Yes, that should be doing the same thing—I think. I'm not completely sure what the business with the cache occurring in replace is. Anyway, replacing the mvars with new ones directly is a good deal better than going through a lambda and back, I'd think! Nice work! :)

I've got a list of technical and stylistic comments; would you like to hear them? Or I can save them for github if you like; feel free to make a PR and just label it WIP if you're still polishing things. :)

[Jireh Loreaux]

When you make the PR, please link both to this thread, and to the one where the tactic was originally mentioned.

[Gareth Ma]

Sorry I fell asleep last night, I'll open a draft PR

[Gareth Ma]

GH PR here, there's some work I know of, but styling suggestions are greatly appreciated @Thomas Murrills @Jireh Loreaux

[Thomas Murrills]

Nice, will review tomorrow! :)

[Gareth Ma]

I think there should also be a dsetm or something, where you just remove the variables set by the previous setm. Is that possible? Can we either maintain some global set of variables set by setm, or perhaps add a tag to the variables created by setm?

[Gareth Ma]

This is the use case that inspired this tactic

  setm (?A : 𝕜) + (?B + ?C - (?D + ?E)) = ?F
  rw [show ∀ A B C D E : 𝕜, A + (B + C - (D + E)) = (A + C - D) - (E - B) by intros ; ring_nf]
  rw [hA, hB, hC, hD, hE, hF] at * ; clear A hA B hB C hC D hD E hE F hF /- Probably doable with a tactic -/

It will be nice if the third line is just dsetm
Or do some indented-based stuff similar to conv, but that sounds hard :P

[Jannis Limperg]

All mechanisms for tracking state between tactic calls suck in some way. You can try to wrap the hypothesis types with an mdata, but some tactics may not preserve the mdata. You can turn setm into a scoped tactic (setm ... => ...) and remember the FVarIds you introduced at the start, but tactics using the revert-intro technique may modify FVarIds. You can also remember the user names of the introduced hypotheses, but these too can change. So I sadly don't see a reliable way to implement this.

[Gareth Ma]

Hi, there seems to be a bug with my tactic and I don't know how to fix it. The problem is I can't use the tactic twice with the same variable names, since (I think) the second ?A will get replaced by the previous definition of A. For example,

example : 4 * 2 = 8 := by
  setm ?A * ?B = (_ : Nat)
  unfold_let A B at *
  clear A B hA hB
  change 4 + 4 = 8
  setm ?A + ?B = (_ : Nat)
  rfl

Trace for the first setm:

▶ 8:3-8:27: information:
mvarIds : [Lean.Name.mkNum `_uniq 316, Lean.Name.mkNum `_uniq 319, Lean.Name.mkNum `_uniq 321]

▶ 8:3-8:27: information:
[Tactic.setm] origPattern : ?A * ?B = ?m.321

Trace for the second setm:

▶ 12:3-12:27: information:
mvarIds : [Lean.Name.mkNum `_uniq 735]

▶ 12:3-12:27: error:
setm: pattern is not definitionally equal to the goal.

▶ 12:3-12:27: information:
[Tactic.setm] origPattern : 4 + 2 = ?m.735

Then it fails with the error.

[Thomas Murrills]

This is actually one of the technical notes I was going to bring up on GitHub :grinning_face_with_smiling_eyes: Basically, once that metavariable ?A exists, it’s still accessible even when assigned. You’ll want to set the usernames of all the mvars to something inaccessible at the end of the tactic to prevent this.

I think it’d be helpful if we had standard mechanisms for avoiding this instead of just going through and writing g.setUsername …, but the thread I started in this stream (#metaprogramming / tactics > Hide intermediate goals from user?) didn’t get any traction, so I never made a PR :P

[Gareth Ma]

Ahhhhh okay. I also tried unsetting the .assign but that didn’t fix the problem. How do I get an inaccessible name?

[Gareth Ma]

Or like just .anonymous?

[Thomas Murrills]

The method I use in the linked thread is just to append "✝", but that's a bit of a hack. .anonymous would probably work. Maybe a better way is to append some randomly generated numbers like happens automatically for metavariables created without a name (e.g. ?m.32124), but I'd need to double-check if this actually prevents e.g. ?m alone from referring to it.

[Jireh Loreaux]

This should be possible with docs#Lean.Core.mkFreshUserName

[Thomas Murrills]

(Also btw I was wrong when I mentioned earlier about getUsername existing! We have FVarId.getUserName, but the canonical way for mvars is (← mvar.getDecl).userName. For some reason. :P)

[Jireh Loreaux]

True, but docs#Lean.MVarId.setUserName exists.

[Thomas Murrills]

Yep! It’s just getting that doesn’t have a name. (I was referring to a message way back where I mentioned getUserName.)

[Jireh Loreaux]

@Thomas Murrills and @Gareth Ma , there is one thing this can't do yet: ?a + _ = ?b

[Jireh Loreaux]

This is because of the allowNaturalHoles := true which is necessary because we're not supplying the expected type.

[Gareth Ma]

Do you want to take over this instead?

[Thomas Murrills]

You're getting ahead of all my comments, I better not wait any longer! :D

[Thomas Murrills]

So, what we want to do there is split the mvarIds we get by kind. The ?a ones are still syntheticOpaque even when allowNaturalHoles := true.

[Jireh Loreaux]

Gareth Ma said:

Do you want to take over this instead?

Nope, you're doing great!

[Thomas Murrills]

We want to keep the non-.syntheticOpaque ones around just to make sure they're assigned at the end of the day, but we only want to do our local decl stuff with the ones that started off as .syntheticOpaque.

[Thomas Murrills]

Does that make sense?

[Jireh Loreaux]

But we still have the problem that we can't elabTermWithHoles something like ?a - ?b = _ without adding type ascriptions (it can't synthesize an instance) because were passing none as the expected type.

[Thomas Murrills]

Oh, hmm, in that case we probably also need to say that we can postpone the synthesis of mvars.

[Thomas Murrills]

Does elabTermWithHoles have an argument for doing that?

[Jireh Loreaux]

no

[Thomas Murrills]

Ah, apparently not. It's not too much trouble to define it:

def elabTermWithHolesPostponing (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType? true) tagSuffix allowNaturalHoles

[Thomas Murrills]

(All we've modified is the argument true to elabTermEnsuringType which lets mvars be postponed.)

[Thomas Murrills]

We'll then want to perform isDefEq to unify what we can, then execute Term.synthesizeSyntheticMVarsNoPostponing. (Note: .synthetic mvars are for typeclass synthesis; .syntheticOpaque are (generally) for user assignment.)

[Thomas Murrills]

Ok, that's a good chance to mention another technical thing, which I think is better to mention here than on GitHub so that I can introduce it from scratch: there's a thing called the metavariable context depth. It's just a number that lives in part of the MetaM state, and determines which metavariables are assignable. Each metavariable remembers the depth it was created at (and we say that such an mvar is "at" that depth). Only metavariables at the current depth or deeper can be assigned.

This lets us prevent assignment of earlier mvars via withNewMCtxDepth, which executes its (monadic) argument at a higher (deeper) depth. You'll see this a lot in front of isDefEq, since we want to be "polite" and not assign any already-present mvars with our isDefEq check.

In this situation, we can't put withNewMCtxDepth directly in front of isDefEq, since that would prevent the mvars from elabTermWithHolesPostponing to not be able to be assigned either. Instead, we want to create the mvars at the new depth as well.

So that's all to say: withNewMCtxDepth should go in front of the bulk of this tactic. :)

[Thomas Murrills]

Also btw, @Jireh Loreaux, are you now taking this over/working on this as well? I see some commits from you on the PR.

[Thomas Murrills]

Oh whoops, I see you said you weren't taking it over. So I guess, which parts do you want to work on and which parts is Gareth working on? Just so I know how to direct my comments, lol. :)

[Jireh Loreaux]

I'm not taking over, I just pushed a few commits I mentioned to Gareth, but I'll be done and let him go for it unless he explicitly asks for my help.

[Thomas Murrills]

Ah I see, cool!

[Thomas Murrills]

I've got to go soon, but before I do, here's my list of suggested changes, including ones we've discussed for summary:

• withNewMCtxDepth (discussed above)
• rename the intermediate mvars (discussed above)
• use elabTermWithHolesPostponing in conjunction with Term.synthesizeSyntheticMVarsNoPostPoning after isDefEq to handle instances (discussed above)
• We should automatically generate sensible names for any ?_ that appears in the pattern
• We should probably have a secondary location: in <loc>. This would determine what actually gets the new fvars substituted in. E.g. if you wanted to substitute everywhere by renaming things in h, setm ... at h in *
• We want to take care to make sure the rfl equations are asserted at the right point, and maybe give the option to not insert them as hypotheses at all

[Jireh Loreaux]

yeah, the rfl equations should go away once lean4#2734 lands in mathlib because they will be unnecessary.

[Jireh Loreaux]

I'm not sure how you would intend to generate sensible names for arbitrary (sub)expressions marked by ?_.

[Gareth Ma]

I need some time to catch up on the discussion, but I will work on this. Thanks for the review, Thomas :)

[Thomas Murrills]

Jireh Loreaux said:

I'm not sure how you would intend to generate sensible names for arbitrary (sub)expressions marked by ?_.

Yeah, I was wondering if there were any existing tools for heuristic naming! E.g. terms of Props should be named h, Nat's should be named n, Lists should be named l, etc., with as many subscripts as necessary to distinguish them from existing names in the context... if not it might be worth making such a tool. (In that case though we can just name the expressions a with a suffix or something here for now.)

[Jireh Loreaux]

I don't think we should do that. It kind of goes against the idea of hygienic naming (at least in spirit, even if not in letter). I think the user should always supply names if they want things introduced into the context.

[Thomas Murrills]

Hmmm. I still think it would be useful to not have to name things yourself, and you could make sure that the names introduced don't conflict with existing names pretty easily. Maybe a compromise would be a Try this: suggestion which replaces the ?_'s with their auto-generated names in this case? But in general, we do introduce things to the context without explicitly naming them ourselves, e.g. via intros or have :=. I'm not totally convinced this is anti-hygienic—is there a type of situation you're thinking of where this causes issues?

[Thomas Murrills]

Also, do you have an issue with more "predictable" auto-generated names for ?_ in this case (e.g. using a₁, a₂, etc.), or just heuristic-generated names?

[Jireh Loreaux]

I think this is a distinct case, different from intros or have :=.

1. intros is name-preserving, so there is (often) an underlying name to be had, and when there isn't the generated name is inaccessible; this is sort of what I mean by hygienic even though that's not entirely what is meant in the macro sense.
2. have := can introduce only one new declaration, and so using this at least makes some sense, even though it's not hygienic in the same way intros is.
3. There are reasons why you might want to intros and not even care about what the names are; for instance, the tactic you apply next closes the goal immediately and can work with unnamed variables.
4. In contrast, (at least in my mind) the entire point of setm is to provide names to things for later reference. If you aren't referencing it later, what is the point to naming it?

[Jireh Loreaux]

Note: I tried to see if my argument in (4) was a straw man. For example, I considered that maybe a rw would work after setm because some of the structure is hidden that rw wouldn't have otherwise seen. But I don't think it is. At least, my naive test works either with or without setm:

example {a b c d : Nat} : (a * b) * (c * d) = (c * d) * (a * b) := by
  rw [mul_comm]

example {a b c d : Nat} : (a * b) * (c * d) = (c * d) * (a * b) := by
  setm ?x * ?y = (?y * ?x : Nat)
  rw [mul_comm]

[Jireh Loreaux]

In addition, we can have references to subexpressions repeated (as in my example above), which is not possible if they're all just ?_. So would ?_ + ?_ = ?_ introduce one new declarations or three?

[Thomas Murrills]

That would introduce three, because each ?_ is independent (this is a general fact, present in e.g. refine). (I'm certainly not suggesting they all be ?_, but the question is "what should happen when the user writes ?_")

I think the question here is "should a tactic be able to introduce a new name"—if ?_ creates an accessible name, you can reference it later just as well as you could have if you wrote ?<name> yourself.

I see the point in making sure the code is readable, though. I'm not totally sure I see the connection to hygiene, as we can solve that problem even if we do introduce names—I suspect we have different ideas as to what the spirit of hygiene is about. :)

I think there are three sensible paths for readability:

• introduce a single kind of accessible name with very predictable behavior, like this—e.g. this₁ etc.
• disallow ?_ in setm
• use a Try this: suggestion to rename ?_'s automatically (cool, but probably not necessary for v1 of the tactic)

[Jireh Loreaux]

What I'm referring to as hygiene is historically related to the actual hygiene issues solved by Lean 4, but at this point they may not be connected. However, what you may not understand, given that you only came to the project with the advent of Lean 4, is that in Lean 3, several tactics (IIRC, cases, by_cases, by_contra, induction, maybe more, or maybe some of these are wrong) would introduce a named (accessible, because this was Lean 3) hypothesis, generally h, into the context when the user didn't supply a name. In Lean 4, this has almost universally been removed. For example:

example (p q : Prop) (foo : p ∨ q) : q ∨ p := by
  cases foo
  · exact Or.inr ‹_› -- unavoidable because the introduced hypothesis has an inaccessible name
  · exact Or.inl ‹_›

(I will admit after testing just now, induction, cases and by_contra all introduce inaccessible names, but by_cases gives you h)

So, my point is that Lean 4 is trying to enforce naming by making things inaccessible. I would suggest that setm exhibits the same behavior: ?_ is allowed, but it generates inaccessible names.

[Jireh Loreaux]

A Try this: is certainly acceptable, because ultimately it means the user is agreeing to the names, but agreed that it's not necessary for v1.

[Thomas Murrills]

Ah, ok, thanks for the context! I considered it, but I wasn't totally sure about the inaccessible names option—I'm not opposed, but like you said, isn't the point of setm to name things? I guess it makes sense if you want to visually clean up your expression but don't want to use the name! Could it be useful for anything else?

[Thomas Murrills]

Hmm...maybe an inaccessible name would still be useful to something that takes in a wildcard location argument?

[Jireh Loreaux]

what do you mean?

[Jireh Loreaux]

oh, nevermind, I see

[Jireh Loreaux]

I'm okay with generating inaccessible names so that things don't break, but I still contend that the whole point is for the user to assign names.

[Gareth Ma]

To be honest, I am kind of lost with the "giving a name or not" discussion, so I will work on the part that I understand first :P I have updated the PR TODO list

[Gareth Ma]

By the way, are tests for tactics required? There doesn't seem to be any in Mathlib right now, but it sounds helpful even just as demo on how to use the tactic

[Jireh Loreaux]

They are in the tests folder.

[Jireh Loreaux]

That's inside the Mathlib4 repo, but outside the Mathlib folder.

[Jireh Loreaux]

And yes, you should have tests.

[Gareth Ma]

Oh that's why I couldn't find them oops

[Jireh Loreaux]

I believe the conclusion of the name discussion is this: if the user writes ?_ + ?a = ?_, then setm should introduce 3 new declarations, one with name a, and two with inaccessible names (those are the ones with a ✝ in the tactic state).

[Gareth Ma]

I am not sure how setm ?A = ?B at <two targets> should work, specifically about the naming. It will try to let A := target1.left and then A := target2.left as well.

[Gareth Ma]

Should we append a number after the variable or something?

[Gareth Ma]

For example,

example (h1 : 1 + 1 = 3) (h2 : 1 + 3 = 5) (h3 : 2 + 2 = 5) : a + b = c := by
  setm ?A + ?B = (_ : Nat) at h1 h2 h3 ⊢
  sorry

Hypotheses introduced:

▶ 1 goal
a b c : Nat
A✝² : Nat := 1
hA✝² : A✝² = 1
B✝² : Nat := 1
hB✝² : B✝² = 1
h1 : A✝² + B✝² = 3
A✝¹ : Nat := 1
hA✝¹ : A✝¹ = 1
B✝¹ : Nat := 3
hB✝¹ : B✝¹ = 3
h2 : A✝¹ + B✝¹ = 5
A✝ : Nat := 2
hA✝ : A✝ = 2
B✝ : Nat := 2
hB✝ : B✝ = 2
h3 : A✝ + B✝ = 5
A : Nat := a
hA : A = a
B : Nat := b
hB : B = b
⊢ A + B = c

[Gareth Ma]

(Would anyone even want to setm at multiple targets though... My original usage was for making rearranging terms easier, and it doesn't make too much sense to rearrange at many goals at once?)

[Jireh Loreaux]

I don't think this is what Thomas meant about multiple locations. Let me write up what it should be.

[Gareth Ma]

This is what's on the branch right now

[Jireh Loreaux]

I know, give me a minute.

[Jireh Loreaux]

Thomas' suggestion was this:

example (h1 : 1 + 1 = 3) (h2 : 1 + 3 = 5) (h3 : 2 + 2 = 5) : a + b = c := by
  setm ?A + ?B = (?C : Nat) at h2 in h1 h2 h3
  sorry

would result in the goal state:

h1 : A + A = B
h2 : A + B = C
h3 : 2 + 2 = C
⊢ a + b + c

[Gareth Ma]

So we should only allow one location for the at part?

[Jireh Loreaux]

By the way, I've had a think about Thomas' comment about a second location, and I think it's not quite what we want. Instead, I think the syntax should be:

syntax (name := setM) "setm" term (usingArg)? (location)? : tactic

The point is that you could then feed an arbitrary term (usingArg), not just hypotheses or the goal, as the thing to match, but it would still support these, and if none is provided then we just use the goal. Then the location is just the list of places we want to do the rewriting. Note that usingArg only allows a single term, which the behavior we want, but then we can rewrite at multiple locations.

[Jireh Loreaux]

One reason not to do this, and it's the same with Thomas' point about rewriting in multiple locations, is that it runs into the same reducible defeq problem you had before when you were using rewrite to do the replacement.

[Jireh Loreaux]

Now, personally, my feeling is that if users want to set ?a and ?b where ?a is a subexpression of ?b, then they should do it in two steps, and that's not overly burdensome. Likewise, if they are trying to give two names to reducibly defeq things, then they shouldn't, and they should give them the same name. Reducible defeq is a very strong (weak? I don't know what the correct adjective is here) form of equality (i.e., most things won't be defeq under this).

[Gareth Ma]

What is usingArg? Do you mind giving an example of like the setm command

[Gareth Ma]

I think your syntax involves typing the actual expression you are matching? As in setm 1 + 2 = 3 using ?A + ?B = ?C or something? But that's what I am trying to avoid with this tactic

[Jireh Loreaux]

usingArg is by definition (you can right-click on hover and click "Go to definition") is "using " term

[Jireh Loreaux]

No, it would be setm ?A + ?B = ?C using h1 at h1 h2 h3 ⊢.

[Jireh Loreaux]

But, crucially, you could replace h1 with any term (and it would match on the type of the resulting expression)

[Jireh Loreaux]

Let me give an example.

[Gareth Ma]

Makes sense, so like setm ?A + ?B = ?A using Nat.add_zero 3 or whatever it's called

[Gareth Ma]

Is that the same as what Thomas suggested but with different words

[Gareth Ma]

Okay, I think I can implement that

[Jireh Loreaux]

example (h : ∀ n, (n + 2) ^ 2 - n ^ 2 = 4 * n + 4) (k : ℕ) (h' : (k + 2) ^ 2 = k ^ 2 + 4 * k + 4) :
    True := by
  setm ?a - ?b = ?c + 4 using h k at h'
  /-
  h : ∀ n, (n + 2) ^ 2 - n ^ 2 = 4 * n + 4
  k : ℕ
  a : ℕ := (k + 2) ^ 2
  b : ℕ := k ^ 2
  c : ℕ := 4 * k
  h' : a = b + c + 4)
  ⊢ True
  -/
  trivial

[Jireh Loreaux]

Maybe you want to see if @Thomas Murrills agrees with this idea first, so it's not just me spitballing.

[Gareth Ma]

If I understand correctly, Thomas' idea is a subset of yours, replacing using -> at and at -> in

[Jireh Loreaux]

Yes, they are pretty similar.

[Jireh Loreaux]

I think the point is that there should be two steps:

1. matching and introducing lets
2. rewriting at the appropriate places.

which means that setMCore should probably return a list (or array) of FVarIds corresponding to the new let declarations, and these can be used by the rewriting procedure.

[Thomas Murrills]

I like the using idea a lot! :) It does make more sense to use at to specify which hypotheses are affected instead of which are used.

[Gareth Ma]

Hi sorry I was a bit busy with other stuff but I am working on it now. I don't understand how to write the elab tactic header thing. This works:

syntax (name := setM) "setm" term (" using " term)? (location)? : tactic
elab_rules : tactic
| `(tactic| setm $stx $[using $usingArg]? $[$loc]?) => do

But this doesn't

elab (name := setM) "setm" stx:term usingArg:(" using " term)? loc:(location)? : tactic => do

For that I mean when I log usingArg, it says it's none even when I am using using. What is the correct syntax for the elab?

[Gareth Ma]

Okay I got the using thing done, it's surprisingly easy

[Gareth Ma]

I am glad that I wrote the tests beforehand though, I broke every single one of them :P

[Gareth Ma]

Just a thought that came to mind. Say I write something like setm ?A + ?B = _ using h k at h1 h2 h3. Should we also introduce h k into the context?

[Gareth Ma]

Otherwise we will have a bunch of As and Bs but no equation linking them directly (in the context)

[Gareth Ma]

I think it's easily possible, but I don't know what to name it. this? What if the user wants to change the name, what should the syntax be :/

[Gareth Ma]

Hi, I did some work now @Thomas Murrills at PR
Looking at the TODOs, I don't think I understand what the remaining two mean :joy: Do you mind explaining a bit? I read the discussion from 2 days ago, where you said

So that's all to say: withNewMCtxDepth should go in front of the bulk of this tactic. :)

but I don't understand what you mean - maybe pointing at the code will be nice for this one :D And about handling instances, I will try that tomorrow. But if you can provide a test that currently fails that will be great too :D

[Gareth Ma]

I learned a whole ton working on this tactic, it's pretty great, and I am actually using it in my main project(?) and proof too.

[Jireh Loreaux]

The withNewMCtxDepth should go before you create any metavariables, so before the elabTermWithHoles

[Jireh Loreaux]

As for a test that fails, suppose the goal is 2 + 3 = 5. We want setm ?a + ?b = _ to succeed without a type ascription

[Jireh Loreaux]

I don't think we need to introduce the term supplied after using into the context. After all, it may frequently just be a hypothesis that already exists in the context.

[Jireh Loreaux]

Also, note that the usingArg I was referring to before was docs#Mathlib.Tactic.usingArg

[Gareth Ma]

Jireh Loreaux said:

I don't think we need to introduce the term supplied after using into the context. After all, it may frequently just be a hypothesis that already exists in the context.

Hmm but think about the example I gave

[Gareth Ma]

I will have to type setm ?A+?B=_ using h a; have := h a

[Gareth Ma]

will something like setm ?A+?B=_ using this:h a be fine? :thinking:

[Gareth Ma]

Jireh Loreaux said:

Also, note that the usingArg I was referring to before was docs#Mathlib.Tactic.usingArg

I think I saw that but also if you look at the entire mathlib Tactic, it’s not really used, people just do it my way

[Gareth Ma]

Just grep “ using “ term

[Gareth Ma]

(Sorry as you can tell I’m on phone

[Gareth Ma]

I am back on computer. This is what I meant: Screenshot-2023-10-27-at-10.05.03.png

Though we can definitely do a PR or something, that'll be cool.

[Gareth Ma]

This doesn't work, it says "unknown metavariable ..." Screenshot-2023-10-27-at-10.57.10.png

[Gareth Ma]

Very weird bugs...

import Mathlib.Tactic

lemma fails : 1 + 3 - (3 : ℝ) = 1 := by
  setm ?A + ?B - ?B = (1 : ℝ)
  rewrite [show ∀ A B : ℝ, A + B - B = A from fun A B => add_sub_cancel A B]
  unfold_let A B ; clear hA hB A B
  setm ?A = (1 : ℝ)
  /-
  ▶ 8:8-8:10: error:
  synthetic hole has already been defined and assigned to value incompatible with the current context
    A

  ▶ 8:3-8:20: error:
  setm: ?A = (1 : ℝ) is not definitionally equal to the goal.
  -/
  trivial

lemma works : 1 + 3 - (3 : ℝ) = 1 := by
  setm ?A + ?B - ?B = (1 : ℝ)
  rewrite [show A + B - B = A from add_sub_cancel A B]
  unfold_let A B ; clear hA hB A B
  setm ?A = (1 : ℝ)
  trivial

[Gareth Ma]

I think I need help with this example, it's quite confusing...

[Jireh Loreaux]

Sorry, I don't think I have time to look at this today.

[Thomas Murrills]

Unfortunately I also probably won't have time today :sweat_smile: But I will (also) look over things/respond when I next have the chance!! :)

[Gareth Ma]

No worries, as always it’s not in a rush. I’ll push with the failed cases first

[Thomas Murrills]

I'm looking at this again now :)

[Gareth Ma]

Ah sorry didn’t see this. I really hope the Zulip people implement “subscribe to thread” with push notifs ASAP

[Gareth Ma]

Maybe I should write a browser extension for it lol

[Gareth Ma]

Anyways yes, the latest code I sent with fails and works is my latest progress

[Thomas Murrills]

@Gareth Ma It’s ok, I was looking and then got called away, lol :sweat_smile: I’m going to keep looking tomorrow!

[Thomas Murrills]

Okay, so I'll mention some stuff here as I notice it! :)

Also, I don't want to simply be telling you stuff to do, so feel free to simply react to something if you'd be okay with me pushing a commit for it, since I am playing with it on my end anyway to make sure what I'm saying makes sense, and could easily do so if it's convenient. Of course I also don't want to get in the way of learning, so, totally up to you, just wanted to give the option. :)

[Thomas Murrills]

The issue with "unknown goal" when adding withNewMCtxDepth is because withNewMCtxDepth does more than reset the depth when it's done—it actually resets the whole mvar context to whatever it was when it started. (I wasn't expecting this, tbh.) So, all metavariables created during this time should be gone in the result: assigned and replaced with their assignments, essentially. The fact that we replace the main goal with one we've created inside withNewMCtxDepth is the issue.

This makes our job a little tricky if we want to use withNewMCtxDepth. Inside withNewMCtxDepth, we have to

1. create the mvars in elabTermWithHoles
2. perform isDefEq to assign them
3. make sure all newly-created mvars are assigned

while also making sure we do not create the goal we'll replace the main goal with (or any other goals that make it outside).

We could manipulate the depth ourselves, but I'd rather not be bespoke here. The simplest option is to simply return the elaborated expression, the array of MVarIds we'll be replacing, and their assignments. But I'm reluctant to even be in possession of MVarIds that the mctx doesn't know about, and it seems like a lot of manual management. It's just a bit awkward.

I'm not sure what the best solution is to this issue. Maybe it is actually worth just creating a new combinator like withNewMCtxDepth but which behaves differently and doesn't reset the mctx. In the meantime not increasing the depth at all seems ok-ish. I'll think about it, but I'd be interested to hear what more experienced metaprogrammers would do here.

[Thomas Murrills]

Ok, some small things:

[Thomas Murrills]

• Instead of mvarIdsPairs.forM fun (mvarIdOld, mvarExprNew) => do, we should simply be able to use for (mvarIdOld, mvarExprNew) in mvarIdsPairs do

[Thomas Murrills]

• fun takes match alternatives, so fun x => match x with | ... | ... is equivalent to just fun | ... | ...!

[Thomas Murrills]

A more major thing: we seem to be using the username of the mvar quite heavily; we shouldn't, as this doesn't reflect the actual logic we want to implement. Rather, we should

1. split the mvars we get from elabTermWithHoles into .syntheticOpaque ones and otherwise
2. synthesize the postponed mvars
3. make sure all the non-originally-syntheticOpaque mvars are assigned by the end of the isDefEq`
4. just iterate through all the (formerly) .syntheticOpaque ones instead of matching on the username

(Note that we only want to set the syntheticOpaque ones to natural anyway.)

Likewise, we do a lot of copying usernames from old mvars to new ones, and we shouldn't do that (nor should we need to).

[Thomas Murrills]

Instead of using evalTactic and exprToSyntax, I think it'd be better style to use MVarId.assert—or even assertAfter to get the hypotheses in a nice place!

[Thomas Murrills]

Again, happy to contribute instead of just saying what needs to be done, lol. Lmk either way! :)

[Gareth Ma]

I think I can try it out first :) i will be away from keyboard until Sunday then I’ll work on it!

[Kyle Miller]

I'd suggest using a different strategy than trying to fight with metavariable names. What you can do is create fresh metavariables for each ?n that appears in the expression, record the provided names, create a local context with let bindings for each of these, then elaborate, do a defeq check, and replace the main goal.

For the local context, a trick you can do is that for metavariable ?n, you create yet another new metavariable ?n', create let n := ?n' in the local context, and then assign ?n := ?n'. That way when you elaborate the pattern you get the replacement of ?n by n for free.

One thing to be careful about is that you should elaborate in the context with these new locals to get the replacements to work correctly, but you don't want the names to be accessible yet. You can use mkFreshUserName for these locals to temporarily make them inaccessible, and then you rename them later.

Also, watch out, elabTermWithHoles is not what you want. It doesn't take into account the goal when it elaborates. Here's an example that fails:

example (x y : Int) : x + 1 + y = 2 := by
  setm ?z + ?w = 2
  sorry

You can get it to succeed by changing the pattern to ?z + ?w = (2 : Int). The issue is that elabTermWithHoles causes default instances to be entertained.

I've made an implementation using this strategy, just for the setm patt syntax -- no using or at clauses.

code

/-
Copyright (c) 2023 Gareth Ma. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gareth Ma
-/
import Lean
import Mathlib.Tactic.DefEqTransformations

/-!
# The `setm` tactic

The `setm` tactic ("`set` with matching") is used for introducing `let` declarations representing
subexpressions of the goal or in the types of local hypotheses.

For example, if the goal is `⊢ (x + 5) ^ 2 + (2 * y + x) * (x + 5) + 3 = 28` (with `x y : ℕ`), then
`setm ?a ^ 2 + ?b * ?a + 3 = 28` would introduce `a : ℕ := x + 5` and `b : ℕ := 2 * y + 5` into the
context and change the goal to `a ^ 2 + b * a + 3 = 28`
-/

namespace Mathlib.Tactic
open Lean Parser Tactic Elab Tactic Meta

initialize registerTraceClass `Tactic.setm

structure SetMReplaceState where
  /-- Collected mvars to use for each fvar that we want to introduce.
  A name can be anonymous, and in that case it gets an auto-generated name. -/
  mvars : Array (Name × MVarId) := #[]

abbrev SetMReplaceM := StateT SetMReplaceState TermElabM

/-- Collect all synthetic holes and replace them with fresh metavariables. -/
def replaceWithMVars (stx : Term) : SetMReplaceM Term := do
  let stx ← stx.raw.replaceM fun stx => do
    if let `(?$n:ident) := stx then
      let .str .anonymous n := n.getId
        | throwError "In {stx}, the name must either be an atomic string or be a hole (`_`)."
      if let some (_, mvar) := (← get).mvars.find? (·.1 == n) then
        withRef stx <| Term.exprToSyntax (.mvar mvar)
      else
        let mvar ← mkFreshExprMVar none
        modify fun s => {s with mvars := s.mvars |>.push (n, mvar.mvarId!)}
        withRef stx <| Term.exprToSyntax mvar
    else if let `(?_) := stx then
      let mvar ← mkFreshExprMVar none
      modify fun s => {s with mvars := s.mvars |>.push (.anonymous, mvar.mvarId!)}
      withRef stx <| Term.exprToSyntax mvar
    else
      pure none
  return ⟨stx⟩

/-- Creates locals for each mvar. The `Option` in the resulting array records whether we should
later make the given variable be accessible. -/
partial def createLocals {α : Type} (mvars : Array (Name × MVarId))
    (m : Array (Option Name × Expr) → TermElabM α) : TermElabM α :=
  let rec run (i : Nat) (fvars : Array (Option Name × Expr)) : TermElabM α := do
    if i < mvars.size then
      let (n, mvar) := mvars[i]!
      let (r?, n) ← do
        if n.isAnonymous then
          pure (none, ← mkFreshUserName `x)
        else
          pure (some n, ← mkFreshUserName n)
      -- Create a new mvar so that we can assign the old one to the created fvar
      let mvar' ← mkFreshExprMVar (← mvar.getType)
      withLetDecl n (← mvar.getType) mvar' fun fvar => do
        mvar.assignIfDefeq fvar
        run (i + 1) (fvars.push (r?, fvar))
    else
      m fvars
  run 0 #[]

/--
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).

For example, if the goal is `⊢ (x + 5) ^ 2 + (2 * y + x) * (x + 5) + 3 = 28` (with `x y : ℕ`), then
`setm ?a ^ 2 + ?b * ?a + 3 = 28` would introduce `a : ℕ := x + 5` and `b : ℕ := 2 * y + 5` into the
context and change the goal to `a ^ 2 + b * a + 3 = 28`.

Likewise if the local context contains `h : (x + 5) ^ 2 + (2 * y + x) * (x + 5) + 3 = 28`
(with `x y : ℕ`), then `setm ?a ^ 2 + ?b * ?a + 3 = 28 at h` would introduce `a : ℕ := x + 5` and
`b : ℕ := 2 * y + 5` into the context and changes the type to `h : a ^ 2 + b * a + 3 = 28`. -/
syntax (name := setM) "setm" term (" using " term)? (location)? : tactic

elab_rules : tactic
| `(tactic| setm $stx) => do
  let g ← getMainGoal
  let g' ← g.withContext do
    let (pattern, {mvars}) ← (replaceWithMVars stx).run {}
    createLocals mvars fun fvars => do
      Term.withSynthesize do
        let pattern ← Term.elabTerm pattern none
        let g' ← mkFreshExprSyntheticOpaqueMVar pattern (tag := (← g.getTag))
        -- Make the variables from the named synthetic holes be accessible:
        g'.mvarId!.modifyLCtx fun ctx => Id.run do
          let mut ctx := ctx
          for (r?, fvar) in fvars do
            if let some r := r? then
              ctx := ctx.setUserName fvar.fvarId! r
          pure ctx
        g'.mvarId!.withContext do
          if ← withAssignableSyntheticOpaque (isDefEq pattern (← g.getType)) then
            g.assign <| ← mkLetFVars (fvars.map (·.2)) g'
            pure g'.mvarId!
          else
            throwError "setm pattern{indentD pattern}\nis not definitionally equal {
              ""}to the goal{indentD (← g.getType)}\n\nContext:{g'.mvarId!}"
  replaceMainGoal [g']

example (x y : Nat) : (x + 5) ^ 2 + (2 * y + x) * (x + 5) + 3 = 28 := by
  setm ?a ^ 2 + ?b * ?a + 3 = 28
  /-
  x y : Nat
  a : Nat := x + 5
  b : Nat := 2 * y + x
  ⊢ a ^ 2 + b * a + 3 = 28
  -/
  sorry

example (x y : Nat) : (x + 5) ^ 2 + (2 * y + x) * (x + 5) + 3 = 28 := by
  setm ?a ^ 2 + ?_ * ?a + 3 = 28
  /-
  x y : Nat
  a : Nat := x + 5
  x✝ : Nat := 2 * y + x
  ⊢ a ^ 2 + x✝ * a + 3 = 28
  -/
  sorry

example (x y : Int) : x + 1 + y = 2 := by
  setm ?z + ?w = 2
  /-
  x y : Int
  z : Int := x + 1
  w : Int := y
  ⊢ z + w = 2
  -/
  sorry

[Thomas Murrills]

Kyle Miller said:

Also, watch out, elabTermWithHoles is not what you want. ... The issue is that elabTermWithHoles causes default instances to be entertained.

Note this part of the conversation, which addresses that:

Thomas Murrills said:

Ah, apparently not. It's not too much trouble to define it:

def elabTermWithHolesPostponing (stx : Syntax) (expectedType? : Option Expr) (tagSuffix : Name) (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
  withCollectingNewGoalsFrom (elabTermEnsuringType stx expectedType? true) tagSuffix allowNaturalHoles

[Thomas Murrills]

(I do switch back to just calling it elabTermWithHoles for convenience later on in the conversation, though. Really elabTermWithHoles should take a mayPostpone argument...)

[Thomas Murrills]

Kyle Miller said:

For the local context, a trick you can do is that for metavariable ?n, you create yet another new metavariable ?n', create let n := ?n' in the local context, and then assign ?n := ?n'. That way when you elaborate the pattern you get the replacement of ?n by n for free.

I liked this trick! I extended it to a slightly different assignment than the one given here, where we assign ?n to the fvar n, then perform the isDefEq check. This means we don't need withAssignableSyntheticOpaque. (Which is maybe the assignment you meant to write, if there was a typo? I'm not sure.)

More generally, I have a different strategy I thought I'd share, which in some senses is cleaner, but requires a bit more metaprogramming infrastructure than we have currently—mostly in the form of tweaks to existing things:

1. elabTermWithHoles should provide the option to do three things differently: (1) preserve the MetavarKind of the holes (by default, .natural holes are made .syntheticOpaque when allowNaturalHoles := true) (2) not tag the untagged new goals—currently it tags them all using the parent tag (3) take a mayPostpone argument to pass to elabTermEnsuringType. I create elabTermWithHoles' for this.
2. Currently withNewMCtxDepth resets the whole MCtx once it finishes, meaning you lose all mvars and assignments created during it. However, the advice for matching like this is to create the terms inside a withNewMCtxDepth—it would be convenient to have a toggle for whether to reset the context or not. I introduce withNewMCtxNoReset for this, which could use a better name. It also lowers the depth of any mvars back to the resulting ambient depth upon exiting. (In the future it could use another line of code to only bother doing this for unassigned mvars.) I'm assuming that we want the ambient depth never to be lower than the depth of any mvar, given how isAssignable is written.
3. I introduce withoutCreatingAccessibleGoals as a generic combinator for hiding metavariables created during a tactic. By default, only new assigned metavariables are made to have an inaccessible name.

Note that the above makes up the bulk of the following code; the actual setm-relevant parts are the two definitions at the bottom.

Now, @Gareth Ma, feel free to ignore this and/or use this! Like Kyle, I've left off all using and at functionality. If you'd like me to PR my utilities, I'm happy to do so (if Kyle and/or others think they're reasonable and useful in other circumstances, that is; this is just a draft).

Also, by the way, I realized I was wrong about there not existing an MVarId.getUserName—only it's not called getUserName, it's called getTag! I had forgotten that metavariables' usernames were sometimes called "tags". (I think this is a holdover from Lean 3 when metavariables actually had things called tags?)

[Thomas Murrills]

code

import Lean
import Mathlib.Tactic.DefEqTransformations

/-!
# The `setm` tactic

The `setm` tactic ("`set` with matching") is used for introducing `let` declarations representing
subexpressions of the goal or in the types of local hypotheses.

For example, if the goal is `⊢ (x + 5) ^ 2 + (2 * y + x) * (x + 5) + 3 = 28` (with `x y : ℕ`), then
`setm ?a ^ 2 + ?b * ?a + 3 = 28` would introduce `a : ℕ := x + 5` and `b : ℕ := 2 * y + 5` into the
context and change the goal to `a ^ 2 + b * a + 3 = 28`
-/

namespace Mathlib.Tactic
open Lean Parser Tactic Elab Tactic Meta

/--
  Like `withCollectingNewGoalsFrom`, execute `k`, and collect new "holes" in the resulting
  expression. However, this function differs in two key respects:

  1. It preserves the `MetavarKind` of each metavariable (in contrast, `withCollectingNewGoalsFrom`
  turns natural holes into synthetic opaque holes and uses `withAssignableSyntheticOpaque` when
  `allowNaturalHoles := true`)
  2. It does not tag all untagged goals.

-/
def withCollectingNewGoalsFrom' (k : TacticM Expr)
    (allowNaturalHoles := false) : TacticM (Expr × List MVarId) := do
  let mvarCounterSaved := (← getMCtx).mvarCounter
  let val ← k
  let newMVarIds ← getMVarsNoDelayed val
  /- ignore let-rec auxiliary variables, they are synthesized automatically later -/
  let newMVarIds ← newMVarIds.filterM fun mvarId => return !(← Term.isLetRecAuxMVar mvarId)
  /- Filter out all mvars that were created prior to `k`. -/
  let newMVarIds ← filterOldMVars newMVarIds mvarCounterSaved
  /- If `allowNaturalHoles := false`, all natural mvarIds must be assigned.
  Passing this guard ensures that `newMVarIds` does not contain unassigned natural mvars. -/
  unless allowNaturalHoles do
    let naturalMVarIds ← newMVarIds.filterM fun mvarId => return (← mvarId.getKind).isNatural
    logUnassignedAndAbort naturalMVarIds
  let newMVarIds ← sortMVarIdsByIndex newMVarIds.toList
  return (val, newMVarIds)

/-- Like `elabTermWithHoles`, but with three key differences:

  1. It preserves the `MetavarKind` of each metavariable when `allowNaturalHoles := true`
  2. It does not tag untagged goals
  3. It enables postponing metavariables via `mayPostpone := true` (the default is
  `mayPostpone := false`)
-/
def elabTermWithHoles' (stx : Syntax) (expectedType? : Option Expr) (allowNaturalHoles := false)
    (mayPostpone := false) : TacticM (Expr × List MVarId) := do
  withCollectingNewGoalsFrom' (elabTermEnsuringType stx expectedType? mayPostpone) allowNaturalHoles

set_option autoImplicit true in
/-- Executes `k`, and makes all of the metavariables created during `k` inaccessible to the user by
acting on their username with `mkFreshUserName`.

By default, only assigned metavariables are made inaccessible.

The argument `shouldHide : MVarId → m Bool` can be specified to hide metavariable names using a
condition other than assignment status; when `← shouldHide mvarId` is `true`, `mvarId` will be
renamed with an inaccessible name. -/
def withoutCreatingAccessibleGoals [Monad m] [MonadLiftT CoreM m] [MonadMCtx m] (k : m α)
    (shouldHide : MVarId → m Bool := MVarId.isAssigned) : m α := do
  let initialMVarCounter := (← getMCtx).mvarCounter
  let val ← k
  for (mvarId, decl) in (← getMCtx).decls do
    if decl.index >= initialMVarCounter
        && !decl.userName.isInaccessibleUserName
        && (← shouldHide mvarId)
    then
      let newUserName ← mkFreshUserName decl.userName
      modifyMCtx fun mctx => mctx.setMVarUserName mvarId newUserName
  return val

/-- Decrease the depth of a `MetaVarContext` as well as the depths of all metavariables in it to at
most `depth`. If `levelAssignDepth` is given, decrease the `levelAssignDepth` and the `lDepth`.

Note that the resulting `MetavarContext`'s `depth` and `levelAssignDepth` will be exactly `depth`
and `levelAssignDepth`; it is possible they are raised by `decDepthTo`. This ensures that the
resulting `MetavarContext` has no mvars with higher depth than the ambient depth. -/
def _root_.Lean.MetavarContext.decDepthTo (mctx : MetavarContext) (depth : Nat)
    (levelAssignDepth : Option Nat := none) : MetavarContext := Id.run do
  -- Could possibly avoid changing the depth for assigned mvars.
  let decls := mctx.decls.map fun decl => if decl.depth > depth then { decl with depth } else decl
  if let some levelAssignDepth := levelAssignDepth then
    let lDepth := mctx.lDepth.map (min levelAssignDepth)
    pure { mctx with decls, depth, lDepth, levelAssignDepth }
  else
    pure { mctx with decls, depth }

set_option autoImplicit true in
private def withNewMCtxDepthNoResetImp (allowLevelAssignments : Bool) (x : MetaM α) : MetaM α := do
  let saved ← get
  let postponed := saved.postponed
  let depth := saved.mctx.depth
  let levelAssignDepth := if allowLevelAssignments then none else some saved.mctx.levelAssignDepth
  modify fun s => { s with mctx := s.mctx.incDepth allowLevelAssignments, postponed := {} }
  try
    x
  finally
    modify fun s =>
      { s with mctx := s.mctx.decDepthTo depth levelAssignDepth, postponed := s.postponed ++ postponed }

set_option autoImplicit true in
/--
  `withNewMCtxDepthNoReset k` is like `withNewMCtxDepth`, but does not reset the whole mvar context
  after evaluation. This means that metavariables created within `withNewMCtxDepthNoReset` (and
  their assignments) persist after `withNewMCtxDepthNoReset`. The prior `depth`,
  `levelAssignDepth`, are restored; all mvar depths (and, if level
  assignments were *not* allowed, level mvar depths) are lowered to at most prior depth. This
  ensures that the ambient depth is not lower than the depth of any mvar.

  `k` is run with no postponed mvars initially; any
  postponed mvars created during `k` are accumulated and retained.
-/
def withNewMCtxDepthNoReset [MonadControlT MetaM n] [Monad n] (k : n α)
    (allowLevelAssignments := false) : n α :=
  mapMetaM (withNewMCtxDepthNoResetImp allowLevelAssignments) k


/-! # setm -/

/-- Introduce `let n : type := val` to the local context of `goal` for each element
`(n, type, val)` of `locals`. If `n` is `.anonymous`, then an inaccessible version of `x is used
for the name. -/
def _root_.Lean.MVarId.createLocals (goal : MVarId) (locals : Array (Name × Expr × Expr)) :
    MetaM (Array FVarId × MVarId) := do
  let mut g := goal
  for (name, type, val) in locals.reverse do
    let name ← if name.isAnonymous then mkFreshUserName `x else pure name
    g ← g.define name type val
  g.introNP locals.size

/-- [`setm` docstring] -/
elab "setm " patt:term : tactic => withMainContext <| withoutCreatingAccessibleGoals <|
  withNewMCtxDepthNoReset <| Term.withSynthesize do
    let g ← getMainGoal
    let savedUserName ← g.getTag
    let (e, gs) ← elabTermWithHoles' patt none (allowNaturalHoles := true) (mayPostpone := true)
    let gs := gs.toArray
    -- Extract synthetic opaque goals (`?l`/`?_`) and natural goals (`_`) in `patt`.
    let ldeclGoals   ← gs.filterM fun g => return (← g.getKind).isSyntheticOpaque
    let placeholders ← gs.filterM fun g => return (← g.getKind).isNatural
    -- Create `fvars` consisting of `let l : _ := _` for each `?l` in `patt`.
    let (fvars, g) ← g.createLocals <|← ldeclGoals.mapM fun l => l.withContext do
      let name ← l.getTag
      let type ← mkFreshExprMVar none
      let val  ← mkFreshExprMVar type
      pure (name, type, val)
    g.withContext do
      -- Assign each `?l` in `patt` to the corresponding new fvar in the context of `g`.
      for i in [:ldeclGoals.size] do
        ldeclGoals[i]!.assign (.fvar fvars[i]!)
      -- Unify `patt` with the goal, and assign it.
      let g ← g.change e -- Should wrap or inline for a better error message!
      logUnassignedAndAbort placeholders -- Ensure all `_` are assigned
      g.setUserName savedUserName
      replaceMainGoal [g]