Learning metaprogramming

Stream: metaprogramming / tactics

[metakuntyyy]

So yesterday I started learning metaprogramming and trying to print some information in the context. Today I wanted to see how I can create simple conclusions in a tactic.

import Lean
open Lean Elab Command Meta Tactic

syntax (name := c) "testTactic2"  : tactic

@[tactic c] def myTactic2 : Tactic := fun _ => withMainContext do
  let hyps := (← getLocalHyps).toList
  let c := hyps[0]!.fvarId!
  let type := ← c.getType
  logInfo m! "{type.ctorName}"
  let four := mkNatLit 4
  let d := Expr.instantiate1 type four
  logInfo m! "{d}"
  return

example (h: ∀ x: Nat , x < 3) : False := by
  testTactic2
  sorry

I have played around a little bit. I want to instantiate x with four and I expected the logInfo to return 4<3 which I hoped I could add to the context. It, however prints h.

[Robin Arnez]

You're probably looking for instantiateForall

[Robin Arnez]

Or alternatively, you can use type.bindingBody!.instantiate1 four

[metakuntyyy]

Yes, it did work with instantiateForall, however I couldn't figure out by reading the docs what instantiate1 is supposed to do. It appears to do nothing.

[Robin Arnez]

instantiate1 instantiates loose bound variables. Remember, in ∀ x : Nat, x < 3 the body of the forall is represented as #0 < 3 with the bound variable #0 referring to the x (#0 = innermost bound variable, #1 = one outer, etc.). When you use instantiate1 on ∀ x : Nat, x < 3, it doesn't do anything because the only bound variable #0 is already bound by x. This is usually the case: Instead of having loose bound variables (.bvar n) we usually use free variables (.fvar x) which refer to variables from the local context. So instantiate1 usually doesn't do anything. But if you have loose bound variables, such as in the term #0 < 3, it will happily instantiate them (in particular the first one).

[metakuntyyy]

What would one such example be where instantiate1 does something, just so that I have a working reference

[Robin Arnez]

Again, you can take the binding body of the forall and then instantiate:

import Lean
open Lean Elab Command Meta Tactic

elab "testTactic2" : tactic => withMainContext do
  let hyps := (← getLocalHyps).toList
  let c := hyps[0]!.fvarId!
  let type := ← c.getType
  logInfo m! "{type.ctorName}"
  let four := mkNatLit 4
  let d := type.bindingBody!
  logInfo m! "{d}"
  let d := d.instantiate1 four
  logInfo m! "{d}"
  return

example (h: ∀ x : Nat, x < 3) : False := by
  testTactic2
  sorry

As you can see, it's #0 < 3 => 4 < 3

[metakuntyyy]

Ok, now I am trying to add 4<3 to the list of hypotheses so that it can be displayed and added to the infoview

import Lean
open Lean Elab Command Meta Tactic

syntax (name := c) "testTactic2"  : tactic


@[tactic c] def myTactic2 : Tactic := fun _ => withMainContext do
  let hyps := (← getLocalHyps).toList
  let c := hyps[0]!.fvarId!
  let type := ← c.getType
  logInfo m! "{type.ctorName}"
  let four := mkNatLit 4
  let d ← instantiateForall type [four].toArray
  logInfo m! "{d}"
  let fv ← mkFreshFVarId
  let lctx← getLCtx
  let ldecl := Lean.mkLocalDeclEx 44 fv Name.anonymous d .default
  have decl := lctx.addDecl ldecl

  return


example (h: ∀ x : Nat, x < 3) : False := by
  testTactic2
  sorry

Seems not very idiomatic, addDecl is supposed to be a low-level API, I can't find a higher level api that lets me just add the local hypothesis.

[Aaron Liu]

I think the best way is to create a new goal withLocalDecl and assign the old one

[metakuntyyy]

Ah, I see. Let me try it out myself.

[metakuntyyy]

Are you sure that is what I want. This is the description of withLocalDecl

 Create a free variable `x` with name, binderInfo and type, add it to the context and run in `k`. Then revert the context.

Why would I want to revert the context, Also I don't understand how to pass the parameter to k.

import Lean
open Lean Elab Command Meta Tactic

syntax (name := c) "testTactic2"  : tactic


@[tactic c] def myTactic2 : Tactic := fun _ => withMainContext do
  let hyps := (← getLocalHyps).toList
  let c := hyps[0]!.fvarId!
  let type := ← c.getType
  logInfo m! "{type.ctorName}"
  let four := mkNatLit 4
  let d ← instantiateForall type [four].toArray
  logInfo m! "{d}"
  let fv ← mkFreshFVarId
  let x := withLocalDecl (String.toName "xy") .default d (k:=fun x => sorry)

  return

[Aaron Liu]

I think I did it!

What I did

import Lean
open Lean Elab Command Meta Tactic

syntax (name := c) "testTactic2"  : tactic


@[tactic c] def myTactic2 : Tactic := fun _ => withMainContext do
  let hyps := (← getLocalHyps).toList
  let c := hyps[0]!.fvarId!
  let type := ← c.getType
  logInfo m! "{type.ctorName}"
  let four := mkNatLit 4
  let d ← instantiateForall type [four].toArray
  logInfo m! "{d}"
  let goal ← getMainGoal
  let (mvarId, ass) ← withLocalDecl .anonymous .default d fun e => do
    let mvar ← mkFreshExprSyntheticOpaqueMVar (← goal.getType) (← goal.getTag)
    let ass ← mkLambdaFVars #[e] mvar
    pure (mvar.mvarId!, Expr.app ass (.app (.fvar c) four))
  goal.assign ass
  replaceMainGoal [mvarId]

example (h: ∀ x : Nat, x < 3) : False := by
  testTactic2
  sorry

[metakuntyyy]

Ah, nice. But I wanted to add it to the infoview and not replace the goal, I want that to the right it shows xy: 4 < 3

[Aaron Liu]

Like this?

import Lean
open Lean Elab Command Meta Tactic

syntax (name := c) "testTactic2"  : tactic


@[tactic c] def myTactic2 : Tactic := fun _ => withMainContext do
  let hyps := (← getLocalHyps).toList
  let c := hyps[0]!.fvarId!
  let type := ← c.getType
  logInfo m! "{type.ctorName}"
  let four := mkNatLit 4
  let d ← instantiateForall type [four].toArray
  logInfo m! "{d}"
  let goal ← getMainGoal
  let (mvarId, ass) ← withLocalDecl `xy .default d fun e => do
    let mvar ← mkFreshExprSyntheticOpaqueMVar (← goal.getType) (← goal.getTag)
    let ass ← mkLambdaFVars #[e] mvar
    pure (mvar.mvarId!, Expr.app ass (.app (.fvar c) four))
  goal.assign ass
  replaceMainGoal [mvarId]

example (h: ∀ x : Nat, x < 3) : False := by
  testTactic2
  sorry

[Aaron Liu]

Why do you want it to not replace the goal?

[metakuntyyy]

Well, I try to take baby steps. Also

  let (mvarId, ass) ← withLocalDecl (String.toName "xy") .default d fun e => do

works as well which is nice.

[metakuntyyy]

Ah I see that this works, it adds it to the context. This seems very confusing to me as I expected it to just be able to push `xy d to the context. It seems to be a more convoluted operation.

[metakuntyyy]

The book uses this operation, it seems very useful on the first glance to me https://leanprover-community.github.io/mathlib4_docs/Lean/Elab/Tactic/Basic.html#Lean.Elab.Tactic.liftMetaTactic