Inducción – Página 3

Pruebas de length (repeat x n) = n

PorJosé A. Alonso 7 septiembre 20218 septiembre 2021

En Lean están definidas las funciones length y repeat tales que

(length xs) es la longitud de la lista xs. Por ejemplo,

     length [1,2,5,2] = 4

1	length [1,2,5,2] = 4

(repeat x n) es la lista que tiene el elemento x n veces. Por ejemplo,

     repeat 7 3 = [7, 7, 7]

1	repeat 7 3 = [7, 7, 7]

Demostrar que

   length (repeat x n) = n

1	length (repeat x n) = n

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

import data.list.basic
open nat
open list

variable {α : Type}
variable (x : α)
variable (n : ℕ)

example :
  length (repeat x n) = n :=
sorry

import data.list.basic

open nat

open list

variable {α : Type}

variable (x : α)

variable (n : ℕ)

example :

length (repeat x n) = n :=

sorry

[expand title=»Soluciones con Lean»]

import data.list.basic
open nat
open list

set_option pp.structure_projections false

variable {α : Type}
variable (x : α)
variable (n : ℕ)

-- 1ª demostración
example :
  length (repeat x n) = n :=
begin
  induction n with n HI,
  { calc length (repeat x 0)
          = length []                : congr_arg length (repeat.equations._eqn_1 x)
      ... = 0                        : length.equations._eqn_1 },
  { calc length (repeat x (succ n))
         = length (x :: repeat x n)  : congr_arg length (repeat.equations._eqn_2 x n)
     ... = length (repeat x n) + 1   : length.equations._eqn_2 x (repeat x n)
     ... = n + 1                     : congr_arg2 (+) HI rfl
     ... = succ n                    : rfl, },
end

-- 2ª demostración
example :
  length (repeat x n) = n :=
begin
  induction n with n HI,
  { calc length (repeat x 0)
          = length []                : rfl
      ... = 0                        : rfl },
  { calc length (repeat x (succ n))
         = length (x :: repeat x n)  : rfl
     ... = length (repeat x n) + 1   : rfl
     ... = n + 1                     : by rw HI
     ... = succ n                    : rfl, },
end

-- 3ª demostración
example : length (repeat x n) = n :=
begin
  induction n with n HI,
  { refl, },
  { dsimp,
    rw HI, },
end

-- 4ª demostración
example : length (repeat x n) = n :=
begin
  induction n with n HI,
  { simp, },
  { simp [HI], },
end

-- 5ª demostración
example : length (repeat x n) = n :=
by induction n ; simp [*]

-- 6ª demostración
example : length (repeat x n) = n :=
nat.rec_on n
  ( show length (repeat x 0) = 0, from
      calc length (repeat x 0)
           = length []                : rfl
       ... = 0                        : rfl )
  ( assume n,
    assume HI : length (repeat x n) = n,
    show length (repeat x (succ n)) = succ n, from
      calc length (repeat x (succ n))
           = length (x :: repeat x n) : rfl
       ... = length (repeat x n) + 1  : rfl
       ... = n + 1                    : by rw HI
       ... = succ n                   : rfl )

-- 7ª demostración
example : length (repeat x n) = n :=
nat.rec_on n
  ( by simp )
  ( λ n HI, by simp [HI])

-- 8ª demostración
example : length (repeat x n) = n :=
length_repeat x n

-- 9ª demostración
example : length (repeat x n) = n :=
by simp

-- 10ª demostración
lemma length_repeat_1 :
  ∀ n, length (repeat x n) = n
| 0 := by calc length (repeat x 0)
               = length ([] : list α)         : rfl
           ... = 0                            : rfl
| (n+1) := by calc length (repeat x (n + 1))
                   = length (x :: repeat x n) : rfl
               ... = length (repeat x n) + 1  : rfl
               ... = n + 1                    : by rw length_repeat_1

-- 11ª demostración
lemma length_repeat_2 :
  ∀ n, length (repeat x n) = n
| 0     := by simp
| (n+1) := by simp [*]

100

101

102

103

104

105

106

107

import data.list.basic

open nat

open list

set_option pp.structure_projections false

variable {α : Type}

variable (x : α)

variable (n : ℕ)

-- 1ª demostración

example :

length (repeat x n) = n :=

begin

induction n with n HI,

{ calc length (repeat x 0)

= length [] : congr_arg length (repeat.equations._eqn_1 x)

... = 0 : length.equations._eqn_1 },

{ calc length (repeat x (succ n))

= length (x :: repeat x n) : congr_arg length (repeat.equations._eqn_2 x n)

... = length (repeat x n) + 1 : length.equations._eqn_2 x (repeat x n)

... = n + 1 : congr_arg2 (+) HI rfl

... = succ n : rfl, },

end

-- 2ª demostración

example :

length (repeat x n) = n :=

begin

induction n with n HI,

{ calc length (repeat x 0)

= length [] : rfl

... = 0 : rfl },

{ calc length (repeat x (succ n))

= length (x :: repeat x n) : rfl

... = length (repeat x n) + 1 : rfl

... = n + 1 : by rw HI

... = succ n : rfl, },

end

-- 3ª demostración

example : length (repeat x n) = n :=

begin

induction n with n HI,

{ refl, },

{ dsimp,

rw HI, },

end

-- 4ª demostración

example : length (repeat x n) = n :=

begin

induction n with n HI,

{ simp, },

{ simp [HI], },

end

-- 5ª demostración

example : length (repeat x n) = n :=

by induction n ; simp [*]

-- 6ª demostración

example : length (repeat x n) = n :=

nat.rec_on n

( show length (repeat x 0) = 0, from

calc length (repeat x 0)

= length [] : rfl

... = 0 : rfl )

( assume n,

assume HI : length (repeat x n) = n,

show length (repeat x (succ n)) = succ n, from

calc length (repeat x (succ n))

= length (x :: repeat x n) : rfl

... = length (repeat x n) + 1 : rfl

... = n + 1 : by rw HI

... = succ n : rfl )

-- 7ª demostración

example : length (repeat x n) = n :=

nat.rec_on n

( by simp )

( λ n HI, by simp [HI])

-- 8ª demostración

example : length (repeat x n) = n :=

length_repeat x n

-- 9ª demostración

example : length (repeat x n) = n :=

by simp

-- 10ª demostración

lemma length_repeat_1 :

∀ n, length (repeat x n) = n

| 0 := by calc length (repeat x 0)

= length ([] : list α) : rfl

... = 0 : rfl

| (n+1) := by calc length (repeat x (n + 1))

= length (x :: repeat x n) : rfl

... = length (repeat x n) + 1 : rfl

... = n + 1 : by rw length_repeat_1

-- 11ª demostración

lemma length_repeat_2 :

∀ n, length (repeat x n) = n

| 0 := by simp

| (n+1) := by simp [*]

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 "Pruebas_de_length_(repeat_x_n)_Ig_n"
imports Main
begin

(* 1ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  have "length (replicate 0 x) = length ([] :: 'a list)"
    by (simp only: replicate.simps(1))
  also have "… = 0"
    by (rule list.size(3))
  finally show "length (replicate 0 x) = 0"
    by this
next
  fix n
  assume HI : "length (replicate n x) = n"
  have "length (replicate (Suc n) x) =
        length (x # replicate n x)"
    by (simp only: replicate.simps(2))
  also have "… = length (replicate n x) + 1"
    by (simp only: list.size(4))
  also have "… = Suc n"
    by (simp only: HI)
  finally show "length (replicate (Suc n) x) = Suc n"
    by this
qed

(* 2ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  show "length (replicate 0 x) = 0"
    by simp
next
  fix n
  assume "length (replicate n x) = n"
  then show "length (replicate (Suc n) x) = Suc n"
    by simp
qed

(* 3ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed

(* 4ª demostración⁾*)
lemma "length (replicate n x) = n"
  by (rule length_replicate)

end

theory "Pruebas_de_length_(repeat_x_n)_Ig_n"

imports Main

begin

(* 1ª demostración⁾*)

lemma "length (replicate n x) = n"

proof (induct n)

have "length (replicate 0 x) = length ([] :: 'a list)"

by (simp only: replicate.simps(1))

also have "… = 0"

by (rule list.size(3))

finally show "length (replicate 0 x) = 0"

by this

fix n

assume HI : "length (replicate n x) = n"

have "length (replicate (Suc n) x) =

length (x # replicate n x)"

by (simp only: replicate.simps(2))

also have "… = length (replicate n x) + 1"

by (simp only: list.size(4))

also have "… = Suc n"

by (simp only: HI)

finally show "length (replicate (Suc n) x) = Suc n"

by this

qed

(* 2ª demostración⁾*)

lemma "length (replicate n x) = n"

proof (induct n)

show "length (replicate 0 x) = 0"

by simp

fix n

assume "length (replicate n x) = n"

then show "length (replicate (Suc n) x) = Suc n"

by simp

qed

(* 3ª demostración⁾*)

lemma "length (replicate n x) = n"

proof (induct n)

case 0

then show ?case by simp

case (Suc n)

then show ?case by simp

qed

(* 4ª demostración⁾*)

lemma "length (replicate n x) = n"

by (rule length_replicate)

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]

La suma de los n primeros impares es n^2

PorJosé A. Alonso 3 septiembre 202129 agosto 2021

En Lean, se puede definir el n-ésimo número primo por

   def impar (n : ℕ) := 2 * n + 1

1	def impar (n : ℕ) := 2 * n + 1

Además, en la librería finset están definidas las funciones

   range :: ℕ → finset ℕ
   sum :: finset α → (α → β) → β

1 2	range :: ℕ → finset ℕ sum :: finset α → (α → β) → β

tales que

+ (range n) es el conjunto de los n primeros números naturales. Por ejemplo, el valor de (range 3) es {0, 1, 2}.
+ (sum A f) es la suma del conjunto obtenido aplicando la función f a los elementos del conjunto finito A. Por ejemplo, el valor de (sum (range 3) impar) es 9.

Demostrar que la suma de los n primeros números impares es n².

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

import data.finset
import tactic.ring
open nat

variable (n : ℕ)

def impar (n : ℕ) := 2 * n + 1

example :
  finset.sum (finset.range n) impar = n ^ 2 :=
sorry

import data.finset

import tactic.ring

open nat

variable (n : ℕ)

def impar (n : ℕ) := 2 * n + 1

example :

finset.sum (finset.range n) impar = n ^ 2 :=

sorry

[expand title=»Soluciones con Lean»]

import data.finset
import tactic.ring
open nat

set_option pp.structure_projections false

variable (n : ℕ)

def impar (n : ℕ) := 2 * n + 1

-- 1ª demostración
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
begin
  induction n with m HI,
  { calc finset.sum (finset.range 0) impar
          = 0
            : by simp
     ...  = 0 ^ 2
            : rfl, },
  { calc finset.sum (finset.range (succ m)) impar
         = finset.sum (finset.range m) impar + impar m
           : finset.sum_range_succ impar m
     ... = m ^ 2 + impar m
           : congr_arg2 (+) HI rfl
     ... = m ^ 2 + 2 * m + 1
           : rfl
     ... = (m + 1) ^ 2
           : by ring_nf
     ... = succ m ^ 2
           : rfl },
end

-- 2ª demostración
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
begin
  induction n with d hd,
  { refl, },
  { rw finset.sum_range_succ,
    rw hd,
    change d ^ 2 + (2 * d + 1) = (d + 1) ^ 2,
    ring_nf, },
end

import data.finset

import tactic.ring

open nat

set_option pp.structure_projections false

variable (n : ℕ)

def impar (n : ℕ) := 2 * n + 1

-- 1ª demostración

example :

finset.sum (finset.range n) impar = n ^ 2 :=

begin

induction n with m HI,

{ calc finset.sum (finset.range 0) impar

= 0

: by simp

... = 0 ^ 2

: rfl, },

{ calc finset.sum (finset.range (succ m)) impar

= finset.sum (finset.range m) impar + impar m

: finset.sum_range_succ impar m

... = m ^ 2 + impar m

: congr_arg2 (+) HI rfl

... = m ^ 2 + 2 * m + 1

: rfl

... = (m + 1) ^ 2

: by ring_nf

... = succ m ^ 2

: rfl },

end

-- 2ª demostración

example :

finset.sum (finset.range n) impar = n ^ 2 :=

begin

induction n with d hd,

{ refl, },

{ rw finset.sum_range_succ,

rw hd,

change d ^ 2 + (2 * d + 1) = (d + 1) ^ 2,

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 "La_suma_de_los_n_primeros_impares_es_n^2"
imports Main
begin

definition impar :: "nat ⇒ nat" where
  "impar n ≡ 2 * n + 1"

lemma "sum impar {i::nat. i < n} = n⇧2"
proof (induct n)
  show "sum impar {i. i < 0} = 0⇧2"
    by simp
next
  fix n
  assume HI : "sum impar {i. i < n} = n⇧2"
  have "{i. i < Suc n} = {i. i < n} ∪ {n}"
    by auto
  then have "sum impar {i. i < Suc n} =
             sum impar {i. i < n} + impar n"
    by simp
  also have "… = n⇧2 + (2 * n + 1)"
    using HI impar_def by simp
  also have "… = (n + 1)⇧2"
    by algebra
  also have "… = (Suc n)⇧2"
    by simp
  finally show "sum impar {i. i < Suc n} = (Suc n)⇧2" .
qed

end

theory "La_suma_de_los_n_primeros_impares_es_n^2"

imports Main

begin

definition impar :: "nat ⇒ nat" where

"impar n ≡ 2 * n + 1"

lemma "sum impar {i::nat. i < n} = n⇧2"

proof (induct n)

show "sum impar {i. i < 0} = 0⇧2"

by simp

fix n

assume HI : "sum impar {i. i < n} = n⇧2"

have "{i. i < Suc n} = {i. i < n} ∪ {n}"

by auto

then have "sum impar {i. i < Suc n} =

sum impar {i. i < n} + impar n"

by simp

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

using HI impar_def by simp

also have "… = (n + 1)⇧2"

by algebra

also have "… = (Suc n)⇧2"

by simp

finally show "sum impar {i. i < Suc n} = (Suc n)⇧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]

Relación entre los índices de las subsucesiones y los de la sucesión

PorJosé A. Alonso 29 agosto 202123 agosto 2021

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

1	uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ {n m}, n < m → φ n < φ m

1 2	def extraccion (φ : ℕ → ℕ) := ∀ {n m}, n < m → φ n < φ m

Demostrar que si φ es una función de extracción, entonces

   ∀ n, n ≤ φ n

1	∀ n, n ≤ φ n

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

import tactic
open nat

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ) :=
  ∀ {n m}, n < m → φ n < φ m

example :
  extraccion φ → ∀ n, n ≤ φ n :=
sorry

import tactic

open nat

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ) :=

∀ {n m}, n < m → φ n < φ m

example :

extraccion φ → ∀ n, n ≤ φ n :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open nat

variable {φ : ℕ → ℕ}

set_option pp.structure_projections false

def extraccion (φ : ℕ → ℕ) :=
  ∀ {n m}, n < m → φ n < φ m

-- 1ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    have h1 : m < succ m := lt_add_one m,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h h1, },
end

-- 2ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h (lt_add_one m), },
end

-- 3ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
assume h : extraccion φ,
assume n,
nat.rec_on n
  ( show 0 ≤ φ 0,
      from nat.zero_le (φ 0) )
  ( assume m,
    assume HI : m ≤ φ m,
    have h1 : m < succ m,
      from lt_add_one m,
    have h2 : m < φ (succ m), from
      calc m ≤ φ m        : HI
         ... < φ (succ m) : h h1,
    show succ m ≤ φ (succ m),
      from nat.succ_le_of_lt h2)

import tactic

open nat

variable {φ : ℕ → ℕ}

set_option pp.structure_projections false

def extraccion (φ : ℕ → ℕ) :=

∀ {n m}, n < m → φ n < φ m

-- 1ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

begin

intros h n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

have h1 : m < succ m := lt_add_one m,

calc m ≤ φ m : HI

... < φ (succ m) : h h1, },

end

-- 2ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

begin

intros h n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : h (lt_add_one m), },

end

-- 3ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

assume h : extraccion φ,

assume n,

nat.rec_on n

( show 0 ≤ φ 0,

from nat.zero_le (φ 0) )

( assume m,

assume HI : m ≤ φ m,

have h1 : m < succ m,

from lt_add_one m,

have h2 : m < φ (succ m), from

calc m ≤ φ m : HI

... < φ (succ m) : h h1,

show succ m ≤ φ (succ m),

from nat.succ_le_of_lt h2)

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 Relacion_entre_los_indices_de_las_subsucesiones_y_de_la_sucesion
imports Main
begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

(* En la demostración se usará el siguiente lema *)
lemma extraccionE:
  assumes "extraccion φ"
          "n < m"
  shows   "φ n < φ m"
proof -
  have "∀ n m. n < m ⟶ φ n < φ m"
    using assms(1) by (unfold extraccion_def)
  then have "n < m ⟶ φ n < φ m"
    by (elim allE)
  then show "φ n < φ m"
    using assms(2) by (rule mp)
qed

(* 1ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "φ n < φ (Suc n)"
  proof -
    have "n < Suc n"
      by (rule lessI)
    with assms show "φ n < φ (Suc n)"
      by (rule extraccionE)
  qed
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed

(* 2ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "… < φ (Suc n)"
  using assms
  proof (rule extraccionE)
    show "n < Suc n"
      by (rule lessI)
  qed
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed

(* 3ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "… < φ (Suc n)"
    by (rule extraccionE [OF assms lessI])
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed

(* 4ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by simp
next
  fix n
  assume HI : "n ≤ φ n"
  also have "φ n < φ (Suc n)"
    using assms extraccion_def by blast
  finally show "Suc n ≤ φ (Suc n)"
    by simp
qed

end

theory Relacion_entre_los_indices_de_las_subsucesiones_y_de_la_sucesion

imports Main

begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where

"extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

(* En la demostración se usará el siguiente lema *)

lemma extraccionE:

assumes "extraccion φ"

"n < m"

shows "φ n < φ m"

proof -

have "∀ n m. n < m ⟶ φ n < φ m"

using assms(1) by (unfold extraccion_def)

then have "n < m ⟶ φ n < φ m"

by (elim allE)

then show "φ n < φ m"

using assms(2) by (rule mp)

qed

(* 1ª demostración *)

lemma

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0"

by (rule le0)

fix n

assume "n ≤ φ n"

also have "φ n < φ (Suc n)"

proof -

have "n < Suc n"

by (rule lessI)

with assms show "φ n < φ (Suc n)"

by (rule extraccionE)

qed

finally show "Suc n ≤ φ (Suc n)"

by (rule Suc_leI)

qed

(* 2ª demostración *)

lemma

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0"

by (rule le0)

fix n

assume "n ≤ φ n"

also have "… < φ (Suc n)"

using assms

proof (rule extraccionE)

show "n < Suc n"

by (rule lessI)

qed

finally show "Suc n ≤ φ (Suc n)"

by (rule Suc_leI)

qed

(* 3ª demostración *)

lemma

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0"

by (rule le0)

fix n

assume "n ≤ φ n"

also have "… < φ (Suc n)"

by (rule extraccionE [OF assms lessI])

finally show "Suc n ≤ φ (Suc n)"

by (rule Suc_leI)

qed

(* 4ª demostración *)

lemma

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0"

by simp

fix n

assume HI : "n ≤ φ n"

also have "φ n < φ (Suc n)"

using assms extraccion_def by blast

finally show "Suc n ≤ φ (Suc n)"

by simp

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]

Teorema de Nicómaco

PorJosé A. Alonso 30 enero 202021 agosto 2021

Demostrar el teorema de Nicómaco que afirma que la suma de los cubos de los n primeros números naturales es igual que el cuadrado de la suma de los n primeros números naturales; es decir, para todo número natural n se tiene que

1³ + 2³ + ... + n³ = (1 + 2 + ... + n)²

1	1³ + 2³ + ... + n³ = (1 + 2 + ... + n)²

Soluciones con Isabelle/HOL

theory Teorema_de_Nicomaco
imports Main
begin

(* (suma n) es la suma de los primeros números naturales. *)
fun suma :: "nat ⇒ nat" where
  "suma 0 = 0"
| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)
fun sumaCubos :: "nat ⇒ nat" where
  "sumaCubos 0 = 0"
| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)
lemma "2 * suma n = n^2 + n"
proof (induct n)
  show "2 * suma 0 = 0^2 + 0" by simp
next
  fix n
  assume "2 * suma n = n^2 + n"
  then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"
    by simp
  also have "… = (Suc n)^2 + Suc n"
    by (simp add: power2_eq_square)
  finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"
    by this
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_suma:
  "2 * suma n = n^2 + n"
  by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0^2 + 0)^2"
    by simp
next
  fix n
  assume "4 * sumaCubos n = (n^2 + n)^2"
  then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"
    by simp
  then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"
  by (simp add: algebra_simps
                power2_eq_square
                power3_eq_cube )
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_sumaCubos:
  "4 * sumaCubos n = (n^2 + n)^2"
  by (induct n) (auto simp add: algebra_simps
                                power2_eq_square
                                power3_eq_cube)

(* Lema auxiliar *)
lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"
  by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)
theorem teorema_de_Nicomaco:
  "sumaCubos n = (suma n)^2"
  by (simp only: formula_suma formula_sumaCubos aux)

end

theory Teorema_de_Nicomaco

imports Main

begin

(* (suma n) es la suma de los primeros números naturales. *)

fun suma :: "nat ⇒ nat" where

"suma 0 = 0"

| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)

fun sumaCubos :: "nat ⇒ nat" where

"sumaCubos 0 = 0"

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

(* Fórmula para la suma *)

lemma "2 * suma n = n^2 + n"

proof (induct n)

show "2 * suma 0 = 0^2 + 0" by simp

fix n

assume "2 * suma n = n^2 + n"

then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"

by simp

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

by (simp add: power2_eq_square)

finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"

by this

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_suma:

"2 * suma n = n^2 + n"

by (induct n) (auto simp add: power2_eq_square)

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

proof (induct n)

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

by simp

fix n

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

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

by simp

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

by (simp add: algebra_simps

power2_eq_square

power3_eq_cube )

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_sumaCubos:

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

by (induct n) (auto simp add: algebra_simps

power2_eq_square

power3_eq_cube)

(* Lema auxiliar *)

lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"

by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)

theorem teorema_de_Nicomaco:

"sumaCubos n = (suma n)^2"

by (simp only: formula_suma formula_sumaCubos aux)

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>