Merge pull request #46 from objectionary/z-property

Add Z-property to ARS

Minimal/ARS.lean

@@ -33,6 +33,11 @@ def trans {a b c : α} (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : R
   | .refl => by assumption
   | .head x tail => (trans tail hbc).head x
 
+def size {a b : α} (hab : ReflTransGen r a b) : Nat
+  := match hab with
+    | .refl => 0
+    | .head _ tail => 1 + size tail
+
 end ReflTransGen
 
 /-- Two elements can be `join`ed if there exists an element to which both are related -/
@@ -107,3 +112,78 @@ def weak_equiv_keeps_confluence
     let r1ac := r2_to_r1 r2ac
     let ⟨w, r1bw, r1cw⟩ := conf a b c r1ab r1ac
     ⟨w, r1_to_r2 r1bw, r1_to_r2 r1cw⟩
+
+
+@[simp]
+def ZProperty (r : α → α → Type u)
+  := Σ f : α → α, ∀ {a b}, r a b → ReflTransGen r b (f a) × ReflTransGen r (f a) (f b)
+
+
+def lift_f
+  {a b : α}
+  (ab : ReflTransGen r a b)
+  (z : ZProperty r)
+  : ReflTransGen r (z.fst a) (z.fst b)
+  := match ab with
+    | .refl => .refl
+    | @ReflTransGen.head _ _ _ _u _ au ub =>
+      let ⟨_, fa_fu⟩ := z.snd au
+      let fu_fb := lift_f ub z
+      ReflTransGen.trans fa_fu fu_fb
+
+def aux
+  {a b u : α}
+  (au : r a u)
+  (u_b : ReflTransGen r u b)
+  (z : ZProperty r)
+  : ReflTransGen r b (z.fst b)
+  := match u_b with
+    | .refl => let ⟨u_fa, fa_fu⟩ := z.snd au; ReflTransGen.trans u_fa fa_fu
+    | @ReflTransGen.head _ _ _ _s _ as sb =>
+      aux as sb z
+
+def step
+  {a b c : α}
+  (ab : r a b)
+  (ac : ReflTransGen r a c)
+  (z : ZProperty r)
+  : ReflTransGen r b (z.fst c)
+  := let fa_fc := lift_f ac z
+     let b_fa  := (z.snd ab).fst
+     ReflTransGen.trans b_fa fa_fc
+
+theorem decr {a b c} (ab : r a b) (b_c : ReflTransGen r b c)
+  : b_c.size < (ReflTransGen.head ab b_c).size
+  := match b_c with
+  | .refl => by simp [ReflTransGen.size]
+  | .head _ _ => by
+      simp [ReflTransGen.size]
+
+def z_confluence
+  (z : ZProperty r)
+  {a b c : α}
+  (a_b : ReflTransGen r a b)
+  (a_c : ReflTransGen r a c)
+  : Join (ReflTransGen r) b c
+  := match hab : a_b with
+    | .refl => ⟨c, a_c, .refl⟩
+    | .head au u_b => match hac : a_c with
+      | .refl => by
+        rename_i hb _
+        exact ⟨b, .refl, hb ▸ a_b⟩
+      | .head as s_c =>
+        let u_fc := step au a_c z
+        let ⟨w, b_w, fc_w⟩ := z_confluence z u_b u_fc
+        by
+        rename_i hc
+        exact ⟨w, b_w, ReflTransGen.trans (aux as s_c z) (hc ▸ fc_w)⟩
+termination_by a_b.size
+decreasing_by
+  simp_wf
+  rename_i as' s_c' _ _ _ _
+  exact decr as' s_c'
+
+def z_implies_confluence
+  (z : ZProperty r)
+  : Confluence r
+  := λ _ _ _ ab ac => z_confluence z ab ac

lake-manifest.json

@@ -1,11 +1,61 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "dc167d260ff7ee9849b436037add06bed15104be",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
+   "name": "MD4Lean",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5c11428272fe190b7e726ebe448f93437d057b74",
+   "name": "UnicodeBasic",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/mhuisi/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bf066c328bcff19aa93adf4d24c4e896c0d4eaca",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "nightly",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/doc-gen4",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "114aabc6f0f8d117eb1a853c0dc1591126d9c559",
+   "name": "«doc-gen4»",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "1d25ec7ec98d6d9fb526c997aa014bcabbad8b72",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ae6ea60e9d8bc2d4b37ff02115854da2e1b710d0",
+   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -41,21 +91,11 @@
    "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/lean4-cli",
-   "type": "git",
-   "subDir": null,
-   "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
-   "name": "Cli",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68cd8ae0f5b996176d1243d94c56e17de570e3bf",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "780b09c212da1d3a59b84d431f8c5565fb4b1555",
+   "rev": "d7ada26614c81bc1ac3c8135fadb4494e1019bec",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc1
+leanprover/lean4:v4.11.0-rc2