feat: de Bruijn Syntax for Untyped Lambda Calculus and a proof of Church-Rosser with Parallel Reduction by zayn7lie · Pull Request #475 · leanprover/cslib

zayn7lie · 2026-04-07T11:09:02Z

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 · 2026-04-14T00:00:56Z

@zayn7lie Please rebase on upstream rather than merge

Thanks for notification, sorry for confusion.

chenson2018 · 2026-04-14T00:36:49Z

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 · 2026-04-14T10:46:17Z

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 · 2026-04-14T11:04:50Z

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

zayn7lie · 2026-04-14T11:19:36Z

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 · 2026-04-14T11:29:53Z

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.

eric-wieser · 2026-04-28T02:22:27Z

+    (h₁ : ∀ {a b}, r a b → p a b)
+    (h₂ : ∀ {a b}, p a b → ReflTransGen r a b) :
+    ∀ {a b}, ReflTransGen r a b ↔ ReflTransGen p a b := by


Perhaps better as

Suggested change

(h₁ : ∀ {a b}, r a b → p a b)

(h₂ : ∀ {a b}, p a b → ReflTransGen r a b) :

∀ {a b}, ReflTransGen r a b ↔ ReflTransGen p a b := by

(h₁ : r ≤ p)

(h₂ : p ≤ ReflTransGen r) :

ReflTransGen r = ReflTransGen p := by

I think this was discussed on Zulip?

Yes, this thread. I'd use the naming and shorter proof discussed there as well.

commits/ef3c7ebafc5c3091ae123b5c30b9912cc539d818

eric-wieser · 2026-04-28T02:24:39Z

+      | Par.var t => cases em (t = n) with
+          | inl h => 
+              simp_all only [sub, subst, ↓reduceIte, 
+                decre_incre_elim, incre_par]
+          | inr h => cases em (t < n) with


I think this is better handled with obtain h | h | h := lt_trichotomy t n

eric-wieser · 2026-04-28T02:25:09Z

+notation:max "𝕧" str => Term.var str
+notation:max "λ." t => Term.abs t
+infixl:77 "·" => Term.app


These should use @[inherit_doc]

The application notation is also problematic, as it conflicts the core \. notation.

eric-wieser · 2026-04-28T02:26:22Z

+/-- `subst j s t` substitutes `j` with term `s` in `t`. -/
+@[expose] public def subst (j : Nat) (s : Term) : Term → Term
+  | var k   => if k = j then s else var k
+  | abs t   => abs (subst (j + 1) (incre 1 0 s) t)
+  | app t u => app (subst j s t) (subst j s u)
+
+/-- `decre i l t` decrements `i` for all free vars `≥ l + i`.
+    the reason using `l + i` is that it is more explicit for
+    free variable elimination. For example, after eliminating
+    `var k` for Term `t` from the most outside, `decre 1 k t`
+    will close the gap caused by `k` elimination. -/
+@[expose] public def decre (i : Nat) (l : Nat) : Term → Term
+  | var k   => if l + i ≤ k then var (k - i) else var k
+  | abs t   => abs (decre i (l + 1) t)
+  | app t u => app (decre i l t) (decre i l u)


Should this be a single operation?

Hmm, I don't think I've ever seen it done that way before? It might be awkward not having incre and decre as inverses. I'm not sure though.

eric-wieser · 2026-04-28T02:27:36Z

+  | var : Nat → Term
+  | abs : Term → Term
+  | app : Term → Term → Term


Please write a docstring for each of these

I mean put a docstring on each one, not add to the main docstring.

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?

chenson2018 · 2026-04-13T23:18:10Z

Let's follow the convention of naming this file Basic.lean.

chenson2018 · 2026-04-13T23:20:30Z

+-/
+
+
+namespace Lambda


The namespacing should closely follow the previous lamba calculi developments. I think that would make this Cslib.LambdaCalculus.Unscoped.Untyped.

chenson2018 · 2026-04-13T23:21:06Z

+open Term
+namespace Term


It is redundant to both open and then enter a namespace

Suggested change

open Term

namespace Term

namespace Term

chenson2018 · 2026-04-13T23:22:33Z

+infixl:77 "·" => Term.app
+
+/-- `incre i l t` increments `i` for all free vars `≥ l`. -/
+@[expose] public def incre (i : Nat) (l : Nat) : Term → Term


As I mentioned previously, I would remove everywhere you use public and @[expose] in favor of @[expose] public section

chenson2018 · 2026-04-13T23:30:07Z

+  induction t generalizing l with
+  | var k => simp_all only [incre, Nat.add_zero, ite_self]
+  | abs t ih => simp_all only [incre]
+  | app t u iht ihu => simp_all only [incre]


These simp are terminal, so do not need to be squeezed. Personally I would just write

Suggested change

induction t generalizing l with

| var k => simp_all only [incre, Nat.add_zero, ite_self]

| abs t ih => simp_all only [incre]

| app t u iht ihu => simp_all only [incre]

induction t generalizing l with grind [incre]

chenson2018 · 2026-04-28T03:00:42Z

+notation:max "𝕧" str => Term.var str
+notation:max "λ." t => Term.abs t
+infixl:77 "·" => Term.app


The application notation is also problematic, as it conflicts the core \. notation.

chenson2018 · 2026-04-28T03:07:31Z

+    (h₁ : ∀ {a b}, r a b → p a b)
+    (h₂ : ∀ {a b}, p a b → ReflTransGen r a b) :
+    ∀ {a b}, ReflTransGen r a b ↔ ReflTransGen p a b := by


Yes, this thread. I'd use the naming and shorter proof discussed there as well.

…lation`, and add `rtc_eq_of_sandwich`

…multi-step closure

eric-wieser · 2026-05-05T17:48:44Z

+    (t·u) ↠β (t'·u) := by
+  induction h with
+  | refl => exact refl (t·u)
+  | tail hab hbc ih => exact tail ih (Beta.appL hbc)


Suggested change

(t·u) ↠β (t'·u) := by

induction h with

| refl => exact refl (t·u)

| tail hab hbc ih => exact tail ih (Beta.appL hbc)

(t·u) ↠β (t'·u) :=

h.lift (· ·u) fun _ _ => .appL

etc

eric-wieser · 2026-05-05T21:44:18Z

+theorem app {t t' u u'}
+    (ht : t ↠β t') (hu : u ↠β u') :
+    (app t u) ↠β (app t' u') := 
+  Relation.ReflTransGen.trans (appL ht) (appR hu) 


perhaps:

Suggested change

Relation.ReflTransGen.trans (appL ht) (appR hu)

(appL ht).trans (appR hu)

eric-wieser · 2026-05-05T21:49:43Z

+/-- Notation typeclass for substitution, t[n := s] ≃ t.sub n s 
+    which substitute nth variable in t with s. -/
+instance : Cslib.HasSubstitution Term Nat Term 
+  where subst := sub


There's no reason to explain where whta the typeclass is for

Suggested change

/-- Notation typeclass for substitution, t[n := s] ≃ t.sub n s

which substitute nth variable in t with s. -/

instance : Cslib.HasSubstitution Term Nat Term

where subst := sub

instance : Cslib.HasSubstitution Term Nat Term where

subst := sub

Also, was this written by an AI?

Sorry, I do not know about the style. This part is written by me.

zayn7lie requested review from chenson2018 and fmontesi as code owners April 7, 2026 11:09

chenson2018 self-assigned this Apr 7, 2026

chenson2018 requested changes Apr 10, 2026

View reviewed changes

zayn7lie changed the title ~~feat: Church–Rosser theorem (Q1308502) for ULC (de Bruijn)~~ feat: de Bruijn Syntax for Untyped Lambda Calculus and a proof of Church-Rosser with Parallel Reduction Apr 10, 2026

zayn7lie requested a review from chenson2018 April 11, 2026 23:58

zayn7lie force-pushed the main branch from b52a1c3 to bf31f0b Compare April 14, 2026 00:25

zayn7lie force-pushed the main branch from bf31f0b to 91db832 Compare April 27, 2026 17:28

eric-wieser reviewed Apr 28, 2026

View reviewed changes

Comment thread Cslib/Languages/LambdaCalculus/Unscoped/Untyped/DeBruijnSyntax.lean Outdated

eric-wieser reviewed Apr 28, 2026

View reviewed changes

chenson2018 reviewed Apr 28, 2026

View reviewed changes

zayn7lie added 9 commits May 5, 2026 12:29

feat: Church–Rosser theorem (Q1308502) for ULC (de Bruijn)

117aa37

upd: change dir

8118179

upd: localize from to

3927231

upd: eliminate for de bruijn syntax and explicit all and

801911f

upd: eliminate for diamond and Confluent definition

60584c1

upd: generalize decrement for consistency

642dcda

upd: instantiate with

f705972

upd: newline between theorems

cf76a74

upd: clean up ConfluentReduction.lean to `Cslib.Foundations.Data.Re…

86c6282

…lation`, and add `rtc_eq_of_sandwich`

zayn7lie added 4 commits May 5, 2026 12:29

upd: clean up ConfluentReduction.lean to `Cslib.Foundations.Data.Re…

5245bae

…lation`, and add `rtc_eq_of_sandwich`

upd: clarification for consistency of decre

a0a325b

upd: reduction_sys for generating notations for reductions and the …

1d867fb

…multi-step closure

fix: notation typeclass for substitution

cd4b371

zayn7lie force-pushed the main branch from 91db832 to cd4b371 Compare May 5, 2026 16:30

zayn7lie added 2 commits May 5, 2026 12:50

fix: sandwich

ef3c7eb

fix: par_subst - lt_trichotomy

227f618

eric-wieser reviewed May 5, 2026

View reviewed changes

zayn7lie added 8 commits May 5, 2026 13:55

fix: syntax - disambiuity

f10bc4b

upd: syntax - sub - specify type

ac6e547

upd: syntax - Term - docstring

088c042

upd: xyntax - incre_rfl - proof

7ce6832

fix: namespace

01049fc

upd: open term redundent

1b9eba8

upd: \@\[expose\] public section

437d801

upd: betareduction - proof simp

0d7928a

zayn7lie requested review from chenson2018 and eric-wieser May 5, 2026 21:39

upd: typo

dac794a

eric-wieser reviewed May 5, 2026

View reviewed changes

upd: betareduction

e123ae1

eric-wieser reviewed May 5, 2026

View reviewed changes

fix: debruijn - where

ed88f4d

	Relation.ReflTransGen.trans (appL ht) (appR hu)
	(appL ht).trans (appR hu)

Conversation

zayn7lie commented Apr 7, 2026

Main contributions

Design choices

Use of AI

Uh oh!

chenson2018 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

zayn7lie commented Apr 14, 2026

Uh oh!

chenson2018 commented Apr 14, 2026

Uh oh!

zayn7lie commented Apr 14, 2026

Uh oh!

lengyijun commented Apr 14, 2026

Uh oh!

zayn7lie commented Apr 14, 2026

Uh oh!

chenson2018 commented Apr 14, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chenson2018 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment