Learning about metaprogramming

Stream: lean4

[Adam Topaz]

Hi all, I wanted to learn a little bit of metaprogramming in Lean4, so I am trying to write a version of mathlib's apply_fun tactic.
So far, I have something fairly rudimentary with the following code (note: this is still very far from the full capability of mathlib's apply_fun tactic):

import Lean

open Lean Elab.Tactic

syntax "applyFun " term " at " ident : tactic

elab_rules : tactic
| `(tactic|applyFun $f:term at $i:ident) =>
  withMainContext do
    let goal ← getMainGoal
    match (← getLCtx).findFromUserName? i.getId with
    | some d => do
        evalTactic $ ← `(tactic|have $i := congrArg $f $i)
        try replaceMainGoal [← Meta.clear (← getMainGoal) d.fvarId]
        catch | _ => return
    | none => Meta.throwTacticEx `applyFun goal f!"Hypothesis named {i} not found."

example (a b : Nat) (f : Nat → α) (h : a = b) : f a = f b := by
  applyFun f at h
  exact h

This seems to work (at least in the example) when we actually apply a function.
However, one thing I cannot figure out is how to make this work if f has some type that has an appropriate CoeFun instance (the mathlib Lean3 version is able to do this, and much more!). Can someone point me in the right direction here?
Also, I am very new to metaprogramming and programming in Lean4 in general, any advice about improving the code above would be much appreciated!

[David Renshaw]

Style-wise, the concrete syntax should remain apply_fun. See https://github.com/leanprover-community/mathlib4/blob/dda51df299ce844cc686ecbd6f08c17a4a247078/Mathlib/Mathport/Syntax.lean#L426

[Arthur Paulino]

I think you want to do

try
  evalTactic $ ← `(tactic|have $i := congrArg $f $i)
  replaceMainGoal [← Meta.clear (← getMainGoal) d.fvarId]
catch _ => Meta.throwTacticEx `applyFun goal "tactic failed"

So even the have foo := congrArg ... is guarded from errors

[Arthur Paulino]

I've never done instance inference in metaprogramming before, but I believe you could try mkAppM with the inferInstance function unless someone else tells us a more appropriate method

[Arthur Paulino]

How do I do this without writing syntax in my elaborator?

let natInt ← elabTerm (← `(Nat × Int)) none

[Alexander Bentkamp]

let natInt ← mkAppM ``Prod #[mkConst ``Nat, mkConst ``Int]

[Arthur Paulino]

Thanks! I had done

mkAppM ``Prod.mk ...

before, but I suspected I had done something wrong

[Jannis Limperg]

(FYI const ``Nat [] is now the preferred form and will save you from the mkConst footgun of forgetting to specify the universe levels. Also, here you can use mkAppN instead of mkAppM.)

[Arthur Paulino]

Jannis Limperg said:

(FYI const ``Nat [] is now the preferred form and will save you from the mkConst footgun of forgetting to specify the universe levels. Also, here you can use mkAppN instead of mkAppM.)

Where is const?

[Arthur Paulino]

Ah, Expr.const probably

[Scott Morrison]

Regarding the mkConst footgun, mathlib4 now defines (in Mathlib.Lean.Expr.Basic)

/-- Same as `mkConst`, but with fresh level metavariables. -/
def mkConst' (constName : Name) : MetaM Expr := do
  return mkConst constName (← (← getConstInfo constName).levelParams.mapM fun _ => mkFreshLevelMVar)

Better names and/or homes welcome if someone wants to move it upstream.

[Gabriel Ebner]

I believe the function should be called mkConstWithFreshMVarLevels and should be put in Lean/Meta/Basic.lean, roughly around here.