Lean 4 export and projections

Stream: lean4

[Siddhartha Gadgil]

I am working on attempting a Trepplein port (currently reading and documenting the code). For handling the additional Lean 4 export (as described and implemented in https://github.com/leanprover/lean4export), it appears to me that I need to add:

• an expression type for projections, and parsing to this.
• reduction rules for this.

My guess is that the following is what has to be added. Could @Sebastian Ullrich or some other expert clarify?

• We have a new type of expressions with two parameters - a name (of a structure) and an index.
• A structure is an inductive type with no indices and a single introduction rule.
• The reduction rule generalizes reducing (Prod.mk x y).2 to y, i.e., we have one reduction rule for each structure.
• The automatically generated functions like Prod.fst are not part of the foundations, but are defined using recursion and exported as declarations.

Also https://github.com/leanprover/lean4export is on an old version of lean.

[Siddhartha Gadgil]

Incidentally, the https://github.com/siddhartha-gadgil/trepplein4 and https://siddhartha-gadgil.github.io/trepplein4/trepplein/index.html are online

[Sebastian Ullrich]

Do you know about the corresponding section in my thesis?

[Siddhartha Gadgil]

No. Can you link to the thesis and the section? I will read it.

[Siddhartha Gadgil]

My google searching (earlier) had led to various masters theses instead.

[Sebastian Ullrich]

https://lean-lang.org/papers/thesis-sebastian.pdf#subsection.3.2.1

[Siddhartha Gadgil]

One thing I had missed is that inferType also has to be implemented for projections (following the section of the thesis).

It looks as though for the next section we need further reduction rules.I am guessing that we should reduce, for example Prod.mk x.1 x.2 to x. Does that look correct?

More details and mistakes will emerge once I am running and testing stuff. But this is enough for me to work with the next few days.

[Siddhartha Gadgil]

A related question/clarification: it seems to me that to infer types etc. of the projection map, the kernel environment should have structure information. In trepplein (for Lean 3) there were only declarations and deduction rules.

Is that correct? If so, should this be added for inductive types if they are structures?
Finally: am I correct that while a structure can have parameters, it cannot have indices?

[Siddhartha Gadgil]

(deleted)

[Siddhartha Gadgil]

I missed the fact that the export format also has the record type, so this should be part of the expression. Decomposing that as Pis should be enough to infer type.

[Siddhartha Gadgil]

If someone can take a look, either I am misunderstanding something or there is a small error in trepplein at https://github.com/siddhartha-gadgil/trepplein4/blob/c3befdf00821d209d5d8b790be82259c55c31114/src/main/scala/trepplein/typechecker.scala#L258 (this is code I have not modified).

It seems to me that for an expression like f a b : P a b, only b is instantiated and the result will have a de Bruin indexed variable in place of a. This is because instantiation is called only once if everything is already in normal form.

I will work on making testing such things easier.