Remove sorry from z-confluence

Minimal/ARS.lean

@@ -156,33 +156,32 @@ 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
+  | .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)
   {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⟩
+  := 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)

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": "ad26fe1ebccc9d5b7ca9111d5daf9b4488374415",
    "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": "173d2e189fd79bd332fb19bffac0dce43ec8acb8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

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