Locally Nameless Beta Confluence

[chenson2018]

This PR would add a proof of beta reduction confluence for the locally nameless representation of the lambda calculus. I have used the new reduction_sys attribute, which seems to work well. There are a few relatively small issues I have marked with TODO comments. These could be addressed in a future PR, but I will mention them here:

• It is useful to have a lemma of the form rs.Red = Rel, where rs is the reduction system generated from Rel. I think this could automatically be generated with the reduction system.
• Occasionally the notation causes problems for automation like aesop, where you end up needing to carrying around two versions of a proof.
• My proof for the diamond property of parallel reduction is long. I tried using the Takahashi translation proof, but had trouble doing this for locally nameless terms.

Edit: I fixed the issue with Trans

[chenson2018]

Side comment: would we like to configure GitHub to merge PRs as a squash commit? I personally like this because it makes the history cleaner, but I know people have differing opinions.

[fmontesi]

Yeah, squash and merge sounds good, especially for PRs with so many commits.

[fmontesi]

Half-way through it, looking good so far. You still have quite a few definitions (also from the previous pr, I think) where the order of parameters is different from the corresponding notation. I'd consider switching, for example: in defs about terms for opening and closing, I'd make the first parameter the term being manipulated. This will allow for dot-notation, which is pretty nice.

Do you see counter-indications to what I'm saying?

(I think I understand the reasoning behind your current approach btw, it makes the signature at the end a clean Term -> Term in many cases.)

[chenson2018]

Half-way through it, looking good so far. You still have quite a few definitions (also from the previous pr, I think) where the order of parameters is different from the corresponding notation. I'd consider switching, for example: in defs about terms for opening and closing, I'd make the first parameter the term being manipulated. This will allow for dot-notation, which is pretty nice.

Do you see counter-indications to what I'm saying?

(I think I understand the reasoning behind your current approach btw, it makes the signature at the end a clean Term -> Term in many cases.)

This PR does not introduce any new notations (outside of using reduction_sys), so these would be previously reviewed definitions. There are exactly four notations defined in LocallyNameless.Basic: opening, closing, and their specializations to the closest binding.

My opinion on the dot notation is similar to Yael's in the Zulip discussion the other day. In Mathlib, the idiomatic pattern seems to be treating notation as the cannonical form and building an "API" around them. We seem to be following this idiom with our notations for reduction, substitution, etc., and ideally we would never see the non-notation terms and dot notation at all (perhaps needing delaborators to realize this fully). I do like dot notation myself on occasion, but I think it is considered a bit of an anti-pattern to be concerned with argument layout in this way. I also find it a hassle for functions with multiple paramaters of the same type to have to think about the order in which they were used. And finally yes, I like the aesthetic of pattern matching on a Term -> Term, though of course this is not a reason to make a decision one way or another.

In short, I think the order of paramaters for a definition used as notation should be treated as irrelevant. It's no big deal at all to change it if you would like, but I think as we encounter situations where it seems we need to work with these terms directly we should be thinking about why the abstraction of using these notations as API has broken down and aim to fix this.

(A very long message to conclude something doesn't matter 😂)

[fmontesi]

Mmmh.... Ok, I think I'm sold! 😀