Telescope dance

Stream: lean4

[Patrick Massot]

I'm returning to porting Verbose Lean. The last big missing piece compared to the Lean 3 version is the help tactic. It relies on a custom version of Expr where bounded quantifiers are first-class citizen. Of course it requires a parser turning regular Expr into this custom type. This requires juggling with bvar vs fvar. In Lean 3 this was the tactic.mk_local'/expr.instantiate_var dance. My understanding is that forallTelescope is meant to replace this but I had no luck. The custom expression type, a conversion to string and the beginning of the parser can be found below. The example does show a free variable instead of a loose bvar but it doesn't get pretty printed so I guess the context is still off.

import Lean

open Lean Meta Elab Tactic

inductive MyExpr
| forall_rel (var_Name : Name) (typ : Expr) (rel : String) (rel_rhs : Expr) (propo : MyExpr) : MyExpr
| forall_simple (var_Name : Name) (typ : Expr) (propo : MyExpr) : MyExpr
| exist_rel (var_Name : Name) (typ : Expr) (rel : String) (rel_rhs : Expr) (propo : MyExpr) : MyExpr
| exist_simple (var_Name : Name) (typ : Expr) (propo : MyExpr) : MyExpr
| conjunction (propo propo' : MyExpr) : MyExpr
| disjunction (propo propo' : MyExpr) : MyExpr
| impl (le re : Expr) (lhs : MyExpr) (rhs : MyExpr) : MyExpr
| iff (le re : Expr) (lhs rhs : MyExpr) : MyExpr
| equal (le re : Expr) : MyExpr
| ineq (le : Expr) (symb : String) (re : Expr) : MyExpr
| prop (e : Expr) : MyExpr
| data (e : Expr) : MyExpr
deriving Repr

def MyExpr.toStr : MyExpr → MetaM String
| (forall_rel var_name typ rel rel_rhs propo) => do
    let rhs := toString (← ppExpr rel_rhs)
    let p ← propo.toStr
    pure $ "∀ " ++ var_name.toString ++ rel ++ (toString rhs) ++ ", " ++ p
| (forall_simple var_name typ propo) => do
    let p ← propo.toStr
    pure $ "∀ " ++ var_name.toString ++ ", " ++ p
| (exist_rel var_name typ rel rel_rhs propo) => do
    let rhs := toString (← ppExpr rel_rhs)
    let p ← MyExpr.toStr propo
    pure $ "∃ " ++ var_name.toString ++ rel ++ rhs ++ ", " ++ p
| (exist_simple var_name typ propo) => do
    let p ← MyExpr.toStr propo
    pure $ "∃ " ++ var_name.toString ++ ", " ++ p
| (conjunction propo propo') => do
    let p ← MyExpr.toStr propo
    let p' ← MyExpr.toStr propo'
    pure $ p ++ " ∧ " ++ p'
| (disjunction propo propo') => do
    let p ← MyExpr.toStr propo
    let p' ← MyExpr.toStr propo'
    pure $ p ++ " ∨ " ++ p'
| (impl le re lhs rhs) => do
  let l ← MyExpr.toStr lhs
  let r ← MyExpr.toStr rhs
  pure $ l ++ " → " ++ r
| (iff le re lhs rhs) => do
  let l ← MyExpr.toStr lhs
  let r ← MyExpr.toStr rhs
  pure $ l ++ " ↔ " ++ r
| (equal le re) => do
  let l := toString (← ppExpr le)
  let r := toString (← ppExpr re)
  pure $ l ++ " = " ++ r
| (ineq le symb re) => do
  let l := toString (← ppExpr le)
  let r := toString (← ppExpr re)
  pure $ l ++ symb ++ r
| (prop e) => do return toString (← ppExpr e)
| (data e) => do return toString (← ppExpr e)

#check mkForallFVars

partial def parse : Expr → MetaM MyExpr
 | e@(Expr.forallE n t b bi) => do
   forallTelescope e fun xs A => do
     dbg_trace "Types of xs: {← xs.mapM (fun x ↦ do ppExpr (← inferType x))}"
     dbg_trace "xs: {xs}"
     dbg_trace "pretty xs {← xs.mapM ppExpr}"
     dbg_trace "Pretty A: {← ppExpr A}"
     match xs.toList with
     | [] => unreachable!
     | [x] => return MyExpr.forall_simple n t (← parse (b.instantiate #[x]))
     | x::hx::xs => do
       dbg_trace "more" ; throwError ""


 | e => do
    if (← instantiateMVars (← inferType e)).isProp then
      return .prop e
    else
      return .data e



elab "test" x:term : tactic => withMainContext do
  let e ← Elab.Tactic.elabTerm x none
  let p ← parse e
  dbg_trace "Parse output: {← p.toStr}"
  dbg_trace "Parse output: {repr p}"

example (P : ℕ → Prop) : True := by
  test ∀ n, P n
  --test ∀ n > 0, P n
  trivial

[Patrick Massot]

The corresponding Lean 3 code was:

meta def parse : expr → tactic my_expr
| e@(expr.pi n bi t b) := do
    var ← tactic.mk_local' n bi t,
    match (expr.instantiate_var b var) with
    | e'@(expr.pi n' bi' t' b') :=
      do { (x, y, symbole) ← rel_symb t',
           when (x.local_pp_name ≠ n) $ tactic.fail "",
             var' ← tactic.mk_local' n' bi' t',
           my_expr.forall_rel n t symbole y <$> parse (expr.instantiate_var b' var') } <|>
      do { typ ← parse t,
           body ← parse e',
           if e.is_arrow then
              pure (impl t e' typ body)
           else
             pure $ my_expr.forall_simple n t body }
    | e' := do
           typ ← parse t,
           body ← parse e',
            if e.is_arrow then
              pure (impl t e' typ body)
            else
              forall_simple n t <$> parse (expr.instantiate_var b var)
    end
|`(@Exists %%α %%p) :=
  do {
    `(@Exists %%α' %%p') ← pure p.binding_body,
    var ← tactic.mk_local' p.binding_name p.binding_info p.binding_domain,
    (x, y, symbole) ← rel_symb α'.binding_body,
    exist_rel p.binding_name α symbole y <$> parse (expr.instantiate_var p' var).binding_body } <|>
  do {
    var ← tactic.mk_local' p.binding_name p.binding_info p.binding_domain,
    exist_simple p.binding_name α <$> parse (expr.instantiate_var p.binding_body var)
    }
|`(and %%e %%e') := do
    p ← parse e,
    p' ← parse e',
    pure $ conjunction p p'
|`(or %%e %%e') := do
    p ← parse e,
    p' ← parse e',
    pure $ disjunction p p'
|`(iff %%e %%e') := do
    p ← parse e,
    p' ← parse e',
    pure $ ssi e e' p p'
|`(eq %%e %%e') := pure $ egal e e'
| `(%%x < %%y) := pure $ ineq x " < " y
| `(%%x ≤ %%y) := pure $ ineq x " ≤ " y
| `(%%x > %%y) := pure $ ineq x " > " y
| `(%%x ≥ %%y) := pure $ ineq x " ≥ " y
| e := do { e' ← tactic.delta unfold_defs e,
            tactic.trace  "Remarque : La commande",
            tactic.trace  " On déplie nom,",
            tactic.trace  "ou",
            tactic.trace  " On déplie nom dans hyp,",
            tactic.trace  "permet de déplier la définition nom dans le but ou dans une hypothèse hyp.",
            tactic.trace  "",
            parse e' } <|>
       do { t ← tactic.infer_type e, pure $ if t = `(Prop) then prop e else data e } <|> pure (prop e)

[Marcus Rossel]

I think your context might be off because forallTelescope deletes the fvars it creates after the call completes. From the metaprogramming book:

Given type = ∀ (x₁ : T₁) ... (xₙ : Tₙ), U x₁ ... xₙ, this function creates one fvar fᵢ for each ∀-bound variable xᵢ and replaces each xᵢ with fᵢ in the conclusion U. It then calls the computation k, passing it the fᵢ and the conclusion U f₁ ... fₙ. Within this computation, the fᵢ are registered in the local context; afterwards, they are deleted again (similar to withLocalDecl).

I'm not sure if this is the solution you want, but:

forallMetaTelescope behaves like the corresponding non-meta function, but the bound variables are replaced by new mvars instead of fvars. Unlike the non-meta functions, the meta functions do not delete the new metavariables after performing some computation, so the metavariables remain in the environment indefinitely.

[Patrick Massot]

I'm not sure I want mvars instead. I don't know what I did. I never fully understood what Lean 3 was doing here, this was cargo-cult code.

[Thomas Murrills]

What's the motivation behind instantiating the body of the forall with an fvar? Do you essentially just want to MyExpr.toStr to print the bvar using its name?

[Thomas Murrills]

Also, do you do anything specifically different with toStr, or do you just try to emulate normal delaboration? If the latter, why not simply turn MyExpr back into an Expr and let delaboration handle it normally (and use pp*/format utilities if you need a string)?

[Thomas Murrills]

(If you do do something different, it might still be worth just making a custom delaborator instead of recreating the bvar-pretty-printing code—or possibly creating your own syntax categories and going from MyExpr to Syntax instead)

[Patrick Massot]

I do various things with the MyExpr, this is not simply trying to find a complicated way to pretty-print an expression. It doesn't seem extravagant to want that, and it was easy in Lean 3.

[Thomas Murrills]

Oh, okay—I'm still confused as to why you want fvars in the body of a forall. Shouldn't they still be bvars?

[Patrick Massot]

I want to have access to their user name

[Thomas Murrills]

I can't help but feel that access to that name should occur inside a forallSimpleTelescope or some such which behaves like forallTelescope—otherwise you've got fvars in the local context for variables which are actually bound

[Patrick Massot]

Does anyone understand precisely what Lean 3 was doing there? Because whatever it did was good enough for me.

[Kyle Miller]

Just a first thing, rather than forallTelescope, the idiomatic thing seems to be to use withLocalDecl, as in

 | Expr.forallE n t b bi => do
  withLocalDecl n bi t fun x => do
    return MyExpr.forall_simple n t (← parse (b.instantiate1 x))

forallTelescope can give you too much if there are nested foralls.

[Kyle Miller]

The next thing is that I think local context handling works different in Lean 4, where it's using a reader monad rather than a state monad, so you can't add an fvar in a non-scoped way -- my understanding of the Lean 3 way was that you added a local variable and it stuck around. If you pass along a LocalContext yourself you should be able to circumvent this.

[Kyle Miller]

You could also use continuation-passing style.

[Patrick Massot]

Kyle Miller said:

You could also use continuation-passing style.

I have seen those words before but I have no idea what they mean.

[Patrick Massot]

Kyle Miller said:

forallTelescope can give you too much if there are nested foralls.

I want to see some nesting here, since I want to distinguish between ∀x, P x and ∀ x > 0, P x. That's why the snippet was considering different cases depending on the length of xs. But it's clearly bounded, I don't need to support arbitrary nesting.

[Kyle Miller]

You can match on different nestings of .forallE yourself, but I could see forallTelescope working too. By the way, there's forallBoundedTelescope for limiting the nesting

[Kyle Miller]

The small annoyance in the logic is handling \forall x, \forall y, P x too

[Kyle Miller]

Here, I just hacked together threading the context manually:

import Lean

open Lean Meta Elab Tactic

inductive MyExpr
| forall_rel (var_Name : Name) (typ : Expr) (rel : String) (rel_rhs : Expr) (propo : MyExpr) : MyExpr
| forall_simple (var_Name : Name) (typ : Expr) (propo : MyExpr) : MyExpr
| exist_rel (var_Name : Name) (typ : Expr) (rel : String) (rel_rhs : Expr) (propo : MyExpr) : MyExpr
| exist_simple (var_Name : Name) (typ : Expr) (propo : MyExpr) : MyExpr
| conjunction (propo propo' : MyExpr) : MyExpr
| disjunction (propo propo' : MyExpr) : MyExpr
| impl (le re : Expr) (lhs : MyExpr) (rhs : MyExpr) : MyExpr
| iff (le re : Expr) (lhs rhs : MyExpr) : MyExpr
| equal (le re : Expr) : MyExpr
| ineq (le : Expr) (symb : String) (re : Expr) : MyExpr
| prop (e : Expr) : MyExpr
| data (e : Expr) : MyExpr
deriving Repr

def MyExpr.toStr : MyExpr → MetaM String
| (forall_rel var_name typ rel rel_rhs propo) => do
    let rhs := toString (← ppExpr rel_rhs)
    let p ← propo.toStr
    pure $ "∀ " ++ var_name.toString ++ rel ++ (toString rhs) ++ ", " ++ p
| (forall_simple var_name typ propo) => do
    let p ← propo.toStr
    pure $ "∀ " ++ var_name.toString ++ ", " ++ p
| (exist_rel var_name typ rel rel_rhs propo) => do
    let rhs := toString (← ppExpr rel_rhs)
    let p ← MyExpr.toStr propo
    pure $ "∃ " ++ var_name.toString ++ rel ++ rhs ++ ", " ++ p
| (exist_simple var_name typ propo) => do
    let p ← MyExpr.toStr propo
    pure $ "∃ " ++ var_name.toString ++ ", " ++ p
| (conjunction propo propo') => do
    let p ← MyExpr.toStr propo
    let p' ← MyExpr.toStr propo'
    pure $ p ++ " ∧ " ++ p'
| (disjunction propo propo') => do
    let p ← MyExpr.toStr propo
    let p' ← MyExpr.toStr propo'
    pure $ p ++ " ∨ " ++ p'
| (impl le re lhs rhs) => do
  let l ← MyExpr.toStr lhs
  let r ← MyExpr.toStr rhs
  pure $ l ++ " → " ++ r
| (iff le re lhs rhs) => do
  let l ← MyExpr.toStr lhs
  let r ← MyExpr.toStr rhs
  pure $ l ++ " ↔ " ++ r
| (equal le re) => do
  let l := toString (← ppExpr le)
  let r := toString (← ppExpr re)
  pure $ l ++ " = " ++ r
| (ineq le symb re) => do
  let l := toString (← ppExpr le)
  let r := toString (← ppExpr re)
  pure $ l ++ symb ++ r
| (prop e) => do return toString (← ppExpr e)
| (data e) => do return toString (← ppExpr e)

#check mkForallFVars

partial def parse (ctx : LocalContext) : Expr → MetaM (LocalContext × MyExpr)
 | Expr.forallE n t b bi => do
  let fvarId ← mkFreshFVarId
  let ctx := ctx.mkLocalDecl fvarId n t bi
  let (ctx', b') ← parse ctx (b.instantiate1 (.fvar fvarId))
  return (ctx', MyExpr.forall_simple n t b')
 | e => withLCtx ctx {} do
    if (← instantiateMVars (← inferType e)).isProp then
      return (ctx, .prop e)
    else
      return (ctx, .data e)



elab "test" x:term : tactic => withMainContext do
  let e ← Elab.Tactic.elabTerm x none
  let (ctx, p) ← parse (← getLCtx) e
  withLCtx ctx {} do
    let g ← mkFreshTypeMVar
    logInfo m!"g = {g.mvarId!}"
    dbg_trace "Parse output: {← p.toStr}"

example (P : Nat → Prop) : True := by
  test ∀ n, P n
  --test ∀ n > 0, P n
  trivial

[Kyle Miller]

It prints Parse output: ∀ n, P n

[Kyle Miller]

The main bug to watch out for is to not forget to do withLCtx ctx {} around things that need a type calculation, like inferType

[Kyle Miller]

(The {} is filling in the local instances. I'm assuming you don't need to track those for what you're doing?)

[Kyle Miller]

Here's with continuation-passing style:

partial def parse (e : Expr) (ret : MyExpr → MetaM MyExpr) : MetaM MyExpr :=
  match e with
  | Expr.forallE n t b bi =>
    withLocalDecl n bi t fun x =>
      parse (b.instantiate1 x) fun b' =>
        ret <| MyExpr.forall_simple n t b'
  | e => do
    if (← instantiateMVars (← inferType e)).isProp then
      ret <| .prop e
    else
      ret <| .data e

elab "test" x:term : tactic => withMainContext do
  let e ← Elab.Tactic.elabTerm x none
  discard <| parse e fun p => do
    let g ← mkFreshTypeMVar
    logInfo m!"g = {g.mvarId!}"
    dbg_trace "Parse output: {← p.toStr}"
    return p

[Kyle Miller]

Notice that ret gets called from within the context of the withLocalDecl, so the body of the function passed to parse in the test elaborator still has everything in context.

[Kyle Miller]

I'm not sure I coded CPS completely right, since it's a little weird having to do return p at the end artificially

[Thomas Murrills]

I think the issue with return p is just that the type signature should be def parse (e : Expr) (ret : MyExpr → MetaM α) : MetaM α

[Kyle Miller]

Thanks @Thomas Murrills

partial def parse {α : Type} (e : Expr) (ret : MyExpr → MetaM α) : MetaM α :=
  match e with
  | Expr.forallE n t b bi =>
    withLocalDecl n bi t fun x =>
      parse (b.instantiate1 x) fun b' =>
        ret <| MyExpr.forall_simple n t b'
  | e => do
    if (← instantiateMVars (← inferType e)).isProp then
      ret <| .prop e
    else
      ret <| .data e

elab "test" x:term : tactic => withMainContext do
  let e ← Elab.Tactic.elabTerm x none
  parse e fun p => do
    let g ← mkFreshTypeMVar
    logInfo m!"g = {g.mvarId!}"
    dbg_trace "Parse output: {← p.toStr}"

[Patrick Massot]

Thanks! I will try to understand all that tomorrow.

[Thomas Murrills]

One small potential refinement I can think of here is including the local decl's fvar as an argument to forall_simple, e.g. such that we can write

...
withLocalDecl n bi t fun x =>
      parse (b.instantiate1 x) fun b' =>
        ret <| MyExpr.forall_simple n x t b'
...

Otherwise, you might not be able to tell which fvar came from which binder (or from the broader context) if usernames happen to clash! :) But whether you'll actually need this depends on your specific application.

[Patrick Massot]

Update: I now want to generalize the signature parse {α : Type} (e : Expr) (ret : MyExpr → MetaM α) : MetaM α replacing both occurences of MetaM α by something more general. In the intended application MetaM is replaced by SuggestionM where abbrev SuggestionM := StateRefT (Array SuggestionItem) MetaM. I made it work using

partial def parse {α : Type}
    {n : Type → Type} [MonadControlT MetaM n] [MonadLiftT MetaM n] [Monad n]
    [Inhabited (n α)] [MonadMCtx n]
    (e : Expr) (ret : MyExpr → n α) : n α :=

obtained by adding instance arguments for every complain from Lean, and checking it works in the intended use case. But I feel I'm missing a magic word here.

[Mario Carneiro]

the last two instances are unnecessary

[Mario Carneiro]

but yes this is the general idea

[Mario Carneiro]

There is a function map1MetaM which is designed specifically for making these kind of functions, you may find it easier

[Patrick Massot]

I missed those messages from last night. The last two instances are needed for me. The first one allows to use unreachable! and the second one is needed to use instantiateMVars.

[Mario Carneiro]

you can use have : n α := ret default before using unreachable! (or at the beginning or somewhere else convenient) to remove the first instance

[Patrick Massot]

docs#instInhabitedMetaM is not inherited using the other type classes.

[Mario Carneiro]

you can use liftM instantiateMVars for the second one

[Patrick Massot]

The liftM trick works, but I can't get rid of Inhabited so far.