building expressions with intermediate metavariables

Stream: lean4

[Scott Morrison]

How does one construct terms like Iff.mpr (@Int.add_one_le_iff _ _) p without handling metavariables manually?

import Lean
import Std.Data.Int.Lemmas
import Qq

open Lean Meta Elab Tactic Qq

-- Given a proof of `a < b` in the integers, produce the proof of `a + 1 ≤ b`
-- using `Int.add_one_le_iff : ∀ {a b : Int}, a + 1 ≤ b ↔ a < b`

example {a b : Int} (p : a < b) : a + 1 ≤ b := Iff.mpr (@Int.add_one_le_iff _ _) p

-- Now in `Expr`:

def foo (p : Expr) : MetaM Expr := do
  return mkApp (← mkAppM ``Iff.mpr #[← mkAppOptM ``Int.add_one_le_iff #[none, none]]) p

-- Fails with `AppBuilder for 'mkAppOptM', result contains metavariables`
#eval foo q(Int.zero_lt_one)

(I don't want an answer using Qq! :-)

[Mario Carneiro]

I'm very confused by the question, because you say you don't want Qq or metavariables and you are using both

[Mario Carneiro]

do you know what a and b are? You need metavariables to figure them out from p alone

[Scott Morrison]

Sorry, I was only using Qq in order to fake some input for the #eval. I don't want to use it in foo.

[Scott Morrison]

And when I said I don't want to handle metavariables manually I'm hoping to not have to use mkFreshExprMVar while building the expression.

[Scott Morrison]

I don't know what a and b are, except of course that I can find them by decomposing ← inferType p.

[Scott Morrison]

I'm happy, I guess, to relax my constraint about not using Qq inside foo. Either way, I'd like to know how others would do this, and hoping that it is a one liner! In lean 3 we would have just written something like to_expr ``(add_one_le_iff.mpr %%p)

[Mario Carneiro]

the analogous one-liner in lean 4 is evalExpr (<- `(add_one_le_iff.mpr $p))

[Scott Morrison]

but that requires going against the stream, converting my Expr back into a TSyntax `term...

[Scott Morrison]

which I guess I can do in some way by pretty printing, but I'm stumped for now.

[Mario Carneiro]

Ah, the trick for that is to create a metavariable, immediately assign it, and put syntax for the metavariable in the syntax

[Mario Carneiro]

I think there is a function to do this for you