Produce proof expression containing let_fun

Stream: lean4

[Bhavik Mehta]

I'm trying to produce a proof term, where there's a certain amount of shared subexpressions in the final proof. So, I'd like to use let_fun (or similar) to produce let_fun x := long_proof; h x x instead of h long_proof long_proof. I found docs#Lean.Meta.mkLetFun, which seems like exactly what I want, but I don't understand how to manage the fvars to make this happen. As an example, I'm first trying to make a tactic which produces let_fun x := sorry; x, but I get panic because of unknown free variables. What am I doing wrong?

import Lean

open Lean Elab Meta Tactic

elab "test" : tactic => liftMetaFinishingTactic fun goal ↦ do
  let t ← goal.getType
  let i := FVarId.mk `h1
  let p ← mkLetFun (.fvar i) (← mkSorry t false) (.fvar i)
  goal.assign p

example : 2 = 3 := by test

[Bhavik Mehta]

For concreteness, here's the proof term I want the test tactic to create here:

example : 2 = 3 := let_fun h1 := (sorry : 2 = 3); h1

[Aaron Liu]

This is what I would do

elab "test" : tactic => liftMetaFinishingTactic fun goal ↦ do
  let t ← goal.getType
  let i ← mkFreshExprMVar (some t)
  let p ← mkLetFun i (← mkSorry t false) i
  goal.assign p

[Bhavik Mehta]

Oh, with a new mvar instead of a new fvar, interesting

[Robin Arnez]

If you want an fvar:

elab "test" : tactic => liftMetaFinishingTactic fun goal ↦ do
  let t ← goal.getType
  let value ← mkSorry t false
  let p ← withLocalDecl `h1 .default t fun fvar => do
    let expr := fvar
    mkLetFun fvar value expr
  goal.assign p

You can't just use FVarId.mk to make a new fvar because then it won't be in the local context. Instead, use something like withLocalDecl

[Aaron Liu]

I couldn't find the function withLocalDecl, which is why I used an mvar

[Bhavik Mehta]

I don't particularly mind whether it's an mvar or an fvar; I just presumed fvar was the thing to use here! Does it make a difference which one I use?

Robin Arnez said:

it won't be in the local context

Interesting: since this is meant to be a finishing tactic I imagined that it doesn't matter whether it's in the local context, since the new binding wouldn't be user-facing... Thanks for the fix!

[Robin Arnez]

Well it uses it in particular for the type so it does need to exist in the local context

[Aaron Liu]

Bhavik Mehta said:

Interesting: since this is meant to be a finishing tactic I imagined that it doesn't matter whether it's in the local context, since the new binding wouldn't be user-facing... Thanks for the fix!

mkLetFun needs it to be in the local context to work, that's where the error was coming from.

[Bhavik Mehta]

Aaron Liu said:

mkLetFun needs it to be in the local context to work, that's where the error was coming from.

Makes sense, but does that mean mkLetFun was the wrong thing to use?

[Aaron Liu]

You can also use Qq to construct the expression without any MetaM

[Bhavik Mehta]

I ended up using the mvar solution and it works nicely, thanks!