Constructing forall/exists syntax

Stream: lean4

[Jesse Vogel]

I want to manipulate some syntax in Lean, which in the end should result in syntax describing an ∃ or ∀ statement. Given as input some syntax describing the identifiers and their types, I came up with the following function.

def constructExists (args : Array (Array Syntax × Syntax)) (body : Syntax) : Syntax :=
  mkNode `«term∃_,_» #[
    mkAtom "∃",
    mkNode `Lean.explicitBinders #[
      mkNode `null $ args.map λ (ids, type) =>
        mkNode `Lean.bracketedExplicitBinders #[
          mkAtom "(",
          mkNode `null (ids.map λ id => mkNode `Lean.binderIdent #[ id ]),
          mkAtom ":",
          type,
          mkAtom ")"
        ]
    ],
    mkAtom ",",
    body
  ]

This method works for me (at least for all my inputs), but to me it seems a bit ad hoc. I must say I'm no expert on syntax at all, but it feels like this function might break at some point in the future? Similarly, I tried to define a function to construct ∀-statements, but this one does not work (the resulting syntax does not parse well..)

def constructForAll (args : Array (Array Syntax × Syntax)) (body : Syntax) : Syntax :=
  mkNode `Lean.Parser.Term.forall #[
    mkAtom "∀",
    mkNode `Lean.explicitBinders #[
      mkNode `null $ args.map λ (ids, type) =>
        mkNode `Lean.bracketedExplicitBinders #[
          mkAtom "(",
          mkNode `null (ids.map λ id => mkNode `Lean.binderIdent #[ id ]),
          mkAtom ":",
          type,
          mkAtom ")"
        ]
    ],
    mkAtom ",",
    body
  ]

Do any of you know what the best/correct way is to achieve this?

[Henrik Böving]

you want to work in a monad that support syntax quotations via the MonadQuotation typeclass such as MacroM, for a full list of implementors see docs4#Lean.MonadQuotation. Then you can use syntax such as:

macro "const" e:term : term => `(fun x => $e)

the one on the right hand side of the arrow here in order to generate your Syntax.

[François G. Dorais]

To expand on Henrik's comment:

open Lean

def mkForall (xs : Array (Syntax × Syntax)) (e : Syntax) : MacroM Syntax :=
  let vs := xs.map Prod.fst
  let ts := xs.map Prod.snd
  `(∀ $[($vs : $ts)]*, $e)

[Jesse Vogel]

Thank you very much! Using the mkForall works, but for some reason if I try to make an analogue mkExists something goes wrong. Consider the following minimal example: if I use mkForall everything is fine, but if I switch to mkExists it complains unknown identifier 'T'. Why does this happen?

import Lean
open Lean
open Lean.Elab
open Lean.Elab.Term
open Command

set_option trace.debug true

def mkForall (xs : Array (Syntax × Syntax)) (e : Syntax) : Command.CommandElabM Syntax :=
  let vs := xs.map Prod.fst
  let ts := xs.map Prod.snd
  `(∀ $[($vs : $ts)]*, $e)

def mkExists (xs : Array (Syntax × Syntax)) (e : Syntax) : Command.CommandElabM Syntax :=
  let vs := xs.map Prod.fst
  let ts := xs.map Prod.snd
  `(∃ $[($vs : $ts)]*, $e)

declare_syntax_cat binder
syntax "(" ident ":" term ")" : binder

declare_syntax_cat binders
syntax binder+ : binders

elab cmd:"#test" q:binders : command => do
  match q with
  | `(binders| $p:binder*) => do
    -- Make array of identifier-type pairs
    let arr := p.map λ b => match b with
    | `(binder| ($i:ident : $t:term)) => (i, t)
    | _ => unreachable!
    -- Construct syntax
    let stx ← mkExists arr (←`(True)) -- Using this one complains
    -- let stx ← mkForall arr (←`(True)) -- This one is fine
    -- Elaborate syntax to expression
    let result ← liftTermElabM none do
      let expr ← elabTerm stx none
      trace[debug] "expr = {expr}"

  | _ => unreachable!

#test (T : Type) (t : T)

[Sebastian Ullrich]

If composed syntax quotations misbehave, it is usually due to missing annotations

def mkExists (xs : Array (Syntax × Syntax)) (e : Syntax) : Command.CommandElabM Syntax :=
  let vs := xs.map Prod.fst
  let ts := xs.map Prod.snd
  `(∃ $[($vs:ident : $ts)]*, $e)

The binder syntax of exists and forall is not identical