Inducción – Calculemus

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]

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

Razonamiento sobre árboles binarios: Aplanamiento e imagen especular

PorJosé A. Alonso 13 septiembre 20218 septiembre 2021

El árbol correspondiente a

/ \

2 4

/ \

1 5

se puede representar por el término

   nodo 3 (nodo 2 (hoja 1) (hoja 5)) (hoja 4)

1	nodo 3 (nodo 2 (hoja 1) (hoja 5)) (hoja 4)

usando el tipo de dato arbol definido por

   inductive arbol (α : Type) : Type
   | hoja : α → arbol
   | nodo : α → arbol → arbol → arbol

inductive arbol (α : Type) : Type

| hoja : α → arbol

| nodo : α → arbol → arbol → arbol

La imagen especular del árbol anterior es

/ \

4 2

/ \

5 1

y la lista obtenida aplanándolo (recorriéndolo en orden infijo) es

   [4, 3, 5, 2, 1]

1	[4, 3, 5, 2, 1]

La definición de la función que calcula la imagen especular es

   def espejo : arbol α → arbol α
   | (hoja x)     := hoja x
   | (nodo x i d) := nodo x (espejo d) (espejo i)

def espejo : arbol α → arbol α

| (hoja x) := hoja x

| (nodo x i d) := nodo x (espejo d) (espejo i)

y la que aplana el árbol es

   def aplana : arbol α → list α
   | (hoja x)     := [x]
   | (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)

def aplana : arbol α → list α

| (hoja x) := [x]

| (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)

Demostrar que

   aplana (espejo a) = rev (aplana a)

1	aplana (espejo a) = rev (aplana a)

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

import tactic
open list

variable {α : Type}

inductive arbol (α : Type) : Type
| hoja : α → arbol
| nodo : α → arbol → arbol → arbol

namespace arbol

variables (a i d : arbol α)
variable  (x : α)

def espejo : arbol α → arbol α
| (hoja x)     := hoja x
| (nodo x i d) := nodo x (espejo d) (espejo i)

def aplana : arbol α → list α
| (hoja x)     := [x]
| (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)

example :
  aplana (espejo a) = reverse (aplana a) :=
sorry

end arbol

import tactic

open list

variable {α : Type}

inductive arbol (α : Type) : Type

| hoja : α → arbol

| nodo : α → arbol → arbol → arbol

namespace arbol

variables (a i d : arbol α)

variable (x : α)

def espejo : arbol α → arbol α

| (hoja x) := hoja x

| (nodo x i d) := nodo x (espejo d) (espejo i)

def aplana : arbol α → list α

| (hoja x) := [x]

| (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)

example :

aplana (espejo a) = reverse (aplana a) :=

sorry

end arbol

[expand title=»Soluciones con Lean»]

import tactic
open list

variable {α : Type}

-- Para que no use la notación con puntos
set_option pp.structure_projections false

inductive arbol (α : Type) : Type
| hoja : α → arbol
| nodo : α → arbol → arbol → arbol

namespace arbol

variables (a i d : arbol α)
variable  (x : α)

def espejo : arbol α → arbol α
| (hoja x)     := hoja x
| (nodo x i d) := nodo x (espejo d) (espejo i)

@[simp]
lemma espejo_1 :
  espejo (hoja x) = hoja x :=
rfl

@[simp]
lemma espejo_2 :
  espejo (nodo x i d) = nodo x (espejo d) (espejo i) :=
rfl

def aplana : arbol α → list α
| (hoja x)     := [x]
| (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)

@[simp]
lemma aplana_1 :
  aplana (hoja x) = [x] :=
rfl

@[simp]
lemma aplana_2 :
  aplana (nodo x i d) = (aplana i) ++ [x] ++ (aplana d) :=
rfl

-- 1ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { rw espejo_1,
    rw aplana_1,
    rw reverse_singleton, },
  { rw espejo_2,
    rw aplana_2,
    rw [Hi, Hd],
    rw aplana_2,
    rw reverse_append,
    rw reverse_append,
    rw reverse_singleton,
    rw append_assoc, },
end

-- 2ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { calc aplana (espejo (hoja x))
         = aplana (hoja x)
             : congr_arg aplana (espejo_1 x)
     ... = [x]
             : aplana_1 x
     ... = reverse [x]
             : reverse_singleton x
     ... = reverse (aplana (hoja x))
             : congr_arg reverse (aplana_1 x).symm, },
  { calc aplana (espejo (nodo x i d))
         = aplana (nodo x (espejo d) (espejo i))
             : congr_arg aplana (espejo_2 i d x)
     ... = (aplana (espejo d) ++ [x]) ++ aplana (espejo i)
             : aplana_2 (espejo d) (espejo i) x
     ... = (reverse (aplana d) ++ [x]) ++ aplana (espejo i)
             : congr_arg2 (++) (congr_arg2 (++) Hd rfl) rfl
     ... = (reverse (aplana d) ++ [x]) ++ reverse (aplana i)
             : congr_arg2 (++) rfl Hi
     ... = (reverse (aplana d) ++ reverse [x]) ++ reverse (aplana i)
             : congr_arg2 (++) (congr_arg2 (++) rfl (reverse_singleton x).symm) rfl
     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)
             : congr_arg2 (++) (reverse_append [x] (aplana d)).symm rfl
     ... = reverse (aplana i ++ ([x] ++ aplana d))
             : (reverse_append (aplana i) ([x] ++ aplana d)).symm
     ... = reverse ((aplana i ++ [x]) ++ aplana d)
             : congr_arg reverse (append_assoc (aplana i) [x] (aplana d)).symm
     ... = reverse (aplana (nodo x i d))
             : congr_arg reverse (aplana_2 i d x), },
end

-- 3ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { calc aplana (espejo (hoja x))
         = aplana (hoja x)
             : by simp only [espejo_1]
     ... = [x]
             : by rw aplana_1
     ... = reverse [x]
             : by rw reverse_singleton
     ... = reverse (aplana (hoja x))
             : by simp only [aplana_1], },
  { calc aplana (espejo (nodo x i d))
         = aplana (nodo x (espejo d) (espejo i))
             : by simp only [espejo_2]
     ... = aplana (espejo d) ++ [x] ++ aplana (espejo i)
             : by rw aplana_2
     ... = reverse (aplana d) ++ [x] ++ reverse (aplana i)
             : by rw [Hi, Hd]
     ... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)
             : by simp only [reverse_singleton]
     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)
             : by simp only [reverse_append]
     ... = reverse (aplana i ++ ([x] ++ aplana d))
             : by simp only [reverse_append]
     ... = reverse (aplana i ++ [x] ++ aplana d)
             : by simp only [append_assoc]
     ... = reverse (aplana (nodo x i d))
             : by simp only [aplana_2], },
end

-- 3ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { calc aplana (espejo (hoja x))
         = aplana (hoja x)           : by simp
     ... = [x]                       : by simp
     ... = reverse [x]               : by simp
     ... = reverse (aplana (hoja x)) : by simp, },
  { calc aplana (espejo (nodo x i d))
         = aplana (nodo x (espejo d) (espejo i))
             : by simp
     ... = aplana (espejo d) ++ [x] ++ aplana (espejo i)
             : by simp
     ... = reverse (aplana d) ++ [x] ++ reverse (aplana i)
             : by simp [Hi, Hd]
     ... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)
             : by simp
     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)
             : by simp
     ... = reverse (aplana i ++ ([x] ++ aplana d))
             : by simp
     ... = reverse (aplana i ++ [x] ++ aplana d)
             : by simp
     ... = reverse (aplana (nodo x i d))
             : by simp },
end

-- 5ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { simp, },
  { calc aplana (espejo (nodo x i d))
         = reverse (aplana d) ++ [x] ++ reverse (aplana i)
             : by simp [Hi, Hd]
     ... = reverse (aplana (nodo x i d))
             : by simp },
end

-- 6ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
begin
  induction a with x x i d Hi Hd,
  { simp, },
  { simp [Hi, Hd], },
end

-- 7ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
by induction a ; simp [*]

-- 8ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
arbol.rec_on a
  ( assume x,
    calc aplana (espejo (hoja x))
         = aplana (hoja x)
             : by simp only [espejo_1]
     ... = [x]
             : by rw aplana_1
     ... = reverse [x]
             : by rw reverse_singleton
     ... = reverse (aplana (hoja x))
             : by simp only [aplana_1])
  ( assume x i d,
    assume Hi : aplana (espejo i) = reverse (aplana i),
    assume Hd : aplana (espejo d) = reverse (aplana d),
    calc aplana (espejo (nodo x i d))
         = aplana (nodo x (espejo d) (espejo i))
             : by simp only [espejo_2]
     ... = aplana (espejo d) ++ [x] ++ aplana (espejo i)
             : by rw aplana_2
     ... = reverse (aplana d) ++ [x] ++ reverse (aplana i)
             : by rw [Hi, Hd]
     ... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)
             : by simp only [reverse_singleton]
     ... = reverse ([x] ++ aplana d) ++ reverse (aplana i)
             : by simp only [reverse_append]
     ... = reverse (aplana i ++ ([x] ++ aplana d))
             : by simp only [reverse_append]
     ... = reverse (aplana i ++ [x] ++ aplana d)
             : by simp only [append_assoc]
     ... = reverse (aplana (nodo x i d))
             : by simp only [aplana_2])

-- 9ª demostración
example :
  aplana (espejo a) = reverse (aplana a) :=
arbol.rec_on a
  (λ x, by simp)
  (λ x i d Hi Hd, by simp [Hi, Hd])

-- 10ª demostración
lemma aplana_espejo :
  ∀ a : arbol α, aplana (espejo a) = reverse (aplana a)
| (hoja x)     := by simp
| (nodo x i d) := by simp [aplana_espejo i,
                           aplana_espejo d]

end arbol

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

import tactic

open list

variable {α : Type}

-- Para que no use la notación con puntos

set_option pp.structure_projections false

inductive arbol (α : Type) : Type

| hoja : α → arbol

| nodo : α → arbol → arbol → arbol

namespace arbol

variables (a i d : arbol α)

variable (x : α)

def espejo : arbol α → arbol α

| (hoja x) := hoja x

| (nodo x i d) := nodo x (espejo d) (espejo i)

@[simp]

lemma espejo_1 :

espejo (hoja x) = hoja x :=

rfl

@[simp]

lemma espejo_2 :

espejo (nodo x i d) = nodo x (espejo d) (espejo i) :=

rfl

def aplana : arbol α → list α

| (hoja x) := [x]

| (nodo x i d) := (aplana i) ++ [x] ++ (aplana d)

@[simp]

lemma aplana_1 :

aplana (hoja x) = [x] :=

rfl

@[simp]

lemma aplana_2 :

aplana (nodo x i d) = (aplana i) ++ [x] ++ (aplana d) :=

rfl

-- 1ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

begin

induction a with x x i d Hi Hd,

{ rw espejo_1,

rw aplana_1,

rw reverse_singleton, },

{ rw espejo_2,

rw aplana_2,

rw [Hi, Hd],

rw aplana_2,

rw reverse_append,

rw reverse_singleton,

rw append_assoc, },

end

-- 2ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

begin

induction a with x x i d Hi Hd,

{ calc aplana (espejo (hoja x))

= aplana (hoja x)

: congr_arg aplana (espejo_1 x)

... = [x]

: aplana_1 x

... = reverse [x]

: reverse_singleton x

... = reverse (aplana (hoja x))

: congr_arg reverse (aplana_1 x).symm, },

{ calc aplana (espejo (nodo x i d))

= aplana (nodo x (espejo d) (espejo i))

: congr_arg aplana (espejo_2 i d x)

... = (aplana (espejo d) ++ [x]) ++ aplana (espejo i)

: aplana_2 (espejo d) (espejo i) x

... = (reverse (aplana d) ++ [x]) ++ aplana (espejo i)

: congr_arg2 (++) (congr_arg2 (++) Hd rfl) rfl

... = (reverse (aplana d) ++ [x]) ++ reverse (aplana i)

: congr_arg2 (++) rfl Hi

... = (reverse (aplana d) ++ reverse [x]) ++ reverse (aplana i)

: congr_arg2 (++) (congr_arg2 (++) rfl (reverse_singleton x).symm) rfl

... = reverse ([x] ++ aplana d) ++ reverse (aplana i)

: congr_arg2 (++) (reverse_append [x] (aplana d)).symm rfl

... = reverse (aplana i ++ ([x] ++ aplana d))

: (reverse_append (aplana i) ([x] ++ aplana d)).symm

... = reverse ((aplana i ++ [x]) ++ aplana d)

: congr_arg reverse (append_assoc (aplana i) [x] (aplana d)).symm

... = reverse (aplana (nodo x i d))

: congr_arg reverse (aplana_2 i d x), },

end

-- 3ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

begin

induction a with x x i d Hi Hd,

{ calc aplana (espejo (hoja x))

= aplana (hoja x)

: by simp only [espejo_1]

... = [x]

: by rw aplana_1

... = reverse [x]

: by rw reverse_singleton

... = reverse (aplana (hoja x))

: by simp only [aplana_1], },

{ calc aplana (espejo (nodo x i d))

= aplana (nodo x (espejo d) (espejo i))

: by simp only [espejo_2]

... = aplana (espejo d) ++ [x] ++ aplana (espejo i)

: by rw aplana_2

... = reverse (aplana d) ++ [x] ++ reverse (aplana i)

: by rw [Hi, Hd]

... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)

: by simp only [reverse_singleton]

... = reverse ([x] ++ aplana d) ++ reverse (aplana i)

: by simp only [reverse_append]

... = reverse (aplana i ++ ([x] ++ aplana d))

: by simp only [reverse_append]

... = reverse (aplana i ++ [x] ++ aplana d)

: by simp only [append_assoc]

... = reverse (aplana (nodo x i d))

: by simp only [aplana_2], },

end

-- 3ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

begin

induction a with x x i d Hi Hd,

{ calc aplana (espejo (hoja x))

= aplana (hoja x) : by simp

... = [x] : by simp

... = reverse [x] : by simp

... = reverse (aplana (hoja x)) : by simp, },

{ calc aplana (espejo (nodo x i d))

= aplana (nodo x (espejo d) (espejo i))

: by simp

... = aplana (espejo d) ++ [x] ++ aplana (espejo i)

: by simp

... = reverse (aplana d) ++ [x] ++ reverse (aplana i)

: by simp [Hi, Hd]

... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)

: by simp

... = reverse ([x] ++ aplana d) ++ reverse (aplana i)

: by simp

... = reverse (aplana i ++ ([x] ++ aplana d))

: by simp

... = reverse (aplana i ++ [x] ++ aplana d)

: by simp

... = reverse (aplana (nodo x i d))

: by simp },

end

-- 5ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

begin

induction a with x x i d Hi Hd,

{ simp, },

{ calc aplana (espejo (nodo x i d))

= reverse (aplana d) ++ [x] ++ reverse (aplana i)

: by simp [Hi, Hd]

... = reverse (aplana (nodo x i d))

: by simp },

end

-- 6ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

begin

induction a with x x i d Hi Hd,

{ simp, },

{ simp [Hi, Hd], },

end

-- 7ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

by induction a ; simp [*]

-- 8ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

arbol.rec_on a

( assume x,

calc aplana (espejo (hoja x))

= aplana (hoja x)

: by simp only [espejo_1]

... = [x]

: by rw aplana_1

... = reverse [x]

: by rw reverse_singleton

... = reverse (aplana (hoja x))

: by simp only [aplana_1])

( assume x i d,

assume Hi : aplana (espejo i) = reverse (aplana i),

assume Hd : aplana (espejo d) = reverse (aplana d),

calc aplana (espejo (nodo x i d))

= aplana (nodo x (espejo d) (espejo i))

: by simp only [espejo_2]

... = aplana (espejo d) ++ [x] ++ aplana (espejo i)

: by rw aplana_2

... = reverse (aplana d) ++ [x] ++ reverse (aplana i)

: by rw [Hi, Hd]

... = reverse (aplana d) ++ reverse [x] ++ reverse (aplana i)

: by simp only [reverse_singleton]

... = reverse ([x] ++ aplana d) ++ reverse (aplana i)

: by simp only [reverse_append]

... = reverse (aplana i ++ ([x] ++ aplana d))

: by simp only [reverse_append]

... = reverse (aplana i ++ [x] ++ aplana d)

: by simp only [append_assoc]

... = reverse (aplana (nodo x i d))

: by simp only [aplana_2])

-- 9ª demostración

example :

aplana (espejo a) = reverse (aplana a) :=

arbol.rec_on a

(λ x, by simp)

(λ x i d Hi Hd, by simp [Hi, Hd])

-- 10ª demostración

lemma aplana_espejo :

∀ a : arbol α, aplana (espejo a) = reverse (aplana a)

| (hoja x) := by simp

| (nodo x i d) := by simp [aplana_espejo i,

aplana_espejo d]

end arbol

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

datatype 'a arbol = hoja "'a"
                  | nodo "'a" "'a arbol" "'a arbol"

fun espejo :: "'a arbol ⇒ 'a arbol" where
  "espejo (hoja x)     = (hoja x)"
| "espejo (nodo x i d) = (nodo x (espejo d) (espejo i))"

fun aplana :: "'a arbol ⇒ 'a list" where
  "aplana (hoja x)     = [x]"
| "aplana (nodo x i d) = (aplana i) @ [x] @ (aplana d)"

(* Lema auxiliar *)
(* ============= *)

(* 1ª demostración del lema auxiliar *)
lemma "rev [x] = [x]"
proof -
  have "rev [x] = rev [] @ [x]"
    by (simp only: rev.simps(2))
  also have "… = [] @ [x]"
    by (simp only: rev.simps(1))
  also have "… = [x]"
    by (simp only: append.simps(1))
  finally show ?thesis
    by this
qed

(* 2ª demostración del lema auxiliar *)
lemma rev_unit: "rev [x] = [x]"
by simp

(* Lema principal *)
(* ============== *)

(* ?ª demostración *)
lemma
  fixes a :: "'b arbol"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x :: 'b
  have "aplana (espejo (hoja x)) = aplana (hoja x)"
    by (simp only: espejo.simps(1))
  also have "… = [x]"
    by (simp only: aplana.simps(1))
  also have "… = rev [x]"
    by (rule rev_unit [symmetric])
  also have "… = rev (aplana (hoja x))"
    by (simp only: aplana.simps(1))
  finally show "?P (hoja x)"
    by this
next
  fix x :: 'b
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (nodo x i d)"
  proof -
    have "aplana (espejo (nodo x i d)) =
          aplana (nodo x (espejo d) (espejo i))"
      by (simp only: espejo.simps(2))
    also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))"
      by (simp only: aplana.simps(2))
    also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))"
      by (simp only: h1 h2)
    also have "… = rev ((aplana i) @ [x] @ (aplana d))"
      by (simp only: rev_append rev_unit append_assoc)
    also have "… = rev (aplana (nodo x i d))"
      by (simp only: aplana.simps(2))
    finally show ?thesis
      by this
 qed
qed

(* 2ª demostración *)
lemma
  fixes a :: "'b arbol"
  shows "aplana (espejo a) = rev (aplana a)" (is "?P a")
proof (induct a)
  fix x
  show "?P (hoja x)" by simp
next
  fix x
  fix i assume h1: "?P i"
  fix d assume h2: "?P d"
  show "?P (nodo x i d)"
  proof -
    have "aplana (espejo (nodo x i d)) =
          aplana (nodo x (espejo d) (espejo i))" by simp
    also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))"
      by simp
    also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))"
      using h1 h2 by simp
    also have "… = rev ((aplana i) @ [x] @ (aplana d))" by simp
    also have "… = rev (aplana (nodo x i d))" by simp
    finally show ?thesis .
 qed
qed

(* 3ª demostración *)
lemma "aplana (espejo a) = rev (aplana a)"
proof (induct a)
case (hoja x)
then show ?case by simp
next
  case (nodo x i d)
  then show ?case by simp
qed

(* 4ª demostración *)
lemma "aplana (espejo a) = rev (aplana a)"
  by (induct a) simp_all

end

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

theory Razonamiento_sobre_arboles_binarios_Aplanamiento_e_imagen_especular

imports Main

begin

datatype 'a arbol = hoja "'a"

| nodo "'a" "'a arbol" "'a arbol"

fun espejo :: "'a arbol ⇒ 'a arbol" where

"espejo (hoja x) = (hoja x)"

| "espejo (nodo x i d) = (nodo x (espejo d) (espejo i))"

fun aplana :: "'a arbol ⇒ 'a list" where

"aplana (hoja x) = [x]"

| "aplana (nodo x i d) = (aplana i) @ [x] @ (aplana d)"

(* Lema auxiliar *)

(* ============= *)

(* 1ª demostración del lema auxiliar *)

lemma "rev [x] = [x]"

proof -

have "rev [x] = rev [] @ [x]"

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

also have "… = [] @ [x]"

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

also have "… = [x]"

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

finally show ?thesis

by this

qed

(* 2ª demostración del lema auxiliar *)

lemma rev_unit: "rev [x] = [x]"

by simp

(* Lema principal *)

(* ============== *)

(* ?ª demostración *)

lemma

fixes a :: "'b arbol"

shows "aplana (espejo a) = rev (aplana a)" (is "?P a")

proof (induct a)

fix x :: 'b

have "aplana (espejo (hoja x)) = aplana (hoja x)"

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

also have "… = [x]"

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

also have "… = rev [x]"

by (rule rev_unit [symmetric])

also have "… = rev (aplana (hoja x))"

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

finally show "?P (hoja x)"

by this

fix x :: 'b

fix i assume h1: "?P i"

fix d assume h2: "?P d"

show "?P (nodo x i d)"

proof -

have "aplana (espejo (nodo x i d)) =

aplana (nodo x (espejo d) (espejo i))"

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

also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))"

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

also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))"

by (simp only: h1 h2)

also have "… = rev ((aplana i) @ [x] @ (aplana d))"

by (simp only: rev_append rev_unit append_assoc)

also have "… = rev (aplana (nodo x i d))"

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

finally show ?thesis

by this

qed

(* 2ª demostración *)

lemma

fixes a :: "'b arbol"

shows "aplana (espejo a) = rev (aplana a)" (is "?P a")

proof (induct a)

fix x

show "?P (hoja x)" by simp

fix x

fix i assume h1: "?P i"

fix d assume h2: "?P d"

show "?P (nodo x i d)"

proof -

have "aplana (espejo (nodo x i d)) =

aplana (nodo x (espejo d) (espejo i))" by simp

also have "… = (aplana (espejo d)) @ [x] @ (aplana (espejo i))"

by simp

also have "… = (rev (aplana d)) @ [x] @ (rev (aplana i))"

using h1 h2 by simp

also have "… = rev ((aplana i) @ [x] @ (aplana d))" by simp

also have "… = rev (aplana (nodo x i d))" by simp

finally show ?thesis .

qed

(* 3ª demostración *)

lemma "aplana (espejo a) = rev (aplana a)"

proof (induct a)

case (hoja x)

then show ?case by simp

case (nodo x i d)

then show ?case by simp

qed

(* 4ª demostración *)

lemma "aplana (espejo a) = rev (aplana a)"

by (induct a) 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]