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

Cslib/Foundations/Data/Relation.lean

@@ -51,6 +51,22 @@ theorem ReflTransGen.to_eqvGen (h : ReflTransGen r a b) : EqvGen r a b := by
 theorem SymmGen.to_eqvGen (h : SymmGen r a b) : EqvGen r a b := by
   induction h <;> grind
 
+/-- Sandwich: if `r ⊆ p ⊆ r*` then `r* = p*`. -/
+theorem ReflTransGen.sandwich_to_eq {α} {r p : α → α → Prop}
+    (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
+  intro a b
+  constructor
+  · intro hr
+    induction hr with
+    | refl => exact ReflTransGen.refl
+    | tail hab hbc ih => exact ReflTransGen.tail ih (h₁ hbc)
+  · intro hp
+    induction hp with
+    | refl => exact ReflTransGen.refl
+    | tail hab hbc ih => exact ReflTransGen.trans ih (h₂ hbc)
+
 attribute [scoped grind →] ReflGen.to_eqvGen TransGen.to_eqvGen ReflTransGen.to_eqvGen
   SymmGen.to_eqvGen
 

Cslib/Languages/LambdaCalculus/Unscoped/Untyped/BetaReduction.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 zayn7lie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zayn Wang
+-/
+module
+
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.DeBruijnSyntax
+public import Cslib.Foundations.Data.Relation
+
+/-!
+# One-step β-reduction and its reflexive-transitive closure
+
+This file defines the usual compatible one-step β-reduction on de Bruijn lambda terms.
+It also introduces its reflexive-transitive closure and proves basic closure lemmas for
+application and abstraction.
+
+## Main definitions
+
+* `Lambda.Beta`: one-step β-reduction.
+* `Lambda.BetaStar`: the reflexive-transitive closure of `Beta`.
+
+## Main lemmas
+
+Inside `namespace BetaStar` we provide the standard constructors and congruence lemmas:
+
+* `BetaStar.refl`
+* `BetaStar.head`
+* `BetaStar.tail`
+* `BetaStar.trans`
+* `BetaStar.appL`, `BetaStar.appR`, `BetaStar.app`
+* `BetaStar.abs`
+
+These lemmas are used later to compare β-reduction with parallel reduction.
+-/
+
+
+namespace Lambda
+open Term
+
+/-- One-step β-reduction (compatible closure). -/
+@[reduction_sys "β"]
+public inductive Beta : Term → Term → Prop
+  | abs  {t t'}        : Beta t t' → Beta (λ.t) (λ.t')
+  | 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
+
+namespace BetaStar
+
+public theorem refl (t : Term) : BetaStar t t :=
+  Relation.ReflTransGen.refl
+
+public theorem head {a b c} (hab : Beta a b) (hbc : BetaStar b c) :
+    BetaStar a c :=
+  Relation.ReflTransGen.head hab hbc
+
+public theorem tail {a b c} (hab : BetaStar a b) (hbc : Beta b c) :
+    BetaStar a c :=
+  Relation.ReflTransGen.tail hab hbc
+
+public theorem trans {a b c}
+    (hab : BetaStar a b) (hbc : BetaStar b c) :
+    BetaStar a c :=
+  Relation.ReflTransGen.trans hab hbc
+
+public theorem appL {t t' u : Term} (h : BetaStar t t') :
+    BetaStar (t·u) (t'·u) := by
+  induction h with
+  | refl => exact BetaStar.refl (t·u)
+  | tail hab hbc ih => exact BetaStar.tail ih (Beta.appL hbc)
+
+public theorem appR {t u u' : Term} (h : BetaStar u u') :
+    BetaStar (t·u) (t·u') := by
+  induction h with
+  | refl => exact BetaStar.refl (t·u)
+  | tail hab hbc ih => exact BetaStar.tail ih (Beta.appR hbc)
+
+public theorem app {t t' u u'}
+    (ht : BetaStar t t')
+    (hu : BetaStar u u') :
+    BetaStar (t·u) (t'·u') := by
+  induction ht with
+  | refl => exact BetaStar.appR hu
+  | tail hab hbc ih => exact BetaStar.tail ih (Beta.appL hbc)
+
+public theorem abs {t t' : Term} (h : BetaStar t t') :
+    BetaStar (λ.t) (λ.t') := by
+  induction h with
+  | refl => exact BetaStar.refl (λ.t)
+  | tail hab hbc ih => exact BetaStar.tail ih (Beta.abs hbc)
+
+end BetaStar
+end Lambda

Cslib/Languages/LambdaCalculus/Unscoped/Untyped/ChurchRosser.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 zayn7lie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Zayn Wang
+-/
+module
+
+public import Cslib.Foundations.Data.Relation
+public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.ParallelReduction
+
+/-!
+# The Church–Rosser theorem for β-reduction
+
+This file proves confluence of β-reduction on de Bruijn lambda terms.  The proof follows
+the classical route:
+
+1. define parallel β-reduction,
+2. show that parallel reduction has the diamond property using complete developments,
+3. compare parallel reduction with ordinary β-reduction via reflexive-transitive closure,
+4. transport confluence back to β-reduction.
+
+## Main results
+
+* `diamond_par`: parallel reduction is diamond.
+* `churchRosser_beta`: β-reduction is confluent.
+
+## Implementation note
+
+The proof relies on the generic rewriting lemmas from `ConfluentReduction` together with
+the complete-development machinery from `ParallelReduction`.
+-/
+
+namespace Lambda
+open Relation
+
+/-- Parallel Reduction is Diamond. -/
+private lemma diamond_par : Diamond Par := by
+  intro a b c hab hac
+  exact ⟨a.dev, par_to_dev hab, par_to_dev hac⟩
+
+/-- Church–Rosser: β is confluent (on RTC). -/
+public theorem churchRosser_beta : Confluent Beta := by
+  -- Confluence of Par from diamond
+  have hPar : Confluent Par :=
+    Diamond.toConfluent (r := Par) diamond_par
+  -- Identify BetaStar and ParStar via sandwich
+  have hEq {a b : Term} : BetaStar a b ↔ ParStar a b :=
+      ReflTransGen.sandwich_to_eq (r := Beta) (p := Par)
+    (by intro a b h; exact beta_subset_par h)
+    (by intro a b h; exact par_subset_betaStar h)
+  -- Transport confluence
+  intro a b c hab hac
+  have hab' : ParStar a b := (hEq).1 hab
+  have hac' : ParStar a c := (hEq).1 hac
+  rcases hPar hab' hac' with ⟨d, hbd, hcd⟩
+  exact ⟨d, (hEq).2 hbd, (hEq).2 hcd⟩
+
+end Lambda