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
|
1 |
a * b = a * c ↔ b = c. |
En Lean la clase de los monoides cancelativos por la izquierda es left_cancel_monoid y la propiedad cancelativa por la izquierda es
|
1 |
mul_left_cancel_iff : a * b = a * c ↔ b = c |
Demostrar que si M es un monoide cancelativo por la izquierda y a, b ∈ M, entonces
|
1 |
a * b = a ↔ b = 1 |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 |
import algebra.group.basic universe u variables {M : Type u} [left_cancel_monoid M] variables {a b : M} example : a * b = a ↔ b = 1 := 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 |
import algebra.group.basic universe u variables {M : Type u} [left_cancel_monoid M] variables {a b : M} -- ?ª demostración -- =============== example : a * b = a ↔ b = 1 := begin split, { intro h, rw ← @mul_left_cancel_iff _ _ a b 1, rw mul_one, exact h, }, { intro h, rw h, exact mul_one a, }, end -- ?ª 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 -- ?ª demostración -- =============== example : a * b = a ↔ b = 1 := mul_right_eq_self -- ?ª demostración -- =============== example : a * b = a ↔ b = 1 := by finish |
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 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 |
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 |
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]