ForMatUS: Pruebas en Lean de (x + y) + z = (x + z) + y
He añadido a la lista Lógica con Lean el vídeo en el que se comentan 10 pruebas en Lean de la peopiedad
|
1 |
(x + y) + z = (x + z) + y |
usando los estilos declarativos, aplicativos, funcional y automático.
A continuación, se muestra el vídeo
|
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 |
-- ---------------------------------------------------- -- Ej. 1. Demostrar que para todo x, y, z en ℤ se tiene -- (x + y) + z = (x + z) + y -- ---------------------------------------------------- import tactic import data.int.basic variables (x y z : ℤ) -- 1ª demostración example : (x + y) + z = (x + z) + y := calc (x + y) + z = x + (y + z) : add_assoc x y z ... = x + (z + y) : eq.subst (add_comm y z) rfl ... = (x + z) + y : eq.symm (add_assoc x z y) -- 2ª demostración example : (x + y) + z = (x + z) + y := calc (x + y) + z = x + (y + z) : by rw add_assoc ... = x + (z + y) : by rw [add_comm y z] ... = (x + z) + y : by rw add_assoc -- 3ª demostración example : (x + y) + z = (x + z) + y := begin rw add_assoc, rw add_comm y z, rw add_assoc, end example : (x + y) + z = (x + z) + y := begin rw [add_assoc, add_comm y z, add_assoc], end -- 4ª demostración example : (x + y) + z = (x + z) + y := by rw [add_assoc, add_comm y z, add_assoc] -- 5ª demostración example : (x + y) + z = (x + z) + y := -- by library_search add_right_comm x y z -- 6ª demostración example : (x + y) + z = (x + z) + y := -- by hint by omega -- 7ª demostración example : (x + y) + z = (x + z) + y := by linarith -- 8ª demostración example : (x + y) + z = (x + z) + y := by nlinarith -- 9ª demostración example : (x + y) + z = (x + z) + y := by ring -- 10ª demostración example : (x + y) + z = (x + z) + y := by finish |