Suma de potencias de dos
Demostrar que
1 |
1 + 2 + 2² + 2³ + ... + 2⁽ⁿ⁻¹⁾ = 2ⁿ - 1 |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 11 |
import algebra.big_operators import tactic open finset nat open_locale big_operators variable (n : ℕ) example : ∑ k in range n, 2^k = 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 |
import algebra.big_operators import tactic open finset nat open_locale big_operators set_option pp.structure_projections false variable (n : ℕ) example : ∑ k in range n, 2^k = 2^n - 1 := begin induction n with n HI, { simp, }, { calc ∑ k in range (succ n), 2^k = ∑ k in range n, 2^k + 2^n : sum_range_succ (λ x, 2 ^ x) n ... = (2^n - 1) + 2^n : congr_arg2 (+) HI rfl ... = (2^n + 2^n) - 1 : by omega ... = 2^n * 2 - 1 : by {congr; simp} ... = 2^(succ n) - 1 : by {congr' 1; ring_nf}, }, 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 |
theory Suma_de_potencias_de_dos imports Main begin (* 1ª demostración *) lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1" proof (induct n) show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1" by simp next fix n assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1" have "(∑k≤Suc n. (2::nat)^k) = (∑k≤n. (2::nat)^k) + 2^Suc n" by simp also have "… = (2^(n+1) - 1) + 2^Suc n" using HI by simp also have "… = 2^(Suc n + 1) - 1" by simp finally show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1" . qed (* 2ª demostración *) lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1" proof (induct n) show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1" by simp next fix n assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1" have "(∑k≤Suc n. (2::nat)^k) = (2^(n+1) - 1) + 2^Suc n" using HI by simp then show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1" by simp qed (* 3ª demostración *) lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1" proof (induct n) case 0 then show ?case by simp next case (Suc n) then show ?case by simp qed (* 4ª demostración *) lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1" by (induct n) simp_all |
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]