José A. Alonso

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]

Si f es continua en a y el límite de u(n) es a, entonces el límite de f(u(n)) es f(a)

PorJosé A. Alonso 17 septiembre 202114 septiembre 2021

En Lean, se puede definir que a es el límite de la sucesión u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, \|u n - a\| < ε

y que f es continua en a por

   def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

1 2	def continua_en_punto (f : ℝ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ δ > 0, ∀ x, \|x - a\| ≤ δ → \|f x - f a\| ≤ ε

Demostrar que si f es continua en a y el límite de uₙ es a, entonces el límite de f(uₙ) es f(a).

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

import data.real.basic

variable {f : ℝ → ℝ}
variable {a : ℝ}
variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
sorry

import data.real.basic

variable {f : ℝ → ℝ}

variable {a : ℝ}

variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable {f : ℝ → ℝ}
variable {a : ℝ}
variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

-- 1ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,
  cases hu δ hδ1 with k hk,
  use k,
  intros n hn,
  apply hδ2,
  exact hk n hn,
end

-- 2ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,
  cases hu δ hδ1 with k hk,
  exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,
end

-- 3ª demostración
example
  (hf : continua_en_punto f a)
  (hu : limite u a)
  : limite (f ∘ u) (f a) :=
begin
  intros ε hε,
  obtain ⟨δ, hδ1, hδ2⟩ := hf ε hε,
  obtain ⟨k, hk⟩ := hu δ hδ1,
  exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,
end

import data.real.basic

variable {f : ℝ → ℝ}

variable {a : ℝ}

variable {u : ℕ → ℝ}

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| ≤ ε

def continua_en_punto (f : ℝ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ δ > 0, ∀ x, |x - a| ≤ δ → |f x - f a| ≤ ε

-- 1ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,

cases hu δ hδ1 with k hk,

use k,

intros n hn,

apply hδ2,

exact hk n hn,

end

-- 2ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

rcases hf ε hε with ⟨δ, hδ1, hδ2⟩,

cases hu δ hδ1 with k hk,

exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,

end

-- 3ª demostración

example

(hf : continua_en_punto f a)

(hu : limite u a)

: limite (f ∘ u) (f a) :=

begin

intros ε hε,

obtain ⟨δ, hδ1, hδ2⟩ := hf ε hε,

obtain ⟨k, hk⟩ := hu δ hδ1,

exact ⟨k, λ n hn, hδ2 (u n) (hk n hn)⟩,

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 CS_de_continuidad
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

definition continua_en_punto :: "(real ⇒ real) ⇒ real ⇒ bool" where
  "continua_en_punto f a ⟷
   (∀ε>0. ∃δ>0. ∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

(* 1ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
  proof (intro allI impI)
    fix n
    assume "n ≥ k"
    then have "¦u n - a¦ ≤ δ"
      using hk by auto
    then show "¦(f ∘ u) n - f a¦ ≤ ε"
      using hδ2 by simp
  qed
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    by auto
qed

(* 2ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hk hδ2 by simp
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    by auto
qed

(* 3ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where hδ1 : "δ > 0" and
                      hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def hδ1 by auto
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hk hδ2 by auto
qed

(* 4ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "0 < ε"
  then obtain δ where
              hδ : "δ > 0 ∧ (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"
    using assms(1) continua_en_punto_def by auto
  then obtain k where "∀n≥k. ¦u n - a¦ ≤ δ"
    using assms(2) limite_def by auto
  then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"
    using hδ by auto
qed

(* 5ª demostración *)
lemma
  assumes "continua_en_punto f a"
          "limite u a"
  shows "limite (f ∘ u) (f a)"
  using assms continua_en_punto_def limite_def
  by force

end

theory CS_de_continuidad

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ ≤ ε)"

definition continua_en_punto :: "(real ⇒ real) ⇒ real ⇒ bool" where

"continua_en_punto f a ⟷

(∀ε>0. ∃δ>0. ∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

(* 1ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def hδ1 by auto

have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

proof (intro allI impI)

fix n

assume "n ≥ k"

then have "¦u n - a¦ ≤ δ"

using hk by auto

then show "¦(f ∘ u) n - f a¦ ≤ ε"

using hδ2 by simp

qed

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

by auto

qed

(* 2ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def hδ1 by auto

have "∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hk hδ2 by simp

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

by auto

qed

(* 3ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where hδ1 : "δ > 0" and

hδ2 :" (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

obtain k where hk : "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def hδ1 by auto

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hk hδ2 by auto

qed

(* 4ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

proof (unfold limite_def; intro allI impI)

fix ε :: real

assume "0 < ε"

then obtain δ where

hδ : "δ > 0 ∧ (∀x. ¦x - a¦ ≤ δ ⟶ ¦f x - f a¦ ≤ ε)"

using assms(1) continua_en_punto_def by auto

then obtain k where "∀n≥k. ¦u n - a¦ ≤ δ"

using assms(2) limite_def by auto

then show "∃k. ∀n≥k. ¦(f ∘ u) n - f a¦ ≤ ε"

using hδ by auto

qed

(* 5ª demostración *)

lemma

assumes "continua_en_punto f a"

"limite u a"

shows "limite (f ∘ u) (f a)"

using assms continua_en_punto_def limite_def

by force

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]

Los límites son menores o iguales que las cotas superiores

PorJosé A. Alonso 16 septiembre 202111 septiembre 2021

En Lean, se puede definir que a es el límite de la sucesión u por

   def limite (u : ℕ → ℝ) (a : ℝ) :=
     ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

1 2	def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ k, ∀ n ≥ k, \|u n - a\| < ε

y que a es una cota superior de u por

   def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
     ∀ n, u n ≤ a

1 2	def cota_superior (u : ℕ → ℝ) (a : ℝ) := ∀ n, u n ≤ a

Demostrar que si x es el límite de la sucesión u e y es una cota superior de u, entonces x ≤ y.

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

import data.real.basic

variable  (u : ℕ → ℝ)
variables (x y : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
  ∀ n, u n ≤ a

example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
sorry

import data.real.basic

variable (u : ℕ → ℝ)

variables (x y : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=

∀ n, u n ≤ a

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variable  (u : ℕ → ℝ)
variables (x y : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=
  ∀ n, u n ≤ a

lemma aux :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split ; linarith,
end

-- 1º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k rfl.ge,
  replace hk : -ε < u k - x := neg_lt_of_abs_lt hk,
  replace hk : x < u k + ε := neg_lt_sub_iff_lt_add'.mp hk,
  apply le_of_lt,
  exact lt_add_of_lt_add_right hk (hy k),
end

-- 2º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k rfl.ge,
  apply le_of_lt,
  calc x < u k + ε : neg_lt_sub_iff_lt_add'.mp (neg_lt_of_abs_lt hk)
     ... ≤ y + ε   : add_le_add_right (hy k) ε,
end

-- 3º demostración
example
  (hx : limite u x)
  (hy : cota_superior u y)
  : x ≤ y :=
begin
  apply aux,
  intros ε hε,
  cases hx ε hε with k hk,
  specialize hk k (by linarith),
  rw abs_lt at hk,
  linarith [hy k],
end

import data.real.basic

variable (u : ℕ → ℝ)

variables (x y : ℝ)

notation `|`x`|` := abs x

def limite (u : ℕ → ℝ) (a : ℝ) :=

∀ ε > 0, ∃ k, ∀ n ≥ k, |u n - a| < ε

def cota_superior (u : ℕ → ℝ) (a : ℝ) :=

∀ n, u n ≤ a

lemma aux :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split ; linarith,

end

-- 1º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k rfl.ge,

replace hk : -ε < u k - x := neg_lt_of_abs_lt hk,

replace hk : x < u k + ε := neg_lt_sub_iff_lt_add'.mp hk,

apply le_of_lt,

exact lt_add_of_lt_add_right hk (hy k),

end

-- 2º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k rfl.ge,

apply le_of_lt,

calc x < u k + ε : neg_lt_sub_iff_lt_add'.mp (neg_lt_of_abs_lt hk)

... ≤ y + ε : add_le_add_right (hy k) ε,

end

-- 3º demostración

example

(hx : limite u x)

(hy : cota_superior u y)

: x ≤ y :=

begin

apply aux,

intros ε hε,

cases hx ε hε with k hk,

specialize hk k (by linarith),

rw abs_lt at hk,

linarith [hy k],

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 Los_limites_son_menores_o_iguales_que_las_cotas_superiores
imports Main HOL.Real
begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"

definition cota_superior :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "cota_superior u c ⟷ (∀n. u n ≤ c)"

(* 1ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then have "¦u k - x¦ < ε"
    by simp
  then have "-ε < u k - x"
    by simp
  then have "x < u k + ε"
    by simp
  moreover have "u k ≤ y"
    using assms(2) cota_superior_def by simp
  ultimately show "x ≤ y + ε"
    by simp
qed

(* 2ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then have "x < u k + ε"
    by auto
  moreover have "u k ≤ y"
    using assms(2) cota_superior_def by simp
  ultimately show "x ≤ y + ε"
    by simp
qed

(* 3ª demostración *)
lemma
  fixes x y :: real
  assumes "limite u x"
          "cota_superior u y"
  shows   "x ≤ y"
proof (rule field_le_epsilon)
  fix ε :: real
  assume "0 < ε"
  then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"
    using assms(1) limite_def by auto
  then show "x ≤ y + ε"
    using assms(2) cota_superior_def
    by (smt (verit) order_refl)
qed

end

theory Los_limites_son_menores_o_iguales_que_las_cotas_superiores

imports Main HOL.Real

begin

definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"

definition cota_superior :: "(nat ⇒ real) ⇒ real ⇒ bool" where

"cota_superior u c ⟷ (∀n. u n ≤ c)"

(* 1ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then have "¦u k - x¦ < ε"

by simp

then have "-ε < u k - x"

by simp

then have "x < u k + ε"

by simp

moreover have "u k ≤ y"

using assms(2) cota_superior_def by simp

ultimately show "x ≤ y + ε"

by simp

qed

(* 2ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then have "x < u k + ε"

by auto

moreover have "u k ≤ y"

using assms(2) cota_superior_def by simp

ultimately show "x ≤ y + ε"

by simp

qed

(* 3ª demostración *)

lemma

fixes x y :: real

assumes "limite u x"

"cota_superior u y"

shows "x ≤ y"

proof (rule field_le_epsilon)

fix ε :: real

assume "0 < ε"

then obtain k where hk : "∀n≥k. ¦u n - x¦ < ε"

using assms(1) limite_def by auto

then show "x ≤ y + ε"

using assms(2) cota_superior_def

by (smt (verit) order_refl)

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]

Pruebas de «(∀ ε > 0, y ≤ x + ε) → y ≤ x»

PorJosé A. Alonso 15 septiembre 202110 septiembre 2021

Sean x, y ∈ ℝ. Demostrar que

   (∀ ε > 0, y ≤ x + ε) →  y ≤ x

1	(∀ ε > 0, y ≤ x + ε) → y ≤ x

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

import data.real.basic

variables {x y : ℝ}

example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
sorry

import data.real.basic

variables {x y : ℝ}

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic

variables {x y : ℝ}

-- 1ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split,
  { apply half_pos,
    exact sub_pos.mpr h, },
  { calc x + (y - x) / 2
         = (x + y) / 2   : by ring_nf
     ... < (y + y) / 2   : div_lt_div_of_lt zero_lt_two (add_lt_add_right h y)
     ... = (2 * y) / 2   : congr_arg2 (/) (two_mul y).symm rfl
     ... = y             : by ring_nf, },
end

-- 2ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split,
  { exact half_pos (sub_pos.mpr h), },
  { calc x + (y - x) / 2
         = (x + y) / 2   : by ring_nf
     ... < (y + y) / 2   : by linarith
     ... = (2 * y) / 2   : by ring_nf
     ... = y             : by ring_nf, },
end

-- 3ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split,
  { linarith },
  { linarith },
end

-- 4ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  contrapose!,
  intro h,
  use (y-x)/2,
  split ; linarith,
end

-- 5ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  intro h1,
  by_contradiction h2,
  replace h2 : x < y := not_le.mp h2,
  rcases (exists_between h2) with ⟨z, h3, h4⟩,
  replace h3 : 0 < z - x := sub_pos.mpr h3,
  replace h1 : y ≤ x + (z - x) := h1 (z - x) h3,
  replace h1 : y ≤ z := by finish,
  have h4 : y < y := gt_of_gt_of_ge h4 h1,
  exact absurd h4 (irrefl y),
end

-- 6ª demostración
example :
  (∀ ε > 0, y ≤ x + ε) → y ≤ x :=
begin
  intro h1,
  by_contradiction h2,
  replace h2 : x < y := not_le.mp h2,
  rcases (exists_between h2) with ⟨z, hxz, hzy⟩,
  apply lt_irrefl y,
  calc y ≤ x + (z - x) : h1 (z - x) (sub_pos.mpr hxz)
     ... = z           : by ring
     ... < y           : hzy,
end

import data.real.basic

variables {x y : ℝ}

-- 1ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split,

{ apply half_pos,

exact sub_pos.mpr h, },

{ calc x + (y - x) / 2

= (x + y) / 2 : by ring_nf

... < (y + y) / 2 : div_lt_div_of_lt zero_lt_two (add_lt_add_right h y)

... = (2 * y) / 2 : congr_arg2 (/) (two_mul y).symm rfl

... = y : by ring_nf, },

end

-- 2ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split,

{ exact half_pos (sub_pos.mpr h), },

{ calc x + (y - x) / 2

= (x + y) / 2 : by ring_nf

... < (y + y) / 2 : by linarith

... = (2 * y) / 2 : by ring_nf

... = y : by ring_nf, },

end

-- 3ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split,

{ linarith },

end

-- 4ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

contrapose!,

intro h,

use (y-x)/2,

split ; linarith,

end

-- 5ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

intro h1,

by_contradiction h2,

replace h2 : x < y := not_le.mp h2,

rcases (exists_between h2) with ⟨z, h3, h4⟩,

replace h3 : 0 < z - x := sub_pos.mpr h3,

replace h1 : y ≤ x + (z - x) := h1 (z - x) h3,

replace h1 : y ≤ z := by finish,

have h4 : y < y := gt_of_gt_of_ge h4 h1,

exact absurd h4 (irrefl y),

end

-- 6ª demostración

example :

(∀ ε > 0, y ≤ x + ε) → y ≤ x :=

begin

intro h1,

by_contradiction h2,

replace h2 : x < y := not_le.mp h2,

rcases (exists_between h2) with ⟨z, hxz, hzy⟩,

apply lt_irrefl y,

calc y ≤ x + (z - x) : h1 (z - x) (sub_pos.mpr hxz)

... = z : by ring

... < y : hzy,

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 CS_de_y_le_x
imports Main HOL.Real
begin

(* 1ª demostración *)
lemma
  fixes x y :: real
  shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"
proof (rule impI)
  assume h1 : "(∀ε>0. y ≤ x + ε)"
  show "y ≤ x"
  proof (rule ccontr)
    assume "¬ (y ≤ x)"
    then have "x < y"
      by simp
    then have "(y - x) / 2 > 0"
      by simp
    then have "y ≤ x + (y - x) / 2"
      using h1 by blast
    then have "2 * y ≤ 2 * x + (y - x)"
      by argo
    then have "y ≤ x"
      by simp
    then show False
      using ‹¬ (y ≤ x)› by simp
  qed
qed

(* 2ª demostración *)
lemma
  fixes x y :: real
  shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"
proof (rule impI)
  assume h1 : "(∀ε>0. y ≤ x + ε)"
  show "y ≤ x"
  proof (rule ccontr)
    assume "¬ (y ≤ x)"
    then have "x < y"
      by simp
    then obtain z where hz : "x < z ∧ z < y"
      using Rats_dense_in_real by blast
    then have "0 < z -x"
      by simp
    then have "y ≤ x + (z - x)"
      using h1 by blast
    then have "y ≤ z"
      by simp
    then show False
      using hz by simp
  qed
qed

(* 3ª demostración *)
lemma
  fixes x y :: real
  shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"
proof (rule impI)
  assume h1 : "(∀ε>0. y ≤ x + ε)"
  show "y ≤ x"
  proof (rule dense_le)
    fix z
    assume "z < y"
    then have "0 < y - z"
      by simp
    then have "y ≤ x + (y - z)"
      using h1 by simp
    then have "0 ≤ x - z"
      by simp
    then show "z ≤ x"
      by simp
  qed
qed

(* 4ª demostración *)
lemma
  fixes x y :: real
  shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"
  by (simp add: field_le_epsilon)

end

theory CS_de_y_le_x

imports Main HOL.Real

begin

(* 1ª demostración *)

lemma

fixes x y :: real

shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"

proof (rule impI)

assume h1 : "(∀ε>0. y ≤ x + ε)"

show "y ≤ x"

proof (rule ccontr)

assume "¬ (y ≤ x)"

then have "x < y"

by simp

then have "(y - x) / 2 > 0"

by simp

then have "y ≤ x + (y - x) / 2"

using h1 by blast

then have "2 * y ≤ 2 * x + (y - x)"

by argo

then have "y ≤ x"

by simp

then show False

using ‹¬ (y ≤ x)› by simp

qed

(* 2ª demostración *)

lemma

fixes x y :: real

shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"

proof (rule impI)

assume h1 : "(∀ε>0. y ≤ x + ε)"

show "y ≤ x"

proof (rule ccontr)

assume "¬ (y ≤ x)"

then have "x < y"

by simp

then obtain z where hz : "x < z ∧ z < y"

using Rats_dense_in_real by blast

then have "0 < z -x"

by simp

then have "y ≤ x + (z - x)"

using h1 by blast

then have "y ≤ z"

by simp

then show False

using hz by simp

qed

(* 3ª demostración *)

lemma

fixes x y :: real

shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"

proof (rule impI)

assume h1 : "(∀ε>0. y ≤ x + ε)"

show "y ≤ x"

proof (rule dense_le)

fix z

assume "z < y"

then have "0 < y - z"

by simp

then have "y ≤ x + (y - z)"

using h1 by simp

then have "0 ≤ x - z"

by simp

then show "z ≤ x"

by simp

qed

(* 4ª demostración *)

lemma

fixes x y :: real

shows "(∀ε>0. y ≤ x + ε) ⟶ y ≤ x"

by (simp add: field_le_epsilon)

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]

Si x es el supremo de A, entonces ∀ y, y < x → ∃ a ∈ A, y < a

PorJosé A. Alonso 14 septiembre 20218 septiembre 2021

En Lean se puede definir que x es una cota superior de A por

   def cota_superior (A : set ℝ) (x : ℝ) :=
     ∀ a ∈ A, a ≤ x

1 2	def cota_superior (A : set ℝ) (x : ℝ) := ∀ a ∈ A, a ≤ x

y x es el supremo de A por

   def es_supremo (A : set ℝ) (x : ℝ) :=
     cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

1 2	def es_supremo (A : set ℝ) (x : ℝ) := cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

Demostrar que si x es el supremo de A, entonces

   ∀ y, y < x → ∃ a ∈ A, y < a

1	∀ y, y < x → ∃ a ∈ A, y < a

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

import data.real.basic
variable {A : set ℝ}
variable {x : ℝ}

def cota_superior (A : set ℝ) (x : ℝ) :=
  ∀ a ∈ A, a ≤ x

def es_supremo (A : set ℝ) (x : ℝ) :=
  cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
sorry

import data.real.basic

variable {A : set ℝ}

variable {x : ℝ}

def cota_superior (A : set ℝ) (x : ℝ) :=

∀ a ∈ A, a ≤ x

def es_supremo (A : set ℝ) (x : ℝ) :=

cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

sorry

[expand title=»Soluciones con Lean»]

import data.real.basic
variable {A : set ℝ}
variable {x : ℝ}

def cota_superior (A : set ℝ) (x : ℝ) :=
  ∀ a ∈ A, a ≤ x

def es_supremo (A : set ℝ) (x : ℝ) :=
  cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

-- 1ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  by_contradiction,
  push_neg at h,
  have h1 : x ≤ y := hx.2 y h,
  replace h1 : ¬(y < x) := not_lt_of_le h1,
  exact h1 hy,
end

-- 2ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  by_contradiction,
  push_neg at h,
  apply absurd hy,
  apply not_lt_of_le,
  apply hx.2 y,
  exact h,
end

-- 3ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  by_contradiction,
  push_neg at h,
  exact absurd hy (not_lt_of_le (hx.2 y h)),
end

-- 4ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  contrapose hy,
  push_neg at hy,
  push_neg,
  unfold es_supremo at hx,
  cases hx with h1 h2,
  apply h2 y,
  unfold cota_superior,
  exact hy,
end

-- 5ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  contrapose hy,
  push_neg at hy,
  push_neg,
  cases hx with h1 h2,
  exact h2 y hy,
end

-- 6ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intros y hy,
  contrapose hy,
  push_neg at hy,
  push_neg,
  exact hx.right y hy,
end

-- 7ª demostración
example
  (hx : es_supremo A x)
  : ∀ y, y < x → ∃ a ∈ A, y < a :=
begin
  intro y,
  contrapose!,
  exact hx.right y,
end

import data.real.basic

variable {A : set ℝ}

variable {x : ℝ}

def cota_superior (A : set ℝ) (x : ℝ) :=

∀ a ∈ A, a ≤ x

def es_supremo (A : set ℝ) (x : ℝ) :=

cota_superior A x ∧ ∀ y, cota_superior A y → x ≤ y

-- 1ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

by_contradiction,

push_neg at h,

have h1 : x ≤ y := hx.2 y h,

replace h1 : ¬(y < x) := not_lt_of_le h1,

exact h1 hy,

end

-- 2ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

by_contradiction,

push_neg at h,

apply absurd hy,

apply not_lt_of_le,

apply hx.2 y,

exact h,

end

-- 3ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

by_contradiction,

push_neg at h,

exact absurd hy (not_lt_of_le (hx.2 y h)),

end

-- 4ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

contrapose hy,

push_neg at hy,

push_neg,

unfold es_supremo at hx,

cases hx with h1 h2,

apply h2 y,

unfold cota_superior,

exact hy,

end

-- 5ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

contrapose hy,

push_neg at hy,

push_neg,

cases hx with h1 h2,

exact h2 y hy,

end

-- 6ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intros y hy,

contrapose hy,

push_neg at hy,

push_neg,

exact hx.right y hy,

end

-- 7ª demostración

example

(hx : es_supremo A x)

: ∀ y, y < x → ∃ a ∈ A, y < a :=

begin

intro y,

contrapose!,

exact hx.right y,

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 "Si_x_es_el_supremo_de_A_entonces_forall_y_y_lt_x_to_exists_a_in_A_y_lt_a"
  imports Main HOL.Real
begin

definition cota_superior :: "(real set) ⇒ real ⇒ bool" where
  "cota_superior A x ⟷ (∀a∈A. a ≤ x)"

definition es_supremo :: "(real set) ⇒ real ⇒ bool" where
  "es_supremo A x ⟷ (cota_superior A x ∧
                       (∀ y. cota_superior A y ⟶ x ≤ y))"

(* 1ª demostración *)
lemma
  assumes "es_supremo A x"
  shows   "∀y<x. ∃a∈A. y < a"
proof (intro allI impI)
  fix y
  assume "y < x"
  show "∃a∈A. y < a"
  proof (rule ccontr)
    assume "¬ (∃a∈A. y < a)"
    then have "∀a∈A. a ≤ y"
      by auto
    then have "cota_superior A y"
      using cota_superior_def by simp
    then have "x ≤ y"
      using assms es_supremo_def by simp
    then have "x < x"
      using ‹y < x› by simp
    then show False by simp
  qed
qed

(* 2ª demostración *)
lemma
  assumes "es_supremo A x"
  shows   "∀y<x. ∃a∈A. y < a"
proof (intro allI impI)
  fix y
  assume "y < x"
  show "∃a∈A. y < a"
  proof (rule ccontr)
    assume "¬ (∃a∈A. y < a)"
    then have "cota_superior A y"
      using cota_superior_def by auto
    then show "False"
      using assms es_supremo_def ‹y < x› by auto
  qed
qed


end

theory "Si_x_es_el_supremo_de_A_entonces_forall_y_y_lt_x_to_exists_a_in_A_y_lt_a"

imports Main HOL.Real

begin

definition cota_superior :: "(real set) ⇒ real ⇒ bool" where

"cota_superior A x ⟷ (∀a∈A. a ≤ x)"

definition es_supremo :: "(real set) ⇒ real ⇒ bool" where

"es_supremo A x ⟷ (cota_superior A x ∧

(∀ y. cota_superior A y ⟶ x ≤ y))"

(* 1ª demostración *)

lemma

assumes "es_supremo A x"

shows "∀y<x. ∃a∈A. y < a"

proof (intro allI impI)

fix y

assume "y < x"

show "∃a∈A. y < a"

proof (rule ccontr)

assume "¬ (∃a∈A. y < a)"

then have "∀a∈A. a ≤ y"

by auto

then have "cota_superior A y"

using cota_superior_def by simp

then have "x ≤ y"

using assms es_supremo_def by simp

then have "x < x"

using ‹y < x› by simp

then show False by simp

qed

(* 2ª demostración *)

lemma

assumes "es_supremo A x"

shows "∀y<x. ∃a∈A. y < a"

proof (intro allI impI)

fix y

assume "y < x"

show "∃a∈A. y < a"

proof (rule ccontr)

assume "¬ (∃a∈A. y < a)"

then have "cota_superior A y"

using cota_superior_def by auto

then show "False"

using assms es_supremo_def ‹y < x› by auto

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]

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]

Pruebas de que la función espejo de los árboles binarios es involutiva

PorJosé A. Alonso 12 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)

usado 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

cuyo término es

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

1	nodo 3 (hoja 4) (nodo 2 (hoja 5) (hoja 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)

Demostrar que la función espejo es involutiva; es decir,

   espejo (espejo a) = a

1	espejo (espejo a) = a

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

import tactic

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)

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

end arbol

import tactic

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)

example :

espejo (espejo a) = a :=

sorry

end arbol

[expand title=»Soluciones con Lean»]

import tactic

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)

@[simp]
lemma espejo_1 :
  espejo (hoja x) = hoja x :=
espejo.equations._eqn_1 x

@[simp]
lemma espejo_2 :
  espejo (nodo x i d) = nodo x (espejo d) (espejo i) :=
espejo.equations._eqn_2 x i d

-- 1ª demostración
example :
  espejo (espejo a) = a :=
begin
  induction a with x x i d Hi Hd,
  { rw espejo_1,
    rw espejo_1, },
  { rw espejo_2,
    rw espejo_2,
    rw Hi,
    rw Hd, },
end

-- 2ª demostración
example :
  espejo (espejo a) = a :=
begin
  induction a with x x i d Hi Hd,
  { calc espejo (espejo (hoja x))
         = espejo (hoja x)
             : congr_arg espejo (espejo_1 x)
     ... = hoja x
             : espejo_1 x, },
  { calc espejo (espejo (nodo x i d))
         = espejo (nodo x (espejo d) (espejo i))
             : congr_arg espejo (espejo_2 i d x)
     ... = nodo x (espejo (espejo i)) (espejo (espejo d))
             : espejo_2 (espejo d) (espejo i) x
     ... = nodo x i (espejo (espejo d))
             : congr_arg2 (nodo x) Hi rfl
     ... = nodo x i d
             : congr_arg2 (nodo x) rfl Hd, },
end

-- 3ª demostración
example :
  espejo (espejo a) = a :=
begin
  induction a with x x i d Hi Hd,
  { calc espejo (espejo (hoja x))
         = espejo (hoja x)
             : congr_arg espejo (espejo_1 x)
     ... = hoja x
             : by rw espejo_1, },
  { calc espejo (espejo (nodo x i d))
         = espejo (nodo x (espejo d) (espejo i))
             : congr_arg espejo (espejo_2 i d x)
     ... = nodo x (espejo (espejo i)) (espejo (espejo d))
             : by rw espejo_2
     ... = nodo x i (espejo (espejo d))
             : by rw Hi
     ... = nodo x i d
             : by rw Hd, },
end

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

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

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

-- 7ª demostración
example :
  espejo (espejo a) = a :=
arbol.rec_on a
  ( assume x,
    calc espejo (espejo (hoja x))
         = espejo (hoja x)
             : congr_arg espejo (espejo_1 x)
     ... = hoja x
             : espejo_1 x)
  ( assume x i d,
    assume Hi : espejo (espejo i) = i,
    assume Hd : espejo (espejo d) = d,
    calc espejo (espejo (nodo x i d))
         = espejo (nodo x (espejo d) (espejo i))
             : congr_arg espejo (espejo_2 i d x)
     ... = nodo x (espejo (espejo i)) (espejo (espejo d))
             : by rw espejo_2
     ... = nodo x i (espejo (espejo d))
             : by rw Hi
     ... = nodo x i d
             : by rw Hd )

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

-- 9ª demostración
lemma espejo_espejo :
  ∀ a : arbol α, espejo (espejo a) = a
| (hoja x)     := by simp
| (nodo x i d) := by simp [espejo_espejo i, espejo_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

import tactic

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)

@[simp]

lemma espejo_1 :

espejo (hoja x) = hoja x :=

espejo.equations._eqn_1 x

@[simp]

lemma espejo_2 :

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

espejo.equations._eqn_2 x i d

-- 1ª demostración

example :

espejo (espejo a) = a :=

begin

induction a with x x i d Hi Hd,

{ rw espejo_1,

rw espejo_1, },

{ rw espejo_2,

rw espejo_2,

rw Hi,

rw Hd, },

end

-- 2ª demostración

example :

espejo (espejo a) = a :=

begin

induction a with x x i d Hi Hd,

{ calc espejo (espejo (hoja x))

= espejo (hoja x)

: congr_arg espejo (espejo_1 x)

... = hoja x

: espejo_1 x, },

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

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

: congr_arg espejo (espejo_2 i d x)

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

: espejo_2 (espejo d) (espejo i) x

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

: congr_arg2 (nodo x) Hi rfl

... = nodo x i d

: congr_arg2 (nodo x) rfl Hd, },

end

-- 3ª demostración

example :

espejo (espejo a) = a :=

begin

induction a with x x i d Hi Hd,

{ calc espejo (espejo (hoja x))

= espejo (hoja x)

: congr_arg espejo (espejo_1 x)

... = hoja x

: by rw espejo_1, },

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

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

: congr_arg espejo (espejo_2 i d x)

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

: by rw espejo_2

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

: by rw Hi

... = nodo x i d

: by rw Hd, },

end

-- 4ª demostración

example :

espejo (espejo a) = a :=

begin

induction a with x x i d Hi Hd,

{ calc espejo (espejo (hoja x))

= espejo (hoja x)

: by simp

... = hoja x

: by simp },

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

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

: by simp

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

: by simp

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

: by simp [Hi]

... = nodo x i d

: by simp [Hd], },

end

-- 5ª demostración

example :

espejo (espejo a) = a :=

begin

induction a with _ x i d Hi Hd,

{ simp, },

{ simp [Hi, Hd], },

end

-- 6ª demostración

example :

espejo (espejo a) = a :=

by induction a ; simp [*]

-- 7ª demostración

example :

espejo (espejo a) = a :=

arbol.rec_on a

( assume x,

calc espejo (espejo (hoja x))

= espejo (hoja x)

: congr_arg espejo (espejo_1 x)

... = hoja x

: espejo_1 x)

( assume x i d,

assume Hi : espejo (espejo i) = i,

assume Hd : espejo (espejo d) = d,

calc espejo (espejo (nodo x i d))

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

: congr_arg espejo (espejo_2 i d x)

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

: by rw espejo_2

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

: by rw Hi

... = nodo x i d

: by rw Hd )

-- 8ª demostración

example :

espejo (espejo a) = a :=

arbol.rec_on a

(λ x, by simp )

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

-- 9ª demostración

lemma espejo_espejo :

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

| (hoja x) := by simp

| (nodo x i d) := by simp [espejo_espejo i, espejo_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 Pruebas_de_que_la_funcion_espejo_de_los_arboles_binarios_es_involutiva
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))"

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

(* 2ª demostración *)
lemma
  fixes a :: "'b arbol"
  shows "espejo (espejo a) = 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 "espejo (espejo (nodo x i d)) =
          espejo (nodo x (espejo d) (espejo i))" by simp
    also have "… = nodo x (espejo (espejo i)) (espejo (espejo d))"
      by simp
    also have "… = nodo x i d" using h1 h2 by simp
    finally show ?thesis .
 qed
qed

(* 3ª demostración *)
lemma
  "espejo (espejo a ) = a"
by (induct a) simp_all

end

theory Pruebas_de_que_la_funcion_espejo_de_los_arboles_binarios_es_involutiva

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

(* 1ª demostración *)

lemma

fixes a :: "'b arbol"

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

proof (induct a)

fix x

show "?P (hoja x)"

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

fix x

fix i assume h1: "?P i"

fix d assume h2: "?P d"

show "?P (nodo x i d)"

proof -

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

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

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

also have "… = nodo x (espejo (espejo i)) (espejo (espejo d))"

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

also have "… = nodo x i d"

by (simp only: h1 h2)

finally show ?thesis

by this

qed

(* 2ª demostración *)

lemma

fixes a :: "'b arbol"

shows "espejo (espejo a) = 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 "espejo (espejo (nodo x i d)) =

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

also have "… = nodo x (espejo (espejo i)) (espejo (espejo d))"

by simp

also have "… = nodo x i d" using h1 h2 by simp

finally show ?thesis .

qed

(* 3ª demostración *)

lemma

"espejo (espejo a ) = 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]

Pruebas de equivalencia de definiciones de inversa

PorJosé A. Alonso 11 septiembre 20217 septiembre 2021

En Lean, está definida la función

   reverse : list α → list α

1	reverse : list α → list α

tal que (reverse xs) es la lista obtenida invirtiendo el orden de los elementos de xs. Por ejemplo,

   reverse  [3,2,5,1] = [1,5,2,3]

1	reverse [3,2,5,1] = [1,5,2,3]

Su definición es

   def reverse_core : list α → list α → list α
   | []     r := r
   | (a::l) r := reverse_core l (a::r)

   def reverse : list α → list α :=
   λ l, reverse_core l []

def reverse_core : list α → list α → list α

| [] r := r

| (a::l) r := reverse_core l (a::r)

def reverse : list α → list α :=

λ l, reverse_core l []

Una definición alternativa es

   def inversa : list α → list α
   | []        := []
   | (x :: xs) := inversa xs ++ [x]

def inversa : list α → list α

| [] := []

| (x :: xs) := inversa xs ++ [x]

Demostrar que las dos definiciones son equivalentes; es decir,

   reverse xs = inversa xs

1	reverse xs = inversa xs

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

import data.list.basic
open list

variable  {α : Type*}
variable  (x : α)
variables (xs ys : list α)

def inversa : list α → list α
| []        := []
| (x :: xs) := inversa xs ++ [x]

example : reverse xs = inversa xs :=
sorry

import data.list.basic

open list

variable {α : Type*}

variable (x : α)

variables (xs ys : list α)

def inversa : list α → list α

| [] := []

| (x :: xs) := inversa xs ++ [x]

example : reverse xs = inversa xs :=

sorry

[expand title=»Soluciones con Lean»]

import data.list.basic
open list

variable  {α : Type*}
variable  (x : α)
variables (xs ys : list α)

-- Definición y reglas de simplificación de inversa
-- ================================================

def inversa : list α → list α
| []        := []
| (x :: xs) := inversa xs ++ [x]

@[simp]
lemma inversa_nil :
  inversa ([] : list α) = [] :=
rfl

@[simp]
lemma inversa_cons :
  inversa (x :: xs) = inversa xs ++ [x] :=
rfl

-- Reglas de simplificación de reverse_core
-- ========================================

@[simp]
lemma reverse_core_nil :
  reverse_core [] ys = ys :=
rfl

@[simp]
lemma reverse_core_cons :
  reverse_core (x :: xs) ys = reverse_core xs (x :: ys) :=
rfl

-- Lema auxiliar: reverse_core xs ys = (inversa xs) ++ ys
-- ======================================================

-- 1ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { calc reverse_core [] ys
         = ys                        : reverse_core_nil ys
     ... = [] ++ ys                  : (nil_append ys).symm
     ... = inversa [] ++ ys          : congr_arg2 (++) inversa_nil.symm rfl, },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : reverse_core_cons a as ys
     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))
     ... = inversa as ++ ([a] ++ ys) : congr_arg2 (++) rfl singleton_append
     ... = (inversa as ++ [a]) ++ ys : (append_assoc (inversa as) [a] ys).symm
     ... = inversa (a :: as) ++ ys   : congr_arg2 (++) (inversa_cons a as).symm rfl},
end

-- 2ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { calc reverse_core [] ys
         = ys                        : by rw reverse_core_nil
     ... = [] ++ ys                  : by rw nil_append
     ... = inversa [] ++ ys          : by rw inversa_nil },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : by rw reverse_core_cons
     ... = inversa as ++ (a :: ys)   : by rw (HI (a :: ys))
     ... = inversa as ++ ([a] ++ ys) : by rw singleton_append
     ... = (inversa as ++ [a]) ++ ys : by rw append_assoc
     ... = inversa (a :: as) ++ ys   : by rw inversa_cons },
end

-- 3ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { calc reverse_core [] ys
         = ys                        : rfl
     ... = [] ++ ys                  : rfl
     ... = inversa [] ++ ys          : rfl },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : rfl
     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))
     ... = inversa as ++ ([a] ++ ys) : rfl
     ... = (inversa as ++ [a]) ++ ys : by rw append_assoc
     ... = inversa (a :: as) ++ ys   : rfl },
end

-- 3ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { calc reverse_core [] ys
         = ys                        : by simp
     ... = [] ++ ys                  : by simp
     ... = inversa [] ++ ys          : by simp },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : by simp
     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))
     ... = inversa as ++ ([a] ++ ys) : by simp
     ... = (inversa as ++ [a]) ++ ys : by simp
     ... = inversa (a :: as) ++ ys   : by simp },
end

-- 4ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { by simp, },
  { calc reverse_core (a :: as) ys
         = reverse_core as (a :: ys) : by simp
     ... = inversa as ++ (a :: ys)   : (HI (a :: ys))
     ... = inversa (a :: as) ++ ys   : by simp },
end

-- 5ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { simp, },
  { simp [HI (a :: ys)], },
end

-- 6ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
by induction xs generalizing ys ; simp [*]

-- 7ª demostración del lema auxiliar
example :
  reverse_core xs ys = (inversa xs) ++ ys :=
begin
  induction xs with a as HI generalizing ys,
  { rw reverse_core_nil,
    rw inversa_nil,
    rw nil_append, },
  { rw reverse_core_cons,
    rw (HI (a :: ys)),
    rw inversa_cons,
    rw append_assoc,
    rw singleton_append, },
end

-- 8ª demostración  del lema auxiliar
@[simp]
lemma inversa_equiv :
  ∀ xs : list α, ∀ ys, reverse_core xs ys = (inversa xs) ++ ys
| []         := by simp
| (a :: as)  := by simp [inversa_equiv as]

-- Demostraciones del lema principal
-- =================================

-- 1ª demostración
example : reverse xs = inversa xs :=
calc reverse xs
     = reverse_core xs [] : rfl
 ... = inversa xs ++ []   : by rw inversa_equiv
 ... = inversa xs         : by rw append_nil

-- 2ª demostración
example : reverse xs = inversa xs :=
by simp [inversa_equiv, reverse]

-- 3ª demostración
example : reverse xs = inversa xs :=
by simp [reverse]

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

import data.list.basic

open list

variable {α : Type*}

variable (x : α)

variables (xs ys : list α)

-- Definición y reglas de simplificación de inversa

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

def inversa : list α → list α

| [] := []

| (x :: xs) := inversa xs ++ [x]

@[simp]

lemma inversa_nil :

inversa ([] : list α) = [] :=

rfl

@[simp]

lemma inversa_cons :

inversa (x :: xs) = inversa xs ++ [x] :=

rfl

-- Reglas de simplificación de reverse_core

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

@[simp]

lemma reverse_core_nil :

reverse_core [] ys = ys :=

rfl

@[simp]

lemma reverse_core_cons :

reverse_core (x :: xs) ys = reverse_core xs (x :: ys) :=

rfl

-- Lema auxiliar: reverse_core xs ys = (inversa xs) ++ ys

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

-- 1ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ calc reverse_core [] ys

= ys : reverse_core_nil ys

... = [] ++ ys : (nil_append ys).symm

... = inversa [] ++ ys : congr_arg2 (++) inversa_nil.symm rfl, },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : reverse_core_cons a as ys

... = inversa as ++ (a :: ys) : (HI (a :: ys))

... = inversa as ++ ([a] ++ ys) : congr_arg2 (++) rfl singleton_append

... = (inversa as ++ [a]) ++ ys : (append_assoc (inversa as) [a] ys).symm

... = inversa (a :: as) ++ ys : congr_arg2 (++) (inversa_cons a as).symm rfl},

end

-- 2ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ calc reverse_core [] ys

= ys : by rw reverse_core_nil

... = [] ++ ys : by rw nil_append

... = inversa [] ++ ys : by rw inversa_nil },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : by rw reverse_core_cons

... = inversa as ++ (a :: ys) : by rw (HI (a :: ys))

... = inversa as ++ ([a] ++ ys) : by rw singleton_append

... = (inversa as ++ [a]) ++ ys : by rw append_assoc

... = inversa (a :: as) ++ ys : by rw inversa_cons },

end

-- 3ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ calc reverse_core [] ys

= ys : rfl

... = [] ++ ys : rfl

... = inversa [] ++ ys : rfl },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : rfl

... = inversa as ++ (a :: ys) : (HI (a :: ys))

... = inversa as ++ ([a] ++ ys) : rfl

... = (inversa as ++ [a]) ++ ys : by rw append_assoc

... = inversa (a :: as) ++ ys : rfl },

end

-- 3ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ calc reverse_core [] ys

= ys : by simp

... = [] ++ ys : by simp

... = inversa [] ++ ys : by simp },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : by simp

... = inversa as ++ (a :: ys) : (HI (a :: ys))

... = inversa as ++ ([a] ++ ys) : by simp

... = (inversa as ++ [a]) ++ ys : by simp

... = inversa (a :: as) ++ ys : by simp },

end

-- 4ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ by simp, },

{ calc reverse_core (a :: as) ys

= reverse_core as (a :: ys) : by simp

... = inversa as ++ (a :: ys) : (HI (a :: ys))

... = inversa (a :: as) ++ ys : by simp },

end

-- 5ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ simp, },

{ simp [HI (a :: ys)], },

end

-- 6ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

by induction xs generalizing ys ; simp [*]

-- 7ª demostración del lema auxiliar

example :

reverse_core xs ys = (inversa xs) ++ ys :=

begin

induction xs with a as HI generalizing ys,

{ rw reverse_core_nil,

rw inversa_nil,

rw nil_append, },

{ rw reverse_core_cons,

rw (HI (a :: ys)),

rw inversa_cons,

rw append_assoc,

rw singleton_append, },

end

-- 8ª demostración del lema auxiliar

@[simp]

lemma inversa_equiv :

∀ xs : list α, ∀ ys, reverse_core xs ys = (inversa xs) ++ ys

| [] := by simp

| (a :: as) := by simp [inversa_equiv as]

-- Demostraciones del lema principal

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

-- 1ª demostración

example : reverse xs = inversa xs :=

calc reverse xs

= reverse_core xs [] : rfl

... = inversa xs ++ [] : by rw inversa_equiv

... = inversa xs : by rw append_nil

-- 2ª demostración

example : reverse xs = inversa xs :=

by simp [inversa_equiv, reverse]

-- 3ª demostración

example : reverse xs = inversa xs :=

by simp [reverse]

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

(* Definición alternativa *)
(* ====================== *)

fun inversa_aux :: "'a list ⇒ 'a list ⇒ 'a list" where
  "inversa_aux [] ys     = ys"
| "inversa_aux (x#xs) ys = inversa_aux xs (x#ys)"

fun inversa :: "'a list ⇒ 'a list" where
  "inversa xs = inversa_aux xs []"

(* Lema auxiliar: inversa_aux xs ys = (rev xs) @ ys *)
(* ================================================ *)

(* 1ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  fix ys :: "'a list"
  have "inversa_aux [] ys = ys"
    by (simp only: inversa_aux.simps(1))
  also have "… = [] @ ys"
    by (simp only: append.simps(1))
  also have "… = rev [] @ ys"
    by (simp only: rev.simps(1))
  finally show "inversa_aux [] ys = rev [] @ ys"
    by this
next
  fix a ::'a and xs :: "'a list"
  assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"
  show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"
  proof -
    fix ys
    have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)"
      by (simp only: inversa_aux.simps(2))
    also have "… = rev xs@(a#ys)"
      by (simp only: HI)
    also have "… = rev xs @ ([a] @ ys)"
      by (simp only: append.simps)
    also have "… = (rev xs @ [a]) @ ys"
      by (simp only: append_assoc)
    also have "… = rev (a # xs) @ ys"
      by (simp only: rev.simps(2))
    finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys"
      by this
  qed
qed

(* 2ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  fix ys :: "'a list"
  have "inversa_aux [] ys = ys" by simp
  also have "… = [] @ ys" by simp
  also have "… = rev [] @ ys" by simp
  finally show "inversa_aux [] ys = rev [] @ ys" .
next
  fix a ::'a and xs :: "'a list"
  assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"
  show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"
  proof -
    fix ys
    have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)" by simp
    also have "… = rev xs@(a#ys)" using HI by simp
    also have "… = rev xs @ ([a] @ ys)" by simp
    also have "… = (rev xs @ [a]) @ ys" by simp
    also have "… = rev (a # xs) @ ys" by simp
    finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" .
  qed
qed

(* 3ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  fix ys :: "'a list"
  show "inversa_aux [] ys = rev [] @ ys" by simp
next
  fix a ::'a and xs :: "'a list"
  assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"
  show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"
  proof -
    fix ys
    have "inversa_aux (a#xs) ys = rev xs@(a#ys)" using HI by simp
    also have "… = rev (a # xs) @ ys" by simp
    finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" .
  qed
qed

(* 4ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  show "⋀ys. inversa_aux [] ys = rev [] @ ys" by simp
next
  fix a ::'a and xs :: "'a list"
  assume "⋀ys. inversa_aux xs ys = rev xs@ys"
  then show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys" by simp
qed

(* 5ª demostración del lema auxiliar *)
lemma
  "inversa_aux xs ys = (rev xs) @ ys"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed

(* 6ª demostración del lema auxiliar *)
lemma inversa_equiv:
  "inversa_aux xs ys = (rev xs) @ ys"
by (induct xs arbitrary: ys) simp_all

(* Demostraciones del lema principal *)
(* ================================= *)

(* 1ª demostración *)
lemma "inversa xs = rev xs"
proof -
  have "inversa xs = inversa_aux xs []"
    by (rule inversa.simps)
  also have "… = (rev xs) @ []"
    by (rule inversa_equiv)
  also have "… = rev xs"
    by (rule append.right_neutral)
  finally show "inversa xs = rev xs"
    by this
qed

(* 2ª demostración *)
lemma "inversa xs = rev xs"
proof -
  have "inversa xs = inversa_aux xs []"  by simp
  also have "… = (rev xs) @ []" by (rule inversa_equiv)
  also have "… = rev xs" by simp
  finally show "inversa xs = rev xs" .
qed

(* 3ª demostración *)
lemma "inversa xs = rev xs"
by (simp add: inversa_equiv)

end

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

theory Pruebas_de_equivalencia_de_definiciones_de_inversa

imports Main

begin

(* Definición alternativa *)

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

fun inversa_aux :: "'a list ⇒ 'a list ⇒ 'a list" where

"inversa_aux [] ys = ys"

| "inversa_aux (x#xs) ys = inversa_aux xs (x#ys)"

fun inversa :: "'a list ⇒ 'a list" where

"inversa xs = inversa_aux xs []"

(* Lema auxiliar: inversa_aux xs ys = (rev xs) @ ys *)

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

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

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

fix ys :: "'a list"

have "inversa_aux [] ys = ys"

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

also have "… = [] @ ys"

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

also have "… = rev [] @ ys"

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

finally show "inversa_aux [] ys = rev [] @ ys"

by this

fix a ::'a and xs :: "'a list"

assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"

show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"

proof -

fix ys

have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)"

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

also have "… = rev xs@(a#ys)"

by (simp only: HI)

also have "… = rev xs @ ([a] @ ys)"

by (simp only: append.simps)

also have "… = (rev xs @ [a]) @ ys"

by (simp only: append_assoc)

also have "… = rev (a # xs) @ ys"

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

finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys"

by this

qed

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

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

fix ys :: "'a list"

have "inversa_aux [] ys = ys" by simp

also have "… = [] @ ys" by simp

also have "… = rev [] @ ys" by simp

finally show "inversa_aux [] ys = rev [] @ ys" .

fix a ::'a and xs :: "'a list"

assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"

show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"

proof -

fix ys

have "inversa_aux (a#xs) ys = inversa_aux xs (a#ys)" by simp

also have "… = rev xs@(a#ys)" using HI by simp

also have "… = rev xs @ ([a] @ ys)" by simp

also have "… = (rev xs @ [a]) @ ys" by simp

also have "… = rev (a # xs) @ ys" by simp

finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" .

qed

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

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

fix ys :: "'a list"

show "inversa_aux [] ys = rev [] @ ys" by simp

fix a ::'a and xs :: "'a list"

assume HI: "⋀ys. inversa_aux xs ys = rev xs@ys"

show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys"

proof -

fix ys

have "inversa_aux (a#xs) ys = rev xs@(a#ys)" using HI by simp

also have "… = rev (a # xs) @ ys" by simp

finally show "inversa_aux (a#xs) ys = rev (a#xs)@ys" .

qed

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

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

show "⋀ys. inversa_aux [] ys = rev [] @ ys" by simp

fix a ::'a and xs :: "'a list"

assume "⋀ys. inversa_aux xs ys = rev xs@ys"

then show "⋀ys. inversa_aux (a#xs) ys = rev (a#xs)@ys" by simp

qed

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

lemma

"inversa_aux xs ys = (rev xs) @ ys"

proof (induct xs arbitrary: ys)

case Nil

then show ?case by simp

case (Cons a xs)

then show ?case by simp

qed

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

lemma inversa_equiv:

"inversa_aux xs ys = (rev xs) @ ys"

by (induct xs arbitrary: ys) simp_all

(* Demostraciones del lema principal *)

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

(* 1ª demostración *)

lemma "inversa xs = rev xs"

proof -

have "inversa xs = inversa_aux xs []"

by (rule inversa.simps)

also have "… = (rev xs) @ []"

by (rule inversa_equiv)

also have "… = rev xs"

by (rule append.right_neutral)

finally show "inversa xs = rev xs"

by this

qed

(* 2ª demostración *)

lemma "inversa xs = rev xs"

proof -

have "inversa xs = inversa_aux xs []" by simp

also have "… = (rev xs) @ []" by (rule inversa_equiv)

also have "… = rev xs" by simp

finally show "inversa xs = rev xs" .

qed

(* 3ª demostración *)

lemma "inversa xs = rev xs"

by (simp add: inversa_equiv)

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]