Los monoides booleanos son conmutativos

Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.

Un monoide \(M\) es booleano si
\[ (∀ x ∈ M)[x·x = 1] \]
y es conmutativo si
\[ (∀ x, y ∈ M)[x·y = y·x] \]

En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son

Demostrar con Lean4 que los monoides booleanos son conmutativos.

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

1. Demostración en lenguaje natural

Sean \(a, b ∈ M\). Se verifica la siguiente cadena de igualdades
\begin{align}
a·b &= (a·b)·1 &&\text{[por mul_one]} \\
&= (a·b)·(a·a) &&\text{[por hipótesis, \(a·a = 1\)]} \\
&= ((a·b)·a)·a &&\text{[por mul_assoc]} \\
&= (a·(b·a))·a &&\text{[por mul_assoc]} \\
&= (1·(a·(b·a)))·a &&\text{[por one_mul]} \\
&= ((b·b)·(a·(b·a)))·a &&\text{[por hipótesis, \(b·b = 1\)]} \\
&= (b·(b·(a·(b·a))))·a &&\text{[por mul_assoc]} \\
&= (b·((b·a)·(b·a)))·a &&\text{[por mul_assoc]} \\
&= (b·1)·a &&\text{[por hipótesis, \((b·a)·(b·a) = 1\)]} \\
&= b·a &&\text{[por mul_one]}
\end{align}

2. Demostraciones con Lean4

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

3. Demostraciones con Isabelle/HOL

Escribe un comentario