Help with writing tactic `setm`

Stream: metaprogramming / tactics

[Gareth Ma]

bump

[Thomas Murrills]

Btw, I think I also included (some/all of) these utilities in a PR for refine?, but it was requested that the refine? PR be split into utils and refine? itself, and then that the meta utils PR be split further into individual API contributions: #8503

[Thomas Murrills]

(I haven’t had the motivation to do so since, but maybe this would prompt that.)

And reflecting on it now, I think some of these would maybe be “better” as modifications to core than as mathlib4 contributions which just copy a core function and add more functionality which could be easily included in the core implementation but just isn’t. But I’m not sure how fast those PRs would move, or if they’d be welcome at all…

[Thomas Murrills]

But looking back at this thread, just using Kyle’s implementation might be quickest for getting something in. I forget if there was some advantage conferred by using this alternative strategy besides being less bespoke after introducing metaprogramming infrastructure.

[Gareth Ma]

I imagine modifying core will be very very slow.

[Gareth Ma]

FYI I bumped this thread because of https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/too.20many.20FunLikes/near/428202012

[Thomas Murrills]

It’s not always very slow—plus, now(?) there’s code ownership for certain parts, giving those code owners the ability to review and merge things using their own judgment, which I imagine speeds things up a bit.

[Gareth Ma]

My only experience was looking at https://github.com/leanprover/lean4/issues/2414

[Gareth Ma]

But the code ownership part sounds good

[Thomas Murrills]

In any case I do think that in this specific case the Kyle way is definitely the most efficient way to get it landing, even considering recent speedups. :)

[Gareth Ma]

I will reread it and see what I can do lol, it's been a while since I wrote any metaprogramming

[Thomas Murrills]

Also, would it be possible to change the name of this topic to something setm related? :eyes:

[Gareth Ma]

:skull: :skull: Yes yes definitely

[Gareth Ma]

Screenshot-2024-03-21-at-20.27.54.png

I can't rename the thread because I can't move some messages. I think it's because the messages are more than 7 days old.

[Gareth Ma]

Can you or others with permission do it for me? The new thread can be called setm development thread or something

[Bhavik Mehta]

Has there been progress on this tactic / the PR? I just came across a case where this would be useful to me!

[Kyle Miller]

In case it's helpful, in lean4#6022 the change tactic will be able to assign named metavariables, for example

example (x y z : Nat) : x + y = z := by
  change ?a = _
  let w := ?a
  -- now `w : Nat := x + y`

[Bhavik Mehta]

oh interesting! does that mean there's an alternative (simpler?) implementation of setm available as a combination change + let?

[Jireh Loreaux]

I also just found a need for setm. @Kyle Miller will it be as simple as a change + set macro? Also, note that on the live server on the latest nightly, the change has red squiggles underneath, but no error message appears:

import Lean

example (x y z : Nat) (h : x + y = z) : x + y = z := by
  change ?a = _
  let w := ?a
  -- now `w : Nat := x + y`
  exact h

[Kyle Miller]

I think that's a transient error Jireh. I've heard that somehow the live server can get into a state where the squiggles are from a union of multiple versions running simultaneously.

[Kyle Miller]

I just checked myself, and I didn't get squiggles.

[Kyle Miller]

Can you remind me what setm is supposed to do to the goal? If it's supposed to be a = z in the end, then you can do it with a different order:

example (x y z : Nat) (h : x + y = z) : x + y = z := by
  let a : ?_ := ?a
  change a = _
  /-
  a : Nat := x + y
  ⊢ a = z
  -/
  exact h

[Jireh Loreaux]

It should also replace x + y with a in h, just like the set tactic. This can be accomplished with change + set like so (I just copied the set tactic file into the below so it will work on the nightly without Mathlib):

import Lean.Elab.Tactic.ElabTerm

namespace Mathlib.Tactic
open Lean Elab Elab.Tactic Meta

syntax setArgsRest := ppSpace ident (" : " term)? " := " term (" with " "← "? ident)?

syntax (name := setTactic) "set" "!"? setArgsRest : tactic

macro "set!" rest:setArgsRest : tactic => `(tactic| set ! $rest:setArgsRest)

elab_rules : tactic
| `(tactic| set%$tk $[!%$rw]? $a:ident $[: $ty:term]? := $val:term $[with $[←%$rev]? $h:ident]?) =>
  withMainContext do
    let (ty, vale) ← match ty with
    | some ty =>
      let ty ← Term.elabType ty
      pure (ty, ← elabTermEnsuringType val ty)
    | none =>
      let val ← elabTerm val none
      pure (← inferType val, val)
    let fvar ← liftMetaTacticAux fun goal ↦ do
      let (fvar, goal) ← (← goal.define a.getId ty vale).intro1P
      pure (fvar, [goal])
    withMainContext <|
      Term.addTermInfo' (isBinder := true) a (mkFVar fvar)
    if rw.isNone then
      evalTactic (← `(tactic| try rewrite [show $(← Term.exprToSyntax vale) = $a from rfl] at *))
    match h, rev with
    | some h, some none =>
      evalTactic (← `(tactic| have%$tk
        $h : $a = ($(← Term.exprToSyntax vale) : $(← Term.exprToSyntax ty)) := rfl))
    | some h, some (some _) =>
      evalTactic (← `(tactic| have%$tk
        $h : ($(← Term.exprToSyntax vale) : $(← Term.exprToSyntax ty)) = $a := rfl))
    | _, _ => pure ()

end Mathlib.Tactic

example (x y z : Nat) (h : x + y = z) : x + y = z := by
  change ?a = _
  set a := ?a
  exact h