fix: notation typeclass for substitution

Author: zayn7lie

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

@@ -9,7 +9,7 @@ public import Cslib.Languages.LambdaCalculus.Unscoped.Untyped.DeBruijnSyntax
 public import Cslib.Foundations.Data.Relation
 
 /-!
-# One-step β-reduction and its reflexive-transitive closure
+# 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
@@ -18,25 +18,20 @@ 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`
+* `BetaStar.appL`, `BetaStar.appR`, `BetaStar.app`, `BetaStar.abs`
 
 These lemmas are used later to compare β-reduction with parallel reduction.
 -/
 
 
 namespace Lambda
 open Term
+open Relation.ReflTransGen
 
 /-- One-step β-reduction (compatible closure). -/
 @[reduction_sys "β"]
@@ -45,51 +40,33 @@ public inductive Beta : Term → Term → Prop
   | 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
+public theorem appL {t t' u : Term} (h : t ↠β t') :
+    (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)
+  | refl => exact refl (t·u)
+  | tail hab hbc ih => exact tail ih (Beta.appL hbc)
 
-public theorem appR {t u u' : Term} (h : BetaStar u u') :
-    BetaStar (t·u) (t·u') := by
+public theorem appR {t u u' : Term} (h : u ↠β u') :
+    (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)
+  | refl => exact refl (t·u)
+  | tail hab hbc ih => exact 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
+    (ht : t ↠β t') (hu : u ↠β u') :
+    (t·u) ↠β (t'·u') := by
   induction ht with
-  | refl => exact BetaStar.appR hu
-  | tail hab hbc ih => exact BetaStar.tail ih (Beta.appL hbc)
+  | refl => exact appR hu
+  | tail hab hbc ih => exact tail ih (Beta.appL hbc)
 
-public theorem abs {t t' : Term} (h : BetaStar t t') :
-    BetaStar (λ.t) (λ.t') := by
+public theorem abs {t t' : Term} (h : t ↠β t') :
+    (λ.t) ↠β (λ.t') := by
   induction h with
-  | refl => exact BetaStar.refl (λ.t)
-  | tail hab hbc ih => exact BetaStar.tail ih (Beta.abs hbc)
+  | refl => exact refl (λ.t)
+  | tail hab hbc ih => exact tail ih (Beta.abs hbc)
 
 end BetaStar
 end Lambda

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

@@ -44,14 +44,14 @@ public theorem churchRosser_beta : Confluent Beta := by
   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 :=
+  have hEq {a b : Term} : a ↠β b ↔ 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
+  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⟩
 

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

@@ -80,11 +80,13 @@ infixl:77 "·" => Term.app
   | 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) := decre 1 n (subst n (incre 1 n s) t)
+@[expose] public def sub (t : Term) (n : Nat) (s : Term) := 
+  decre 1 n (subst n (incre 1 n s) t)
 
-@[expose] public instance : 
-    Cslib.HasSubstitution Term Nat Term where
-  subst t n s := t.sub n s
+/-- Notation typeclass for substitution, t[n := s] ≃ t.sub n s 
+    which substitute nth variable in t with s. -/
+@[expose] public instance : Cslib.HasSubstitution Term Nat Term 
+  where subst := sub
 
 /-- Increment of 0 is identity -/
 @[simp] public theorem incre_rfl {l t} : incre 0 l t = t := by
@@ -95,7 +97,8 @@ infixl:77 "·" => Term.app
 
 /-- Decrement of increment with same bound is the same.
 Lemma for `var_sub` -/
-@[simp] public theorem decre_incre_elim {l t} : decre 1 l (incre 1 l t) = t := by
+@[simp] public theorem decre_incre_elim {l t} : 
+    decre 1 l (incre 1 l t) = t := by
   induction t generalizing l with
   | var k =>
       unfold decre incre

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

@@ -51,35 +51,35 @@ public inductive Par : Term → Term → Prop
 public abbrev ParStar := Relation.ReflTransGen Par
 
 /-- reflexivity of Par. -/
-@[simp] public theorem par_refl {t} : Par t t := by
+@[simp] public theorem par_refl {t} : t ⭢∥ t := by
   induction t with
   | var n => exact Par.var n
   | app t u iht ihu => exact Par.app iht ihu
   | abs t iht => exact Par.abs iht
 
 /-- `Beta ⊆ Par`. -/
-public theorem beta_subset_par {a b} (h : Beta a b) : Par a b := by
+public theorem beta_subset_par {a b} (h : a ⭢β b) : a ⭢∥ b := by
   induction h with
   | appL h ih => exact Par.app ih par_refl
   | appR h ih => exact Par.app par_refl ih
   | abs h ih  => exact Par.abs ih
   | red t s  => exact Par.red par_refl par_refl
 
 /-- Simulation lemma: `Par ⊆ BetaStar`. -/
-public theorem par_subset_betaStar {a b} (h : Par a b) :
-    BetaStar a b := by
+public theorem par_subset_betaStar {a b} (h : a ⭢∥ b) :
+    a ↠β b := by
   induction h with
-  | var n => exact BetaStar.refl (𝕧 n)
+  | var n => exact refl (𝕧 n)
   | app hpt hpu hbt hbu =>
-      exact BetaStar.trans
+      exact .trans
               (BetaStar.appL hbt) (BetaStar.appR hbu)
   | abs h ht => exact BetaStar.abs ht
   | red ht hs iht ihs =>
-      exact BetaStar.trans (BetaStar.appL (BetaStar.abs iht))
-        (BetaStar.tail (BetaStar.appR ihs) (Beta.red _ _))
+      exact .trans (BetaStar.appL (BetaStar.abs iht))
+        (.tail (BetaStar.appR ihs) (Beta.red _ _))
 
-@[simp] public theorem incre_par {a b i l} (h : Par a b) :
-    Par (incre i l a) (incre i l b) := by
+@[simp] public theorem incre_par {a b i l} (h : a ⭢∥ b) :
+    (incre i l a) ⭢∥ (incre i l b) := by
   induction h generalizing l with
   | var n => exact par_refl
   | abs ht ih => exact Par.abs ih
@@ -95,9 +95,9 @@ public theorem par_subset_betaStar {a b} (h : Par a b) :
       exact Par.red iht ihs
 
 /-- Substitution lemma for `par_to_dev`. -/
-private lemma par_subst {t t' u u'} (ht : Par t t') (hu : Par u u')
+private lemma par_subst {t t' u u'} (ht : t ⭢∥ t') (hu : u ⭢∥ u')
   (k : Nat) (n : Nat) :
-    Par (t.sub n (incre k 0 u)) (t'.sub n (incre k 0 u')) := by
+    (t.sub n (incre k 0 u)) ⭢∥ (t'.sub n (incre k 0 u')) := by
   match t, t' with
   | var t, var t' => match ht with
       | Par.var t => cases em (t = n) with
@@ -146,7 +146,7 @@ public def Term.dev : Term → Term
   | t·u     => t.dev·u.dev
 
 /-- t.dev is a par reduction for t. -/
-public theorem par_dev (t : Term) : Par t t.dev :=
+public theorem par_dev (t : Term) : t ⭢∥ t.dev :=
   match t with
   | 𝕧 n     => Par.var n
   | λ.t     => Par.abs (par_dev t)
@@ -157,7 +157,7 @@ public theorem par_dev (t : Term) : Par t t.dev :=
       | app t₁ t₂ => Par.app (par_dev (t₁·t₂)) (par_dev u)
 
 /-- t.dev is max par reduction for t. -/
-public theorem par_to_dev {t u} (h : Par t u) : Par u (t.dev) := by
+public theorem par_to_dev {t u} (h : t ⭢∥ u) : u ⭢∥ (t.dev) := by
   match t, u with
   | var t', var u' =>
       match h with | Par.var t' => exact Par.var t'