Suma de los primeros cuadrados
Demostrar que la suma de los primeros cuadrados
1 |
0² + 1² + 2² + 3² + ··· + n² |
es n(n+1)(2n+1)/6.
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import data.nat.basic import tactic open nat variable (n : ℕ) @[simp] def sumaCuadrados : ℕ → ℕ | 0 := 0 | (n+1) := sumaCuadrados n + (n+1)^2 example : 6 * sumaCuadrados n = n* (n + 1) * (2 * 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 |
import data.nat.basic import tactic open nat variable (n : ℕ) set_option pp.structure_projections false @[simp] def sumaCuadrados : ℕ → ℕ | 0 := 0 | (n+1) := sumaCuadrados n + (n+1)^2 -- 1ª demostración example : 6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) := begin induction n with n HI, { simp, }, { calc 6 * sumaCuadrados (succ n) = 6 * (sumaCuadrados n + (n+1)^2) : by simp ... = 6 * sumaCuadrados n + 6 * (n+1)^2 : by ring_nf ... = n * (n + 1) * (2 * n + 1) + 6 * (n+1)^2 : by {congr; rw HI} ... = (n + 1) * (n * (2 * n + 1) + 6 * (n+1)) : by ring_nf ... = (n + 1) * (2 * n^2 + 7 * n + 6) : by ring_nf ... = (n + 1) * (n + 2) * (2 * n + 3) : by ring_nf ... = succ n * (succ n + 1) * (2 * succ n + 1) : by refl, }, end -- 2ª demostración example : 6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1) := begin induction n with n HI, { simp, }, { calc 6 * sumaCuadrados (succ n) = 6 * (sumaCuadrados n + (n+1)^2) : by simp ... = 6 * sumaCuadrados n + 6 * (n+1)^2 : by ring_nf ... = n * (n + 1) * (2 * n + 1) + 6 * (n+1)^2 : by {congr; rw HI} ... = (n + 1) * (n + 2) * (2 * n + 3) : by ring_nf ... = succ n * (succ n + 1) * (2 * succ n + 1) : by refl, }, 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 |
theory Suma_de_los_primeros_cuadrados imports Main begin fun sumaCuadrados :: "nat ⇒ nat" where "sumaCuadrados 0 = 0" | "sumaCuadrados (Suc n) = sumaCuadrados n + (Suc n)^2" (* 1ª demostración *) lemma "6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1)" proof (induct n) show "6 * sumaCuadrados 0 = 0 * (0 + 1) * (2 * 0 + 1)" by simp next fix n assume HI : "6 * sumaCuadrados n = n * (n + 1) * (2 * n + 1)" have "6 * sumaCuadrados (Suc n) = 6 * (sumaCuadrados n + (n + 1)^2)" by simp also have "… = 6 * sumaCuadrados n + 6 * (n + 1)^2" by simp also have "… = n * (n + 1) * (2 * n + 1) + 6 * (n + 1)^2" using HI by simp also have "… = (n + 1) * (n * (2 * n + 1) + 6 * (n+1))" by algebra also have "… = (n + 1) * (2 * n^2 + 7 * n + 6)" by algebra also have "… = (n + 1) * (n + 2) * (2 * n + 3)" by algebra also have "… = (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1)" by algebra also have "… = Suc n * (Suc n + 1) * (2 * Suc n + 1)" by (simp only: Suc_eq_plus1) finally show "6 * sumaCuadrados (Suc n) = Suc n * (Suc n + 1) * (2 * Suc n + 1)" by this qed (* 2ª demostración *) lemma "6 * sumaCuadrados n = n* (n + 1) * (2 * n + 1)" proof (induct n) show "6 * sumaCuadrados 0 = 0 * (0 + 1) * (2 * 0 + 1)" by simp next fix n assume HI : "6 * sumaCuadrados n = n * (n + 1) * (2 * n + 1)" have "6 * sumaCuadrados (Suc n) = 6 * sumaCuadrados n + 6 * (n + 1)^2" by simp also have "… = n * (n + 1) * (2 * n + 1) + 6 * (n + 1)^2" using HI by simp also have "… = (n + 1) * ((n + 1) + 1) * (2 * (n + 1) + 1)" by algebra finally show "6 * sumaCuadrados (Suc n) = Suc n * (Suc n + 1) * (2 * Suc n + 1)" by (simp only: Suc_eq_plus1) qed 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]