Calling an `Expr` that has type `MetaM` in a `MetaM` program

Stream: metaprogramming / tactics

[Théophile]

Hello!

I am currently writing a tactic, which will encounter some expressions, and I would like to allow users to associate these expressions with a MetaM function that my tactic could call. For example, users could say something like "when you encounter the term f x y z, use the metaprogram m_f: MVarId -> Expr -> MetaM Unit", and my tactic would internally call m_f.

For example something like

class HasMetaprogram {a} (x: a) where
  prog: Lean.MVarId → Lean.Expr → Lean.MetaM Unit

def f (n: Nat): Nat := n+n

instance {n}: HasMetaprogram (f (10*n)) where
  prog mvarid expr := do
    -- do something smart that assign mvarid
    -- `expr` is the expression of `f (10*n)` that may be useful
    mvarid.assign (.const ``Unit.unit [])

Now onto the question: given an expression f (10*n), I can easily get the Expr which has type Lean.MVarId → Lean.Expr → Lean.MetaM Unit, but how can I "call" this expression within my tactic?

[Théophile]

This is a bit of a #xy, so here is the actual problem I am trying to solve (but it is a bit long to explain).

In my development, I have defined many functions and corresponding theorems, and I wrote a tactic which, among many things, lookup for the theorem corresponding to a given function call. To this end, I am using Lean's typeclass mechanism as a database of theorems, in a fashion similar to this code:

class Theorem (x: a) (property: outParam (a → Prop)) where
  pf: property x

def f (n: Nat): Nat := n+n

instance: Theorem (f n) (fun res => res = 2*n) where
  pf := by grind [f]

then, when my tactic would encounter the expression f n, it invokes typeclass synthesis on Theorem (f n) ?property, which instantiates the metavariable ?property to fun res => res = 2*n, and uses this afterward.

In reality, things are slightly more complex, I sometimes need to associate a function with a class of theorems. This class of theorem is parametrized by another type, as shown in this code:

class Theorem (x: a) (y: b) (property: outParam (a → Prop)) where
  pf: property x

def f (n: Nat): Nat := n+n

-- the property here is a bit silly, but I do have real usecases for this in my full development
instance: Theorem (f n) (y: Nat) (fun res => res = 2*n + 0*y) where
  pf := by grind [f]

I then rely on users to provide this value y when using my tactic, which will synthetize an instance of Theorem (f n) y ?property

Now onto my question: although in some cases, the chosen value of y is a crucial argument in the proof, in some other cases, there is only one sensible value to choose for y. For example, it may be than when I encounter f n, I know there should be in the context h: p n y0, and in this case y0 is the only sensible choice for y. This value is easily found by using docs#Lean.MVarId.assumption on the goal p n ?y. In other words, I can write a MetaM that will find this value of y automatically.

I would therefore like users to be able to provide MetaM function that will find such y, which is what I asked in my first message. But maybe there is a different way toward this goal?

[Aaron Liu]

What happens when you get something like

instance {n}: HasMetaprogram (f (n + 1)) where
  prog mvarid expr := do
    -- do something smart that assign mvarid
    -- `expr` is the expression of `f (n + 1)` that may be useful
    if n == 0 then mvarid.assign (.const ``Unit.unit [])
    else mvarid.assign (.app (.app (.const ``id [1])
      (.const ``Unit [])) (.const ``Unit.unit []))

[Aaron Liu]

then n is not determined at runtime

[Aaron Liu]

maybe you can do something like what norm_num does

[Théophile]

Ah, indeed I would not be happy if provided such a metaprogram. In real scenarios I only need the Expr version of n, not its actual value. But I understand this hints toward the fact what I want may not be possible (at least not in the form of typeclass)

[Théophile]

I could do the following instead:

def prog_f_n_plus_1 (mvarid: MVarId) (e: Expr): MetaM Unit := do
    -- do something smart that assign mvarid
    -- `expr` is the expression of `f (n + 1)` that may be useful
    mvarid.assign (.const ``Unit.unit [])

instance {n}: HasMetaprogram (f (n + 1)) where
  prog mvarid expr := prog_f_n_plus_1

Then I can get the Name corresponding to prog_f_n_plus_1, and I don't have such dependency problem.

[Théophile]

maybe you can do something like what norm_num does

Ah, maybe like this snippet of code?

/-- Read a `norm_num` extension from a declaration of the right type. -/
def mkNormNumExt (n : Name) : ImportM NormNumExt := do
  let { env, opts, .. } ← read
  IO.ofExcept <| unsafe env.evalConstCheck NormNumExt opts ``NormNumExt n

(NormNumExt does contain a MetaM program)

[Aaron Liu]

Théophile said:

maybe you can do something like what norm_num does

Ah, maybe like this snippet of code?

/-- Read a `norm_num` extension from a declaration of the right type. -/
def mkNormNumExt (n : Name) : ImportM NormNumExt := do
  let { env, opts, .. } ← read
  IO.ofExcept <| unsafe env.evalConstCheck NormNumExt opts ``NormNumExt n

(NormNumExt does contain a MetaM program)

yeah like that

[Théophile]

I got something to work using docs#Lean.evalConstCheck, thanks!!