feat: add several definitions and theorems about reduction systems

Cslib/Foundations/Semantics/ReductionSystem/Basic.lean

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi, Thomas Waring
 -/
 
+import Cslib.Foundations.Data.Relation
 import Cslib.Init
 import Mathlib.Logic.Relation
+import Mathlib.Order.WellFounded
 import Mathlib.Util.Notation3
 
 /-!
@@ -26,26 +28,208 @@ structure ReductionSystem (Term : Type u) where
   Red : Term → Term → Prop
 
 
+variable {Term : Type u} (rs : ReductionSystem Term)
+
 section MultiStep
 
 /-! ## Multi-step reductions -/
 
 /-- Multi-step reduction relation. -/
-abbrev ReductionSystem.MRed (rs : ReductionSystem Term) :=
+abbrev ReductionSystem.MRed :=
   Relation.ReflTransGen rs.Red
 
 /-- All multi-step reduction relations are reflexive. -/
 @[refl]
-theorem ReductionSystem.MRed.refl (rs : ReductionSystem Term) (t : Term) : rs.MRed t t :=
+theorem ReductionSystem.MRed.refl (t : Term) : rs.MRed t t :=
   Relation.ReflTransGen.refl
 
 /-- Any reduction is a multi-step -/
-theorem ReductionSystem.MRed.single (rs : ReductionSystem Term) (h : rs.Red a b) :
+theorem ReductionSystem.MRed.single {a b : Term} (h : rs.Red a b) :
   rs.MRed a b :=
   Relation.ReflTransGen.single h
 
+theorem ReductionSystem.MRed.step {a b c : Term} (hab : rs.MRed a b) (hbc : rs.Red b c) :
+    rs.MRed a c :=
+  Relation.ReflTransGen.tail hab hbc
+
+theorem ReductionSystem.MRed.trans {a b c : Term} (hab : rs.MRed a b) (hbc : rs.MRed b c) :
+    rs.MRed a c :=
+  Relation.ReflTransGen.trans hab hbc
+
+theorem ReductionSystem.MRed.cases_iff {a b : Term} :
+    rs.MRed a b ↔ b = a ∨ ∃ c : Term, rs.MRed a c ∧ rs.Red c b :=
+  Relation.ReflTransGen.cases_tail_iff rs.Red a b
+
+@[induction_eliminator]
+private theorem ReductionSystem.MRed.induction_on {motive : ∀ {x y}, rs.MRed x y → Prop}
+    (refl : ∀ t : Term, motive (MRed.refl rs t))
+    (step : ∀ (a b c : Term) (hab : rs.MRed a b) (hbc : rs.Red b c), motive hab →
+      motive (MRed.step rs hab hbc))
+    {a b : Term} (h : rs.MRed a b) : motive h := by
+  induction h with
+  | refl => exact refl a
+  | @tail c d hac hcd ih => exact step a c d hac hcd ih
+
 end MultiStep
 
+
+section Reverse
+
+/-- Reverse reduction relation -/
+def ReductionSystem.RRed : Term → Term → Prop :=
+  Function.swap rs.Red
+
+theorem ReductionSystem.single {a b : Term} (h : rs.Red a b) : rs.RRed b a := h
+
+end Reverse
+
+section Equivalence
+
+/-- Equivalence closure relation -/
+def ReductionSystem.Equiv : Term → Term → Prop := Relation.EqvGen rs.Red
+
+theorem ReductionSystem.Equiv.refl (t : Term) : rs.Equiv t t :=
+  Relation.EqvGen.refl t
+
+theorem ReductionSystem.Equiv.single {a b : Term} (h : rs.Red a b) : rs.Equiv a b :=
+  Relation.EqvGen.rel a b h
+
+theorem ReductionSystem.Equiv.symm {a b : Term} (h : rs.Equiv a b) : rs.Equiv b a :=
+  Relation.EqvGen.symm a b h
+
+theorem ReductionSystem.Equiv.trans {a b c : Term} (h₁ : rs.Equiv a b) (h₂ : rs.Equiv b c) :
+    rs.Equiv a c :=
+  Relation.EqvGen.trans a b c h₁ h₂
+
+theorem ReductionSystem.Equiv.ofMRed {a b : Term} (h : rs.MRed a b) : rs.Equiv a b := by
+  induction h with
+  | refl t => exact refl rs t
+  | step a b c hab hbc ih => apply Equiv.trans rs ih (single rs hbc)
+
+@[induction_eliminator]
+private theorem ReductionSystem.Equiv.induction_on {motive : ∀ {x y}, rs.Equiv x y → Prop}
+    (rel : ∀ (a b : Term) (hab : rs.Red a b), motive (Equiv.single rs hab))
+    (refl : ∀ t : Term, motive (Equiv.refl rs t))
+    (symm : ∀ (a b : Term) (hab : rs.Equiv a b), motive hab → motive (Equiv.symm rs hab))
+    (trans : ∀ (a b c : Term) (hab : rs.Equiv a b) (hbc : rs.Equiv b c), motive hab → motive hbc →
+      motive (Equiv.trans rs hab hbc))
+    {a b : Term} (h : rs.Equiv a b) : motive h := by
+  induction h with
+  | rel a b hab => exact rel a b hab
+  | refl t => exact refl t
+  | symm a b hab ih => exact symm a b hab ih
+  | trans a b c hab hbc ih₁ ih₂ => exact trans a b c hab hbc ih₁ ih₂
+
+end Equivalence
+
+section Join
+
+/-- Join relation -/
+def ReductionSystem.Join : Term → Term → Prop :=
+  Relation.Join rs.Red
+
+theorem ReductionSystem.Join_def {a b : Term} :
+    rs.Join a b ↔ ∃ c : Term, rs.Red a c ∧ rs.Red b c := by rfl
+
+theorem ReductionSystem.Join.symm : Symmetric rs.Join := Relation.symmetric_join
+
+end Join
+
+section MJoin
+
+/-- Multi-step join relation -/
+def ReductionSystem.MJoin : Term → Term → Prop :=
+  Relation.Join rs.MRed
+
+theorem ReductionSystem.MJoin_def {a b : Term} :
+    rs.MJoin a b ↔ ∃ c : Term, rs.MRed a c ∧ rs.MRed b c := by rfl
+
+theorem ReductionSystem.MJoin.refl (t : Term) : rs.MJoin t t := by
+  use t
+
+theorem ReductionSystem.MJoin.symm : Symmetric rs.MJoin := Relation.symmetric_join
+
+end MJoin
+
+/-- A reduction system has de diamond property when all one-step reduction pairs with a common
+origin are joinable -/
+def ReductionSystem.isDiamond : Prop :=
+  Cslib.Diamond rs.Red
+
+theorem ReductionSystem.isDiamond_def : rs.isDiamond ↔
+    ∀ {a b c : Term}, rs.Red a b → rs.Red a c → rs.Join b c :=
+  Iff.rfl
+
+/-- A reduction system is confluent when all multi-step reduction pairs with a common origin are
+multi-step joinable -/
+def ReductionSystem.isConfluent : Prop :=
+  Cslib.Confluence rs.Red
+
+theorem ReductionSystem.isConfluent_def : rs.isConfluent ↔
+    ∀ {a b c : Term}, rs.MRed a b → rs.MRed a c → rs.MJoin b c :=
+  Iff.rfl
+
+/-- A reduction system is Church-Rosser when all equivalent terms are multi-step joinable -/
+def ReductionSystem.isChurchRosser : Prop :=
+  ∀ a b : Term, rs.Equiv a b → rs.MJoin a b
+
+/-- A term is reducible when there exists a one-step reduction from it. -/
+def ReductionSystem.isReducible (t : Term) : Prop :=
+  ∃ t', rs.Red t t'
+
+/-- A term is in normal form when it is not reducible. -/
+def ReductionSystem.isNormalForm (t : Term) : Prop :=
+  ¬ rs.isReducible t
+
+/-- A reduction system is normalizing when every term reduces to at least one normal form. -/
+def ReductionSystem.isNormalizing : Prop :=
+  ∀ t : Term, ∃ n : Term, rs.MRed t n ∧ rs.isNormalForm n
+
+/-- A reduction system is terminating when there are no infinite sequences of one-step reductions.
+-/
+def ReductionSystem.isTerminating : Prop :=
+  ¬ ∃ f : ℕ → Term, ∀ n : ℕ, rs.Red (f n) (f (n + 1))
+
+theorem ReductionSystem.isConfluent_iff_isChurchRosser :
+    rs.isConfluent ↔ rs.isChurchRosser := by
+  apply Iff.intro
+  · intro h _ _ hab
+    rw [MJoin_def]
+    induction hab with
+    | rel a b hab =>
+      exact ⟨b, MRed.single rs hab, MRed.refl rs b⟩
+    | refl t =>
+      use t
+    | symm a b hab ih =>
+      obtain ⟨c, hac, hbc⟩ := ih
+      exact ⟨c, hbc, hac⟩
+    | trans a b c hab hbc ih₁ ih₂ =>
+      obtain ⟨d, hbd, hcd⟩ := ih₂
+      obtain ⟨e, hae, hbe⟩ := ih₁
+      obtain ⟨f, hdf, hef⟩ := (isConfluent_def rs).mp h hbd hbe
+      exact ⟨f, MRed.trans rs hae hef, MRed.trans rs hcd hdf⟩
+  · intro h
+    rw [rs.isConfluent_def]
+    intro a b c hab hac
+    exact h b c (Equiv.trans rs (Equiv.symm rs (Equiv.ofMRed rs hab)) (Equiv.ofMRed rs hac))
+
+theorem ReductionSystem.isTerminating_iff_WellFounded : rs.isTerminating ↔ WellFounded rs.RRed := by
+  unfold isTerminating RRed Function.swap
+  rw [wellFounded_iff_isEmpty_descending_chain, not_iff_comm, not_isEmpty_iff, nonempty_subtype]
+
+theorem ReductionSystem.isNormalizing_of_isTerminating (h : rs.isTerminating) :
+    rs.isNormalizing := by
+  rw [isTerminating_iff_WellFounded] at h
+  intro t
+  apply WellFounded.induction h t
+  intro a ih
+  by_cases ha : rs.isReducible a
+  · obtain ⟨b, hab⟩ := ha
+    obtain ⟨n, hbn, hn⟩ := ih b hab
+    exact ⟨n, MRed.trans rs (MRed.single rs hab) hbn, hn⟩
+  · unfold isNormalForm
+    use a
+
 open Lean Elab Meta Command Term
 
 -- thank you to Kyle Miller for this:

Cslib/Languages/CombinatoryLogic/Defs.lean

@@ -98,16 +98,16 @@ theorem MRed.I (x : SKI) : (I ⬝ x) ↠ x := MRed.single RedSKI <| red_I ..
 theorem MRed.head {a a' : SKI} (b : SKI) (h : a ↠ a') : (a ⬝ b) ↠ (a' ⬝ b) := by
   induction h with
   | refl => apply MRed.refl
-  | @tail a' a'' _ ha'' ih =>
-    apply Relation.ReflTransGen.tail (b := a' ⬝ b) ih
-    exact Red.red_head a' a'' b ha''
+  | step a a' a'' _ ha' ih =>
+    apply MRed.step RedSKI ih
+    exact Red.red_head a' a'' b ha'
 
 theorem MRed.tail (a : SKI) {b b' : SKI} (h : b ↠ b') : (a ⬝ b) ↠ (a ⬝ b') := by
   induction h with
   | refl => apply MRed.refl
-  | @tail b' b'' _ hb'' ih =>
-    apply Relation.ReflTransGen.tail (b := a ⬝ b') ih
-    exact Red.red_tail a b' b'' hb''
+  | step b b' b'' _ hb' ih =>
+    apply MRed.step RedSKI ih
+    exact Red.red_tail a b' b'' hb'
 
 lemma parallel_mRed {a a' b b' : SKI} (ha : a ↠ a') (hb : b ↠ b') :
     (a ⬝ b) ↠ (a' ⬝ b') :=

Cslib/Languages/LambdaCalculus/LocallyNameless/Untyped/FullBeta.lean

@@ -60,14 +60,17 @@ lemma step_lc_l (step : M ⭢βᶠ M') : LC M := by
 theorem redex_app_l_cong (redex : M ↠βᶠ M') (lc_N : LC N) : app M N ↠βᶠ app M' N := by
   induction redex
   case refl => rfl
-  case tail ih r => exact Relation.ReflTransGen.tail r (appR lc_N ih)
+  case step a b c hab hbc ih =>
+    have := appR lc_N hbc
+
+    exact ReductionSystem.MRed.step fullBetaRs ih this
 
 /-- Right congruence rule for application in multiple reduction. -/
 @[scoped grind ←]
 theorem redex_app_r_cong (redex : M ↠βᶠ M') (lc_N : LC N) : app N M ↠βᶠ app N M' := by
   induction redex
   case refl => rfl
-  case tail ih r => exact Relation.ReflTransGen.tail r (appL lc_N ih)
+  case step ih r => exact Relation.ReflTransGen.tail r (appL lc_N ih)
 
 variable [HasFresh Var] [DecidableEq Var]
 
@@ -102,7 +105,7 @@ lemma redex_abs_close {x : Var} (step : M ↠βᶠ M') : (M⟦0 ↜ x⟧.abs ↠
   induction step using Relation.ReflTransGen.trans_induction_on
   case refl => rfl
   case single ih => exact Relation.ReflTransGen.single (step_abs_close ih)
-  case trans l r => exact .trans l r
+  case trans l r => exact Relation.ReflTransGen.trans l r
 
 /-- Multiple reduction of opening implies multiple reduction of abstraction. -/
 theorem redex_abs_cong (xs : Finset Var) (cofin : ∀ x ∉ xs, (M ^ fvar x) ↠βᶠ (M' ^ fvar x)) :