En los monoides, los inversos a la izquierda y a la derecha son iguales
Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.
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 si M es un monide, a ∈ M, b es un inverso de a por la izquierda y c es un inverso de a por la derecha, entonce b = c.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import algebra.group.defs variables {M : Type} [monoid M] variables {a b c : M} example (hba : b * a = 1) (hac : a * c = 1) : b = c := 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 |
import algebra.group.defs variables {M : Type} [monoid M] variables {a b c : M} -- 1ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := begin rw ←one_mul c, rw ←hba, rw mul_assoc, rw hac, rw mul_one b, end -- 2ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := by rw [←one_mul c, ←hba, mul_assoc, hac, mul_one b] -- 3ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := calc b = b * 1 : (mul_one b).symm ... = b * (a * c) : congr_arg (λ x, b * x) hac.symm ... = (b * a) * c : (mul_assoc b a c).symm ... = 1 * c : congr_arg (λ x, x * c) hba ... = c : one_mul c -- 4ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := calc b = b * 1 : by finish ... = b * (a * c) : by finish ... = (b * a) * c : (mul_assoc b a c).symm ... = 1 * c : by finish ... = c : by finish -- 5ª demostración -- =============== example (hba : b * a = 1) (hac : a * c = 1) : b = c := left_inv_eq_right_inv hba hac |
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="isar"> 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 |
theory En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales imports Main begin context monoid begin (* 1ª demostración *) lemma assumes "b ❙* a = ❙1" "a ❙* c = ❙1" shows "b = c" proof - have "b = b ❙* ❙1" by (simp only: right_neutral) also have "… = b ❙* (a ❙* c)" by (simp only: ‹a ❙* c = ❙1›) also have "… = (b ❙* a) ❙* c" by (simp only: assoc) also have "… = ❙1 ❙* c" by (simp only: ‹b ❙* a = ❙1›) also have "… = c" by (simp only: left_neutral) finally show "b = c" by this qed (* 2ª demostración *) lemma assumes "b ❙* a = ❙1" "a ❙* c = ❙1" shows "b = c" proof - have "b = b ❙* ❙1" by simp also have "… = b ❙* (a ❙* c)" using ‹a ❙* c = ❙1› by simp also have "… = (b ❙* a) ❙* c" by (simp add: assoc) also have "… = ❙1 ❙* c" using ‹b ❙* a = ❙1› by simp also have "… = c" by simp finally show "b = c" by this qed (* 3ª demostración *) lemma assumes "b ❙* a = ❙1" "a ❙* c = ❙1" shows "b = c" using assms by (metis assoc left_neutral 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]