Easily writing large Expr

Stream: lean4

[Max Nowak 🐺]

I am probably going to be doing a lot of Expr.app (Expr.forallE ...) ..., with quite large expressions, and that gets very error-prone quickly for larger expressions. Is there some (anti)quotation macro to obtain Expr from Lean4 code?

[Gabriel Ebner]

There's https://github.com/gebner/quote4/

[Max Nowak 🐺]

I don't understand how I would use quote4, sorry :(.
My use case is more mundane, namely this:

  let nil := Constructor.mk `nil (Expr.app
    (Lean.mkConst `Vec2)
    (Expr.app
      (Expr.app (Lean.mkConst `Vec2) (Lean.mkConst `alpha))
      (Lean.mkNatLit 0)
    )
  )

  let cons := Constructor.mk `cons ( ... ) -- this will be ugly...

[Max Nowak 🐺]

Which I will later pass to mkInductiveDeclEs and send that off to the kernel.

[Gabriel Ebner]

That's precisely what you can automate with quote4:

let nil := Constructor.mk `nil q(Vec2 (Vec2 alpha 0))

[Max Nowak 🐺]

Oh wow my Expr construction was wrong, actually :sweat_smile: .
Sweet, I'll try to use it then.

[Max Nowak 🐺]

Hm, what would be the right way of refering to the type I am trying to introduce? I'm trying to introduce a new inductive type Vec2 via mkInductiveDeclEs, which wants a list of constructor expressions. Problem is, I have no Vec2 yet, other than the Name 'Vec2, but I need to create the constructor expressions like ... -> Vec2. How do I do that with q? q( a -> 'Vec2 a n -> 'Vec2 a (n+1)) doesn't seem to work (imagine ' is the backtick).

Would I have to generate Syntax and elab that :/ ?

[Max Nowak 🐺]

fyi, I have barely any idea of what I'm doing :)

[Tomas Skrivan]

@Gabriel Ebner Would it be possible to add a paragraph to your quote4 library readme about exactly this simple use case? I wanted to use it some time ago, but when reading

It combines the intuitiveness of modal sequent calculus with the power and speed of Lean 4's metaprogramming facilities. The Q(·) modality quotes types: Q(α) denotes an expression of type α. The type former comes with the following natural introduction rule:

my brain just shuts down as there are too many words I do not understand. So I actually never bothered to try your library out.

[Max Nowak 🐺]

Same thing happened to me as well. I am smol brain.

[Mario Carneiro]

"the intuitiveness of modal sequent calculus" is an interesting turn of phrase, I can't tell if it's a joke or not

[Gabriel Ebner]

Sales pitches are supposed to be juicy! I've added a couple easy examples to the readme.

[Max Nowak 🐺]

Maybe something to show that this is easily possible:

let thing : Q(...) := ...
let expr : Expr := thing -- just works

Otherwise Q(...) seems like some magic type and not immediately obvious what it is.

[Max Nowak 🐺]

Any idea how to do the 'Vec2 thing I asked above?

[Gabriel Ebner]

You can write Vec2 as a local variable:

-- u : Level
-- α : Q(Type $u)
-- n : Nat
let Vec2 : Q(Type $u → Nat → Type $u) := mkConst `Vec2 [u]
q($α → $Vec2 $α $n → $Vec2 $α $(n+1))

[Max Nowak 🐺]

What does $ do actually?

[Gabriel Ebner]

It's an antiquotation (similar to `($x) for syntax).