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,15 @@ 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₁ : r ≤ p)
+    (h₂ : p ≤ ReflTransGen r) :
+    ReflTransGen r = ReflTransGen p := by
+  refine le_antisymm (fun _ _ => ReflTransGen.mono h₁) ?_
+  rw [← Relation.reflTransGen_eq_self (r := ReflTransGen r)]
+  exact fun _ _ ↦ ReflTransGen.mono h₂
+
 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,64 @@
+/-
+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 (Star)
+
+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.
+
+## Main lemmas
+
+Inside `namespace BetaStar` we provide the standard constructors and congruence lemmas:
+
+* `BetaStar.appL`, `BetaStar.appR`, `BetaStar.app`, `BetaStar.abs`
+
+These lemmas are used later to compare β-reduction with parallel reduction.
+-/
+
+@[expose] public section
+
+namespace Cslib.LambdaCalculus.Unscoped.Untyped
+
+open Term
+
+open Relation.ReflTransGen
+
+/-- One-step β-reduction (compatible closure). -/
+@[reduction_sys "β"]
+inductive Beta : Term → Term → Prop
+  | abs  {t t'}        : Beta t t' → Beta (abs t) (abs t')
+  | appL {t t' u}      : Beta t t' → Beta (app t u) (app t' u)
+  | appR {t u u'}      : Beta u u' → Beta (app t u) (app t u')
+  | red  (t' s : Term) : Beta (app (abs t') s) (t'.sub 0 s)
+
+namespace BetaStar
+
+theorem appL {t t' u : Term} (h : t ↠β t') :
+    (app t u) ↠β (app t' u) := h.lift (app · u) (fun _ _ => .appL)
+
+theorem appR {t u u' : Term} (h : u ↠β u') :
+    (app t u) ↠β (app t u') := h.lift (app t ·) (fun _ _ => .appR)
+
+theorem app {t t' u u'}
+    (ht : t ↠β t') (hu : u ↠β u') :
+    (app t u) ↠β (app t' u') := (appL ht).trans (appR hu) 
+
+theorem abs {t t' : Term} (h : t ↠β t') :
+    (abs t) ↠β (abs t') := h.lift Term.abs (fun _ _ => Beta.abs)
+
+end BetaStar
+
+end Cslib.LambdaCalculus.Unscoped.Untyped

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

@@ -0,0 +1,63 @@
+/-
+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`.
+-/
+
+@[expose] public section
+
+namespace Cslib.LambdaCalculus.Unscoped.Untyped
+
+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). -/
+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} : a ↠β b ↔ a ↠∥ b := by
+    have hRel : ReflTransGen Beta = ReflTransGen Par :=
+      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)
+    simp only [hRel] 
+  -- Transport confluence
+  intro a b c hab hac
+  have hab' : a ↠∥ b := (hEq).1 hab
+  have hac' : a ↠∥ c := (hEq).1 hac
+  rcases hPar hab' hac' with ⟨d, hbd, hcd⟩
+  exact ⟨d, (hEq).2 hbd, (hEq).2 hcd⟩
+
+end Cslib.LambdaCalculus.Unscoped.Untyped