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:
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]} \newline &= (x·z)·y &&\text{[por hipótesis]} \newline &= (z·x)·y &&\text{[por la conmutativa]} \newline &= z·(x·y) &&\text{[por la asociativa]} \newline &= z·1 &&\text{[por hipótesis]} \newline &= z &&\text{[por neutro a la derecha]} \end{align}
2. Demostraciones con Lean4
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
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