Delaborating an Expr object

Stream: lean4

[Leni Aniva]

Is there a way to delaborate an Expr object so it becomes another Expr object instead of a syntax?

For example, consider the expression of a + b where a, b are both Nats. Then this expression when fully elaborated is

.app (.app (.app (.const `HAdd.hAdd `Nat) `Nat) `Nat ... -- along with `instHAdd and `instAddNat

but when written out it is just a HAdd.hAdd operator with two fvars:

.app (.app (.const `HAdd.hAdd) (.fvar ...)) (.fvar ...)

The delab function in Delaborator/Basic.lean outputs syntax directly. Is there a way to make it output Exprs?

[Eric Wieser]

What do you mean by "when written out"?

[Kyle Miller]

Elaboration is Syntax -> Expr, and delaboration is Expr -> Syntax. In Lean 3 there didn't used to be Syntax and there indeed were unelaborated Exprs, but it doesn't work that way anymore.

[Leni Aniva]

Eric Wieser said:

What do you mean by "when written out"?

a literal interpretation of a + b only contains a,b, and the HAdd.hAdd operator. That is what I mean

[Leni Aniva]

Kyle Miller said:

Elaboration is Syntax -> Expr, and delaboration is Expr -> Syntax. In Lean 3 there didn't used to be Syntax and there indeed were unelaborated Exprs, but it doesn't work that way anymore.

so there's no intermediate stage between an Expr and Syntax now? Is there another way to determine if an argument can be inferred automatically in the delaborator?

[Eric Wieser]

The term you gave would be @HAdd.hAdd a b, which would be a type error; surely you'd want @HAdd.hAdd _ _ _ _ a b?

[Eric Wieser]

(in Expr there is no such thing as explicit vs implicit arguments; you always have to pass all of them)

[Thomas Murrills]

Leni Aniva said:

Eric Wieser said:

What do you mean by "when written out"?

a literal interpretation of a + b only contains a,b, and the HAdd.hAdd operator. That is what I mean

I think this assumption is the issue. Like Eric said, all Exprs should be type correct, and HAdd.hAdd takes 6 arguments, not 2. When the syntax a + b gets elaborated, it goes straight to the 6-argument version, but with metavariables for the instance and implicit arguments. These then get synthesized and inferred, respectively. (Which is also what Eric said, but just to be clear that this is the process Lean is doing. Unless there are shortcuts. But you can think of this as being the process anyway.)

[Thomas Murrills]

Leni Aniva said:

Kyle Miller said:

Elaboration is Syntax -> Expr, and delaboration is Expr -> Syntax. In Lean 3 there didn't used to be Syntax and there indeed were unelaborated Exprs, but it doesn't work that way anymore.

so there's no intermediate stage between an Expr and Syntax now? Is there another way to determine if an argument can be inferred automatically in the delaborator?

Likewise, the way you determine instance vs. implicit vs. explicit arguments is by looking at the type of the head of the expression, e.g. the type of .const ``HAdd.hAdd _. That type will be a .forallE, and it comes with a .binderInfo for its argument slot which tells you what kind of argument it should be. (You then need to look at the body to get another .forallE for the next argument, and so on.)

[Thomas Murrills]

Though I’m wondering if this is a bit of an #xy problem; is there something specific you want to extract this information for?

[Leni Aniva]

Thomas Murrills said:

Though I’m wondering if this is a bit of an #xy problem; is there something specific you want to extract this information for?

It isn't an xy problem because this data goes directly to train machine learning models

[Mario Carneiro]

why don't you pass the Syntax to the ML model instead of a malformed Expr?

[Leni Aniva]

Mario Carneiro said:

why don't you pass the Syntax to the ML model instead of a malformed Expr?

because the syntax doesn't contain informations about which part is a function call and which part is a lambda, etc., and I think such information could help the ML model learn if it was available somewhere

[Mario Carneiro]

why don't you pass the Expr to the ML model instead of a malformed Expr?

[Leni Aniva]

Mario Carneiro said:

why don't you pass the Expr to the ML model instead of a malformed Expr?

this is what I have been doing. Im just wondering if there's a delaborated version

[Mario Carneiro]

Delaboration produces syntax, but you can turn off pp options to make the syntax more expr-like if you need

[Siddhartha Gadgil]

An option (which I use) is to write custom delaborators to add more information. This is done at https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanAide/VerboseDelabs.lean for example.

[Leni Aniva]

Eric Wieser said:

The term you gave would be @HAdd.hAdd a b, which would be a type error; surely you'd want @HAdd.hAdd _ _ _ _ a b?

this could also work. Is there a way to generate that?

[Leni Aniva]

Mario Carneiro said:

Delaboration produces syntax, but you can turn off pp options to make the syntax more expr-like if you need

This is what I have been doing with a custom parser to parse the prefixed delaboration result

[Eric Wieser]

@Siddhartha Gadgil said:

An option (which I use) is to write custom delaborators to add more information. This is done at https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanAide/VerboseDelabs.lean for example.

Is the (proof =: prop) syntax there any different from the built-in (proof : prop)?

[Siddhartha Gadgil]

Eric Wieser said:

Siddhartha Gadgil said:

An option (which I use) is to write custom delaborators to add more information. This is done at https://github.com/siddhartha-gadgil/LeanAide/blob/main/LeanAide/VerboseDelabs.lean for example.

Is the (proof =: prop) syntax there any different from the built-in (proof : prop)?

I guess only that prop is guaranteed to be a proposition. This is to extract lemmas used in a (term) proof and their further premises, lemmas etc.

[Thomas Murrills]

There’s also sometimes the possibility of reducing your Exprs first, e.g. turning @HAdd.hAdd _ _ _ _ a b into Nat.add a b. Not a universal solution, since not everything of this form can actually reduce, but just wanted to mention it in case it’s relevant for training.

[Leni Aniva]

Thomas Murrills said:

There’s also sometimes the possibility of reducing your Exprs first, e.g. turning @HAdd.hAdd _ _ _ _ a b into Nat.add a b. Not a universal solution, since not everything of this form can actually reduce, but just wanted to mention it in case it’s relevant for training.

Is there a function that can do this?

[Eric Wieser]

It is very unlikely that that is a thing you want to do. Approximately nothing in mathlib is stated about Nat.add

[Leni Aniva]

Eric Wieser said:

It is very unlikely that that is a thing you want to do. Approximately nothing in mathlib is stated about Nat.add

Ah I remember this. I've asked about it before. Is there a way to turn HAdd.hAdd Nat Nat inst... a b into just HAdd.hAdd _ _ _ _ a b? i.e. replacing all the inferable arguments with _