creating proofs in `TermElabM`

Stream: lean4

[Arthur Paulino]

Hi! I am stuck in a challenge of the meta world.
Here you can see es, which is of List Expression. And then here I was able to call the Expression.app constructor, whose second argument is a term of type NEList Expression.

NEList α is basically a non-empty List α. I then used the function List.toNEList to instantiate the term of type NEList Expression. However, the second argument is a proof that the first argument (of type List Expression) is not empty.

In the Parser code it's pretty straightforward, as you can see. But I'm stuck trying to do the same in the meta world. Here I was able to create a term of type List Expression. Now I want to use mkAppM, calling the List.toNEList function. But I don't know how to elaborate the expression for the second argument. Is it possible? If so, how?

Sorry if the text was too long. I hope I was able to provide enough context for my question :pray:

[Simon Hudon]

Many of the primitive tactics are formulated in MetaM and work by taking a MVarId as a parameter and may return one or many MVarIds. You can start by creating a mvar with the right type
using Lean.Meta.mkFreshExprMVar and then call your elaborating function that you may have written in MetaM (and use liftMetaM to make it compatible with TermElabM). If you prefer writing the elaboration in TacticM, you start the same way by creating a mvar and passing it as a parameter to Lean.Elab.Tactic.run.

That should get you started. For more details, I would need to know what your plan is for building that proof automatically.

[Arthur Paulino]

The small goal is to simply be able to call the Expression.app constructor (it requires a proof). The big goal is being able to see (and test) my interpreter with an easy way to instantiate terms of type Program by using an unified syntax. Like this

[Simon Hudon]

Are you saying that my answer is not getting you there or is that a separate question?

[Arthur Paulino]

@Simon Hudon the issue is that, in the Parser code, I have h granted by the result of if h : ¬ es.isEmpty. In the meta code, I also have if h : ¬ es.isEmpty but es is of type List Expr. Whereas in the Parser, es is of type List Expression

[Arthur Paulino]

(deleted)

[Arthur Paulino]

Simon Hudon said:

Are you saying that my answer is not getting you there or is that a separate question?

I'm saying that your answer, as I understood it, would help me building the proof in a "tactic-like" fashion. But in this scenario I would like to build a proof (as an Expr) of the fact that my List Expression is not empty, but all I have is the hypothesis that my List Expr is not empty

[Leonardo de Moura]

We know that l is not the empty list in your example. Then, mkListLit produces a List.cons application. Thus, we can prove that is not empty using reflexivty.
Another trick is to completely avoid proofs and use

def List.toNEList' (a : α) (bs : List α) : NEList α :=
   match bs with
   | [] => .uno a
   | b::bs => .cons a (toNEList' b bs)

Here is an example. It is based on fragments of your code base.

import Lean

inductive NEList (α : Type)
  | uno  : α → NEList α
  | cons : α → NEList α → NEList α
  deriving Repr

def List.toNEList : (l : List α) → ¬ l.isEmpty → NEList α
  | a :: b, _ =>
    if h : ¬ b.isEmpty
      then NEList.cons a $ b.toNEList h
      else NEList.uno a

theorem List.notEmpty_of_eq_false (l : List α) (h : l.isEmpty = false) : ¬ l.isEmpty := by
  simp [h]

def List.toNEList' (a : α) (bs : List α) : NEList α :=
   match bs with
   | [] => .uno a
   | b::bs => .cons a (toNEList' b bs)

inductive Expression
  | var  : String     → Expression
  | app  : String     → NEList Expression → Expression
  deriving Inhabited, Repr

declare_syntax_cat                    expression
syntax ident expression*            : expression
syntax " ( " expression " ) "       : expression


namespace Lean.Elab.Term
open Meta

def elabStringOfIdent (id : Syntax) : Expr :=
  mkStrLit id.getId.toString

partial def elabExpression : Syntax → TermElabM Expr
  | `(expression| $n:ident $[$es:expression]*) => do
    let es ← es.data.mapM elabExpression
    if h : ¬ es.isEmpty then
      let l  ← mkListLit (Lean.mkConst ``Expression) es    -- term of type `List Expression`
      let h  ← mkEqRefl (← mkAppM ``List.isEmpty #[l])     -- h  := (Eq.refl (List.isEmpty <l>))
      let hn ← mkAppM ``List.notEmpty_of_eq_false #[l, h]  -- hn := (List.notEmpty_of_eq_false <l> <h>)
      let nl ← mkAppM ``List.toNEList #[l, hn]             -- nl := (List.toNEList <l> <hn>)
      mkAppM ``Expression.app #[elabStringOfIdent n, nl]   -- app <n> <nl>
    else mkAppM ``Expression.var #[elabStringOfIdent n]
  | _ => throwUnsupportedSyntax

elab "#test1" e:expression:0 : command =>
  Command.liftTermElabM none do
    let e ← elabExpression e
    check e
    IO.println (← Meta.ppExpr e)

partial def elabExpression' : Syntax → TermElabM Expr
  | `(expression| $n:ident $[$es:expression]*) => do
    let es ← es.data.mapM elabExpression
    match es with
    | e::es =>
      let l  ← mkListLit (Lean.mkConst ``Expression) es
      let nl ← mkAppM ``List.toNEList' #[e, l]
      mkAppM ``Expression.app #[elabStringOfIdent n, nl]
    | [] => mkAppM ``Expression.var #[elabStringOfIdent n]
  | _ => throwUnsupportedSyntax

elab "#test2" e:expression:0 : command =>
  Command.liftTermElabM none do
    let e ← elabExpression' e
    check e
    IO.println (← Meta.ppExpr e)

#test2 foo a b

[Arthur Paulino]

Wow Leo, thank you SO MUCH for the deeply thought answer!

[Leonardo de Moura]

BTW, note that your parser is parsing foo a b as foo (a b).

[Arthur Paulino]

Yeah, I'm experimenting with some tricks that should allow me to write

b := 5
a :=
  x := b + 2
  x
a = 7 # true

As well as

a := 2
f x y :=
  z := a + x
  z + y
f 3 5       # 10

[Arthur Paulino]

Added these just because why not

def isEq : NEList α → List α → Prop
  | .cons a as, b :: bs => a = b ∧ isEq as bs
  | .uno  a   , [b]     => a = b
  | _,          _       => False

theorem ListToNEListIsEqList {a : α} {as : List α} :
    isEq (as.toNEList a) (a :: as) := by
  induction as with
  | nil            => rw [List.toNEList, isEq]
  | cons a' as' hi =>
    cases as' with
    | nil      => simp only [List.toNEList, isEq]
    | cons _ _ =>
      simp [List.toNEList, isEq] at hi ⊢
      exact hi

theorem NEListToListEqList {a : α} {as : List α} :
    (as.toNEList a).toList = a :: as := by
  induction as with
  | nil           => rw [List.toNEList, NEList.toList]
  | cons _ as' hi =>
    cases as' with
    | nil      => simp only [List.toNEList, NEList.toList]
    | cons _ _ =>
      simp [List.toNEList, NEList.toList] at hi ⊢
      exact hi