Working with variables in a command

Stream: metaprogramming / tactics

[Chris Henson]

I would like to define a command that given a relation α → α → Prop creates a structure with the relation, using a method that still works if the relation's type contains a variable. Here is an mwe:

structure Bundle (α : Type) where
  rel : α → α → Prop

syntax "create_bundle" ident ident : command
macro_rules
  | `(create_bundle $rel $name) => `(def $name := Bundle.mk $rel)

-- this works fine...
def foo : Nat → Nat → Prop := λ _ _ ↦ True
create_bundle foo foo_bundle
#print foo_bundle   --def foo_bundle : Bundle Nat := { rel := foo }


inductive Term (β : Type)
variable {β : Type}
def bar : Term β → Term β → Prop := λ _ _ ↦ True

/-
don't know how to synthesize implicit argument 'β'
  @bar ?m.1322
context:
β : Type
-/
create_bundle bar bar_bundle

-- What I want is that $rel uses that mvar in its type signature, e.g
def bar_bundle : Bundle (Term β) := {rel := bar}

I tried elaborating the identifier and inferring its type, but didn't know how work with a variable. Intuitively I want the command to get the first type in a relation α → α → Prop (where α might contain variables) and construct a Bundle α.

[Chris Henson]

Here is a bit more of what I've tried, maybe this better communicates what I'm trying to do:

import Lean
open Lean Elab Meta Command Term

structure Bundle (α : Type) where
  rel : α → α → Prop

elab "create_bundle" rel:ident name:ident : command => do
  let rel_type ← liftTermElabM do
    -- let's try to get type of $rel, to annotate `Bundle.mk`
    let rel_expr ← elabTerm rel none
    let rel_expr ← instantiateMVars rel_expr
    let rel_type ← inferType rel_expr
    let rel_type ← instantiateMVars rel_type
    -- here this seems correct
    logInfo rel_type
    return rel_type
  -- but the same thing here gives an mvar error
  logInfo rel_type
  -- and I still need to use it in the below somehow...
  let defn ← `(def $name := Bundle.mk $rel)
  elabCommand defn

def foo : Nat → Nat → Prop := λ _ _ ↦ True
-- logInfo:
--  Nat → Nat → Prop
--  Nat → Nat → Prop
create_bundle foo foo_bundle

inductive Term (β : Type)
variable {β : Type}
def bar : Term β → Term β → Prop := λ _ _ ↦ True

set_option pp.rawOnError true in
/-
The first logInfo seems correct:
  _root_.Term ?m.2393 → _root_.Term ?m.2393 → Prop

But the second indicates I'm doing something wrong with metavariables?
  [Error pretty printing expression: unknown metavariable '?_uniq.2393'. Falling back to raw printer.]
  (Term ?_uniq.2393) -> (Term ?_uniq.2393) -> Prop
-/
create_bundle bar bar_bundle

[Kyle Miller]

What you're seeing in the first log message _root_.Term ?m.2393 → _root_.Term ?m.2393 → Prop is that there are metavariables in the expression. Once you leave liftTermElabM, there's no more metavariable context, so the metavariable definitions are gone, and the term isn't well-formed anymore.

[Chris Henson]

Is there some way then for me to make this definition from within the liftTermElabM? Or otherwise indicate that the metavariable there should be the variable β as it is written in the type signature def bar : Term β → Term β → Prop := ...?

[Kyle Miller]

Yes, definitely:

[Kyle Miller]

import Lean
open Lean Elab Meta Command Term

structure Bundle (α : Type) where
  rel : α → α → Prop

open Lean

elab "create_bundle" rel:ident name:ident : command => do
  liftTermElabM do
    let rel ← realizeGlobalConstNoOverloadWithInfo rel
    let ci ← getConstInfo rel
    forallTelescope ci.type fun args ty => do
      let throwNotRelation := throwError m!"type{indentExpr ci.type}\nis not a relation"
      unless args.size ≥ 2 do
        throwNotRelation
      unless ← isDefEq (← inferType args[args.size - 2]!) (← inferType args[args.size - 1]!) do
        throwNotRelation
      unless (← whnf ty).isProp do
        throwError m!"expecting Prop, not{indentExpr ty}"
      let params := ci.levelParams.map .param
      let rel := mkAppN (.const rel params) args[0...args.size-2]
      let bundle ← mkAppM ``Bundle.mk #[rel]
      let value ← mkLambdaFVars args[0...args.size-2] bundle
      let type ← inferType value
      addAndCompile <| .defnDecl {
        name := name.getId
        levelParams := ci.levelParams
        type
        value
        safety := .safe
        hints := .abbrev
      }
      addTermInfo' name (.const name.getId params) (isBinder := true)
      addDeclarationRangesFromSyntax name.getId name

def foo : Nat → Nat → Prop := λ _ _ ↦ True

create_bundle foo foo_bundle

#print foo_bundle
/-
def foo_bundle : Bundle Nat :=
{ rel := foo }
-/

inductive Term (β : Type)
variable {β : Type}
def bar : Term β → Term β → Prop := λ _ _ ↦ True

create_bundle bar bar_bundle

#check bar_bundle

#print bar_bundle
/-
def bar_bundle : {β : Type} → Bundle (_root_.Term β) :=
fun {β} => { rel := bar }
-/

[Chris Henson]

Thanks Kyle, that's perfect!