upd: clean up ConfluentReduction.lean to Cslib.Foundations.Data.Relation, and add rtc_eq_of_sandwich

Author: zayn7lie

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/ChurchRosser.lean

@@ -5,7 +5,7 @@ Authors: Zayn Wang
 -/
 module
 
-public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.ConfluentReduction
+public import Cslib.Foundations.Data.Relation
 public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.ParallelReduction
 
 /-!
@@ -31,7 +31,7 @@ the complete-development machinery from `ParallelReduction`.
 -/
 
 namespace Lambda
-open Term
+open Relation
 
 /-- Parallel Reduction is Diamond. -/
 private lemma diamond_par : Diamond Par := by
@@ -42,10 +42,10 @@ private lemma diamond_par : Diamond Par := by
 public theorem churchRosser_beta : Confluent Beta := by
   -- Confluence of Par from diamond
   have hPar : Confluent Par :=
-    confluent_of_diamond (r := Par) diamond_par
+    Diamond.toConfluent (r := Par) diamond_par
   -- Identify BetaStar and ParStar via sandwich
   have hEq {a b : Term} : BetaStar a b ↔ ParStar a b :=
-      rtc_eq_of_sandwich (r := Beta) (p := 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)
   -- Transport confluence