septiembre 2021 – Calculemus

Igualdad de bloques de una partición cuando tienen elementos comunes

PorJosé A. Alonso 30 septiembre 202130 septiembre 2021

Este ejercicio es el primero de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X. El desarrollo de dicha serie está basado en la cuarta parte de la primera sesión del curso de Kevin Buzzard Formalising mathematics: workshop 1 — logic, sets, functions, relations.

Una partición de un conjunto A es un conjunto de subconjuntos no vacíos de A tal que todo elemento de A está exactamente en uno de dichos subconjuntos. Es decir, una famila de conjuntos C es una partición de A si se verifican las siguientes condiciones:

Los conjuntos de C son no vacíos; es decir,

     ∀ X ∈ C, X ≠ ∅.

1	∀ X ∈ C, X ≠ ∅.

Los conjuntos de C recubren A; es decir,

     ∀ a ∈ A, ∃ X ∈ C, a ∈ X

1	∀ a ∈ A, ∃ X ∈ C, a ∈ X

Los conjuntos de C son disjuntos entre sí; es decir,

     ∀ X Y ∈ C, X ∩ Y ≠ ∅ → X = Y

1	∀ X Y ∈ C, X ∩ Y ≠ ∅ → X = Y

En Lean, se puede definir el tipo de las particiones sobre un tipo A mediante una estructura con 4 campos:

Un conjunto de subconjuntos de A llamados los bloques de la partición.
Una prueba de que los bloques son no vacíos.
Una prueba de que cada término de tipo A está en uno de los bloques.
Una prueba de que dos bloques con intersección no vacía son iguales.

Su definición es

    @[ext] structure particion (A : Type) :=
    (Bloques    : set (set A))
    (Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
    (Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
    (Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

Con la definición anterior,

P : particion A expresa que P es una partición de A.
Bloques P es el conjunto de los bloque de P.
Hno_vacios P prueba que los bloques de P son no vacíos.
Hrecubren P prueba que los bloque de P recubren a A.
Hdisjuntos P prueba que los bloques de P son disjuntos entre sí

Demostrar que si dos bloques de una partición tienen un elemento en común, entonces son iguales.

Para ello, completar la siguiente teoría de Lean:

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}

example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
sorry

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

sorry

end particion

[expand title=»Soluciones con Lean»]

import tactic

@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}

-- 1ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { rw set.nonempty_def,
    use a,
    split,
    { exact haX, },
    { exact haY, }},
end

-- 2ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { use a,
    exact ⟨haX, haY⟩, },
end

-- 3ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { exact ⟨a, haX, haY⟩, },
end

-- 4ª demostración
lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

end particion

import tactic

@[ext] structure particion (A : Type) :=

(Bloques : set (set A))

(Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)

(Hrecubren : ∀ a, ∃ X ∈ Bloques, a ∈ X)

(Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

namespace particion

variable {A : Type}

variable {P : particion A}

variables {X Y : set A}

-- 1ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

begin

apply P.Hdisjuntos,

{ exact hX, },

{ exact hY, },

{ rw set.nonempty_def,

use a,

split,

{ exact haX, },

{ exact haY, }},

end

-- 2ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

begin

apply P.Hdisjuntos,

{ exact hX, },

{ exact hY, },

{ use a,

exact ⟨haX, haY⟩, },

end

-- 3ª demostración

example

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

begin

apply P.Hdisjuntos,

{ exact hX, },

{ exact hY, },

{ exact ⟨a, haX, haY⟩, },

end

-- 4ª demostración

lemma iguales_si_comun

(hX : X ∈ Bloques P)

(hY : Y ∈ Bloques P)

{a : A}

(haX : a ∈ X)

(haY : a ∈ Y)

: X = Y :=

Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩

end particion

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]

Identidad de Brahmagupta-Fibonacci

PorJosé A. Alonso 26 septiembre 202126 septiembre 2021

Demostrar la identidad de Brahmagupta-Fibonacci

   (a² + b²)(c² + d²) = (ac - bd)² + (ad + bc)²

1	(a² + b²)(c² + d²) = (ac - bd)² + (ad + bc)²

Para ello, completar la siguiente teoría de Lean:

import data.real.basic

variables (a b c d : ℝ)

example :
  (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=
sorry

import data.real.basic

variables (a b c d : ℝ)

example :

(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables (a b c d : ℝ)

-- 1ª demostración
example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=
calc (a^2 + b^2) * (c^2 + d^2)
     = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)
         : right_distrib (a^2) (b^2) (c^2 + d^2)
 ... = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)
         : congr_arg2 (+) (left_distrib (a^2) (c^2) (d^2)) rfl
 ... = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)
         : congr_arg2 (+) rfl (left_distrib (b^2) (c^2) (d^2))
 ... = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)
         : by ring
 ... = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)
         : by ring
 ... = (a*c - b*d)^2 + (a*d + b*c)^2
         : by ring

-- 2ª demostración
example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=
by ring

import data.real.basic

variables (a b c d : ℝ)

-- 1ª demostración

example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=

calc (a^2 + b^2) * (c^2 + d^2)

= a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)

: right_distrib (a^2) (b^2) (c^2 + d^2)

... = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)

: congr_arg2 (+) (left_distrib (a^2) (c^2) (d^2)) rfl

... = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)

: congr_arg2 (+) rfl (left_distrib (b^2) (c^2) (d^2))

... = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)

: by ring

... = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)

: by ring

... = (a*c - b*d)^2 + (a*d + b*c)^2

: by ring

-- 2ª demostración

example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=

by ring

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»]

theory "Identidad_de_Brahmagupta-Fibonacci"
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes a b c d :: real
  shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2"
proof -
  have "(a^2 + b^2) * (c^2 + d^2) = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)"
    by (simp only: distrib_right)
  also have "… = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)"
    by (simp only: distrib_left)
  also have "… = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)"
    by (simp only: distrib_left)
  also have "… = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)"
    by algebra
  also have "… = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)"
    by algebra
  also have "… = (a*c - b*d)^2 + (a*d + b*c)^2"
    by algebra
  finally show "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" .
qed

(* 2ª demostración *)
lemma
  fixes a b c d :: real
  shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2"
by algebra

end

theory "Identidad_de_Brahmagupta-Fibonacci"

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes a b c d :: real

shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2"

proof -

have "(a^2 + b^2) * (c^2 + d^2) = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)"

by (simp only: distrib_right)

also have "… = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)"

by (simp only: distrib_left)

also have "… = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)"

by (simp only: distrib_left)

also have "… = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)"

by algebra

also have "… = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)"

by algebra

also have "… = (a*c - b*d)^2 + (a*d + b*c)^2"

by algebra

finally show "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" .

qed

(* 2ª demostración *)

lemma

fixes a b c d :: real

shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2"

by algebra

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]

Suma de potencias de dos

PorJosé A. Alonso 25 septiembre 202124 septiembre 2021

Demostrar que

   1 + 2 + 2² + 2³ + ... + 2⁽ⁿ⁻¹⁾ = 2ⁿ - 1

1	1 + 2 + 2² + 2³ + ... + 2⁽ⁿ⁻¹⁾ = 2ⁿ - 1

Para ello, completar la siguiente teoría de Lean:

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

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»]

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

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»]

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

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

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

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

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]

Fórmula de Gauss de la suma de los primeros números naturales

PorJosé A. Alonso 24 septiembre 202120 septiembre 2021

La fórmula de Gauss para la suma de los primeros números naturales es

   0 + 1 + 2 + ... + (n-1) = n(n-1)/2

1	0 + 1 + 2 + ... + (n-1) = n(n-1)/2

En un ejercicio anterior se ha demostrado dicha fórmula por inducción. Otra forma de demostrarla, sin usar inducción, es la siguiente: La suma se puede escribir de dos maneras

   S = 0     + 1     + 2     + ... + (n-3) + (n-2) + (n-1)
   S = (n-1) + (n-2) + (n-3) + ... + 2     + 1     + 0

1 2	S = 0 + 1 + 2 + ... + (n-3) + (n-2) + (n-1) S = (n-1) + (n-2) + (n-3) + ... + 2 + 1 + 0

Al sumar, se observa que cada par de números de la misma columna da como suma (n-1), y puesto que hay n columnas en total, se sigue

   2S = n(n-1)

1	2S = n(n-1)

lo que prueba la fórmula.

Demostrar la fórmula de Gauss siguiendo el procedimiento anterior.

Para ello, completar la siguiente teoría de Lean:

import algebra.big_operators.basic
import algebra.big_operators.intervals

open_locale big_operators
open finset nat

variables (n i : ℕ)

example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
sorry

import algebra.big_operators.basic

import algebra.big_operators.intervals

open_locale big_operators

open finset nat

variables (n i : ℕ)

example :

(∑ i in range n, i) * 2 = n * (n - 1) :=

sorry

[expand title=»Soluciones con Lean»]

import algebra.big_operators.basic
import algebra.big_operators.intervals

open_locale big_operators
open finset nat

variables (n i : ℕ)

-- Lema auxiliar
-- =============

-- Se usará el siguiente lema auxiliar del que se presentan distintas
-- demostraciones.

-- 1ª demostración del lema auxiliar
example : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=
begin
  intros x hx,
  replace hx : x < n := mem_range.1 hx,
  replace hx : x ≤ n - 1 := le_pred_of_lt hx,
  exact nat.add_sub_cancel' hx,
end

-- 2ª demostración del lema auxiliar
example : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=
begin
  intros x hx,
  exact nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx)),
end

-- 3ª demostración del lema auxiliar
lemma auxiliar : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=
λ x hx, nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx))

-- Lema principal
-- ==============

-- 1ª demostración
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
calc (∑ i in range n, i) * 2
     = (∑ i in range n, i) + (∑ i in range n, i)
         : mul_two _
 ... = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))
         : congr_arg2 (+) rfl (sum_range_reflect id n).symm
 ... = ∑ i in range n, (i + (n - 1 - i))
         : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1)
         : sum_congr rfl (auxiliar n)
 ... = card (range n) • (n - 1)
         : sum_const (n - 1)
 ... = card (range n) * (n - 1)
         : nat.nsmul_eq_mul _ _
 ... = n * (n - 1)
         : congr_arg2 (*) (card_range n) rfl

-- 2ª demostración
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
calc (∑ i in range n, i) * 2
     = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))
         : by rw [sum_range_reflect (λ i, i) n, mul_two]
 ... = ∑ i in range n, (i + (n - 1 - i))
         : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1)
         : sum_congr rfl (auxiliar n)
 ... = n * (n - 1)
         : by rw [sum_const, card_range, nat.nsmul_eq_mul]

import algebra.big_operators.basic

import algebra.big_operators.intervals

open_locale big_operators

open finset nat

variables (n i : ℕ)

-- Lema auxiliar

-- =============

-- Se usará el siguiente lema auxiliar del que se presentan distintas

-- demostraciones.

-- 1ª demostración del lema auxiliar

example : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=

begin

intros x hx,

replace hx : x < n := mem_range.1 hx,

replace hx : x ≤ n - 1 := le_pred_of_lt hx,

exact nat.add_sub_cancel' hx,

end

-- 2ª demostración del lema auxiliar

example : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=

begin

intros x hx,

exact nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx)),

end

-- 3ª demostración del lema auxiliar

lemma auxiliar : ∀ x, x ∈ range n → x + (n - 1 - x) = n - 1 :=

λ x hx, nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx))

-- Lema principal

-- ==============

-- 1ª demostración

example :

(∑ i in range n, i) * 2 = n * (n - 1) :=

calc (∑ i in range n, i) * 2

= (∑ i in range n, i) + (∑ i in range n, i)

: mul_two _

... = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))

: congr_arg2 (+) rfl (sum_range_reflect id n).symm

... = ∑ i in range n, (i + (n - 1 - i))

: sum_add_distrib.symm

... = ∑ i in range n, (n - 1)

: sum_congr rfl (auxiliar n)

... = card (range n) • (n - 1)

: sum_const (n - 1)

... = card (range n) * (n - 1)

: nat.nsmul_eq_mul _ _

... = n * (n - 1)

: congr_arg2 (*) (card_range n) rfl

-- 2ª demostración

example :

(∑ i in range n, i) * 2 = n * (n - 1) :=

calc (∑ i in range n, i) * 2

= (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))

: by rw [sum_range_reflect (λ i, i) n, mul_two]

... = ∑ i in range n, (i + (n - 1 - i))

: sum_add_distrib.symm

... = ∑ i in range n, (n - 1)

: sum_congr rfl (auxiliar n)

... = n * (n - 1)

: by rw [sum_const, card_range, nat.nsmul_eq_mul]

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»]

theory Formula_de_Gauss_de_la_suma
imports Main
begin

lemma
  fixes n :: nat
  shows "2 * (∑i<n. i) = n * (n - 1)"
proof -
  have "2 * (∑i<n. i) = (∑i<n. i) + (∑i<n. i)"
    by simp
  also have "… = (∑i<n. i) + (∑i<n. n - Suc i)"
    using sum.nat_diff_reindex [where g = id] by auto
  also have "… = (∑i<n. (i + (n - Suc i)))"
    using sum.distrib [where A = "{..<n}" and
                             g = id and
                             h = "λi. n - Suc i"] by auto
  also have "… = (∑i<n. n - 1)"
    by simp
  also have "… = n * (n -1)"
    using sum_constant by auto
  finally show "2 * (∑i<n. i) = n * (n - 1)" .
qed

end

theory Formula_de_Gauss_de_la_suma

imports Main

begin

lemma

fixes n :: nat

shows "2 * (∑i<n. i) = n * (n - 1)"

proof -

have "2 * (∑i<n. i) = (∑i<n. i) + (∑i<n. i)"

by simp

also have "… = (∑i<n. i) + (∑i<n. n - Suc i)"

using sum.nat_diff_reindex [where g = id] by auto

also have "… = (∑i<n. (i + (n - Suc i)))"

using sum.distrib [where A = "{..<n}" and

g = id and

h = "λi. n - Suc i"] by auto

also have "… = (∑i<n. n - 1)"

by simp

also have "… = n * (n -1)"

using sum_constant by auto

finally show "2 * (∑i<n. i) = n * (n - 1)" .

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]

Prueba de (1+p)ⁿ ≥ 1+np

PorJosé A. Alonso 23 septiembre 202118 septiembre 2021

Sean p ∈ ℝ y n ∈ ℕ tales que p > -1. Demostrar que

   (1 + p)ⁿ ≥ 1 + np

1	(1 + p)ⁿ ≥ 1 + np

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
open nat

variable (p : ℝ)
variable (n : ℕ)

example
  (h : p > -1)
  : (1 + p)^n ≥ 1 + n*p :=
begin
sorry

import data.real.basic

open nat

variable (p : ℝ)

variable (n : ℕ)

example

(h : p > -1)

: (1 + p)^n ≥ 1 + n*p :=

begin

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

variable (p : ℝ)
variable (n : ℕ)

set_option pp.structure_projections false

example
  (h : p > -1)
  : (1 + p)^n ≥ 1 + n*p :=
begin
  induction n with n HI,
  { simp, },
  { have h1 : 1 + p > 0 := iff.mp neg_lt_iff_pos_add' h,
    have h2 : p*p ≥ 0 := mul_self_nonneg p,
    replace h2 : ↑n*(p*p) ≥ 0 := mul_nonneg (cast_nonneg n) h2,
    calc (1 + p)^succ n
         = (1 + p)^n * (1 + p)
             : pow_succ' (1 + p) n
     ... ≥ (1 + n * p) * (1 + p)
             : (mul_le_mul_right h1).mpr HI
     ... = (1 + p + n*p) + n*(p*p)
             : by ring !
     ... ≥ 1 + p + n*p
             : le_add_of_nonneg_right h2
     ... = 1 + (n + 1) * p
             : by ring !
     ... = 1 + ↑(succ n) * p
             : by norm_num },
end

import data.real.basic

open nat

variable (p : ℝ)

variable (n : ℕ)

set_option pp.structure_projections false

example

(h : p > -1)

: (1 + p)^n ≥ 1 + n*p :=

begin

induction n with n HI,

{ simp, },

{ have h1 : 1 + p > 0 := iff.mp neg_lt_iff_pos_add' h,

have h2 : p*p ≥ 0 := mul_self_nonneg p,

replace h2 : ↑n*(p*p) ≥ 0 := mul_nonneg (cast_nonneg n) h2,

calc (1 + p)^succ n

= (1 + p)^n * (1 + p)

: pow_succ' (1 + p) n

... ≥ (1 + n * p) * (1 + p)

: (mul_le_mul_right h1).mpr HI

... = (1 + p + n*p) + n*(p*p)

: by ring !

... ≥ 1 + p + n*p

: le_add_of_nonneg_right h2

... = 1 + (n + 1) * p

: by ring !

... = 1 + ↑(succ n) * p

: by norm_num },

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»]

theory "Prueba_de_(1+p)^n_mayor_o_igual_que_1+np"
imports Main HOL.Real
begin

lemma
  fixes p :: real
  assumes "p > -1"
  shows "(1 + p)^n ≥ 1 + n*p"
proof (induct n)
  show "(1 + p) ^ 0 ≥ 1 + real 0 * p"
    by simp
next
  fix n
  assume HI : "(1 + p)^n ≥ 1 +  n * p"
  have "1 + Suc n * p = 1 + (n + 1) * p"
    by simp
  also have "… = 1 + n*p + p"
    by (simp add: distrib_right)
  also have "… ≤ (1 + n*p + p) + n*(p*p)"
    by simp
  also have "… = (1 + n * p) * (1 + p)"
    by algebra
  also have "… ≤ (1 + p)^n * (1 + p)"
    using HI assms by simp
  also have "… = (1 + p)^(Suc n)"
    by simp
  finally show "1 + Suc n * p ≤ (1 + p)^(Suc n)" .
qed

end

theory "Prueba_de_(1+p)^n_mayor_o_igual_que_1+np"

imports Main HOL.Real

begin

lemma

fixes p :: real

assumes "p > -1"

shows "(1 + p)^n ≥ 1 + n*p"

proof (induct n)

show "(1 + p) ^ 0 ≥ 1 + real 0 * p"

by simp

fix n

assume HI : "(1 + p)^n ≥ 1 + n * p"

have "1 + Suc n * p = 1 + (n + 1) * p"

by simp

also have "… = 1 + n*p + p"

by (simp add: distrib_right)

also have "… ≤ (1 + n*p + p) + n*(p*p)"

by simp

also have "… = (1 + n * p) * (1 + p)"

by algebra

also have "… ≤ (1 + p)^n * (1 + p)"

using HI assms by simp

also have "… = (1 + p)^(Suc n)"

by simp

finally show "1 + Suc n * p ≤ (1 + p)^(Suc n)" .

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]

Suma de los primeros cubos

PorJosé A. Alonso 22 septiembre 202117 septiembre 2021

Demostrar que la suma de los primeros cubos

   0³ + 1³ + 2³ + 3³ + ··· + n³

1	0³ + 1³ + 2³ + 3³ + ··· + n³

es (n(n+1)/2)²

Para ello, completar la siguiente teoría de Lean:

import data.nat.basic
import tactic
open nat

variable (n : ℕ)

def sumaCubos : ℕ → ℕ
| 0     := 0
| (n+1) := sumaCubos n + (n+1)^3

example :
  4 * sumaCubos n = (n*(n+1))^2 :=
sorry

import data.nat.basic

import tactic

open nat

variable (n : ℕ)

def sumaCubos : ℕ → ℕ

| 0 := 0

| (n+1) := sumaCubos n + (n+1)^3

example :

4 * sumaCubos n = (n*(n+1))^2 :=

sorry

[expand title=»Soluciones con Lean»]

import data.nat.basic
import tactic
open nat

variable (n : ℕ)

set_option pp.structure_projections false

@[simp]
def sumaCubos : ℕ → ℕ
| 0     := 0
| (n+1) := sumaCubos n + (n+1)^3

-- 1ª demostración
example :
  4 * sumaCubos n = (n*(n+1))^2 :=
begin
  induction n with n HI,
  { simp,
    ring, },
  { calc 4 * sumaCubos (succ n)
         = 4 * (sumaCubos n + (n+1)^3)
           : by simp
     ... = 4 * sumaCubos n + 4*(n+1)^3
           : by ring
     ... = (n*(n+1))^2 + 4*(n+1)^3
           : by {congr; rw HI}
     ... = (n+1)^2*(n^2+4*n+4)
           : by ring
     ... = (n+1)^2*(n+2)^2
           : by ring
     ... = ((n+1)*(n+2))^2
           : by ring
     ... = (succ n * (succ n + 1)) ^ 2
           : by simp, },
end

-- 2ª demostración
example :
  4 * sumaCubos n = (n*(n+1))^2 :=
begin
  induction n with n HI,
  { simp,
    ring, },
  { calc 4 * sumaCubos (succ n)
         = 4 * sumaCubos n + 4*(n+1)^3
           : by {simp ; ring}
     ... = (n*(n+1))^2 + 4*(n+1)^3
           : by {congr; rw HI}
     ... = ((n+1)*(n+2))^2
           : by ring
     ... = (succ n * (succ n + 1)) ^ 2
           : by simp, },
end

import data.nat.basic

import tactic

open nat

variable (n : ℕ)

set_option pp.structure_projections false

@[simp]

def sumaCubos : ℕ → ℕ

| 0 := 0

| (n+1) := sumaCubos n + (n+1)^3

-- 1ª demostración

example :

4 * sumaCubos n = (n*(n+1))^2 :=

begin

induction n with n HI,

{ simp,

ring, },

{ calc 4 * sumaCubos (succ n)

= 4 * (sumaCubos n + (n+1)^3)

: by simp

... = 4 * sumaCubos n + 4*(n+1)^3

: by ring

... = (n*(n+1))^2 + 4*(n+1)^3

: by {congr; rw HI}

... = (n+1)^2*(n^2+4*n+4)

: by ring

... = (n+1)^2*(n+2)^2

: by ring

... = ((n+1)*(n+2))^2

: by ring

... = (succ n * (succ n + 1)) ^ 2

: by simp, },

end

-- 2ª demostración

example :

4 * sumaCubos n = (n*(n+1))^2 :=

begin

induction n with n HI,

{ simp,

ring, },

{ calc 4 * sumaCubos (succ n)

= 4 * sumaCubos n + 4*(n+1)^3

: by {simp ; ring}

... = (n*(n+1))^2 + 4*(n+1)^3

: by {congr; rw HI}

... = ((n+1)*(n+2))^2

: by ring

... = (succ n * (succ n + 1)) ^ 2

: by simp, },

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»]

theory Suma_de_los_primeros_cubos
imports Main
begin

fun sumaCubos :: "nat ⇒ nat" where
  "sumaCubos 0       = 0"
| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* 1ª demostración *)
lemma
  "4 * sumaCubos n = (n*(n+1))^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0 * (0 + 1))^2"
    by simp
next
  fix n
  assume HI : "4 * sumaCubos n = (n * (n + 1))^2"
  have "4 * sumaCubos (Suc n) = 4 * (sumaCubos n + (n+1)^3)"
    by simp
  also have "… = 4 * sumaCubos n + 4*(n+1)^3"
    by simp
  also have "… = (n*(n+1))^2 + 4*(n+1)^3"
    using HI by simp
  also have "… = (n+1)^2*(n^2+4*n+4)"
    by algebra
  also have "… = (n+1)^2*(n+2)^2"
    by algebra
  also have "… = ((n+1)*((n+1)+1))^2"
    by algebra
  also have "… = (Suc n * (Suc n + 1))^2"
    by (simp only: Suc_eq_plus1)
  finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2"
    by this
qed

(* 2ª demostración *)
lemma
  "4 * sumaCubos n = (n*(n+1))^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0 * (0 + 1))^2"
    by simp
next
  fix n
  assume HI : "4 * sumaCubos n = (n * (n + 1))^2"
  have "4 * sumaCubos (Suc n) = 4 * sumaCubos n + 4*(n+1)^3"
    by simp
  also have "… = (n*(n+1))^2 + 4*(n+1)^3"
    using HI by simp
  also have "… = ((n+1)*((n+1)+1))^2"
    by algebra
  also have "… = (Suc n * (Suc n + 1))^2"
    by (simp only: Suc_eq_plus1)
  finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2" .
qed

end

theory Suma_de_los_primeros_cubos

imports Main

begin

fun sumaCubos :: "nat ⇒ nat" where

"sumaCubos 0 = 0"

| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* 1ª demostración *)

lemma

"4 * sumaCubos n = (n*(n+1))^2"

proof (induct n)

show "4 * sumaCubos 0 = (0 * (0 + 1))^2"

by simp

fix n

assume HI : "4 * sumaCubos n = (n * (n + 1))^2"

have "4 * sumaCubos (Suc n) = 4 * (sumaCubos n + (n+1)^3)"

by simp

also have "… = 4 * sumaCubos n + 4*(n+1)^3"

by simp

also have "… = (n*(n+1))^2 + 4*(n+1)^3"

using HI by simp

also have "… = (n+1)^2*(n^2+4*n+4)"

by algebra

also have "… = (n+1)^2*(n+2)^2"

by algebra

also have "… = ((n+1)*((n+1)+1))^2"

by algebra

also have "… = (Suc n * (Suc n + 1))^2"

by (simp only: Suc_eq_plus1)

finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2"

by this

qed

(* 2ª demostración *)

lemma

"4 * sumaCubos n = (n*(n+1))^2"

proof (induct n)

show "4 * sumaCubos 0 = (0 * (0 + 1))^2"

by simp

fix n

assume HI : "4 * sumaCubos n = (n * (n + 1))^2"

have "4 * sumaCubos (Suc n) = 4 * sumaCubos n + 4*(n+1)^3"

by simp

also have "… = (n*(n+1))^2 + 4*(n+1)^3"

using HI by simp

also have "… = ((n+1)*((n+1)+1))^2"

by algebra

also have "… = (Suc n * (Suc n + 1))^2"

by (simp only: Suc_eq_plus1)

finally show "4 * sumaCubos (Suc n) = (Suc n * (Suc n + 1))^2" .

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]

Suma de los primeros cuadrados

PorJosé A. Alonso 21 septiembre 202116 septiembre 2021

Demostrar que la suma de los primeros cuadrados

   0² + 1² + 2² + 3² + ··· + n²

1	0² + 1² + 2² + 3² + ··· + n²

es n(n+1)(2n+1)/6.

Para ello, completar la siguiente teoría de Lean:

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

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»]

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

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»]

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

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

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

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]

Suma de progresión geométrica

PorJosé A. Alonso 20 septiembre 202120 septiembre 2021

Demostrar que la suma de los términos de la progresión geométrica

   a + aq + aq² + ··· + aqnⁿ

1	a + aq + aq² + ··· + aqnⁿ

     a(1 - qⁿ⁺¹)
    -------------
       1 - q

a(1 - qⁿ⁺¹)

-------------

1 - q

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
open nat

variable  (n : ℕ)
variables (a q : ℝ)

def sumaPG : ℝ → ℝ → ℕ → ℝ
| a q 0       := a
| a q (n + 1) := sumaPG a q n + (a * q^(n + 1))

example :
  (1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) :=
sorry

import data.real.basic

open nat

variable (n : ℕ)

variables (a q : ℝ)

def sumaPG : ℝ → ℝ → ℕ → ℝ

| a q 0 := a

| a q (n + 1) := sumaPG a q n + (a * q^(n + 1))

example :

(1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

variable  (n : ℕ)
variables (a q : ℝ)

set_option pp.structure_projections false

@[simp]
def sumaPG : ℝ → ℝ → ℕ → ℝ
| a q 0       := a
| a q (n + 1) := sumaPG a q n + (a * q^(n + 1))

example :
  (1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) :=
begin
  induction n with n HI,
  { simp,
    ac_refl, },
  { calc (1 - q) * sumaPG a q (succ n)
         = (1 - q) * (sumaPG a q n + (a * q^(n + 1)))
           : rfl
     ... = (1 - q) * sumaPG a q n + (1 - q) * (a * q^(n + 1))
           : by ring_nf
     ... = a * (1 - q ^ (n + 1)) + (1 - q) * (a * q^(n + 1))
           : by {congr ; rw HI}
     ... = a * (1 - q ^ (succ n + 1))
           : by ring_nf },
end

import data.real.basic

open nat

variable (n : ℕ)

variables (a q : ℝ)

set_option pp.structure_projections false

@[simp]

def sumaPG : ℝ → ℝ → ℕ → ℝ

| a q 0 := a

| a q (n + 1) := sumaPG a q n + (a * q^(n + 1))

example :

(1 - q) * sumaPG a q n = a * (1 - q^(n + 1)) :=

begin

induction n with n HI,

{ simp,

ac_refl, },

{ calc (1 - q) * sumaPG a q (succ n)

= (1 - q) * (sumaPG a q n + (a * q^(n + 1)))

: rfl

... = (1 - q) * sumaPG a q n + (1 - q) * (a * q^(n + 1))

: by ring_nf

... = a * (1 - q ^ (n + 1)) + (1 - q) * (a * q^(n + 1))

: by {congr ; rw HI}

... = a * (1 - q ^ (succ n + 1))

: by 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»]

theory Suma_de_progresion_geometrica
imports Main HOL.Real
begin

fun sumaPG :: "real ⇒ real ⇒ nat ⇒ real" where
  "sumaPG a q 0 = a"
| "sumaPG a q (Suc n) = sumaPG a q n + (a * q^(n + 1))"

(* 1ª demostración *)
lemma
  "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"
proof (induct n)
  show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))"
    by simp
next
  fix n
  assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))"
  have "(1 - q) * sumaPG a q (Suc n) =
        (1 - q) * (sumaPG a q n + (a * q^(n + 1)))"
    by simp
  also have "… = (1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)"
    by (simp add: algebra_simps)
  also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)"
    using HI by simp
  also have "… = a * (1 - q ^ (n + 1) + (1 - q) * q^(n + 1))"
    by (simp add: algebra_simps)
  also have "… = a * (1 - q ^ (n + 1) +  q^(n + 1) - q^(n + 2))"
    by (simp add: algebra_simps)
  also have "… = a * (1 - q^(n + 2))"
    by simp
  also have "… = a * (1 - q ^ (Suc n + 1))"
    by simp
  finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))"
    by this
qed

(* 2ª demostración *)
lemma
  "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"
proof (induct n)
  show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))"
    by simp
next
  fix n
  assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))"
  have "(1 - q) * sumaPG a q (Suc n) =
        (1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)"
    by (simp add: algebra_simps)
  also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)"
    using HI by simp
  also have "… = a * (1 - q ^ (n + 1) +  q^(n + 1) - q^(n + 2))"
    by (simp add: algebra_simps)
  finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))"
    by simp
qed

(* 3ª demostración *)
lemma
  "(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"
  using power_add
  by (induct n) (auto simp: algebra_simps)

end

theory Suma_de_progresion_geometrica

imports Main HOL.Real

begin

fun sumaPG :: "real ⇒ real ⇒ nat ⇒ real" where

"sumaPG a q 0 = a"

| "sumaPG a q (Suc n) = sumaPG a q n + (a * q^(n + 1))"

(* 1ª demostración *)

lemma

"(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"

proof (induct n)

show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))"

by simp

fix n

assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))"

have "(1 - q) * sumaPG a q (Suc n) =

(1 - q) * (sumaPG a q n + (a * q^(n + 1)))"

by simp

also have "… = (1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)"

by (simp add: algebra_simps)

also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)"

using HI by simp

also have "… = a * (1 - q ^ (n + 1) + (1 - q) * q^(n + 1))"

by (simp add: algebra_simps)

also have "… = a * (1 - q ^ (n + 1) + q^(n + 1) - q^(n + 2))"

by (simp add: algebra_simps)

also have "… = a * (1 - q^(n + 2))"

by simp

also have "… = a * (1 - q ^ (Suc n + 1))"

by simp

finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))"

by this

qed

(* 2ª demostración *)

lemma

"(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"

proof (induct n)

show "(1 - q) * sumaPG a q 0 = a * (1 - q ^ (0 + 1))"

by simp

fix n

assume HI : "(1 - q) * sumaPG a q n = a * (1 - q ^ (n + 1))"

have "(1 - q) * sumaPG a q (Suc n) =

(1 - q) * sumaPG a q n + (1 - q) * a * q^(n + 1)"

by (simp add: algebra_simps)

also have "… = a * (1 - q ^ (n + 1)) + (1 - q) * a * q^(n + 1)"

using HI by simp

also have "… = a * (1 - q ^ (n + 1) + q^(n + 1) - q^(n + 2))"

by (simp add: algebra_simps)

finally show "(1 - q) * sumaPG a q (Suc n) = a * (1 - q ^ (Suc n + 1))"

by simp

qed

(* 3ª demostración *)

lemma

"(1 - q) * sumaPG a q n = a * (1 - q^(n + 1))"

using power_add

by (induct n) (auto simp: algebra_simps)

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]

Suma de progresión aritmética

PorJosé A. Alonso 19 septiembre 202115 septiembre 2021

Demostrar que la suma de los términos de la progresión aritmética

   a + (a + d) + (a + 2 × d) + ··· + (a + n × d)

1	a + (a + d) + (a + 2 × d) + ··· + (a + n × d)

es (n + 1) × (2 × a + n × d) / 2.

Para ello, completar la siguiente teoría de Lean:

import data.real.basic
open nat

variable  (n : ℕ)
variables (a d : ℝ)

@[simp]
def sumaPA : ℝ → ℝ → ℕ → ℝ
| a d 0       := a
| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :
  2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=
sorry

import data.real.basic

open nat

variable (n : ℕ)

variables (a d : ℝ)

@[simp]

def sumaPA : ℝ → ℝ → ℕ → ℝ

| a d 0 := a

| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :

2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
open nat

variable  (n : ℕ)
variables (a d : ℝ)

set_option pp.structure_projections false

@[simp]
def sumaPA : ℝ → ℝ → ℕ → ℝ
| a d 0       := a
| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :
  2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=
begin
  induction n with n HI,
  { simp, },
  { calc 2 * sumaPA a d (succ n)
         = 2 * (sumaPA a d n + (a + (n + 1) * d))
           : rfl
     ... = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)
           : by ring_nf
     ... = ((n + 1) * (2 * a + n * d)) + 2 * (a + (n + 1) * d)
           : by {congr; rw HI}
     ... = (n + 2) * (2 * a + (n + 1) * d)
           : by ring_nf
     ... = (succ n + 1) * (2 * a + succ n * d)
           : congr_arg2 (*) (by norm_cast) rfl, },
end

import data.real.basic

open nat

variable (n : ℕ)

variables (a d : ℝ)

set_option pp.structure_projections false

@[simp]

def sumaPA : ℝ → ℝ → ℕ → ℝ

| a d 0 := a

| a d (n + 1) := sumaPA a d n + (a + (n + 1) * d)

example :

2 * sumaPA a d n = (n + 1) * (2 * a + n * d) :=

begin

induction n with n HI,

{ simp, },

{ calc 2 * sumaPA a d (succ n)

= 2 * (sumaPA a d n + (a + (n + 1) * d))

: rfl

... = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)

: by ring_nf

... = ((n + 1) * (2 * a + n * d)) + 2 * (a + (n + 1) * d)

: by {congr; rw HI}

... = (n + 2) * (2 * a + (n + 1) * d)

: by ring_nf

... = (succ n + 1) * (2 * a + succ n * d)

: congr_arg2 (*) (by norm_cast) rfl, },

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»]

theory Suma_de_progresion_aritmetica
imports Main HOL.Real
begin

fun sumaPA :: "real ⇒ real ⇒ nat ⇒ real" where
  "sumaPA a d 0 = a"
| "sumaPA a d (Suc n) = sumaPA a d n + (a + (n + 1) * d)"

(* 1ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2 * a + n * d)"
proof (induct n)
  show "2 * sumaPA a d 0 =
        (real 0 + 1) * (2 * a + real 0 * d)"
    by simp
next
  fix n
  assume HI : "2 * sumaPA a d n =
               (n + 1) * (2 * a + n * d)"
  have "2 * sumaPA a d (Suc n) =
        2 * (sumaPA a d n + (a + (n + 1) * d))"
    by simp
  also have "… = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)"
    by simp
  also have "… = (n + 1) * (2 * a + n * d) + 2 * (a + (n + 1) * d)"
    using HI by simp
  also have "… = (real (Suc n) + 1) * (2 * a + (Suc n) * d)"
    by (simp add: algebra_simps)
  finally show "2 * sumaPA a d (Suc n) =
                (real (Suc n) + 1) * (2 * a + (Suc n) * d)"
    by this
qed

(* 2ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2*a + n*d)"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by (simp add: algebra_simps)
qed

(* 3ª demostración *)
lemma
  "2 * sumaPA a d n = (n + 1) * (2*a + n*d)"
by (induct n) (simp_all add: algebra_simps)

end

theory Suma_de_progresion_aritmetica

imports Main HOL.Real

begin

fun sumaPA :: "real ⇒ real ⇒ nat ⇒ real" where

"sumaPA a d 0 = a"

| "sumaPA a d (Suc n) = sumaPA a d n + (a + (n + 1) * d)"

(* 1ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2 * a + n * d)"

proof (induct n)

show "2 * sumaPA a d 0 =

(real 0 + 1) * (2 * a + real 0 * d)"

by simp

fix n

assume HI : "2 * sumaPA a d n =

(n + 1) * (2 * a + n * d)"

have "2 * sumaPA a d (Suc n) =

2 * (sumaPA a d n + (a + (n + 1) * d))"

by simp

also have "… = 2 * sumaPA a d n + 2 * (a + (n + 1) * d)"

by simp

also have "… = (n + 1) * (2 * a + n * d) + 2 * (a + (n + 1) * d)"

using HI by simp

also have "… = (real (Suc n) + 1) * (2 * a + (Suc n) * d)"

by (simp add: algebra_simps)

finally show "2 * sumaPA a d (Suc n) =

(real (Suc n) + 1) * (2 * a + (Suc n) * d)"

by this

qed

(* 2ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2*a + n*d)"

proof (induct n)

case 0

then show ?case by simp

case (Suc n)

then show ?case by (simp add: algebra_simps)

qed

(* 3ª demostración *)

lemma

"2 * sumaPA a d n = (n + 1) * (2*a + n*d)"

by (induct n) (simp_all add: algebra_simps)

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]

Suma de los primeros números naturales

PorJosé A. Alonso 18 septiembre 202114 septiembre 2021

Demostrar que la suma de los primeros números naturales

   0 + 1 + 2 + 3 + ··· + n

1	0 + 1 + 2 + 3 + ··· + n

es n × (n + 1)/2

Para ello, completar la siguiente teoría de Lean:

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

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»]

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

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»]

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

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

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)" .

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)" .

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

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

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]