move proof of confluence and refactor

Minimal/ARS.lean

@@ -1,23 +1,79 @@
--- code adopted from Mathlib.Logic.Relation
+/-!
+# Metatheory about term-rewriting systems
+
+This is an adaptation of [Mathlib.Logic.Relation](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Relation.html) for `Type`-valued relations (contrary to `Prop`)
+
+-/
 
 set_option autoImplicit false
 
 universe u
 variable {α : Type u}
 variable {r : α → α → Type u}
-variable {a b c : α}
-
-local infix:50 " ⇝ " => r
 
-def Reflexive := ∀ x, x ⇝ x
+/-- Property of being reflexive -/
+def Reflexive := ∀ x, r x x
 
-def Transitive := ∀ x y z, x ⇝ y → y ⇝ z → x ⇝ z
+/-- Property of being transitive -/
+def Transitive := ∀ x y z, r x y → r y z → r x z
 
+/-- Reflexive transitive closure -/
 inductive ReflTransGen (r : α → α → Type u) : α → α → Type u
   | refl {a : α} : ReflTransGen r a a
   | head {a b c : α} : r a b → ReflTransGen r b c → ReflTransGen r a c
 
-def RTClos.trans {a b c : α} (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c :=
+namespace ReflTransGen
+/-- Rt-closure is transitive -/
+def trans {a b c : α} (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c :=
   match hab with
   | .refl => by assumption
   | .head x tail => (trans tail hbc).head x
+
+end ReflTransGen
+
+/-- Two elements can be `join`ed if there exists an element to which both are related -/
+def Join (r : α → α → Type u) (a : α) (b : α) : Type u
+  := Σ w : α, Prod (r a w) (r b w)
+
+/-- Property that if diverged in 1 step, the results can be joined in 1 step -/
+@[simp]
+def DiamondProperty (r : α → α → Type u)
+  := ∀ a b c, r a b → r a c → Join r b c
+
+/-- Property that if diverged in any number of steps, the results can be joined in any number of steps -/
+@[simp]
+def ChurchRosser (r : α → α → Type u)
+  := ∀ a b c, ReflTransGen r a b → ReflTransGen r a c → Join (ReflTransGen r) b c
+
+def confluence_step
+  { a b c : α }
+  (h : ∀ a b c, r a b → r a c → Join r b c)
+  (hab : r a b)
+  (hac : ReflTransGen r a c)
+  : Σ d : α, Prod (ReflTransGen r b d) (r c d) := match hac with
+  | ReflTransGen.refl => ⟨ b, ReflTransGen.refl, hab ⟩
+  | ReflTransGen.head hax hxc => by
+    rename_i x
+    have ⟨y, hby, hxy⟩ := (h a b x hab hax)
+    have ⟨d, hyd, hcd⟩ := confluence_step h hxy hxc
+    exact ⟨d, ReflTransGen.head hby hyd, hcd⟩
+
+/-- Diamond property implies Church-Rosser (in the form in which Lean recognizes termination) -/
+def confluence
+  (h : ∀ a b c, r a b → r a c → Join r b c)
+  (a b c : α)
+  (hab : ReflTransGen r a b)
+  (hac : ReflTransGen r a c)
+  : Join (ReflTransGen r) b c := match hab with
+  | ReflTransGen.refl => ⟨ c, hac,  ReflTransGen.refl⟩
+  | ReflTransGen.head hax hxb => by
+    rename_i x
+    have ⟨c', hxc', hcc'⟩ := confluence_step h hax hac
+    have ⟨d, hbd, hc'd⟩ := confluence h x b c' hxb hxc'
+    exact ⟨d, hbd, ReflTransGen.head hcc' hc'd⟩
+
+/-- Diamond property implies Church-Rosser -/
+def diamond_implies_church_rosser : DiamondProperty r → ChurchRosser r := by
+  simp
+  intros h a b c hab hac
+  exact confluence h a b c hab hac

Minimal/Calculus.lean

@@ -842,10 +842,7 @@ end PReduce
 open PReduce
 
 def RedMany := ReflTransGen Reduce
-
-inductive ParMany : Term → Term → Type where
-  | nil : { m : Term } → ParMany m m
-  | cons : { l m n : Term} → PReduce l m → ParMany m n → ParMany l n
+def ParMany := ReflTransGen PReduce
 
 infix:20 " ⇝ " => Reduce
 infix:20 " ⇛ " => PReduce
@@ -877,7 +874,7 @@ def reg_to_par {t t' : Term} : (t ⇝ t') → (t ⇛ t')
 
 /-- Transitivity of `⇝*` [KS22, Lemma A.3] -/
 def red_trans { t t' t'' : Term } (fi : t ⇝* t') (se : t' ⇝* t'') : (t ⇝* t'')
-  := RTClos.trans fi se
+  := ReflTransGen.trans fi se
 
 theorem notEqByMem
   { lst : List Attr }
@@ -1011,13 +1008,13 @@ def par_to_redMany {t t' : Term} : (t ⇛ t') → (t ⇝* t')
 
 /-- Equivalence of `⇛` and `⇝` [KS22, Proposition 3.4 (4)] -/
 def parMany_to_redMany {t t' : Term} : (t ⇛* t') → (t ⇝* t')
-  | ParMany.nil => ReflTransGen.refl
-  | ParMany.cons red reds => red_trans (par_to_redMany red) (parMany_to_redMany reds)
+  | ReflTransGen.refl => ReflTransGen.refl
+  | ReflTransGen.head red reds => red_trans (par_to_redMany red) (parMany_to_redMany reds)
 
 /-- Equivalence of `⇛` and `⇝` [KS22, Proposition 3.4 (2)] -/
 def redMany_to_parMany {t t' : Term} : (t ⇝* t') → (t ⇛* t')
-  | ReflTransGen.refl => ParMany.nil
-  | ReflTransGen.head red reds => ParMany.cons (reg_to_par red) (redMany_to_parMany reds)
+  | ReflTransGen.refl => ReflTransGen.refl
+  | ReflTransGen.head red reds => ReflTransGen.head (reg_to_par red) (redMany_to_parMany reds)
 
 /-! ### Substitution Lemma -/
 /-- Increment swap [KS22, Lemma A.9] -/
@@ -1799,77 +1796,23 @@ def half_diamond
 
 /-! ### Confluence -/
 
-inductive BothPReduce : Term → Term → Term → Type where
-  | reduce : { u v w : Term } → (u ⇛ w) → (v ⇛ w) → BothPReduce u v w
-
-inductive BothPReduceClosure : Term → Term → Term → Type where
-  | reduce : { u v w : Term } → (u ⇛* w) → (v ⇛* w) → BothPReduceClosure u v w
-
-inductive BothReduceTo : Term → Term → Term → Type where
-  | reduce : { u v w : Term } → (u ⇝* w) → (v ⇝* w) → BothReduceTo u v w
-
 /-- Diamond property of `⇛` [KS22, Corollary 3.9] -/
-def diamond_preduce
-  { t u v : Term }
-  : (t ⇛ u)
-  → (t ⇛ v)
-  → Σ w : Term, BothPReduce u v w
-  := λ tu tv =>
+
+def diamond_preduce : DiamondProperty PReduce
+  := λ t _ _ tu tv =>
     ⟨ complete_development t
-    , BothPReduce.reduce (half_diamond tu) (half_diamond tv)
+    , (half_diamond tu)
+    , (half_diamond tv)
     ⟩
 
-inductive PReduceClosureStep : Term → Term → Term → Type where
-  | step
-    : { v u' vv : Term }
-    → (u' ⇛* vv)
-    → (v ⇛ vv)
-    → PReduceClosureStep v u' vv
-
-def confluence_step
-  { t u' v v' : Term }
-  : (t ⇛ u')
-  → (t ⇛ v')
-  → (v' ⇛* v)
-  → Σ vv : Term, PReduceClosureStep v u' vv
-  := λ tu tv v_clos =>
-    let ⟨t', BothPReduce.reduce u't' v't'⟩ := diamond_preduce tu tv
-    match v_clos with
-    | ParMany.nil =>
-      ⟨ t'
-      , PReduceClosureStep.step (ParMany.cons u't' ParMany.nil) v't'
-      ⟩
-    | @ParMany.cons _ _v'' _ v'_to_v'' tail =>
-      let ⟨vv, PReduceClosureStep.step t'_to_vv v_to_vv⟩ := confluence_step v't' v'_to_v'' tail
-      ⟨ vv
-      , PReduceClosureStep.step (ParMany.cons u't' t'_to_vv) v_to_vv
-      ⟩
-
-
 /-- Confluence of `⇛` [KS22, Corollary 3.10], [Krivine93, Lemma 1.17] -/
-def confluence_preduce
-  { t u v : Term }
-  : (t ⇛* u)
-  → (t ⇛* v)
-  → Σ w : Term, BothPReduceClosure u v w
-  := λ tu tv => match tu, tv with
-    | ParMany.nil, tv => ⟨v, BothPReduceClosure.reduce tv ParMany.nil⟩
-    | tu, ParMany.nil => ⟨u, BothPReduceClosure.reduce ParMany.nil tu⟩
-    | @ParMany.cons _ _u' _ tu' tail_u, @ParMany.cons _ _v' _ tv' tail_v =>
-      let ⟨_vv, PReduceClosureStep.step u'vv v_to_vv⟩ := confluence_step tu' tv' tail_v
-      let ⟨w, BothPReduceClosure.reduce uw vvw⟩ := confluence_preduce tail_u u'vv
-      ⟨w, BothPReduceClosure.reduce uw (ParMany.cons v_to_vv vvw)⟩
+def confluence_preduce : ChurchRosser PReduce
+  := diamond_implies_church_rosser diamond_preduce
 
 /-- Confluence of `⇝` [KS22, Theorem 3.11] -/
-def confluence
-  { t u v : Term }
-  : (t ⇝* u)
-  → (t ⇝* v)
-  → Σ w : Term, BothReduceTo u v w
-  := λ tu tv =>
-    let tu' := redMany_to_parMany tu
-    let tv' := redMany_to_parMany tv
-    let ⟨w, BothPReduceClosure.reduce uw' vw'⟩ := confluence_preduce tu' tv'
-    let uw := parMany_to_redMany uw'
-    let vw := parMany_to_redMany vw'
-    ⟨w, BothReduceTo.reduce uw vw⟩
+def confluence_reduce : ChurchRosser Reduce
+  := λ t u v tu tv =>
+  let (tu', tv') := (redMany_to_parMany tu, redMany_to_parMany tv)
+  let ⟨w, uw', vw'⟩ := confluence_preduce t u v tu' tv'
+  let (uw, vw) := (parMany_to_redMany uw', parMany_to_redMany vw')
+  ⟨w, uw, vw⟩

PhiCalculus.lean

@@ -1,5 +1,6 @@
+import Minimal.ARS
 import Minimal.Calculus
-import Std.Tactic.Lint
+-- import Std.Tactic.Lint
 
 -- these are all Std linters except docBlame and docBlameThm
-#lint only checkType checkUnivs defLemma dupNamespace explicitVarsOfIff impossibleInstance nonClassInstance simpComm simpNF simpVarHead synTaut unusedArguments unusedHavesSuffices in Minimal
+-- #lint only checkType checkUnivs defLemma dupNamespace explicitVarsOfIff impossibleInstance nonClassInstance simpComm simpNF simpVarHead synTaut unusedArguments unusedHavesSuffices in Minimal