STLC formalization in Lean4

Stream: mathlib4

[Elif Uskuplu]

Hi all, I'm Elif Uskuplu, a recent PhD in math from USC. As a project suggested by @Jeremy Avigad in the Formalization of Mathematics (SLMATH) summer program, I've finished my work about the formalization of STLC in locally nameless syntax in Lean4. One can read the details from the github repository. The important and novel part of the study is that it includes the proof of strong normalization in locally nameless syntax. I would like to contribute to mathlib with my work. I've already an invitation for write permission for non-master branches, and I've accepted. However, I'm new in Lean4 community, so I would like to consult to experts about opening a PR. How STLC should be in mathlib? Please let me know if you have questions and suggestions.

[Yaël Dillies]

@Sky Wilshaw will probably be interested in hearing about this!

[Sky Wilshaw]

This seems really interesting! I've been writing something similar (although I've not been contributing to it for a while). While I haven't gotten as far with the theory as you have, I think my presentation of lambda calculi is more general, and can optionally deal with finitary (co)product types, and should be easily extendable with other features. The code is here if you're interested. I assume that if your code were added into mathlib, it would be desirable to prove it in the most general form, but people more familiar with the process than me should comment on that.

[Elif Uskuplu]

@Sky Wilshaw thanks for the information. Indeed, the more the structure is general, the better it is. In this version, I only have a base type and arrow types, but I can try to add the others if it is needed before submitting a PR. I'll wait for further comments before finalizing.

[Jannis Limperg]

There is no clearly "most general" version of STLC. You can always add more base types and operations, though this can potentially be dealt with by parameterising over base types and primitive operations. More fundamentally, it's not clear whether you should use de Bruijn indices or de Bruijn levels or locally nameless or even named representations of binders and variables; all of these have their pros and cons. Then there are people who like to use intrinsically typed syntax and others who prefer extrinsic types. So unfortunately the state of the art in type theory research seems to be that everyone defines their own little calculus and all these calculi are obviously related to each other, but the relation is not made formal.

What this means for Mathlib is that, in my view, it doesn't make much sense to insist on the usual philosophy that there should be one canonical representation of each concept. Of course, obvious opportunities for generalisation should be taken, but if someone needs STLC with de Bruijn and Mathlib has STLC with locally nameless, I would put both formalisms into Mathlib and relate them with the obvious maps.

Then again, I'm not involved with Mathlib maintenance, so these are just personal opinions.

[Mario Carneiro]

What this means for Mathlib is that, in my view, it doesn't make much sense to insist on the usual philosophy that there should be one canonical representation of each concept.

In my view, what this means for mathlib is that it should not attempt to formalize a specific type theory like STLC but rather formalize a tool for constructing type theories. There is precedent in other libraries: Autosubst in Coq and Nominal Isabelle in Isabelle

[Jannis Limperg]

I can see that. As a refinement of this approach, perhaps the rule should be: Mathlib should only formalise type theories if they're used by something else in Mathlib. For example, if someone wants to use STLC as the internal language of cartesian-closed categories or as a representation of intuitionistic propositional logic, then the specific variant of STLC most useful for this should (well, needs to) be in Mathlib.

[Elif Uskuplu]

Thank you for your comments. It seems that keeping this as a separate repository is the right thing to do in this case. But I also got inspired to expand this work for many different needs, thanks.

[Emilie (Shad Amethyst)]

I'd also throw Iris, made for Coq, into the bucket of existing libraries. They also have a set of custom tactics for reasoning in a hoare-style logic

[Mario Carneiro]

see also https://github.com/leanprover-community/iris-lean/

[Emilie (Shad Amethyst)]

Oooh now that's interesting

[Ira Fesefeldt]

Although the Iris port really is more a MoSeL port at this stage, i.e. no hoare-triples yet.