My first Lean project

Stream: new members

[Daniel]

Hi everyone, I'm Daniel, a math student. For the past few years, I've been studying type theory, logic, and computability, and lately I've been very interested in working on formalization. This is my first project: a formalization of lambda calculus and a proof of the Church-Rosser theorem. It's nothing groundbreaking; I based it on other existing repositories.

project link

I would appreciate any suggestions or recommendations regarding my project. My experience with Lean has been fascinating; I find it an incredible tool with great potential for research, which is why I've decided to write my undergraduate thesis on formalization. I plan to formalize some theorems.

[Michael Rothgang]

Mathlib has a list of 1000+ theorems --- and the Church-Rosser theorem is still listed as unformalised in Lean (which is no longer true). Would you like to make a PR adding your formalisation to the list? You want to modify https://github.com/leanprover-community/mathlib4/blob/master/docs/1000.yaml (search for "Church-Rosser" to find the entry to tweak), and follow the instructions https://leanprover-community.github.io/contribute/index.html on how to contribute.

[Michael Rothgang]

(If you prefer not to, somebody else can also do this for you: but since you did the work, in my opinion you also deserve the honour of making that pull request yourself.)

[Snir Broshi]

Daniel said:

I would appreciate any suggestions or recommendations regarding my project

Would you be willing to submit this to cslib? They already have your definition of Diamond, and a proof of Church-Rosser for SKI calculus, but not for lambda calculus AFAIK

[Daniel]

I had never considered the possibility of making a pull request. I would like to do it, but I consider this formalization of lambda calculus using de Bruijn indices to be very complicated and I don't think it's suitable for inclusion in any library. I'm currently working on a more elegant and less complicated formalization of the lambda calculus; I'll submit the pull request when I finish it. Thanks for the recommendations.

[Chris Henson]

@Daniel Sorry to not see this until now! I see from the README you referenced one my repos that eventually became part of CSLib. However we only moved over the locally nameless representation (for which we do have a proof of confluence here) and did not transfer this deBruijn indices representation, partially because of my own reservations about the shifting being a bit messy. Can I ask what "less complicated formalization" you're planning on next? If it is well scoped indices this has been on my TODO list, but we could certainly work in tandem.

[Daniel]

@Chris Henson Your work was a great tool in guiding me through my formalization process. I was working on a simplification of the locally nameless representation; the formalization itself is quite beautiful and simple, but I didn't like some of the definitions. For example, I've shown things like

$$\begin{align*} \text{Lc } (\lambda N) &\iff \exists L \forall x \notin L, \text{Lc } N^x \\ &\iff \exists x \notin \text{fv}(N), \text{Lc } N^x \\ &\iff \forall x, \text{Lc } N^x \end{align*}$$

This is a great advantage because in the hypotheses I can work with a universal quantifier, but prove with cofinite quantifiers. Even so, that project is in limbo because my supposed simplification has made it more complicated.

Regarding well-scoped indices, I would love to work on them, but what would be the objective of working with this representation? I feel it is more complicated than de Bruijn indices, so I don't feel it is optimal for making proofs, even though I have read very little about it.

[Chris Henson]

Yes, the cofinite quantification can be difficult, and it is easy to back yourself into a corner. It also doesn't work well with certain automation like grind and is awkward if you want to do denotational or categorical semantics.

My objective with well-scoped indices is that I think it is ultimately simpler than the other two approaches. I'd like to write something very close in implementation to Rocq's Autosubst2.

[Daniel]

As I said, I've read very little. Could you send me some references I could use? I had read it before in the Rebound library in Haskell, and thanks to what you told me, I found Kathrin Stark's thesis, and it's very interesting.

[Chris Henson]

Maybe this is a helpful resource: https://github.com/sweirich/pl-semantics-and-types

This is from a course that Stephanie Weirich just taught that uses Autosubst2 in formalizations of several different systems. When you see .sig files, the corresponding .v is the Rocq code that is automatically produced by Autosubst. (It may seem long, but much of this I feel can be written compactly, especially if you involve grind.). The notes are very helpful for following along.

From seeing what has been developed in Rocq and projects like HoTTLean, I am convinced that well-scoped indices sufficiently scale to letting us have more complex type systems in CSLib. I want to ultimately write a Lean implementation of Autosubst2, but in the meantime I'd like to have a regular "by hand" formalization so we can at least compare the ergonomics.

[Daniel]

Thanks Chris, I really appreciate the reference. I'll study those notes and try to write some code. If I have any updates, I'll share them with you.