Pruebas en Lean de “Un número es par si, y sólo si, lo es su cuadrado”
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 3 pruebas en Lean de la propiedad
Un número es par si, y sólo si, lo es su cuadrado-
usando los estilos declarativo, aplicativo y funcional.
A continuación, se muestra el vídeo
y el código de la teoría utilizada
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 |
import data.int.parity open int variable (n : ℤ) -- ---------------------------------------------------- -- Ejercicio. Demostrar que un número es par syss lo es -- su cuadrado. -- ---------------------------------------------------- -- 1ª demostración example : even (n^2) ↔ even n := begin split, { contrapose, rw ← odd_iff_not_even, rw ← odd_iff_not_even, unfold odd, intro h, cases h with k hk, use 2*k*(k+1), rw hk, ring, }, { unfold even, intro h, cases h with k hk, use 2*k^2, rw hk, ring, }, end -- 2ª demostración example : even (n^2) ↔ even n := begin split, { contrapose, rw ← odd_iff_not_even, rw ← odd_iff_not_even, rintro ⟨k, rfl⟩, use 2*k*(k+1), ring, }, { rintro ⟨k, rfl⟩, use 2*k^2, ring, }, end -- 3ª demostración example : even (n^2) ↔ even n := iff.intro ( have h : ¬even n → ¬even (n^2), { assume h1 : ¬even n, have h2 : odd n, from odd_iff_not_even.mpr h1, have h3: odd (n^2), from exists.elim h2 ( assume k, assume hk : n = 2*k+1, have h4 : n^2 = 2*(2*k*(k+1))+1, from calc n^2 = (2*k+1)^2 : by rw hk ... = 4*k^2+4*k+1 : by ring ... = 2*(2*k*(k+1))+1 : by ring, show odd (n^2), from exists.intro (2*k*(k+1)) h4), show ¬even (n^2), from odd_iff_not_even.mp h3 }, show even (n^2) → even n, from not_imp_not.mp h ) ( assume h1 : even n, show even (n^2), from exists.elim h1 ( assume k, assume hk : n = 2*k , have h2 : n^2 = 2*(2*k^2), from calc n^2 = (2*k)^2 : by rw hk ... = 2*(2*k^2) : by ring, show even (n^2), from exists.intro (2*k^2) h2 )) |