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
|
1 |
∀ x ∈ M, x * x = 1 |
y es conmutativo si
|
1 |
∀ x y ∈ M, x * y = y * x |
En Lean, está definida la clase de los monoides (como monoid) y sus propiedades características son
|
1 2 3 |
mul_assoc : (a * b) * c = a * (b * c) one_mul : 1 * a = a mul_one : a * 1 = a |
Demostrar que los monoides booleanos son conmutativos.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import algebra.group.basic universe u variables {M : Type u} [monoid M] example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := sorry |
[expand title=»Soluciones con Lean»]
|
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 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 |
import algebra.group.basic universe u variables {M : Type u} [monoid M] -- 1ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := begin intros a b, calc a * b = (a * b) * 1 : (mul_one (a * b)).symm ... = (a * b) * (a * a) : congr_arg ((*) (a*b)) (h a).symm ... = ((a * b) * a) * a : (mul_assoc (a*b) a a).symm ... = (a * (b * a)) * a : congr_arg (* a) (mul_assoc a b a) ... = (1 * (a * (b * a))) * a : congr_arg (* a) (one_mul (a*(b*a))).symm ... = ((b * b) * (a * (b * a))) * a : congr_arg (* a) (congr_arg (* (a*(b*a))) (h b).symm) ... = (b * (b * (a * (b * a)))) * a : congr_arg (* a) (mul_assoc b b (a*(b*a))) ... = (b * ((b * a) * (b * a))) * a : congr_arg (* a) (congr_arg ((*) b) (mul_assoc b a (b*a)).symm) ... = (b * 1) * a : congr_arg (* a) (congr_arg ((*) b) (h (b*a))) ... = b * a : congr_arg (* a) (mul_one b), end -- 2ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := begin intros a b, calc a * b = (a * b) * 1 : by simp only [mul_one] ... = (a * b) * (a * a) : by simp only [h] ... = ((a * b) * a) * a : by simp only [mul_assoc] ... = (a * (b * a)) * a : by simp only [mul_assoc] ... = (1 * (a * (b * a))) * a : by simp only [one_mul] ... = ((b * b) * (a * (b * a))) * a : by simp only [h] ... = (b * (b * (a * (b * a)))) * a : by simp only [mul_assoc] ... = (b * ((b * a) * (b * a))) * a : by simp only [mul_assoc] ... = (b * 1) * a : by simp only [h] ... = b * a : by simp only [mul_one] end -- 3ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := begin intros a b, calc a * b = (a * b) * 1 : by simp ... = (a * b) * (a * a) : by simp [h] ... = ((a * b) * a) * a : by simp [mul_assoc] ... = (a * (b * a)) * a : by simp [mul_assoc] ... = (1 * (a * (b * a))) * a : by simp ... = ((b * b) * (a * (b * a))) * a : by simp [h] ... = (b * (b * (a * (b * a)))) * a : by simp [mul_assoc] ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc] ... = (b * 1) * a : by simp [h] ... = b * a : by simp, end -- 4ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := begin intros a b, calc a * b = (a * b) * (a * a) : by simp [h] ... = (1 * (a * (b * a))) * a : by simp [mul_assoc] ... = ((b * b) * (a * (b * a))) * a : by simp [h] ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc] ... = b * a : by simp [h], end -- 5ª demostración -- =============== example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := begin intros a b, calc a * b = ((b * b) * (a * (b * a))) * a : by simp [h, mul_assoc] ... = (b * ((b * a) * (b * a))) * a : by simp [mul_assoc] ... = b * a : by simp [h], end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones 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 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 80 81 82 83 |
theory Los_monoides_booleanos_son_conmutativos imports Main begin context monoid begin (* 1ª demostración *) lemma assumes "∀ x. x * x = 1" shows "∀ x y. x * y = y * x" proof (rule allI)+ fix a b have "a * b = (a * b) * 1" by (simp only: right_neutral) also have "… = (a * b) * (a * a)" by (simp only: assms) also have "… = ((a * b) * a) * a" by (simp only: assoc) also have "… = (a * (b * a)) * a" by (simp only: assoc) also have "… = (1 * (a * (b * a))) * a" by (simp only: left_neutral) also have "… = ((b * b) * (a * (b * a))) * a" by (simp only: assms) also have "… = (b * (b * (a * (b * a)))) * a" by (simp only: assoc) also have "… = (b * ((b * a) * (b * a))) * a" by (simp only: assoc) also have "… = (b * 1) * a" by (simp only: assms) also have "… = b * a" by (simp only: right_neutral) finally show "a * b = b * a" by this qed (* 2ª demostración *) lemma assumes "∀ x. x * x = 1" shows "∀ x y. x * y = y * x" proof (rule allI)+ fix a b have "a * b = (a * b) * 1" by simp also have "… = (a * b) * (a * a)" by (simp add: assms) also have "… = ((a * b) * a) * a" by (simp add: assoc) also have "… = (a * (b * a)) * a" by (simp add: assoc) also have "… = (1 * (a * (b * a))) * a" by simp also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms) also have "… = (b * (b * (a * (b * a)))) * a" by (simp add: assoc) also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc) also have "… = (b * 1) * a" by (simp add: assms) also have "… = b * a" by simp finally show "a * b = b * a" by this qed (* 3ª demostración *) lemma assumes "∀ x. x * x = 1" shows "∀ x y. x * y = y * x" proof (rule allI)+ fix a b have "a * b = (a * b) * (a * a)" by (simp add: assms) also have "… = (a * (b * a)) * a" by (simp add: assoc) also have "… = ((b * b) * (a * (b * a))) * a" by (simp add: assms) also have "… = (b * ((b * a) * (b * a))) * a" by (simp add: assoc) also have "… = (b * 1) * a" by (simp add: assms) finally show "a * b = b * a" by simp qed (* 4ª demostración *) lemma assumes "∀ x. x * x = 1" shows "∀ x y. x * y = y * x" by (metis assms assoc right_neutral) end end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]
