Merge pull request #29 from objectionary/refactor-church-rosser

Refactor ARS

Author: fizruk

Minimal/ARS.lean

@@ -42,38 +42,37 @@ def DiamondProperty (r : α → α → Type u)
 
 /-- 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)
+def Confluence (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
+def diamond_implies_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
+    let rec 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⟩ := step h hxy hxc
+      exact ⟨d, ReflTransGen.head hby hyd, hcd⟩
     rename_i x
-    have ⟨c', hxc', hcc'⟩ := confluence_step h hax hac
-    have ⟨d, hbd, hc'd⟩ := confluence h x b c' hxb hxc'
+    have ⟨c', hxc', hcc'⟩ := step h hax hac
+    have ⟨d, hbd, hc'd⟩ := diamond_implies_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
+def diamond_implies_confluence : DiamondProperty r → Confluence r := by
   simp
   intros h a b c hab hac
-  exact confluence h a b c hab hac
+  exact diamond_implies_confluence' h a b c hab hac

Minimal/Calculus.lean

@@ -1806,11 +1806,11 @@ def diamond_preduce : DiamondProperty PReduce
     ⟩
 
 /-- Confluence of `⇛` [KS22, Corollary 3.10], [Krivine93, Lemma 1.17] -/
-def confluence_preduce : ChurchRosser PReduce
-  := diamond_implies_church_rosser diamond_preduce
+def confluence_preduce : Confluence PReduce
+  := diamond_implies_confluence diamond_preduce
 
 /-- Confluence of `⇝` [KS22, Theorem 3.11] -/
-def confluence_reduce : ChurchRosser Reduce
+def confluence_reduce : Confluence 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'

lake-manifest.json

@@ -49,7 +49,7 @@
   {"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "d77f6535a34bc65bd00cf6b2e8e7c1edf5ad960b",
+   "rev": "1fa3d92b9aff636c2b64e55c2baf06e3783530ae",
    "name": "std",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",