feat: de Bruijn Syntax for Untyped Lambda Calculus and a proof of Church-Rosser with Parallel Reduction

[zayn7lie]

Main contributions

Q1308502: Church-Rosser theorem in 1000 theorems

• A de Bruijn syntax for λ-terms together with substitution and shifting operations.
• Definition of one-step β-reduction.
• Definition of parallel β-reduction (Par) and its basic properties.
• Abstract confluence infrastructure (Diamond, Confluent) for binary relations.
• Proof that parallel β-reduction satisfies the diamond property.
• Deduction of confluence of β-reduction (Church–Rosser theorem) via standard closure arguments.

The development follows the classical proof strategy:
parallel reduction -> diamond -> confluence -> Church–Rosser.

Design choices

• De Bruijn indices are used to avoid α-equivalence bookkeeping.
• Parallel reduction is defined inductively to enable a direct diamond proof.
• Confluence lemmas are factored through generic relation-theoretic definitions
  (Diamond, Confluent) to keep the proof modular.

Use of AI

• Rough structure for beginning
• Small/trivial structure proof
• Docs/Comment generating
• Final refinement

[chenson2018]

Hi, thanks for your interest in contributing to CSLib! We do have Church-Rosser for locally nameless binding, but I think we are interested in having the more common de Bruijn indices representation as well.

I see there is a disclosure of AI usage, but this looks like its been mostly cleaned up pretty well, so thank you.

Below are some initial reviews about making this fit into CSLib conventions.

[zayn7lie]

@zayn7lie Please rebase on upstream rather than merge

Thanks for notification, sorry for confusion.

[chenson2018]

sub looks too complicated, compared to https://api.cslib.io/docs/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.html#Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.openRec

I don't understand this comment. It looks as I would expect for this binding scheme.

[zayn7lie]

Compared to https://api.cslib.io/docs/Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/Basic.html Some new definition are introduced: incre decre

Are they really necessary ?

Please read the header comment docs of DeBruijnSyntax.lean. I have also referred to https://en.wikipedia.org/wiki/De_Bruijn_index in it. Formal definition has the description for primitive operation (substitution).

[lengyijun]

Can you rename sub to subst, according to proof of locally nameless

[zayn7lie]

Can you rename sub to subst, according to proof of locally nameless

I am somehow hesitant to do that. The current subst is more primitive than sub (sub is already very specific for beta reduction), aligning with incre and decre. And I have also introduced Cslib.HasSubstitution, so we might not need to do anything with sub later, but using t[n:=s]. subst might be more useful for future definition of other kinds of usage. @chenson2018 What would you think about this?

[chenson2018]

I agree that we should almost always use the notation and corresponding naming, which is then based off HasSubstitution.subst. So things using the notation should probably use subst, but I'm not sure I care about the name used in the instance.

I've started a second pass of reviews which I'll try to have complete in a few days.

[chenson2018]

This is still not comprehensive, but a few more comments. The comment about squeezing terminal simp applies throughout and is one factor making proofs much longer than they need to be. Could you work on fixing this a bit?

[zayn7lie]

@chenson2018 Hi, is there any update on this? What should I focus on next?