add equational.lean as generated by Claude code

analysis/Analysis/Misc/equational.lean

@@ -0,0 +1,178 @@
+import Mathlib.Tactic
+
+/-
+A informal proof of the theorem `singleton_law` is provided below.  Claude Code was used to formalize this proof using the following steps:
+
+Step 0: Formalize the `S` and `f` notation.
+
+Step 1: First make Lean formalizations of the *statements* of Lemma 1, Lemma 2 and Lemma 3, but leave the proofs as sorries.  Restructure the existing informal proof so that the statement and proof of each lemma is moved to be near the formal statement of that lemma, expressed as a comment.  Use the `S` and `f` notation as needed to align the formal statements with the informal statements.
+
+Step 2a: Create a high-level skeleton for the proof of Lemma 1 by expressing each step of the informal proof as an appropriate Lean statement with justifications given as a sorry (e.g., a step might become a `have` statement that is given by a sorry).  At this stage of the process, do *not* try to justify the entire proof, and accept each step of the informal proof is valid (other than fixing any minor typos or inaccuracies).  If there is a step which is confusing, replace it with an appropriate sorry and let me know what the issue is, rather than spend a lot of time trying to understand it.  Again, take advantage of the `S` and `f` notation as needed to make the formalization match the informal proof as closely as possible.
+
+Step 2b: Assuming no major issues were encountered in Step 2a, fill in all the sorries in the proof of Lemma 1.
+
+Step 3a: Repeat Step 2a for the proof of Lemma 2.
+
+Step 3b: Repeat Step 2b for the proof of Lemma 2.
+
+Step 4a: Repeat Step 2a for the proof of Lemma 3.
+
+Step 4b: Repeat Step 2b for the proof of Lemma 3.
+
+Step 5a: Repeat Step 2a for the final part of the proof of `singleton_law` after Lemma 3.
+
+Step 5b: Repeat Step 2b for the final part of the proof of `singleton_law` after Lemma 3.
+
+-/
+
+
+class Magma (α : Type _) where
+  op : α → α → α
+
+infix:65 " ◇ " => Magma.op
+
+abbrev Equation1689 (M: Type _) [Magma M] := ∀ x y z : M, x = (y ◇ x) ◇ ((x ◇ z) ◇ z)
+
+abbrev Equation2 (M: Type _) [Magma M] := ∀ x y : M, x = y
+
+variable {M : Type _} [Magma M]
+
+-- Step 0: S and f notation
+-- S z x = (x ◇ z) ◇ z  (written S_z(x) in the informal proof)
+def S (z x : M) : M := (x ◇ z) ◇ z
+
+-- f x y = x ◇ S y x = x ◇ ((x ◇ y) ◇ y)  (written f(x,y) in the informal proof)
+def f (x y : M) : M := x ◇ S y x
+
+/-
+The main equation (Equation1689) is: x = (y ◇ x) ◇ S z x, i.e., x = (y ◇ x) ◇ S z x.
+We denote S_z(x) = S z x = (x ◇ z) ◇ z and f(x,y) = f x y = x ◇ S y x = x ◇ ((x ◇ y) ◇ y).
+-/
+
+-- Auxiliary lemma used in Lemma 1 and Lemma 2:
+-- S b a lies in the left ideal of a, i.e., S b a = a ◇ S z (S b a) for any z.
+lemma S_left_ideal (h : Equation1689 M) (a b z : M) : S b a = a ◇ S z (S b a) := by
+  simp only [S]
+  have key : (a ◇ a) ◇ ((a ◇ b) ◇ b) = a := (h a a b).symm
+  have step := h ((a ◇ b) ◇ b) (a ◇ a) z
+  rw [key] at step
+  exact step
+
+/-
+**Lemma 1:** For any a, b, c, one has S_b(a) = a ◇ f(b,c),  i.e., S b a = a ◇ f b c.
+
+*Proof:* For x = S b a and y ∈ Ma we have y ◇ x = a.  Then apply the main equation to these
+values of x, y to get
+  S b a = a ◇ S z (S b a).
+Then set z = S c b and note that (S b a) ◇ z = ((a ◇ b) ◇ b) ◇ ((b ◇ c) ◇ c) = b to simplify
+the right-hand side above and get, as announced,
+  S b a = a ◇ ((S b a ◇ z) ◇ z) = a ◇ (b ◇ z) = a ◇ f b c.
+-/
+lemma lemma1 (h : Equation1689 M) (a b c : M) : S b a = a ◇ f b c := by
+  have h1 : ∀ z : M, S b a = a ◇ S z (S b a) := S_left_ideal h a b
+  -- The main equation with x = b, y = a ◇ b, z = c gives b = ((a◇b)◇b) ◇ ((b◇c)◇c) = S b a ◇ S c b.
+  have h2 : S b a ◇ S c b = b := by
+    simp only [S]
+    exact (h b (a ◇ b) c).symm
+  -- Therefore S (S c b) (S b a) = (S b a ◇ S c b) ◇ S c b = b ◇ S c b = f b c.
+  have h3 : S (S c b) (S b a) = f b c := by
+    simp only [S, f]
+    simp only [S] at h2
+    rw [h2]
+  -- Combine: S b a = a ◇ S (S c b) (S b a) = a ◇ f b c.
+  calc S b a = a ◇ S (S c b) (S b a) := h1 (S c b)
+    _ = a ◇ f b c := by rw [h3]
+
+/-
+**Lemma 2:** For all a there exist b, c, d such that f(b,c) = S_d(a),  i.e., f b c = S d a.
+
+*Proof:* By definition of f one has f b c = b ◇ S c b.  Taking b = S x a for some x, and
+rewriting b = a ◇ S c b using the first equation in the proof of Lemma 1, we find
+  f b c = (a ◇ S c b) ◇ S c b,
+which has the desired form for d = S c b.  (Thus, the statement actually holds for all a, c.)
+-/
+lemma lemma2 (h : Equation1689 M) (a : M) : ∃ b c d : M, f b c = S d a := by
+  -- Take b := S a a (= S_a(a)), c := a, d := S a (S a a) (= S c b).
+  -- The proof works for all a, c; any x works for b = S x a.
+  refine ⟨S a a, a, S a (S a a), ?_⟩
+  -- From the same argument as the first equation in the proof of Lemma 1 (with b := a, z := a):
+  --   b = S a a = a ◇ S a (S a a) = a ◇ S c b.
+  have hb : S a a = a ◇ S a (S a a) := S_left_ideal h a a a
+  -- f b c = b ◇ S c b = (a ◇ S c b) ◇ S c b = S (S c b) a = S d a.
+  calc f (S a a) a
+      = S a a ◇ S a (S a a)              := rfl
+    _ = (a ◇ S a (S a a)) ◇ S a (S a a) := by congr
+    _ = S (S a (S a a)) a               := rfl
+
+/-
+**Lemma 3:** For all a there exists e such that S_e(a) = a,  i.e., S e a = a.
+
+*Proof:* Left-multiply the equation in Lemma 1 by a³ = (a ◇ a) ◇ a to get (the first equality
+below comes from the main equation)
+  a = ((a ◇ a) ◇ a) ◇ S b a = a³ ◇ (a ◇ f b c).
+Take b, c, d as in Lemma 2 to rewrite a ◇ f b c = a ◇ S d a = f a d.  On the other hand,
+Lemma 1 with a = b and c replaced by d implies a³ = a ◇ f a d, so overall we get
+  a = (a ◇ f a d) ◇ f a d,
+which is as desired for e = f a d.
+-/
+lemma lemma3 (h : Equation1689 M) (a : M) : ∃ e : M, S e a = a := by
+  -- Get b, c, d from Lemma 2, so that f b c = S d a.
+  obtain ⟨b, c, d, hd⟩ := lemma2 h a
+  -- Take e := f a d.
+  refine ⟨f a d, ?_⟩
+  -- The main equation with x = a, y = a ◇ a, z = b gives a = ((a ◇ a) ◇ a) ◇ S b a.
+  have h_main : a = ((a ◇ a) ◇ a) ◇ S b a := by
+    simp only [S]; exact h a (a ◇ a) b
+  -- Lemma 1 gives S b a = a ◇ f b c, so a = ((a ◇ a) ◇ a) ◇ (a ◇ f b c).
+  have h_step2 : a = ((a ◇ a) ◇ a) ◇ (a ◇ f b c) :=
+    h_main.trans (by rw [lemma1 h a b c])
+  -- Since f b c = S d a by hd, a ◇ f b c = a ◇ S d a = f a d.
+  have h_step3 : a ◇ f b c = f a d := by rw [hd]; rfl
+  -- Lemma 1 with b←a, c←d gives S a a = a ◇ f a d, i.e., (a ◇ a) ◇ a = a ◇ f a d.
+  have h_step4 : (a ◇ a) ◇ a = a ◇ f a d := by
+    simpa only [S] using lemma1 h a a d
+  -- Combine: S(f a d) a = (a ◇ f a d) ◇ f a d = ((a ◇ a) ◇ a) ◇ f a d
+  --        = ((a ◇ a) ◇ a) ◇ (a ◇ f b c) = ((a ◇ a) ◇ a) ◇ S b a = a.
+  calc S (f a d) a
+      = (a ◇ f a d) ◇ f a d          := rfl
+    _ = ((a ◇ a) ◇ a) ◇ f a d       := by rw [← h_step4]
+    _ = ((a ◇ a) ◇ a) ◇ (a ◇ f b c) := by rw [← h_step3]
+    _ = ((a ◇ a) ◇ a) ◇ S b a       := by rw [← lemma1 h a b c]
+    _ = a                            := h_main.symm
+
+/-
+*End of the proof:* For any a, y, using e from Lemma 3, the main equation gives
+  a = (y ◇ a) ◇ S e a = (y ◇ a) ◇ a = S a y.
+Inserting this back into the main equation gives (z ◇ y) ◇ a = y for any a, y, z.
+Thus a ◇ b = ((d ◇ a) ◇ c) ◇ b = c for any a, b, c, d, thus a = b ◇ c = d for any a, b, c, d.
+-/
+theorem singleton_law (h : Equation1689 M) : Equation2 M := by
+  -- Step 1: S a b = a for all a, b.
+  -- Lemma 3 gives e with S e a = a; main eq (x=a, z=e) gives a = (y ◇ a) ◇ S e a = (y ◇ a) ◇ a = S a y.
+  have hS : ∀ a b : M, S a b = a := by
+    intro a b
+    obtain ⟨e, he⟩ := lemma3 h a
+    simp only [S]
+    have step := h a b e
+    simp only [S] at he
+    rw [he] at step
+    exact step.symm
+  -- Step 2: (a ◇ b) ◇ c = b for all a, b, c.
+  -- Main eq (x=b, y=a, z=c) gives b = (a ◇ b) ◇ S c b = (a ◇ b) ◇ c by hS.
+  have hrel : ∀ a b c : M, (a ◇ b) ◇ c = b := by
+    intro a b c
+    have step := h b a c
+    have hSraw : (b ◇ c) ◇ c = c := by simpa only [S] using hS c b
+    rw [hSraw] at step
+    exact step.symm
+  -- Step 3: a ◇ b = c for all a, b, c.
+  -- From hrel: (d ◇ a) ◇ c = a, so a ◇ b = ((d ◇ a) ◇ c) ◇ b = c by hrel.
+  have hconst : ∀ a b c : M, a ◇ b = c := by
+    intro a b c
+    have h1 : (a ◇ a) ◇ c = a := hrel a a c
+    have h2 : ((a ◇ a) ◇ c) ◇ b = c := hrel (a ◇ a) c b
+    calc a ◇ b = ((a ◇ a) ◇ c) ◇ b := by rw [h1]
+      _ = c := h2
+  -- Conclude: x = x ◇ x = y.
+  intro x y
+  exact (hconst x x x).symm.trans (hconst x x y)