La semana en Calculemus (11 de mayo de 2024)
Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:
- 1. Producto de potencias de la misma base en monoides
- 2. Equivalencia de inversos iguales al neutro
- 3. Unicidad de inversos en monoides
- 4. Caracterización de producto igual al primer factor
- 5. Unicidad del elemento neutro en los grupos
A continuación se muestran las soluciones.
1. Producto de potencias de la misma base en monoides
En los monoides se define la potencia con exponentes naturales. En Lean la potencia x^n se se caracteriza por los siguientes lemas:
pow_zero : x^0 = 1 pow_succ : x^(succ n) = x * x^n
Demostrar con Lean4 que si \(M\) es un monoide, \(x ∈ M\) y \(m, n ∈ ℕ\), entonces \[ x^{m + n} = x^m x^n \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Defs import Mathlib.Algebra.GroupPower.Basic open Nat variable {M : Type} [Monoid M] variable (x : M) variable (m n : ℕ) example : x^(m + n) = x^m * x^n := by sorry
1.1. Demostración en lenguaje natural
Por inducción en \(m\).
Base: \begin{align} x^{0 + n} &= x^n \newline &= 1 · x^n \newline &= x^0 · x^n &&\text{[por pow_zero]} \end{align}
Paso: Supongamos que \[ x^{m + n} = x^m x^n \tag{HI} \] Entonces \begin{align} x^{(m+1) + n} &= x^{(m + n) + 1} \newline &= x · x^{m + n} &&\text{[por pow_succ]} \newline &= x · (x^m · x^n) &&\text{[por HI]} \newline &= (x · x^m) · x^n \newline &= x^{m+1} · x^n &&\text{[por pow_succ]} \end{align}
1.2. Demostraciones con Lean4
import Mathlib.Algebra.Group.Defs import Mathlib.Algebra.GroupPower.Basic open Nat variable {M : Type} [Monoid M] variable (x : M) variable (m n : ℕ) -- 1ª demostración -- =============== example : x^(m + n) = x^m * x^n := by induction' m with m HI . calc x^(0 + n) = x^n := congrArg (x ^ .) (Nat.zero_add n) _ = 1 * x^n := (Monoid.one_mul (x^n)).symm _ = x^0 * x^n := congrArg (. * (x^n)) (pow_zero x).symm . calc x^(succ m + n) = x^succ (m + n) := congrArg (x ^.) (succ_add m n) _ = x * x^(m + n) := pow_succ x (m + n) _ = x * (x^m * x^n) := congrArg (x * .) HI _ = (x * x^m) * x^n := (mul_assoc x (x^m) (x^n)).symm _ = x^succ m * x^n := congrArg (. * x^n) (pow_succ x m).symm -- 2ª demostración -- =============== example : x^(m + n) = x^m * x^n := by induction' m with m HI . calc x^(0 + n) = x^n := by simp only [Nat.zero_add] _ = 1 * x^n := by simp only [Monoid.one_mul] _ = x^0 * x^n := by simp only [_root_.pow_zero] . calc x^(succ m + n) = x^succ (m + n) := by simp only [succ_add] _ = x * x^(m + n) := by simp only [_root_.pow_succ] _ = x * (x^m * x^n) := by simp only [HI] _ = (x * x^m) * x^n := (mul_assoc x (x^m) (x^n)).symm _ = x^succ m * x^n := by simp only [_root_.pow_succ] -- 3ª demostración -- =============== example : x^(m + n) = x^m * x^n := by induction' m with m HI . calc x^(0 + n) = x^n := by simp [Nat.zero_add] _ = 1 * x^n := by simp _ = x^0 * x^n := by simp . calc x^(succ m + n) = x^succ (m + n) := by simp [succ_add] _ = x * x^(m + n) := by simp [_root_.pow_succ] _ = x * (x^m * x^n) := by simp [HI] _ = (x * x^m) * x^n := (mul_assoc x (x^m) (x^n)).symm _ = x^succ m * x^n := by simp [_root_.pow_succ] -- 4ª demostración -- =============== example : x^(m + n) = x^m * x^n := pow_add x m n -- Lemas usados -- ============ -- variable (y z : M) -- #check (Monoid.one_mul x : 1 * x = x) -- #check (Nat.zero_add n : 0 + n = n) -- #check (mul_assoc x y z : (x * y) * z = x * (y * z)) -- #check (pow_add x m n : x^(m + n) = x^m * x^n) -- #check (pow_succ x n : x ^ succ n = x * x ^ n) -- #check (pow_zero x : x ^ 0 = 1) -- #check (succ_add n m : succ n + m = succ (n + m))
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
1.3. Demostraciones con Isabelle/HOL
theory Producto_de_potencias_de_la_misma_base_en_monoides imports Main begin context monoid_mult begin (* 1ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" proof (induct m) have "x ^ (0 + n) = x ^ n" by (simp only: add_0) also have "… = 1 * x ^ n" by (simp only: mult_1_left) also have "… = x ^ 0 * x ^ n" by (simp only: power_0) finally show "x ^ (0 + n) = x ^ 0 * x ^ n" by this next fix m assume HI : "x ^ (m + n) = x ^ m * x ^ n" have "x ^ (Suc m + n) = x ^ Suc (m + n)" by (simp only: add_Suc) also have "… = x * x ^ (m + n)" by (simp only: power_Suc) also have "… = x * (x ^ m * x ^ n)" by (simp only: HI) also have "… = (x * x ^ m) * x ^ n" by (simp only: mult_assoc) also have "… = x ^ Suc m * x ^ n" by (simp only: power_Suc) finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n" by this qed (* 2ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" proof (induct m) have "x ^ (0 + n) = x ^ n" by simp also have "… = 1 * x ^ n" by simp also have "… = x ^ 0 * x ^ n" by simp finally show "x ^ (0 + n) = x ^ 0 * x ^ n" by this next fix m assume HI : "x ^ (m + n) = x ^ m * x ^ n" have "x ^ (Suc m + n) = x ^ Suc (m + n)" by simp also have "… = x * x ^ (m + n)" by simp also have "… = x * (x ^ m * x ^ n)" using HI by simp also have "… = (x * x ^ m) * x ^ n" by (simp add: mult_assoc) also have "… = x ^ Suc m * x ^ n" by simp finally show "x ^ (Suc m + n) = x ^ Suc m * x ^ n" by this qed (* 3ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" proof (induct m) case 0 then show ?case by simp next case (Suc m) then show ?case by (simp add: algebra_simps) qed (* 4ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" by (induct m) (simp_all add: algebra_simps) (* 5ª demostración *) lemma "x ^ (m + n) = x ^ m * x ^ n" by (simp only: power_add) end end
2. Equivalencia de inversos iguales al neutro
Sea \(M\) un monoide y \(a, b ∈ M\) tales que \(ab = 1\). Demostrar con Lean4 que \(a = 1\) si y sólo si \(b = 1\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] variable {a b : M} example (h : a * b = 1) : a = 1 ↔ b = 1 := by sorry
2.1. Demostración en lenguaje natural
Demostraremos las dos implicaciones.
(⟹) Supongamos que \(a = 1\). Entonces, \begin{align} b &= 1·b &&\text{[por neutro por la izquierda]} \newline &= a·b &&\text{[por supuesto]} \newline &= 1 &&\text{[por hipótesis]} \end{align}
(⟸) Supongamos que \(b = 1\). Entonces, \begin{align} a &= a·1 &&\text{[por neutro por la derecha]} \newline &= a·b &&\text{[por supuesto]} \newline &= 1 &&\text{[por hipótesis]} \end{align}
2.2. Demostraciones con Lean4
import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] variable {a b : M} -- 1ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := by constructor . -- ⊢ a = 1 → b = 1 intro a1 -- a1 : a = 1 -- ⊢ b = 1 calc b = 1 * b := (one_mul b).symm _ = a * b := congrArg (. * b) a1.symm _ = 1 := h . -- ⊢ b = 1 → a = 1 intro b1 -- b1 : b = 1 -- ⊢ a = 1 calc a = a * 1 := (mul_one a).symm _ = a * b := congrArg (a * .) b1.symm _ = 1 := h -- 2ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := by constructor . -- ⊢ a = 1 → b = 1 intro a1 -- a1 : a = 1 -- ⊢ b = 1 rw [a1] at h -- h : 1 * b = 1 rw [one_mul] at h -- h : b = 1 exact h . -- ⊢ b = 1 → a = 1 intro b1 -- b1 : b = 1 -- ⊢ a = 1 rw [b1] at h -- h : a * 1 = 1 rw [mul_one] at h -- h : a = 1 exact h -- 3ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := by constructor . -- ⊢ a = 1 → b = 1 rintro rfl -- h : 1 * b = 1 simpa using h . -- ⊢ b = 1 → a = 1 rintro rfl -- h : a * 1 = 1 simpa using h -- 4ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := by constructor <;> (rintro rfl; simpa using h) -- 5ª demostración -- =============== example (h : a * b = 1) : a = 1 ↔ b = 1 := eq_one_iff_eq_one_of_mul_eq_one h -- Lemas usados -- ============ -- #check (eq_one_iff_eq_one_of_mul_eq_one : a * b = 1 → (a = 1 ↔ b = 1)) -- #check (mul_one a : a * 1 = a) -- #check (one_mul a : 1 * a = a)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
2.3. Demostraciones con Isabelle/HOL
theory Equivalencia_de_inversos_iguales_al_neutro imports Main begin context monoid begin (* 1ª demostración *) lemma assumes "a * b = 1" shows "a = 1 ⟷ b = 1" proof (rule iffI) assume "a = 1" have "b = 1 * b" by (simp only: left_neutral) also have "… = a * b" by (simp only: ‹a = 1›) also have "… = 1" by (simp only: ‹a * b = 1›) finally show "b = 1" by this next assume "b = 1" have "a = a * 1" by (simp only: right_neutral) also have "… = a * b" by (simp only: ‹b = 1›) also have "… = 1" by (simp only: ‹a * b = 1›) finally show "a = 1" by this qed (* 2ª demostración *) lemma assumes "a * b = 1" shows "a = 1 ⟷ b = 1" proof assume "a = 1" have "b = 1 * b" by simp also have "… = a * b" using ‹a = 1› by simp also have "… = 1" using ‹a * b = 1› by simp finally show "b = 1" . next assume "b = 1" have "a = a * 1" by simp also have "… = a * b" using ‹b = 1› by simp also have "… = 1" using ‹a * b = 1› by simp finally show "a = 1" . qed (* 3ª demostración *) lemma assumes "a * b = 1" shows "a = 1 ⟷ b = 1" by (metis assms left_neutral right_neutral) end end
3. 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
3.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}
3.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.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
4. Caracterización de producto igual al primer factor
Un monoide cancelativo por la izquierda es un monoide \(M\) que cumple la propiedad cancelativa por la izquierda; es decir, para todo \(a, b ∈ M\) \[ a·b = a·c ↔ b = c \]
En Lean4 la clase de los monoides cancelativos por la izquierda es LeftCancelMonoid y la propiedad cancelativa por la izquierda es
mul_left_cancel : a * b = a * c → b = c
Demostrar con Lean4 que si \(M\) es un monoide cancelativo por la izquierda y \(a, b ∈ M\), entonces \[ a·b = a ↔ b = 1 \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Basic variable {M : Type} [LeftCancelMonoid M] variable {a b : M} example : a * b = a ↔ b = 1 := by sorry
4.1. Demostración en lenguaje natural
Demostraremos las dos implicaciones.
(⟹) Supongamos que \[ a·b = a \] Por la propiedad del neutro por la derecha tenemos \[ a·1 = a \] Por tanto, \[ a·b = a·1 \] y, por la propiedad cancelativa, \[ b = 1 \]
(⟸) Supongamos que \(b = 1\). Entonces, \begin{align} a·b &= a·1 \newline &= a &&\text{[por el neutro por la derecha]} \end{align}
4.2. Demostraciones con Lean4
import Mathlib.Algebra.Group.Basic variable {M : Type} [LeftCancelMonoid M] variable {a b : M} -- 1ª demostración -- =============== example : a * b = a ↔ b = 1 := by constructor . -- ⊢ a * b = a → b = 1 intro h -- h : a * b = a -- ⊢ b = 1 have h1 : a * b = a * 1 := by calc a * b = a := by exact h _ = a * 1 := (mul_one a).symm exact mul_left_cancel h1 . -- ⊢ b = 1 → a * b = a intro h -- h : b = 1 -- ⊢ a * b = a rw [h] -- ⊢ a * 1 = a exact mul_one a -- 2ª demostración -- =============== example : a * b = a ↔ b = 1 := calc a * b = a ↔ a * b = a * 1 := by rw [mul_one] _ ↔ b = 1 := mul_left_cancel_iff -- 3ª demostración -- =============== example : a * b = a ↔ b = 1 := mul_right_eq_self -- 4ª demostración -- =============== example : a * b = a ↔ b = 1 := by aesop -- Lemas usados -- ============ -- variable (c : M) -- #check (mul_left_cancel : a * b = a * c → b = c) -- #check (mul_one a : a * 1 = a) -- #check (mul_right_eq_self : a * b = a ↔ b = 1)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
4.3. Demostraciones con Isabelle/HOL
theory Caracterizacion_de_producto_igual_al_primer_factor imports Main begin context cancel_comm_monoid_add begin (* 1ª demostración *) lemma "a + b = a ⟷ b = 0" proof (rule iffI) assume "a + b = a" then have "a + b = a + 0" by (simp only: add_0_right) then show "b = 0" by (simp only: add_left_cancel) next assume "b = 0" have "a + 0 = a" by (simp only: add_0_right) with ‹b = 0› show "a + b = a" by (rule ssubst) qed (* 2ª demostración *) lemma "a + b = a ⟷ b = 0" proof assume "a + b = a" then have "a + b = a + 0" by simp then show "b = 0" by simp next assume "b = 0" have "a + 0 = a" by simp then show "a + b = a" using ‹b = 0› by simp qed (* 3ª demostración *) lemma "a + b = a ⟷ b = 0" proof - have "(a + b = a) ⟷ (a + b = a + 0)" by (simp only: add_0_right) also have "… ⟷ (b = 0)" by (simp only: add_left_cancel) finally show "a + b = a ⟷ b = 0" by this qed (* 4ª demostración *) lemma "a + b = a ⟷ b = 0" proof - have "(a + b = a) ⟷ (a + b = a + 0)" by simp also have "… ⟷ (b = 0)" by simp finally show "a + b = a ⟷ b = 0" . qed (* 5ª demostración *) lemma "a + b = a ⟷ b = 0" by (simp only: add_cancel_left_right) (* 6ª demostración *) lemma "a + b = a ⟷ b = 0" by auto end end
5. Unicidad del elemento neutro en los grupos
Demostrar con Lean4 que un grupo sólo posee un elemento neutro.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] example (e : G) (h : ∀ x, x * e = x) : e = 1 := sorry
5.1. Demostración en lenguaje natural
Sea \(e ∈ G\) tal que \[ (∀ x)[x·e = x] \tag{1} \] Entonces, \begin{align} e &= 1.e &&\text{[porque 1 es neutro]} \newline &= 1 &&\text{[por (1)]} \end{align}
5.2. Demostraciones con Lean4
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] -- 1ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := calc e = 1 * e := (one_mul e).symm _ = 1 := h 1 -- 2ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := by have h1 : e = e * e := (h e).symm exact self_eq_mul_left.mp h1 -- 3ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := self_eq_mul_left.mp (h e).symm -- 4ª demostración -- =============== example (e : G) (h : ∀ x, x * e = x) : e = 1 := by aesop -- Lemas usados -- ============ -- variable (a b : G) -- #check (one_mul a : 1 * a = a) -- #check (self_eq_mul_left : b = a * b ↔ a = 1)
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
5.3. Demostraciones con Isabelle/HOL
theory Unicidad_del_elemento_neutro_en_los_grupos imports Main begin context group begin (* 1ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" proof - have "e = 1 * e" by (simp only: left_neutral) also have "… = 1" using assms by (rule allE) finally show "e = 1" by this qed (* 2ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" proof - have "e = 1 * e" by simp also have "… = 1" using assms by simp finally show "e = 1" . qed (* 3ª demostración *) lemma assumes "∀ x. x * e = x" shows "e = 1" using assms by (metis left_neutral) end end