ForMatUS: Pruebas en Lean del desarrollo de un producto de dos sumas
He añadido a la lista Lógica con Lean el vídeo en el que se comentan ??? pruebas en Lean de la propiedad
|
1 |
(a + b) * (c + d) = a * c + b * c + a * d + b * d |
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 |
-- ------------------------------------------------------ -- Ej. 1. Sean a, b, c y d números enteros. Demostrar que -- (a + b) * (c + d) = a * c + b * c + a * d + b * d -- ------------------------------------------------------ import tactic import data.int.basic variables a b c d : ℤ -- 1ª demostración example : (a + b) * (c + d) = a * c + b * c + a * d + b * d := calc (a + b) * (c + d) = (a + b) * c + (a + b) * d : by rw left_distrib ... = (a * c + b * c) + (a + b) * d : by rw right_distrib ... = (a * c + b * c) + (a * d + b * d) : by rw right_distrib ... = a * c + b * c + a * d + b * d : by rw ←add_assoc -- 2ª demostración example : (a + b) * (c + d) = a * c + b * c + a * d + b * d := by rw [left_distrib, right_distrib, right_distrib, ←add_assoc] -- 3ª demostración example : (a + b) * (c + d) = a * c + b * c + a * d + b * d := begin rw left_distrib, rw right_distrib, rw right_distrib, rw ←add_assoc, end -- 4ª demostración example : (a + b) * (c + d) = a * c + b * c + a * d + b * d := calc (a + b) * (c + d) = (a + b) * c + (a + b) * d : by rw mul_add ... = (a * c + b * c) + (a + b) * d : by rw add_mul ... = (a * c + b * c) + (a * d + b * d) : by rw add_mul ... = a * c + b * c + a * d + b * d : by rw ←add_assoc -- 5ª demostración example : (a + b) * (c + d) = a * c + b * c + a * d + b * d := -- by hint by linarith -- 6ª demostración example : (a + b) * (c + d) = a * c + b * c + a * d + b * d := by nlinarith -- 7ª demostración example : (a + b) * (c + d) = a * c + b * c + a * d + b * d := by ring |