Suma de los primeros números naturales
Demostrar que la suma de los primeros números naturales
|
1 |
0 + 1 + 2 + 3 + ··· + n |
es n × (n + 1)/2
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 |
import data.nat.basic import tactic open nat variable (n : ℕ) def suma : ℕ → ℕ | 0 := 0 | (n+1) := suma n + (n+1) example : 2 * suma n = n * (n + 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 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 |
import data.nat.basic import tactic open nat variable (n : ℕ) set_option pp.structure_projections false @[simp] def suma : ℕ → ℕ | 0 := 0 | (n+1) := suma n + (n+1) -- 1ª demostración example : 2 * suma n = n * (n + 1) := begin induction n with n HI, { calc 2 * suma 0 = 2 * 0 : congr_arg ((*) 2) suma.equations._eqn_1 ... = 0 : mul_zero 2 ... = 0 * (0 + 1) : zero_mul (0 + 1), }, { calc 2 * suma (n + 1) = 2 * (suma n + (n + 1)) : congr_arg ((*) 2) (suma.equations._eqn_2 n) ... = 2 * suma n + 2 * (n + 1) : mul_add 2 (suma n) (n + 1) ... = n * (n + 1) + 2 * (n + 1) : congr_arg2 (+) HI rfl ... = (n + 2) * (n + 1) : (add_mul n 2 (n + 1)).symm ... = (n + 1) * (n + 2) : mul_comm (n + 2) (n + 1) }, end -- 2ª demostración example : 2 * suma n = n * (n + 1) := begin induction n with n HI, { calc 2 * suma 0 = 2 * 0 : rfl ... = 0 : rfl ... = 0 * (0 + 1) : rfl, }, { calc 2 * suma (n + 1) = 2 * (suma n + (n + 1)) : rfl ... = 2 * suma n + 2 * (n + 1) : by ring ... = n * (n + 1) + 2 * (n + 1) : by simp [HI] ... = (n + 2) * (n + 1) : by ring ... = (n + 1) * (n + 2) : by ring, }, end -- 3ª demostración example : 2 * suma n = n * (n + 1) := begin induction n with n HI, { simp, }, { calc 2 * suma (n + 1) = 2 * (suma n + (n + 1)) : rfl ... = 2 * suma n + 2 * (n + 1) : by ring ... = n * (n + 1) + 2 * (n + 1) : by simp [HI] ... = (n + 1) * (n + 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 105 106 107 108 109 110 111 112 113 114 115 116 117 |
theory Suma_de_los_primeros_n_numeros_naturales imports Main begin fun suma :: "nat ⇒ nat" where "suma 0 = 0" | "suma (Suc n) = suma n + Suc n" (* 1ª demostración *) lemma "2 * suma n = n * (n + 1)" proof (induct n) have "2 * suma 0 = 2 * 0" by (simp only: suma.simps(1)) also have "… = 0" by (rule mult_0_right) also have "… = 0 * (0 + 1)" by (rule mult_0 [symmetric]) finally show "2 * suma 0 = 0 * (0 + 1)" by this next fix n assume HI : "2 * suma n = n * (n + 1)" have "2 * suma (Suc n) = 2 * (suma n + Suc n)" by (simp only: suma.simps(2)) also have "… = 2 * suma n + 2 * Suc n" by (rule add_mult_distrib2) also have "… = n * (n + 1) + 2 * Suc n" by (simp only: HI) also have "… = n * (n + Suc 0) + 2 * Suc n" by (simp only: One_nat_def) also have "… = n * Suc (n + 0) + 2 * Suc n" by (simp only: add_Suc_right) also have "… = n * Suc n + 2 * Suc n" by (simp only: add_0_right) also have "… = (n + 2) * Suc n" by (simp only: add_mult_distrib) also have "… = Suc (Suc n) * Suc n" by (simp only: add_2_eq_Suc') also have "… = (Suc n + 1) * Suc n" by (simp only: Suc_eq_plus1) also have "… = Suc n * (Suc n + 1)" by (simp only: mult.commute) finally show "2 * suma (Suc n) = Suc n * (Suc n + 1)" by this qed (* 2ª demostración *) lemma "2 * suma n = n * (n + 1)" proof (induct n) have "2 * suma 0 = 2 * 0" by simp also have "… = 0" by simp also have "… = 0 * (0 + 1)" by simp finally show "2 * suma 0 = 0 * (0 + 1)" . next fix n assume HI : "2 * suma n = n * (n + 1)" have "2 * suma (Suc n) = 2 * (suma n + Suc n)" by simp also have "… = 2 * suma n + 2 * Suc n" by simp also have "… = n * (n + 1) + 2 * Suc n" using HI by simp also have "… = n * (n + Suc 0) + 2 * Suc n" by simp also have "… = n * Suc (n + 0) + 2 * Suc n" by simp also have "… = n * Suc n + 2 * Suc n" by simp also have "… = (n + 2) * Suc n" by simp also have "… = Suc (Suc n) * Suc n" by simp also have "… = (Suc n + 1) * Suc n" by simp also have "… = Suc n * (Suc n + 1)" by simp finally show "2 * suma (Suc n) = Suc n * (Suc n + 1)" . qed (* 3ª demostración *) lemma "2 * suma n = n * (n + 1)" proof (induct n) have "2 * suma 0 = 2 * 0" by simp also have "… = 0" by simp also have "… = 0 * (0 + 1)" by simp finally show "2 * suma 0 = 0 * (0 + 1)" . next fix n assume HI : "2 * suma n = n * (n + 1)" have "2 * suma (Suc n) = 2 * (suma n + Suc n)" by simp also have "… = n * (n + 1) + 2 * Suc n" using HI by simp also have "… = (n + 2) * Suc n" by simp also have "… = Suc n * (Suc n + 1)" by simp finally show "2 * suma (Suc n) = Suc n * (Suc n + 1)" . qed (* 4ª demostración *) lemma "2 * suma n = n * (n + 1)" proof (induct n) show "2 * suma 0 = 0 * (0 + 1)" by simp next fix n assume "2 * suma n = n * (n + 1)" then show "2 * suma (Suc n) = Suc n * (Suc n + 1)" by simp qed (* 5ª demostración *) lemma "2 * suma n = n * (n + 1)" proof (induct n) case 0 then show ?case by simp next case (Suc n) then show ?case by simp qed (* 6ª demostración *) lemma "2 * suma n = n * (n + 1)" by (induct n) simp_all 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]