La semana en Calculemus (18 de mayo de 2024)

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

A continuación se muestran las soluciones.

1. Si G es un grupo y a, b ∈ G tales que ab = 1 entonces a⁻¹ = b

Demostrar con Lean4 que si \(a\) es un elemento de un grupo \(G\), entonces \(a\) tiene un único inverso; es decir, si \(b\) es un elemento de \(G\) tal que \(a·b = 1\), entonces \(a⁻¹ = b\).

Para ello, completar la siguiente teoría de Lean4:

1.1. Demostración en lenguaje natural

Por la siguiente cadena de igualdades
\begin{align}
a⁻¹ &= a⁻¹·1 &&\text{[porque 1 es neutro]} \\
&= a⁻¹·(a·b) &&\text{[por hipótesis]} \\
&= (a⁻¹·a)·b &&\text{[por la asociativa]} \\
&= 1·b &&\text{[porque a⁻¹ es el inverso de a]} \\
&= b &&\text{[porque 1 es neutro]}
\end{align}

1.2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

1.3. Demostraciones con Isabelle/HOL

2. Si G es un grupo y a, b ∈ G, entonces (ab)⁻¹ = b⁻¹a⁻¹

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).

Para ello, completar la siguiente teoría de Lean4:

2.1. Demostración en lenguaje natural


Teniendo en cuenta la propiedad
\[(∀ a, b ∈ G)[ab = 1 → a⁻¹ = b] \]
basta demostrar que
\[(a·b)·(b⁻¹·a⁻¹) = 1.\]
que se demuestra mediante la siguiente cadena de igualdades
\begin{align}
(a·b)·(b⁻¹·a⁻¹) &= a·(b·(b⁻¹·a⁻¹)) &&\text{[por la asociativa]} \\
&= a·((b·b⁻¹)·a⁻¹) &&\text{[por la asociativa]} \\
&= a·(1·a⁻¹) &&\text{[por producto con inverso]} \\
&= a·a⁻¹ &&\text{[por producto con uno]} \\
&= 1 &&\text{[por producto con
inverso]}
\end{align}

2.2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

2.3. Demostraciones con Isabelle/HOL

Referencias

3. Si G un grupo y a ∈ G, entonces (a⁻¹)⁻¹ = a

Demostrar con Lean4 que si \(G\) un grupo y \(a ∈ G\), entonces
\[(a⁻¹)⁻¹ = a\]

Para ello, completar la siguiente teoría de Lean4:

3.1. Demostración en lenguaje natural

Por la siguiente cadena de igualdades
\begin{align}
(a⁻¹)⁻¹ &= (a⁻¹)⁻¹·1 &&\text{[porque \(1\) es neutro]} \\
&= (a⁻¹)⁻¹·(a⁻¹·a) &&\text{[porque \(a⁻¹\) es el inverso de \(a\)]} \\
&= ((a⁻¹)⁻¹·a⁻¹)·a &&\text{[por la asociativa]} \\
&= 1·a &&\text{[porque \((a⁻¹)⁻¹\) es el inverso de \(a⁻¹\)]} \\
&= a &&\text{[porque \(1\) es neutro]}
\end{align}

3.2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3.3. Demostraciones con Isabelle/HOL

4. Si G es un grupo y a, b, c ∈ G tales que a·b = a·c, entonces b = c

Demostrar con Lean4 que si \(G\) es un grupo y \(a, b, c ∈ G\) tales que \(a·b = a·c\), entonces \(b = c\).

Para ello, completar la siguiente teoría de Lean4:

4.1. Demostración en lenguaje natural

Por la siguiente cadena de igualdades
\begin{align}
b &= 1·b &&\text{[porque \(1\) es neutro]} \\
&= (a⁻¹·a)·b &&\text{[porque \(a⁻¹\) es el inverso de \(a\)]} \\
&= a⁻¹·(a·b) &&\text{[por la asociativa]} \\
&= a⁻¹·(a·c) &&\text{[por la hipótesis]} \\
&= (a⁻¹·a)·c &&\text{[por la asociativa]} \\
&= 1·c &&\text{[porque \(a⁻¹\) es el inverso de \(a\)]} \\
&= c &&\text{[porque 1 es neutro]}
\end{align}

4.2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

4.3. Demostraciones con Isabelle/HOL

5. Si M es un monoide, a ∈ M y m, n ∈ ℕ, entonces a^(m·n) = (a^m)^n

Demostrar con Lean4 que si \(M\) es un monoide, \(a ∈ M\) y \(m, n ∈ ℕ\), entonces
\[ a^{m·n} = (a^m)^n \]

Para ello, completar la siguiente teoría de Lean4:

5.1. Demostración en lenguaje natural

Por inducción en \(n\).

Caso base: Supongamos que \(n = 0\). Entonces,
\begin{align}
a^{m·0} &= a^0 \\
&= 1 &&\text{[por pow_zero]} \\
&= (a^m)^0 &&\text{[por pow_zero]}
\end{align}

Paso de indución: Supogamos que se verifica para \(n\); es decir,
\[ a^{m·n} = (a^m)^n \tag{HI} \]
Entonces,
\begin{align}
a^{m·(n+1)} &= a^{m·n + m} \\
&= a^{m·n}·a^m \\
&= (a^m)^n·a^m &&\text{[por HI]} \\
&= (a^m)^{n+1} &&\text{[por pow_succ’]}
\end{align}

5.2. Demostraciones con Lean4

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

5.3. Demostraciones con Isabelle/HOL