Lean4 `tactic.assert` equivalent?

Stream: new members

[Ian Benway]

Hi! I'm new to the Zulip and am trying to learn metaprogramming in Lean 4. I was trying to write a tactic for practice that just adds a hypothesis to the local context. I can't seem to find out how to do this—I'm mostly learning from the already implemented mathlib4 tactics. I'd like to have something like Lean 3's tactic.assert. How can I add something simple to the context like that?

[Henrik Böving]

Would docs4#Lean.Meta.assertHypotheses be what you are looking for? Or something from that file in general?

[Ian Benway]

Yes! I don't know how I totally missed that file, thank you.
So my understanding is assert takes in an MVarId, Name, Expr, Expr where I'm needing the type as the first expression and the value as the second expression, it seems. If all I have is i : ident and t : term, in Lean 3, I believe I could do something similar to tactic.assert 'i 't.
How can I get the MVarId from i and the Exprs from t?

[Henrik Böving]

MVarId is just a wrapper around a name docs4#Lean.MVarId so that's trivial to create. I'm not 100 percent sure what a term in lean 3 is in 4, I've not seen this term around here yet. Once you have an expression you can however gets its type by using the docs4#Lean.Meta.inferType function

[Jannis Limperg]

Here's a bird's-eye view of what you need to define your tactic:

• A syntax (name := yourTactic) ... : tactic declaration that defines the syntax of your tactic.
• An elaborator for this syntax:

@[tactic yourTactic]
def elabYourTactic : Tactic   -- Tactic = Syntax -> TacticM Unit

In this elaborator, you can use elabTerm or a variation to turn a Syntax into an Expr.

• In elabYourTactic, use liftMetaTactic or a variation to plug in Meta.assertHypotheses.

Background for the last step: a 'MetaM tactic' is a def of type MVarId -> MetaM (List MVarId). The input MVarId is the initial goal (goals are represented as metavariables); the output represents the goals generated by the tactic. liftMetaTactic applies the MetaM tactic to the first goal in the current goal list.

Hope this helps a bit! The Lean 4 metaprogramming API is a bit daunting coming from Lean 3.

[Ian Benway]

Thank you, Jannis. This was incredibly helpful! I agree with you totally, Lean 4 metaprogramming is super daunting.
I'm still having a bit of trouble though. I'm trying to make my own sort of let tactic, just to get the hang of things. I think I want to make tme below from a TacticM Expr to an Expr. Is that the way to go here, and what do I need to do that?

syntax (name := myLet) "set " ident " : " term " := " term : tactic

@[tactic myLet]
def elabMyLet (i tp tm : Syntax) : Tactic :=
  let nm := `i
  let tme := elabTerm tm (some (mkConst `tp)) --TacticM Expr
  let tpe :=  inferType tme     --Error: tme needs to be of type Expr
  liftMetaTactic λx => (Meta.assert x nm tme tpe)  --Error: tme needs to be of type Expr

elab_rules : tactic
   | `(tactic| set $i:ident : $tp:term := $tm:term) =>
    withMainContext do
    let tdsf := elabMyLet i tp tm