From 71f92ad52ea5c41875d77d13e7db45a6af89f927 Mon Sep 17 00:00:00 2001
From: Anatolay <nihonvasserman228@gmail.com>
Date: Mon, 5 Aug 2024 22:36:02 +0300
Subject: [PATCH 1/3] Add Z property for confluence to the ARS module

---
 Minimal/ARS.lean | 81 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 81 insertions(+)

diff --git a/Minimal/ARS.lean b/Minimal/ARS.lean
index 3161451c..6632a44a 100644
--- a/Minimal/ARS.lean
+++ b/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,79 @@ 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
+
+def 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 _ tail => by
+      simp [ReflTransGen.size]
+      let h : tail.size < 1 + tail.size := Nat.lt_add_of_pos_left Nat.zero_lt_one
+      exact Nat.add_lt_add_left h 1
+
+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 (a_b, a_c) with
+    | (.refl, _) => ⟨c, a_c, .refl⟩
+    | (_, .refl) => ⟨b, .refl, a_b⟩
+    | (.head au u_b, .head as s_c) =>
+      -- TODO: I have no idea how to prove it
+      let eq : a_b = ReflTransGen.head au u_b := sorry
+      let u_fc := step au a_c z
+      let ⟨w, b_w, fc_w⟩ := z_confluence z u_b u_fc
+      ⟨w, b_w, ReflTransGen.trans (aux as s_c z) fc_w⟩
+termination_by a_b.size
+decreasing_by
+  all_goals simp_wf
+  let proof := decr au u_b
+  -- let eq : a_b = ReflTransGen.head au u_b := sorry
+  simp [←eq] at proof
+  exact proof
+
+def z_implies_confluence
+  (z : ZProperty r)
+  : Confluence r
+  := λ _ _ _ ab ac => z_confluence z ab ac

From 43d30e87f50d0c28b4214657bcff0479ad71e053 Mon Sep 17 00:00:00 2001
From: eyihluyc <theviolthevioletandthewine@gmail.com>
Date: Tue, 13 Aug 2024 16:08:42 -0400
Subject: [PATCH 2/3] Remove sorry from the `z_confluence`

---
 Minimal/ARS.lean | 29 +++++++++++++++--------------
 1 file changed, 15 insertions(+), 14 deletions(-)

diff --git a/Minimal/ARS.lean b/Minimal/ARS.lean
index 6632a44a..aeb9c3ac 100644
--- a/Minimal/ARS.lean
+++ b/Minimal/ARS.lean
@@ -167,22 +167,23 @@ def z_confluence
   (a_b : ReflTransGen r a b)
   (a_c : ReflTransGen r a c)
   : Join (ReflTransGen r) b c
-  := match (a_b, a_c) with
-    | (.refl, _) => ⟨c, a_c, .refl⟩
-    | (_, .refl) => ⟨b, .refl, a_b⟩
-    | (.head au u_b, .head as s_c) =>
-      -- TODO: I have no idea how to prove it
-      let eq : a_b = ReflTransGen.head au u_b := sorry
-      let u_fc := step au a_c z
-      let ⟨w, b_w, fc_w⟩ := z_confluence z u_b u_fc
-      ⟨w, b_w, ReflTransGen.trans (aux as s_c z) fc_w⟩
+  := 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
-  all_goals simp_wf
-  let proof := decr au u_b
-  -- let eq : a_b = ReflTransGen.head au u_b := sorry
-  simp [←eq] at proof
-  exact proof
+  simp_wf
+  rename_i as' s_c' _ _ _ _
+  exact decr as' s_c'
 
 def z_implies_confluence
   (z : ZProperty r)

From 48b39ae19caf937c585a7d3158073bea77a608be Mon Sep 17 00:00:00 2001
From: eyihluyc <theviolthevioletandthewine@gmail.com>
Date: Tue, 13 Aug 2024 17:07:22 -0400
Subject: [PATCH 3/3] Update toolchain

---
 Minimal/ARS.lean   |  6 ++---
 lake-manifest.json | 57 +++++++++++++++++++++++++++-------------------
 lean-toolchain     |  2 +-
 3 files changed, 37 insertions(+), 28 deletions(-)

diff --git a/Minimal/ARS.lean b/Minimal/ARS.lean
index aeb9c3ac..ca410211 100644
--- a/Minimal/ARS.lean
+++ b/Minimal/ARS.lean
@@ -152,14 +152,12 @@ def step
      let b_fa  := (z.snd ab).fst
      ReflTransGen.trans b_fa fa_fc
 
-def decr {a b c} (ab : r a b) (b_c : ReflTransGen r b c)
+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 _ tail => by
+  | .head _ _ => by
       simp [ReflTransGen.size]
-      let h : tail.size < 1 + tail.size := Nat.lt_add_of_pos_left Nat.zero_lt_one
-      exact Nat.add_lt_add_left h 1
 
 def z_confluence
   (z : ZProperty r)
diff --git a/lake-manifest.json b/lake-manifest.json
index 410e1a9b..c45de755 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,11 +1,12 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/xubaiw/CMark.lean",
+ [{"url": "https://github.com/acmepjz/md4lean",
    "type": "git",
    "subDir": null,
-   "rev": "ba7b47bd773954b912ecbf5b1c9993c71a166f05",
-   "name": "CMark",
+   "scope": "",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
+   "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -13,34 +14,38 @@
   {"url": "https://github.com/fgdorais/lean4-unicode-basic",
    "type": "git",
    "subDir": null,
-   "rev": "8b53cc65534bc2c6888c3d4c53a3439648213f74",
+   "scope": "",
+   "rev": "5c11428272fe190b7e726ebe448f93437d057b74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/mhuisi/lean4-cli",
+  {"url": "https://github.com/dupuisf/BibtexQuery",
    "type": "git",
    "subDir": null,
-   "rev": "10d88b52fa8d717fa8e29af3abf0c3a2bf175497",
-   "name": "Cli",
+   "scope": "",
+   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
+  {"url": "https://github.com/mhuisi/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "f1f904e00d79a91ca6a76dec6e318531a7fd2a0f",
-   "name": "leanInk",
+   "scope": "",
+   "rev": "bf066c328bcff19aa93adf4d24c4e896c0d4eaca",
+   "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
+   "inputRev": "nightly",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
-   "rev": "2756f6603c992f133c1157bfc07ab11b5a7a6738",
+   "scope": "",
+   "rev": "114aabc6f0f8d117eb1a853c0dc1591126d9c559",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,7 +54,8 @@
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "56d2e4ee226603eb6b90b05f6b944bde42672cd5",
+   "scope": "",
+   "rev": "1d25ec7ec98d6d9fb526c997aa014bcabbad8b72",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,7 +64,8 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "scope": "leanprover-community",
+   "rev": "71f54425e6fe0fa75f3aef33a2813a7898392222",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -67,7 +74,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
+   "scope": "leanprover-community",
+   "rev": "776a5a8f9c789395796e442d78a9d4cb9c4c9d03",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -76,16 +84,18 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "scope": "leanprover-community",
+   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.41",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
+   "scope": "leanprover-community",
+   "rev": "57bd2065f1dbea5e9235646fb836c7cea9ab03b6",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -94,7 +104,8 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "5e843131cccdc65039f2037be5b2a7ea75a3ae9b",
+   "scope": "",
+   "rev": "d7ada26614c81bc1ac3c8135fadb4494e1019bec",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
diff --git a/lean-toolchain b/lean-toolchain
index d8a6d7ef..e7a4f40b 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc1
+leanprover/lean4:v4.11.0-rc2