Menu Close

Día: 8 enero, 2021

ForMatUS: Pruebas en Lean de “La función identidad es menor o igual que la función de extracción”

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 5 pruebas en Lean de la propiedad

Si φ es una función de extracción (es decir, una función creciente de ℕ en ℕ), entonces n ≤ φ n (para todo n).

usando los estilos declarativo y aplicativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
open nat
 
variable {φ :   }
 
set_option pp.structure_projections false
 
-- ----------------------------------------------------
-- Ejercicio 1. Para extraer una sucesión se aplica una
-- función de extracción que conserva el orden; por
-- ejemplo, la subsucesión
--    uₒ, u₂, u₄, u₆, ...
-- se ha obtenido con la función de extracción φ tal
-- que φ(n) = 2*n.
--
-- Definir la función
--    extraccion : (ℕ → ℕ) → Prop
-- tal que (extraccion φ) expresa que φ es una función
-- de extracción
-- ----------------------------------------------------
 
def extraccion : (  )  Prop
| φ :=  n m, n < m  φ n < φ m
 
-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que si φ es una función de
-- extracción, entonces
--    ∀ n, n ≤ φ n
-- ----------------------------------------------------
 
-- 1ª demostración
example :
  extraccion φ   n, n  φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    have h1 : m < succ m,
      from lt_add_one m,
    calc m  φ m        : HI
       ... < φ (succ m) : h m (succ m) h1, },
end
 
-- 2ª demostración
example :
  extraccion φ   n, n  φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le _ },
  { apply nat.succ_le_of_lt,
    calc m  φ m        : HI
       ... < φ (succ m) : by linarith [h m (m+1) (by linarith)] },
end
 
-- 3ª demostración
example :
  extraccion φ   n, n  φ n :=
begin
  intros h n,
  induction n with m HI,
  { linarith },
  { apply nat.succ_le_of_lt,
    linarith [h m (m+1) (by linarith)] },
end
 
-- 4ª demostración
example :
  extraccion φ   n, n  φ n :=
begin
  intros h n,
  induction n with m HI,
  { linarith },
  { exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },
end
 
-- 5ª demostración
example :
  extraccion φ   n, n  φ n :=
assume h : extraccion φ,
assume n,
nat.rec_on n
  ( show 0  φ 0,
      from nat.zero_le (φ 0) )
  ( assume m,
    assume HI : m  φ m,
    have h1 : m < succ m,
      from lt_add_one m,
    have h2 : m < φ (succ m), from
      calc m  φ m        : HI
         ... < φ (succ m) : h m (succ m) h1,
    show succ m  φ (succ m),
      from nat.succ_le_of_lt h2)

ForMatUS: Pruebas en Lean de “Los supremos de las sucesiones no decrecientes son sus límites”

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad

Los supremos de las sucesiones no decrecientes son sus límites

usando los estilos declarativo y aplicativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic
 
variable (u :   )
variable (M : )
 
-- ----------------------------------------------------
-- Nota. Se usarán las siguientes notaciones y
-- definiciones estudiadas anteriormente:
-- + |x| = abs x
-- + limite u c :
--      ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε
-- ----------------------------------------------------
 
notation `|`x`|` := abs x
 
def limite : (  )    Prop :=
λ u c,  ε > 0,  N,  n  N, |u n - c|  ε
 
-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    no_decreciente : (ℕ → ℝ) → Prop
-- tal que (no_decreciente) expresa que la sucesión u
-- es no decreciente.
-- ----------------------------------------------------
 
def no_decreciente : (  )  Prop
| u :=  n m, n  m  u n  u m
 
-- ----------------------------------------------------
-- Ejercicio 2. Definir la función
--    es_sup_suc : ℝ → (ℕ → ℝ) → Prop
-- tal que (es_sup_suc M u) expresa que M es el supremo
-- de la sucesión u.
-- ----------------------------------------------------
 
def es_sup_suc :   (  )  Prop
| M u := ( n, u n  M)   ε > 0,  n₀, u n₀  M - ε
 
-- ----------------------------------------------------
-- Ejercicio 3. Demostrar que si M es un supremo de la
-- sucesión no decreciente u, entonces el límite de u
-- es M.
-- ----------------------------------------------------
 
-- 1ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
begin
  -- unfold limite,
  intros ε hε,
  -- unfold es_sup_suc at h,
  cases h with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { -- unfold no_decreciente at h',
    specialize h' n₀ n hn,
    calc -ε
         = (M - ε) - M : by ring
     ...  u n₀ - M    : sub_le_sub_right hn₀ M
     ...  u n - M     : sub_le_sub_right h' M },
  { calc u n - M
          M - M       : sub_le_sub_right (hM₁ n) M
     ... = 0           : sub_self M
     ...  ε           : le_of_lt hε, },
end
 
-- 2ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
begin
  intros ε hε,
  cases h with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split,
  { linarith [h' n₀ n hn] },
  { linarith [hM₁ n] },
end
 
-- 3ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
begin
  intros ε hε,
  cases h with hM₁ hM₂,
  cases hM₂ ε hε with n₀ hn₀,
  use n₀,
  intros n hn,
  rw abs_le,
  split ; linarith [h' n₀ n hn, hM₁ n],
end
 
-- 4ª demostración
example
  (h : es_sup_suc M u)
  (h' : no_decreciente u)
  : limite u M :=
assume ε,
assume hε : ε > 0,
have hM₁ :  (n : ), u n  M,
  from h.left,
have hM₂ :  (ε : ), ε > 0  ( (n₀ : ), u n₀  M - ε),
  from h.right,
exists.elim (hM₂ ε hε)
  ( assume n₀,
    assume hn₀ : u n₀  M - ε,
    have h1 :  n, n  n₀  |u n - M|  ε,
      { assume n,
        assume hn : n  n₀,
        have h2 : -ε  u n - M,
          { have h'a : u n₀  u n,
              from h' n₀ n hn,
            calc -ε
                 = (M - ε) - M : by ring
             ...  u n₀ - M    : sub_le_sub_right hn₀ M
             ...  u n - M     : sub_le_sub_right h'a M },
        have h3 : u n - M  ε,
          { calc u n - M
                  M - M       : sub_le_sub_right (hM₁ n) M
             ... = 0           : sub_self M
             ...  ε           : le_of_lt hε },
        show |u n - M|  ε,
          from abs_le.mpr (and.intro h2 h3) },
    show  N,  n, n  N  |u n - M|  ε,
      from exists.intro n₀ h1)