Unicidad de inversos en monoides
Demostrar con Lean4 que si \(M\) es un monoide conmutativo y \(x, y, z ∈ M\) tales que \(x·y = 1\) y \(x·z = 1\), entonces \(y = z\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [CommMonoid M] variable {x y z : M} example (hy : x * y = 1) (hz : x * z = 1) : y = z := by sorry |
1. Demostración en lenguaje natural
Por la siguiente cadena de igualdades
\begin{align}
y &= 1·y &&\text{[por neutro a la izquierda]} \\
&= (x·z)·y &&\text{[por hipótesis]} \\
&= (z·x)·y &&\text{[por la conmutativa]} \\
&= z·(x·y) &&\text{[por la asociativa]} \\
&= z·1 &&\text{[por hipótesis]} \\
&= z &&\text{[por neutro a la derecha]}
\end{align}
2. Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 |
import Mathlib.Algebra.Group.Basic variable {M : Type} [CommMonoid M] variable {x y z : M} -- 1ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y := (one_mul y).symm _ = (x * z) * y := congrArg (. * y) hz.symm _ = (z * x) * y := congrArg (. * y) (mul_comm x z) _ = z * (x * y) := mul_assoc z x y _ = z * 1 := congrArg (z * .) hy _ = z := mul_one z -- 2ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y := by simp only [one_mul] _ = (x * z) * y := by simp only [hz] _ = (z * x) * y := by simp only [mul_comm] _ = z * (x * y) := by simp only [mul_assoc] _ = z * 1 := by simp only [hy] _ = z := by simp only [mul_one] -- 3ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := calc y = 1 * y := by simp _ = (x * z) * y := by simp [hz] _ = (z * x) * y := by simp [mul_comm] _ = z * (x * y) := by simp [mul_assoc] _ = z * 1 := by simp [hy] _ = z := by simp -- 4ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := by apply left_inv_eq_right_inv _ hz -- ⊢ y * x = 1 rw [mul_comm] -- ⊢ x * y = 1 exact hy -- 5ª demostración -- =============== example (hy : x * y = 1) (hz : x * z = 1) : y = z := inv_unique hy hz -- Lemas usados -- ============ -- #check (inv_unique : x * y = 1 → x * z = 1 → y = z) -- #check (left_inv_eq_right_inv : y * x = 1 → x * z = 1 → y = z) -- #check (mul_assoc x y z : (x * y) * z = x * (y * z)) -- #check (mul_comm x y : x * y = y * x) -- #check (mul_one x : x * 1 = x) -- #check (one_mul x : 1 * x = x) |
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
3. Demostraciones con Isabelle/HOL
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 |
theory Unicidad_de_inversos_en_monoides imports Main begin context comm_monoid begin (* 1ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" proof - have "y = 1 * y" by (simp only: left_neutral) also have "… = (x * z) * y" by (simp only: ‹x * z = 1›) also have "… = (z * x) * y" by (simp only: commute) also have "… = z * (x * y)" by (simp only: assoc) also have "… = z * 1" by (simp only: ‹x * y = 1›) also have "… = z" by (simp only: right_neutral) finally show "y = z" by this qed (* 2ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" proof - have "y = 1 * y" by simp also have "… = (x * z) * y" using assms(2) by simp also have "… = (z * x) * y" by simp also have "… = z * (x * y)" by simp also have "… = z * 1" using assms(1) by simp also have "… = z" by simp finally show "y = z" by this qed (* 3ª demostración *) lemma assumes "x * y = 1" "x * z = 1" shows "y = z" using assms by auto end end |
