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.

chenson2018 · 2026-04-10T07:12:35Z

+  | app t₁ t₂ ih₁ ih₂ => simp_all
+
+/-- Communitivity of incre. -/
+public theorem incre_comm {i j k l t} :


I think we can clean up some of the arithmetic in theorems like this, but I'll wait until we have more high-level changes done first to give specific suggestions.

Sure, thanks.

chenson2018 · 2026-04-10T07:18:09Z

+  | appL {t t' u}      : Beta t t' → Beta (t·u) (t'·u)
+  | appR {t u u'}      : Beta u u' → Beta (t·u) (t·u')
+  | red  (t' s : Term) : Beta ((λ.t')·s) (t'.sub 0 s)
+public abbrev BetaStar := Relation.ReflTransGen Beta


We use the attribute reduction_sys for generating notations for reductions and the multi-step closure.

commits/2c3aac6ca1538a49b2fb26ad8f8196ecdc11b77b

commits/05d381c02932ca948e6a7bf58477fc937a62ded0

At the same time, would you know how to type ⭢ in Lean for single reduction?

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.

…lation`, and add `rtc_eq_of_sandwich`

…multi-step closure

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.

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:07Z

+  | app t u => app (decre i l t) (decre i l u)
+
+/-- Substitute into the body of a lambda: `(λ.t) s` -/
+@[expose] public def sub (t : Term) (n : Nat) (s : Term) := 


Suggested change

@[expose] public def sub (t : Term) (n : Nat) (s : Term) :=

@[expose] public def sub (t : Term) (n : Nat) (s : Term) : Term :=

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

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.

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 added 13 commits April 27, 2026 13:25

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

2cc8ebc

upd: change dir

df78d25

upd: localize from to

7c62711

upd: eliminate for de bruijn syntax and explicit all and

4e20051

upd: eliminate for diamond and Confluent definition

a551bd9

upd: generalize decrement for consistency

c89adac

upd: instantiate with

3f03614

upd: newline between theorems

231440b

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

e5c5bbd

…lation`, and add `rtc_eq_of_sandwich`

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

c33e118

…lation`, and add `rtc_eq_of_sandwich`

upd: clarification for consistency of decre

fae2be0

upd: reduction_sys for generating notations for reductions and the …

d106175

…multi-step closure

fix: notation typeclass for substitution

91db832

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

chenson2018 reviewed Apr 28, 2026

View reviewed changes

	@[expose] public def sub (t : Term) (n : Nat) (s : Term) :=
	@[expose] public def sub (t : Term) (n : Nat) (s : Term) : Term :=

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!

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!

Choose a reason for hiding this comment

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!

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development