Un número es par si y solo si lo es su cuadrado
Demostrar que un número es par si y solo si lo es su cuadrado.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 |
import data.int.parity import tactic open int variable (n : ℤ) example : even (n^2) ↔ even n := 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 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 |
import data.int.parity import tactic open int variable (n : ℤ) -- 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 )) -- 4ª demostración example : even (n^2) ↔ even n := calc even (n^2) ↔ even (n * n) : iff_of_eq (congr_arg even (sq n)) ... ↔ (even n ∨ even n) : int.even_mul ... ↔ even n : or_self (even n) -- 5ª demostración example : even (n^2) ↔ even n := calc even (n^2) ↔ even (n * n) : by ring_nf ... ↔ (even n ∨ even n) : int.even_mul ... ↔ even n : by simp -- 6ª demostración example : even (n^2) ↔ even n := begin split, { contrapose, intro h, rw ← odd_iff_not_even at *, cases h with k hk, use 2*k*(k+1), 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, }, { intro h, cases h with k hk, use 2*k^2, calc n^2 = (2*k)^2 : by rw hk ... = 2*(2*k^2) : by ring, }, end |
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="lean"> 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 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 |
theory Un_numero_es_par_syss_lo_es_su_cuadrado imports Main begin (* 1ª demostración *) lemma fixes n :: int shows "even (n²) ⟷ even n" proof (rule iffI) assume "even (n²)" show "even n" proof (rule ccontr) assume "odd n" then obtain k where "n = 2*k+1" by (rule oddE) then have "n² = 2*(2*k*(k+1))+1" proof - have "n² = (2*k+1)²" by (simp add: ‹n = 2 * k + 1›) also have "… = 4*k²+4*k+1" by algebra also have "… = 2*(2*k*(k+1))+1" by algebra finally show "n² = 2*(2*k*(k+1))+1" . qed then have "∃k'. n² = 2*k'+1" by (rule exI) then have "odd (n²)" by fastforce then show False using ‹even (n²)› by blast qed next assume "even n" then obtain k where "n = 2*k" by (rule evenE) then have "n² = 2*(2*k²)" by simp then show "even (n²)" by simp qed (* 2ª demostración *) lemma fixes n :: int shows "even (n²) ⟷ even n" proof assume "even (n²)" show "even n" proof (rule ccontr) assume "odd n" then obtain k where "n = 2*k+1" by (rule oddE) then have "n² = 2*(2*k*(k+1))+1" by algebra then have "odd (n²)" by simp then show False using ‹even (n²)› by blast qed next assume "even n" then obtain k where "n = 2*k" by (rule evenE) then have "n² = 2*(2*k²)" by simp then show "even (n²)" by simp qed (* 3ª demostración *) lemma fixes n :: int shows "even (n²) ⟷ even n" proof - have "even (n²) = (even n ∧ (0::nat) < 2)" by (simp only: even_power) also have "… = (even n ∧ True)" by (simp only: less_numeral_simps) also have "… = even n" by (simp only: HOL.simp_thms(21)) finally show "even (n²) ⟷ even n" by this qed (* 4ª demostración *) lemma fixes n :: int shows "even (n²) ⟷ even n" proof - have "even (n²) = (even n ∧ (0::nat) < 2)" by (simp only: even_power) also have "… = even n" by simp finally show "even (n²) ⟷ even n" . qed (* 5ª demostración *) lemma fixes n :: int shows "even (n²) ⟷ even n" by simp 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]