Menu Close

Etiqueta: L.rw

Pruebas de take n xs ++ drop n xs = xs

José A. Alonso-

En Lean están definidas las funciones

   take : nat → list α → nat
   drop : nat → list α → nat
   (++) : list α → list α → list α

tales que

  • (take n xs) es la lista formada por los n primeros elementos de xs. Por ejemplo,
     take 2 [3,5,1,9,7] = [3,5]
  • (drop n xs) es la lista formada eliminando los n primeros elementos de xs. Por ejemplo,
     drop 2 [3,5,1,9,7] = [1,9,7]
  • (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.
     [3,5] ++ [1,9,7] = [3,5,1,9,7]

Dichas funciones están caracterizadas por los siguientes lemas:

   take_zero   : take 0 xs = []
   take_nil    : take n [] = []
   take_cons   : take (succ n) (x :: xs) = x :: take n xs
   drop_zero   : drop 0 xs = xs
   drop_nil    : drop n [] = []
   drop_cons   : drop (succ n) (x :: xs) = drop n xs := rfl
   nil_append  : [] ++ ys = ys
   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que

   take n xs ++ drop n xs = xs

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

import data.list.basic
import tactic
open list nat
 
variable {α : Type}
variable (x : α)
variable (xs : list α)
variable (n : ℕ)
 
lemma drop_zero : drop 0 xs = xs := rfl
lemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl
 
example :
  take n xs ++ drop n xs = xs :=
sorry
Soluciones con Lean
import data.list.basic
import tactic
open list
open nat
 
variable {α : Type}
variable (n : ℕ)
variable (x : α)
variable (xs : list α)
 
lemma drop_zero : drop 0 xs = xs := rfl
lemma drop_cons : drop (succ n) (x :: xs) = drop n xs := rfl
 
-- 1ª demostración
example :
  take n xs ++ drop n xs = xs :=
begin
  induction n with m HI1 generalizing xs,
  { rw take_zero,
    rw drop_zero,
    rw nil_append, },
  { induction xs with a as HI2,
    { rw take_nil,
      rw drop_nil,
      rw nil_append, },
    { rw take_cons,
      rw drop_cons,
      rw cons_append,
      rw (HI1 as), }, },
end
 
-- 2ª demostración
example :
  take n xs ++ drop n xs = xs :=
begin
  induction n with m HI1 generalizing xs,
  { calc take 0 xs ++ drop 0 xs
         = [] ++ drop 0 xs        : by rw take_zero
     ... = [] ++ xs               : by rw drop_zero
     ... = xs                     : by rw nil_append, },
  { induction xs with a as HI2,
    { calc take (succ m) [] ++ drop (succ m) []
           = ([] : list α) ++ drop (succ m) [] : by rw take_nil
       ... = [] ++ []                          : by rw drop_nil
       ... = []                                : by rw nil_append, },
    { calc take (succ m) (a :: as) ++ drop (succ m) (a :: as)
           = (a :: take m as) ++ drop (succ m) (a :: as) : by rw take_cons
       ... = (a :: take m as) ++ drop m as               : by rw drop_cons
       ... = a :: (take m as ++ drop m as)               : by rw cons_append
       ... = a :: as                                     : by rw (HI1 as), }, },
end
 
-- 3ª demostración
example :
  take n xs ++ drop n xs = xs :=
begin
  induction n with m HI1 generalizing xs,
  { simp, },
  { induction xs with a as HI2,
    { simp, },
    { simp [HI1 as], }, },
end
 
-- 4ª demostración
lemma conc_take_drop_1 :
  ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs
| 0 xs := by calc
    take 0 xs ++ drop 0 xs
        = [] ++ drop 0 xs   : by rw take_zero
    ... = [] ++ xs          : by rw drop_zero
    ... = xs                : by rw nil_append
| (succ m) [] := by calc
    take (succ m) [] ++ drop (succ m) []
        = ([] : list α) ++ drop (succ m) [] : by rw take_nil
    ... = [] ++ []                          : by rw drop_nil
    ... = []                                : by rw nil_append
| (succ m) (a :: as) := by calc
    take (succ m) (a :: as) ++ drop (succ m) (a :: as)
        = (a :: take m as) ++ drop (succ m) (a :: as)    : by rw take_cons
    ... = (a :: take m as) ++ drop m as                  : by rw drop_cons
    ... = a :: (take m as ++ drop m as)                  : by rw cons_append
    ... = a :: as                                        : by rw conc_take_drop_1
 
-- 5ª demostración
lemma conc_take_drop_2 :
  ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs
| 0        xs        := by simp
| (succ m) []        := by simp
| (succ m) (a :: as) := by simp [conc_take_drop_2]
 
-- 6ª demostración
lemma conc_take_drop_3 :
  ∀ (n : ℕ) (xs : list α), take n xs ++ drop n xs = xs
| 0        xs        := rfl
| (succ m) []        := rfl
| (succ m) (a :: as) := congr_arg (cons a) (conc_take_drop_3 m as)
 
-- 7ª demostración
example : take n xs ++ drop n xs = xs :=
-- by library_search
take_append_drop n xs
 
-- 8ª demostración
example : take n xs ++ drop n xs = xs :=
by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory "Pruebas_de_take_n_xs_++_drop_n_xs_Ig_xs"
imports Main
begin
 
fun take' :: "nat ⇒ 'a list ⇒ 'a list" where
  "take' n []           = []"
| "take' 0 xs           = []"
| "take' (Suc n) (x#xs) = x # (take' n xs)"
 
fun drop' :: "nat ⇒ 'a list ⇒ 'a list" where
  "drop' n []           = []"
| "drop' 0 xs           = xs"
| "drop' (Suc n) (x#xs) = drop' n xs"
 
(* 1ª demostración *)
lemma "take' n xs @ drop' n xs = xs"
proof (induct rule: take'.induct)
  fix n
  have "take' n [] @ drop' n [] = [] @ drop' n []"
    by (simp only: take'.simps(1))
  also have "… = drop' n []"
    by (simp only: append.simps(1))
  also have "… = []"
    by (simp only: drop'.simps(1))
  finally show "take' n [] @ drop' n [] = []"
    by this
next
  fix x :: 'a and xs :: "'a list"
  have "take' 0 (x#xs) @ drop' 0 (x#xs) =
        [] @ drop' 0 (x#xs)"
    by (simp only: take'.simps(2))
  also have "… = drop' 0 (x#xs)"
    by  (simp only: append.simps(1))
  also have "… = x # xs"
    by  (simp only: drop'.simps(2))
  finally show "take' 0 (x#xs) @ drop' 0 (x#xs) = x#xs"
    by this
next
  fix n :: nat and x :: 'a and xs :: "'a list"
  assume HI: "take' n xs @ drop' n xs = xs"
  have "take' (Suc n) (x # xs) @ drop' (Suc n) (x # xs) =
        (x # (take' n xs)) @ drop' n xs"
    by (simp only: take'.simps(3)
                   drop'.simps(3))
  also have "… = x # (take' n xs @ drop' n xs)"
    by (simp only: append.simps(2))
  also have "… = x#xs"
    by (simp only: HI)
  finally show "take' (Suc n) (x#xs) @ drop' (Suc n) (x#xs) =
                x#xs"
    by this
qed
 
(* 2ª demostración *)
lemma "take' n xs @ drop' n xs = xs"
proof (induct rule: take'.induct)
case (1 n)
  then show ?case by simp
next
  case (2 x xs)
  then show ?case by simp
next
  case (3 n x xs)
  then show ?case by simp
qed
 
(* 3ª demostración *)
lemma "take' n xs @ drop' n xs = xs"
by (induct rule: take'.induct) 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>

Soluciones →

Pruebas de length (xs ++ ys) = length xs + length ys

José A. Alonso-

En Lean están definidas las funciones

   length : list α → nat
   (++)   : list α → list α → list α

tales que

  • (length xs) es la longitud de xs. Por ejemplo,
     length [2,3,5,3] = 4
  • (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.
     [1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]

Dichas funciones están caracterizadas por los siguientes lemas:

   length_nil  : length [] = 0
   length_cons : length (x :: xs) = length xs + 1
   nil_append  : [] ++ ys = ys
   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que

   length (xs ++ ys) = length xs + length ys

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

import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
lemma length_nil  : length ([] : list α) = 0 := rfl
 
example :
  length (xs ++ ys) = length xs + length ys :=
sorry
Soluciones con Lean
import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
lemma length_nil  : length ([] : list α) = 0 := rfl
 
-- 1ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    rw add_assoc,
    rw add_comm (length ys),
    rw add_assoc, },
end
 
-- 2ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    -- library_search,
    exact add_right_comm (length as) (length ys) 1 },
end
 
-- 3ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw length_nil,
    rw zero_add, },
  { rw cons_append,
    rw length_cons,
    rw HI,
    rw length_cons,
    -- by hint,
    linarith, },
end
 
-- 4ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { simp, },
  { simp [HI],
    linarith, },
end
 
-- 5ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { simp, },
  { finish [HI],},
end
 
-- 6ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
by induction xs ; finish [*]
 
-- 7ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { calc length ([] ++ ys)
         = length ys                    : congr_arg length (nil_append ys)
     ... = 0 + length ys                : (zero_add (length ys)).symm
     ... = length [] + length ys        : congr_arg2 (+) length_nil.symm rfl, },
  { calc length ((a :: as) ++ ys)
         = length (a :: (as ++ ys))     : congr_arg length (cons_append a as ys)
     ... = length (as ++ ys) + 1        : length_cons a (as ++ ys)
     ... = (length as + length ys) + 1  : congr_arg2 (+) HI rfl
     ... = (length as + 1) + length ys  : add_right_comm (length as) (length ys) 1
     ... = length (a :: as) + length ys : congr_arg2 (+) (length_cons a as).symm rfl, },
end
 
-- 8ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
begin
  induction xs with a as HI,
  { calc length ([] ++ ys)
         = length ys                    : by rw nil_append
     ... = 0 + length ys                : (zero_add (length ys)).symm
     ... = length [] + length ys        : by rw length_nil },
  { calc length ((a :: as) ++ ys)
         = length (a :: (as ++ ys))     : by rw cons_append
     ... = length (as ++ ys) + 1        : by rw length_cons
     ... = (length as + length ys) + 1  : by rw HI
     ... = (length as + 1) + length ys  : add_right_comm (length as) (length ys) 1
     ... = length (a :: as) + length ys : by rw length_cons, },
end
 
-- 9ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
list.rec_on xs
  ( show length ([] ++ ys) = length [] + length ys, from
      calc length ([] ++ ys)
           = length ys                    : by rw nil_append
       ... = 0 + length ys                : by exact (zero_add (length ys)).symm
       ... = length [] + length ys        : by rw length_nil )
  ( assume a as,
    assume HI : length (as ++ ys) = length as + length ys,
    show length ((a :: as) ++ ys) = length (a :: as) + length ys, from
      calc length ((a :: as) ++ ys)
           = length (a :: (as ++ ys))     : by rw cons_append
       ... = length (as ++ ys) + 1        : by rw length_cons
       ... = (length as + length ys) + 1  : by rw HI
       ... = (length as + 1) + length ys  : by exact add_right_comm (length as) (length ys) 1
       ... = length (a :: as) + length ys : by rw length_cons)
 
-- 10ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
list.rec_on xs
  ( by simp)
  ( λ a as HI, by simp [HI, add_right_comm])
 
-- 11ª demostración
lemma longitud_conc_1 :
  ∀ xs, length (xs ++ ys) = length xs + length ys
| [] := by calc
    length ([] ++ ys)
        = length ys                    : by rw nil_append
    ... = 0 + length ys                : by rw zero_add
    ... = length [] + length ys        : by rw length_nil
| (a :: as) := by calc
    length ((a :: as) ++ ys)
        = length (a :: (as ++ ys))     : by rw cons_append
    ... = length (as ++ ys) + 1        : by rw length_cons
    ... = (length as + length ys) + 1  : by rw longitud_conc_1
    ... = (length as + 1) + length ys  : by exact add_right_comm (length as) (length ys) 1
    ... = length (a :: as) + length ys : by rw length_cons
 
-- 12ª demostración
lemma longitud_conc_2 :
  ∀ xs, length (xs ++ ys) = length xs + length ys
| []        := by simp
| (a :: as) := by simp [longitud_conc_2 as, add_right_comm]
 
-- 13ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
-- by library_search
length_append xs ys
 
-- 14ª demostración
example :
  length (xs ++ ys) = length xs + length ys :=
by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory "Pruebas_de_length(xs_++_ys)_Ig_length_xs+length_ys"
imports Main
begin
 
(* 1ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  have "length ([] @ ys) = length ys"
    by (simp only: append_Nil)
  also have "… = 0 + length ys"
    by (rule add_0 [symmetric])
  also have "… = length [] + length ys"
    by (simp only: list.size(3))
  finally show "length ([] @ ys) = length [] + length ys"
    by this
next
  fix x xs
  assume HI : "length (xs @ ys) = length xs + length ys"
  have "length ((x # xs) @ ys) =
        length (x # (xs @ ys))"
    by (simp only: append_Cons)
  also have "… = length (xs @ ys) + 1"
    by (simp only: list.size(4))
  also have "… = (length xs + length ys) + 1"
    by (simp only: HI)
  also have "… = (length xs + 1) + length ys"
    by (simp only: add.assoc add.commute)
  also have "… = length (x # xs) + length ys"
    by (simp only: list.size(4))
  then show "length ((x # xs) @ ys) = length (x # xs) + length ys"
    by simp
qed
 
(* 2ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  show "length ([] @ ys) = length [] + length ys"
    by simp
next
  fix x xs
  assume "length (xs @ ys) = length xs + length ys"
  then show "length ((x # xs) @ ys) = length (x # xs) + length ys"
    by simp
qed
 
(* 3ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed
 
(* 4ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
by (induct xs) simp_all
 
(* 5ª demostración *)
lemma "length (xs @ ys) = length xs + length ys"
by (fact length_append)
 
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>

Soluciones →

Asociatividad de la concatenación de listas

José A. Alonso-

En Lean la operación de concatenación de listas se representa por (++) y está caracterizada por los siguientes lemas

   nil_append  : [] ++ ys = ys
   cons_append : (x :: xs) ++ y = x :: (xs ++ ys)

Demostrar que la concatenación es asociativa; es decir,

   xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

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

import data.list.basic
import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
sorry
Soluciones con Lean
import data.list.basic
import tactic
open list
 
variable  {α : Type}
variable  (x : α)
variables (xs ys zs : list α)
 
-- 1ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : append.equations._eqn_1 (ys ++ zs)
     ... = ([] ++ ys) ++ zs        : congr_arg2 (++) (append.equations._eqn_1 ys) rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : append.equations._eqn_2 a as (ys ++ zs)
     ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI
     ... = (a :: (as ++ ys)) ++ zs : (append.equations._eqn_2 a (as ++ ys) zs).symm
     ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (append.equations._eqn_2 a as ys).symm rfl, },
end
 
-- 2ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : nil_append (ys ++ zs)
     ... = ([] ++ ys) ++ zs        : congr_arg2 (++) (nil_append ys) rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : cons_append a as (ys ++ zs)
     ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI
     ... = (a :: (as ++ ys)) ++ zs : (cons_append a (as ++ ys) zs).symm
     ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (cons_append a as ys).symm rfl, },
end
 
-- 3ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : by rw nil_append
     ... = ([] ++ ys) ++ zs        : by rw nil_append, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : by rw cons_append
     ... = a :: ((as ++ ys) ++ zs) : by rw HI
     ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
     ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append, },
end
 
-- 4ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : rfl
     ... = ([] ++ ys) ++ zs        : rfl, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : rfl
     ... = a :: ((as ++ ys) ++ zs) : by rw HI
     ... = (a :: (as ++ ys)) ++ zs : rfl
     ... = ((a :: as) ++ ys) ++ zs : rfl, },
end
 
-- 5ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { calc [] ++ (ys ++ zs)
         = ys ++ zs                : by simp
     ... = ([] ++ ys) ++ zs        : by simp, },
  { calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) : by simp
     ... = a :: ((as ++ ys) ++ zs) : congr_arg (cons a) HI
     ... = (a :: (as ++ ys)) ++ zs : by simp
     ... = ((a :: as) ++ ys) ++ zs : by simp, },
end
 
-- 6ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { by simp, },
  { by exact (cons_inj a).mpr HI, },
end
 
-- 7ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
begin
  induction xs with a as HI,
  { rw nil_append,
    rw nil_append, },
  { rw cons_append,
    rw HI,
    rw cons_append,
    rw cons_append, },
end
 
-- 8ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
list.rec_on xs
  ( show [] ++ (ys ++ zs) = ([] ++ ys) ++ zs,
      from calc
        [] ++ (ys ++ zs)
            = ys ++ zs         : by rw nil_append
        ... = ([] ++ ys) ++ zs : by rw nil_append )
  ( assume a as,
    assume HI : as ++ (ys ++ zs) = (as ++ ys) ++ zs,
    show (a :: as) ++ (ys  ++ zs) = ((a :: as) ++ ys) ++ zs,
      from calc
        (a :: as) ++ (ys ++ zs)
            = a :: (as ++ (ys ++ zs)) : by rw cons_append
        ... = a :: ((as ++ ys) ++ zs) : by rw HI
        ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
        ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append)
 
-- 9ª demostración
example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
list.rec_on xs
  (by simp)
  (by simp [*])
 
-- 10ª demostración
lemma conc_asoc_1 :
  ∀ xs, xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
| [] := by calc
    [] ++ (ys ++ zs)
        = ys ++ zs         : by rw nil_append
    ... = ([] ++ ys) ++ zs : by rw nil_append
| (a :: as) := by calc
    (a :: as) ++ (ys ++ zs)
        = a :: (as ++ (ys ++ zs)) : by rw cons_append
    ... = a :: ((as ++ ys) ++ zs) : by rw conc_asoc_1
    ... = (a :: (as ++ ys)) ++ zs : by rw cons_append
    ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append
 
-- 11ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
-- by library_search
append_assoc xs ys zs
 
-- 12ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
by induction xs ; simp [*]
 
-- 13ª demostración
example :
  (xs ++ ys) ++ zs = xs ++ (ys ++ zs) :=
by simp

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
theory Asociatividad_de_la_concatenacion_de_listas
imports Main
begin
 
(* 1ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  have "[] @ (ys @ zs) = ys @ zs"
    by (simp only: append_Nil)
  also have "… = ([] @ ys) @ zs"
    by (simp only: append_Nil)
  finally show "[] @ (ys @ zs) = ([] @ ys) @ zs"
    by this
next
  fix x xs
  assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs"
  have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))"
    by (simp only: append_Cons)
  also have "… = x # ((xs @ ys) @ zs)"
    by (simp only: HI)
  also have "… = (x # (xs @ ys)) @ zs"
    by (simp only: append_Cons)
  also have "… = ((x # xs) @ ys) @ zs"
    by (simp only: append_Cons)
  finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs"
    by this
qed
 
(* 2ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  have "[] @ (ys @ zs) = ys @ zs" by simp
  also have "… = ([] @ ys) @ zs" by simp
  finally show "[] @ (ys @ zs) = ([] @ ys) @ zs" .
next
  fix x xs
  assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs"
  have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))" by simp
  also have "… = x # ((xs @ ys) @ zs)" by simp
  also have "… = (x # (xs @ ys)) @ zs" by simp
  also have "… = ((x # xs) @ ys) @ zs" by simp
  finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" .
qed
 
(* 3ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  show "[] @ (ys @ zs) = ([] @ ys) @ zs" by simp
next
  fix x xs
  assume "xs @ (ys @ zs) = (xs @ ys) @ zs"
  then show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" by simp
qed
 
(* 4ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs)
  then show ?case by simp
qed
 
(* 5ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by (rule append_assoc [symmetric])
 
(* 6ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by (induct xs) simp_all
 
(* 7ª demostración *)
lemma "xs @ (ys @ zs) = (xs @ ys) @ zs"
  by simp
 
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>

Soluciones →

Pruebas de length (repeat x n) = n

José A. Alonso-

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

  • (length xs) es la longitud de la lista xs. Por ejemplo,
     length [1,2,5,2] = 4
  • (repeat x n) es la lista que tiene el elemento x n veces. Por ejemplo,
     repeat 7 3 = [7, 7, 7]

Demostrar que

   length (repeat x n) = n

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

import data.list.basic
open nat
open list
 
variable {α : Type}
variable (x : α)
variable (n : ℕ)
 
example :
  length (repeat x n) = n :=
sorry
Soluciones con Lean
import data.list.basic
open nat
open list
 
set_option pp.structure_projections false
 
variable {α : Type}
variable (x : α)
variable (n : ℕ)
 
-- 1ª demostración
example :
  length (repeat x n) = n :=
begin
  induction n with n HI,
  { calc length (repeat x 0)
          = length []                : congr_arg length (repeat.equations._eqn_1 x)
      ... = 0                        : length.equations._eqn_1 },
  { calc length (repeat x (succ n))
         = length (x :: repeat x n)  : congr_arg length (repeat.equations._eqn_2 x n)
     ... = length (repeat x n) + 1   : length.equations._eqn_2 x (repeat x n)
     ... = n + 1                     : congr_arg2 (+) HI rfl
     ... = succ n                    : rfl, },
end
 
-- 2ª demostración
example :
  length (repeat x n) = n :=
begin
  induction n with n HI,
  { calc length (repeat x 0)
          = length []                : rfl
      ... = 0                        : rfl },
  { calc length (repeat x (succ n))
         = length (x :: repeat x n)  : rfl
     ... = length (repeat x n) + 1   : rfl
     ... = n + 1                     : by rw HI
     ... = succ n                    : rfl, },
end
 
-- 3ª demostración
example : length (repeat x n) = n :=
begin
  induction n with n HI,
  { refl, },
  { dsimp,
    rw HI, },
end
 
-- 4ª demostración
example : length (repeat x n) = n :=
begin
  induction n with n HI,
  { simp, },
  { simp [HI], },
end
 
-- 5ª demostración
example : length (repeat x n) = n :=
by induction n ; simp [*]
 
-- 6ª demostración
example : length (repeat x n) = n :=
nat.rec_on n
  ( show length (repeat x 0) = 0, from
      calc length (repeat x 0)
           = length []                : rfl
       ... = 0                        : rfl )
  ( assume n,
    assume HI : length (repeat x n) = n,
    show length (repeat x (succ n)) = succ n, from
      calc length (repeat x (succ n))
           = length (x :: repeat x n) : rfl
       ... = length (repeat x n) + 1  : rfl
       ... = n + 1                    : by rw HI
       ... = succ n                   : rfl )
 
-- 7ª demostración
example : length (repeat x n) = n :=
nat.rec_on n
  ( by simp )
  ( λ n HI, by simp [HI])
 
-- 8ª demostración
example : length (repeat x n) = n :=
length_repeat x n
 
-- 9ª demostración
example : length (repeat x n) = n :=
by simp
 
-- 10ª demostración
lemma length_repeat_1 :
  ∀ n, length (repeat x n) = n
| 0 := by calc length (repeat x 0)
               = length ([] : list α)         : rfl
           ... = 0                            : rfl
| (n+1) := by calc length (repeat x (n + 1))
                   = length (x :: repeat x n) : rfl
               ... = length (repeat x n) + 1  : rfl
               ... = n + 1                    : by rw length_repeat_1
 
-- 11ª demostración
lemma length_repeat_2 :
  ∀ n, length (repeat x n) = n
| 0     := by simp
| (n+1) := by simp [*]

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>

Soluciones con Isabelle/HOL
theory "Pruebas_de_length_(repeat_x_n)_Ig_n"
imports Main
begin
 
(* 1ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  have "length (replicate 0 x) = length ([] :: 'a list)"
    by (simp only: replicate.simps(1))
  also have "… = 0"
    by (rule list.size(3))
  finally show "length (replicate 0 x) = 0"
    by this
next
  fix n
  assume HI : "length (replicate n x) = n"
  have "length (replicate (Suc n) x) =
        length (x # replicate n x)"
    by (simp only: replicate.simps(2))
  also have "… = length (replicate n x) + 1"
    by (simp only: list.size(4))
  also have "… = Suc n"
    by (simp only: HI)
  finally show "length (replicate (Suc n) x) = Suc n"
    by this
qed
 
(* 2ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  show "length (replicate 0 x) = 0"
    by simp
next
  fix n
  assume "length (replicate n x) = n"
  then show "length (replicate (Suc n) x) = Suc n"
    by simp
qed
 
(* 3ª demostración⁾*)
lemma "length (replicate n x) = n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed
 
(* 4ª demostración⁾*)
lemma "length (replicate n x) = n"
  by (rule length_replicate)
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

Soluciones →

Límite de sucesiones no decrecientes

José A. Alonso-

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

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

   def limite (u: ℕ → ℝ) (a: ℝ) :=
     ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε
<pre lang="text">
donde se usa la notación |x| para el valor absoluto de x
<pre lang="text">
   notation `|`x`|` := abs x

y que la sucesión u es no decreciente por

   def no_decreciente (u : ℕ → ℝ) :=
     ∀ n m, n ≤ m → u n ≤ u m

Demostrar que si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n.

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

import data.real.basic
import tactic
 
variable {u : ℕ → ℝ}
variable (a : ℝ)
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε
 
def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m
 
example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
sorry
Soluciones con Lean
import data.real.basic
import tactic
 
variable {u : ℕ → ℝ}
variable (a : ℝ)
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε
 
def no_decreciente (u : ℕ → ℝ) :=
  ∀ n m, n ≤ m → u n ≤ u m
 
-- 1ª demostración
example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
begin
  intro n,
  by_contradiction H,
  push_neg at H,
  replace H : u n - a > 0 := sub_pos.mpr H,
  cases h (u n - a) H with m hm,
  let k := max n m,
  specialize hm k (le_max_right _ _),
  specialize h' n k (le_max_left _ _),
  replace hm : |u k - a| < u k - a, by
    calc |u k - a| < u n - a : hm
               ... ≤ u k - a : sub_le_sub_right h' a,
  rw ← not_le at hm,
  apply hm,
  exact le_abs_self (u k - a),
end
 
-- 2ª demostración
example
  (h : limite u a)
  (h' : no_decreciente u)
  : ∀ n, u n ≤ a :=
begin
  intro n,
  by_contradiction H,
  push_neg at H,
  cases h (u n - a) (by linarith) with m hm,
  specialize hm (max n m) (le_max_right _ _),
  specialize h' n (max n m) (le_max_left _ _),
  rw abs_lt at hm,
  linarith,
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>

Soluciones con Isabelle/HOL
theory Limite_de_sucesiones_no_decrecientes
imports Main HOL.Real
begin
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"
 
definition no_decreciente :: "(nat ⇒ real) ⇒ bool"
  where "no_decreciente u ⟷ (∀ n m. n ≤ m ⟶ u n ≤ u m)"
 
(* 1ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof (rule allI)
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then have "a < u n"
      by (rule not_le_imp_less)
    then have H : "u n - a > 0"
      by (simp only: diff_gt_0_iff_gt)
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by blast
    let ?k = "max n m"
    have "n ≤ ?k"
      by (simp only: assms(2) no_decreciente_def)
    then have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by blast
    have "¦u ?k - a¦ < u n - a"
      by (simp only: hm)
    also have "… ≤ u ?k - a"
      using ‹u n ≤ u ?k› by (rule diff_right_mono)
    finally have "¦u ?k - a¦ < u ?k - a"
      by this
    then have "¬ u ?k - a ≤ ¦u ?k - a¦"
      by (simp only: not_le_imp_less)
    moreover have "u ?k - a ≤ ¦u ?k - a¦"
      by (rule abs_ge_self)
    ultimately show False
      by (rule notE)
  qed
qed
 
(* 2ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof (rule allI)
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then have H : "u n - a > 0"
      by simp
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by blast
    let ?k = "max n m"
    have "¦u ?k - a¦ < u n - a"
      using hm by simp
    moreover have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by simp
    ultimately have "¦u ?k - a¦ < u ?k - a"
      by simp
    then show False
      by simp
  qed
qed
 
(* 3ª demostración *)
lemma
  assumes "limite u a"
          "no_decreciente u"
  shows   "∀ n. u n ≤ a"
proof
  fix n
  show "u n ≤ a"
  proof (rule ccontr)
    assume "¬ u n ≤ a"
    then obtain m where hm : "∀p≥m. ¦u p - a¦ < u n - a"
      using assms(1) limite_def by fastforce
    let ?k = "max n m"
    have "¦u ?k - a¦ < u n - a"
      using hm by simp
    moreover have "u n ≤ u ?k"
      using assms(2) no_decreciente_def by simp
    ultimately show False
      by simp
  qed
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>

Soluciones →

Las sucesiones divergentes positivas no tienen límites finitos

José A. Alonso-

En Lean, una sucesión u₀, u₁, u₂, … se puede representar mediante una función (u : ℕ → ℝ) de forma que u(n) es uₙ.

Se define que a es el límite de la sucesión u, por

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

donde se usa la notación |x| para el valor absoluto de x

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

La sucesión u diverge positivamente cuando, para cada número real A, se puede encontrar un número natural m tal que, para n > m , se tenga u(n) > A. En Lean se puede definir por

   def diverge_positivamente (u : ℕ → ℝ) :=
     ∀ A, ∃ m, ∀ n ≥ m, u n > A

Demostrar que si u diverge positivamente, entonces ningún número real es límite de u.

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

import data.real.basic
import tactic
 
variable  {u : ℕ → ℝ}
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε
 
def diverge_positivamente (u : ℕ → ℝ) :=
  ∀ A, ∃ m, ∀ n ≥ m, u n > A
 
example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
sorry
Soluciones con Lean
import data.real.basic
import tactic
 
variable  {u : ℕ → ℝ}
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - a| < ε
 
def diverge_positivamente (u : ℕ → ℝ) :=
  ∀ A, ∃ m, ∀ n ≥ m, u n > A
 
-- 1ª demostración
example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
begin
  push_neg,
  intros a ha,
  cases ha 1 zero_lt_one with m1 hm1,
  cases h (a+1) with m2 hm2,
  let m := max m1 m2,
  specialize hm1 m (le_max_left _ _),
  specialize hm2 m (le_max_right _ _),
  replace hm1 : u m - a < 1 := lt_of_abs_lt hm1,
  replace hm2 : 1 < u m - a := lt_sub_iff_add_lt'.mpr hm2,
  apply lt_irrefl (u m),
  calc u m < a + 1 : sub_lt_iff_lt_add'.mp hm1
       ... < u m   : lt_sub_iff_add_lt'.mp hm2,
end
 
-- 2ª demostración
example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
begin
  push_neg,
  intros a ha,
  cases ha 1 (by linarith) with m1 hm1,
  cases h (a+1) with m2 hm2,
  let m := max m1 m2,
  replace hm1 : |u m - a| < 1 := by finish,
  replace hm1 : u m - a < 1   := lt_of_abs_lt hm1,
  replace hm2 : u m > a + 1   := by finish,
  replace hm2 : 1 < u m - a   := lt_sub_iff_add_lt'.mpr hm2,
  apply lt_irrefl (u m),
  calc u m < a + 1 : by linarith
       ... < u m   : by linarith
end
 
-- 3ª demostración
example
  (h : diverge_positivamente u)
  : ¬(∃ a, limite u a) :=
begin
  push_neg,
  intros a ha,
  cases ha 1 (by linarith) with m1 hm1,
  cases h (a+1) with m2 hm2,
  let m := max m1 m2,
  specialize hm1 m (le_max_left _ _),
  specialize hm2 m (le_max_right _ _),
  rw abs_lt at hm1,
  linarith,
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>

Soluciones con Isabelle/HOL
theory Las_sucesiones_divergentes_positivas_no_tienen_limites_finitos
imports Main HOL.Real
begin
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"
 
definition diverge_positivamente :: "(nat ⇒ real) ⇒ bool"
  where "diverge_positivamente u ⟷ (∀A. ∃m. ∀n≥m. u n > A)"
 
(* 1ª demostración *)
lemma
  assumes "diverge_positivamente u"
  shows   "∄a. limite u a"
proof (rule notI)
  assume "∃a. limite u a"
  then obtain a where "limite u a" try
    by auto
  then obtain m1 where hm1 : "∀n≥m1. ¦u n - a¦ < 1"
    using limite_def by fastforce
  obtain m2 where hm2 : "∀n≥m2. u n > a + 1"
    using assms diverge_positivamente_def by blast
  let ?m = "max m1 m2"
  have "u ?m < u ?m" using hm1 hm2
  proof -
    have "?m ≥ m1"
      by (rule max.cobounded1)
    have "?m ≥ m2"
      by (rule max.cobounded2)
    have "u ?m - a < 1"
      using hm1 ‹?m ≥ m1› by fastforce
    moreover have "u ?m > a + 1"
      using hm2 ‹?m ≥ m2› by simp
    ultimately show "u ?m < u ?m"
      by simp
  qed
  then show False
    by auto
qed
 
(* 2ª demostración *)
lemma
  assumes "diverge_positivamente u"
  shows   "∄a. limite u a"
proof (rule notI)
  assume "∃a. limite u a"
  then obtain a where "limite u a" try
    by auto
  then obtain m1 where hm1 : "∀n≥m1. ¦u n - a¦ < 1"
    using limite_def by fastforce
  obtain m2 where hm2 : "∀n≥m2. u n > a + 1"
    using assms diverge_positivamente_def by blast
  let ?m = "max m1 m2"
  have "1 < 1"
  proof -
    have "1 < u ?m - a"
      using hm2
      by (metis add.commute less_diff_eq max.cobounded2)
    also have "… < 1"
      using hm1
      by (metis abs_less_iff max_def order_refl)
    finally show "1 < 1" .
  qed
  then show False
    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>

Soluciones →

La suma de los n primeros impares es n^2

José A. Alonso-

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

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

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

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

tales que

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

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

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

import data.finset
import tactic.ring
open nat
 
variable (n : ℕ)
 
def impar (n : ℕ) := 2 * n + 1
 
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
sorry
Soluciones con Lean
import data.finset
import tactic.ring
open nat
 
set_option pp.structure_projections false
 
variable (n : ℕ)
 
def impar (n : ℕ) := 2 * n + 1
 
-- 1ª demostración
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
begin
  induction n with m HI,
  { calc finset.sum (finset.range 0) impar
          = 0
            : by simp
     ...  = 0 ^ 2
            : rfl, },
  { calc finset.sum (finset.range (succ m)) impar
         = finset.sum (finset.range m) impar + impar m
           : finset.sum_range_succ impar m
     ... = m ^ 2 + impar m
           : congr_arg2 (+) HI rfl
     ... = m ^ 2 + 2 * m + 1
           : rfl
     ... = (m + 1) ^ 2
           : by ring_nf
     ... = succ m ^ 2
           : rfl },
end
 
-- 2ª demostración
example :
  finset.sum (finset.range n) impar = n ^ 2 :=
begin
  induction n with d hd,
  { refl, },
  { rw finset.sum_range_succ,
    rw hd,
    change d ^ 2 + (2 * d + 1) = (d + 1) ^ 2,
    ring_nf, },
end

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>

Soluciones con Isabelle/HOL
theory "La_suma_de_los_n_primeros_impares_es_n^2"
imports Main
begin
 
definition impar :: "nat ⇒ nat" where
  "impar n ≡ 2 * n + 1"
 
lemma "sum impar {i::nat. i < n} = n⇧2"
proof (induct n)
  show "sum impar {i. i < 0} = 0⇧2"
    by simp
next
  fix n
  assume HI : "sum impar {i. i < n} = n⇧2"
  have "{i. i < Suc n} = {i. i < n} ∪ {n}"
    by auto
  then have "sum impar {i. i < Suc n} =
             sum impar {i. i < n} + impar n"
    by simp
  also have "… = n⇧2 + (2 * n + 1)"
    using HI impar_def by simp
  also have "… = (n + 1)⇧2"
    by algebra
  also have "… = (Suc n)⇧2"
    by simp
  finally show "sum impar {i. i < Suc n} = (Suc n)⇧2" .
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

Soluciones →

El punto de acumulación de las sucesiones convergente es su límite

José A. Alonso-

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

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

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

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

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

que a es un límite de u por

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

que u es convergente por

   def convergente (u : ℕ → ℝ) :=
     ∃ a, limite u a

que a es un punto de acumulación de u por

   def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
     ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

Demostrar que si u es una sucesión convergente y a es un punto de acumulación de u, entonces a es un límite de u.

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

import data.real.basic
open nat
 
variable  {u : ℕ → ℝ}
variables {a : ℝ}
 
def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε
 
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a
 
def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a
 
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variable  {u : ℕ → ℝ}
variables {a : ℝ}
 
def extraccion (φ : ℕ → ℕ) :=
  ∀ n m, n < m → φ n < φ m
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε
 
def convergente (u : ℕ → ℝ) :=
  ∃ a, limite u a
 
def punto_acumulacion (u : ℕ → ℝ) (a : ℝ) :=
  ∃ φ, extraccion φ ∧ limite (u ∘ φ) a
 
-- Lemas auxiliares
-- ================
 
lemma unicidad_limite_aux
  {a b: ℝ}
  (ha : limite u a)
  (hb : limite u b)
  : b ≤ a :=
begin
  by_contra h,
  set ε := b - a with hε,
  cases ha (ε/2) (by linarith) with A hA,
  cases hb (ε/2) (by linarith) with B hB,
  set N := max A B with hN,
  have hAN : A ≤ N := le_max_left A B,
  have hBN : B ≤ N := le_max_right A B,
  specialize hA N hAN,
  specialize hB N hBN,
  rw abs_lt at hA hB,
  linarith,
end
 
lemma unicidad_limite
  {a b: ℝ}
  (ha : limite u a)
  (hb : limite u b)
  : a = b :=
le_antisymm (unicidad_limite_aux hb ha)
            (unicidad_limite_aux ha hb)
 
lemma limite_subsucesion_aux
  {φ : ℕ → ℕ}
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end
 
lemma limite_subsucesion
  {φ : ℕ → ℕ}
  {a : ℝ}
  (h : limite u a)
  (hφ : extraccion φ)
  : limite (u ∘ φ) a :=
begin
  intros ε hε,
  cases h ε hε with N hN,
  use N,
  intros k hk,
  calc |(u ∘ φ) k - a|
       = |u (φ k) - a| : rfl
   ... < ε             : hN (φ k) _,
  calc φ k
       ≥ k : limite_subsucesion_aux hφ k
   ... ≥ N : hk,
end
 
-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  unfold convergente at hu,
  cases hu with b hb,
  convert hb,
  unfold punto_acumulacion at ha,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  have hφ₃ : limite (u ∘ φ) b,
    from limite_subsucesion hb hφ₁,
  exact unicidad_limite hφ₂ hφ₃,
end
 
-- 1ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  apply unicidad_limite hφ₂ _,
  exact limite_subsucesion hb hφ₁,
end
 
-- 2ª demostración
example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  cases hu with b hb,
  convert hb,
  rcases ha with ⟨φ, hφ₁, hφ₂⟩,
  exact unicidad_limite hφ₂ (limite_subsucesion hb hφ₁),
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>

Soluciones con Isabelle/HOL
theory El_punto_de_acumulacion_de_las_sucesiones_convergente_es_su_limite
imports Main HOL.Real
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"
  where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool" where
  "limite u c ⟷ (∀ε>0. ∃k. ∀n≥k. ¦u n - c¦ < ε)"
 
definition convergente :: "(nat ⇒ real) ⇒ bool" where
  "convergente u ⟷ (∃ a. limite u a)"
 
definition punto_acumulacion :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "punto_acumulacion u a ⟷ (∃φ. extraccion φ ∧ limite (u ∘ φ) a)"
 
(* Lemas auxiliares *)
 
lemma unicidad_limite_aux :
  assumes "limite u a"
          "limite u b"
  shows   "b ≤ a"
proof (rule ccontr)
  assume "¬ b ≤ a"
  let ?ε = "b - a"
  have "0 < ?ε/2"
    using ‹¬ b ≤ a› by auto
  obtain A where hA : "∀n≥A. ¦u n - a¦ < ?ε/2"
    using assms(1) limite_def ‹0 < ?ε/2› by blast
  obtain B where hB : "∀n≥B. ¦u n - b¦ < ?ε/2"
    using assms(2) limite_def ‹0 < ?ε/2› by blast
  let ?C = "max A B"
  have hCa : "∀n≥?C. ¦u n - a¦ < ?ε/2"
    using hA by simp
  have hCb : "∀n≥?C. ¦u n - b¦ < ?ε/2"
    using hB by simp
  have "∀n≥?C. ¦a - b¦ < ?ε"
  proof (intro allI impI)
    fix n assume "n ≥ ?C"
    have "¦a - b¦ = ¦(a - u n) + (u n - b)¦" by simp
    also have "… ≤ ¦u n - a¦ + ¦u n - b¦" by simp
    finally show "¦a - b¦ < b - a"
      using hCa hCb ‹n ≥ ?C› by fastforce
  qed
  then show False by fastforce
qed
 
lemma unicidad_limite :
  assumes "limite u a"
          "limite u b"
  shows   "a = b"
proof (rule antisym)
  show "a ≤ b" using assms(2) assms(1)
    by (rule unicidad_limite_aux)
next
  show "b ≤ a" using assms(1) assms(2)
    by (rule unicidad_limite_aux)
qed
 
lemma limite_subsucesion_aux :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed
 
lemma limite_subsucesion :
  assumes "subsucesion v u"
          "limite u a"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"
    using assms(2) limite_def by auto
  obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ"
    using assms(1) subsucesion_def by auto
  have "∀k≥N. ¦v k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume "N ≤ k"
    also have "... ≤ φ k"
      by (simp add: limite_subsucesion_aux hφ1)
    finally have "N ≤ φ k" .
    have "¦v k - a¦ = ¦u (φ k) - a¦"
      using hφ2 by simp
    also have "… < ε"
      using hN ‹N ≤ φ k› by simp
    finally show "¦v k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦v k - a¦ < ε"
    by auto
qed
 
(* Demostración *)
lemma
  assumes "convergente u"
          "punto_acumulacion u a"
  shows   "limite u a"
proof -
  obtain b where hb : "limite u b"
    using assms(1) convergente_def by auto
  obtain φ where hφ1 : "extraccion φ" and
                 hφ2 : "limite (u ∘ φ) a"
    using assms(2) punto_acumulacion_def  by auto
  have "limite (u ∘ φ) b"
    using hφ1 hb limite_subsucesion subsucesion_def by blast
  with hφ2 have "a = b"
    by (rule unicidad_limite)
  then show "limite u a"
    using hb by simp
qed
 
end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

Soluciones →

Las subsucesiones tienen el mismo límite que la sucesión

José A. Alonso-

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

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

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

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

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

que v es una subsucesión de u por

   def subsucesion (v u : ℕ → ℝ) :=
     ∃ φ, extraccion φ ∧ v = u ∘ φ

y que a es un límite de u por

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

Demostrar que las subsucesiones de una sucesión convergente tienen el mismo límite que la sucesión.

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

import data.real.basic
open nat
 
variables {u v : ℕ → ℝ}
variable  {a : ℝ}
variable  {φ : ℕ → ℕ}
 
def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m
 
def subsucesion (v u : ℕ → ℝ) :=
  ∃ φ, extraccion φ ∧ v = u ∘ φ
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε
 
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variables {u v : ℕ → ℝ}
variable  {a : ℝ}
variable  {φ : ℕ → ℕ}
 
def extraccion (φ : ℕ → ℕ):=
  ∀ n m, n < m → φ n < φ m
 
def subsucesion (v u : ℕ → ℝ) :=
  ∃ φ, extraccion φ ∧ v = u ∘ φ
 
notation `|`x`|` := abs x
 
def limite (u : ℕ → ℝ) (a : ℝ) :=
  ∀ ε > 0, ∃ N, ∀ k ≥ N, |u k - a| < ε
 
-- En la demostración se usará el siguiente lema.
lemma aux
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intro n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h m (m+1) (lt_add_one m), },
end
 
-- 1ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  unfold limite,
  intros ε hε,
  unfold limite at ha,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  unfold subsucesion at hv,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  apply hN,
  apply le_trans hn,
  exact aux hφ1 n,
end
 
-- 2ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  apply hN,
  exact le_trans hn (aux hφ1 n),
end
 
-- 3ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  use N,
  intros n hn,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  exact hN (φ n) (le_trans hn (aux hφ1 n)),
end
 
-- 4ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  use N,
  exact λ n hn, hN (φ n) (le_trans hn (aux hφ1 n)),
end
 
-- 5ª demostración
example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
begin
  intros ε hε,
  cases ha ε hε with N hN,
  rcases hv with ⟨φ, hφ1, hφ2⟩,
  rw hφ2,
  exact ⟨N, λ n hn, hN (φ n) (le_trans hn (aux hφ1 n))⟩,
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>

Soluciones con Isabelle/HOL
theory Las_subsucesiones_tienen_el_mismo_limite_que_la_sucesion
imports Main HOL.Real
begin
 
definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"
 
definition subsucesion :: "(nat ⇒ real) ⇒ (nat ⇒ real) ⇒ bool"
  where "subsucesion v u ⟷ (∃ φ. extraccion φ ∧ v = u ∘ φ)"
 
definition limite :: "(nat ⇒ real) ⇒ real ⇒ bool"
  where "limite u a ⟷ (∀ε>0. ∃N. ∀k≥N. ¦u k - a¦ < ε)"
 
(* En la demostración se usará el siguiente lema *)
lemma aux :
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0" by simp
next
  fix n assume HI : "n ≤ φ n"
  then show "Suc n ≤ φ (Suc n)"
    using assms extraccion_def
    by (metis Suc_leI lessI order_le_less_subst1)
qed
 
(* Demostración *)
lemma
  assumes "subsucesion v u"
          "limite u a"
  shows   "limite v a"
proof (unfold limite_def; intro allI impI)
  fix ε :: real
  assume "ε > 0"
  then obtain N where hN : "∀k≥N. ¦u k - a¦ < ε"
    using assms(2) limite_def by auto
  obtain φ where hφ1 : "extraccion φ" and hφ2 : "v = u ∘ φ"
    using assms(1) subsucesion_def by auto
  have "∀k≥N. ¦v k - a¦ < ε"
  proof (intro allI impI)
    fix k
    assume "N ≤ k"
    also have "... ≤ φ k"
      by (simp add: aux hφ1)
    finally have "N ≤ φ k" .
    have "¦v k - a¦ = ¦u (φ k) - a¦"
      using hφ2 by simp
    also have "… < ε"
      using hN ‹N ≤ φ k› by simp
    finally show "¦v k - a¦ < ε" .
  qed
  then show "∃N. ∀k≥N. ¦v k - a¦ < ε"
    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>

Soluciones →

El conjunto de las clases de equivalencia es una partición

José A. Alonso-

Demostrar que si R es una relación de equivalencia en X, entonces las clases de equivalencia de R es una partición de X.

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

import tactic
 
variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}
 
def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}
 
def particion (A : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ A, x ∈ B ∧ ∀ C ∈ A, x ∈ C → B = C)) ∧ ∅ ∉ A
 
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
sorry
Soluciones con Lean
import tactic
 
variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}
 
def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}
 
def particion (A : set (set X)) : Prop :=
  (∀ x, (∃ B ∈ A, x ∈ B ∧ ∀ C ∈ A, x ∈ C → B = C)) ∧ ∅ ∉ A
 
lemma aux
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
λ z hz, h.2.2 hxy hz
 
-- 1ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        apply le_antisymm,
        { exact aux h hx, },
        { exact aux h (h.2.1 hx), }}}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end
 
-- 2ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use (clase R y),
    split,
    { use y, },
    { split,
      { exact h.1 y, },
      { intros x hx,
        exact le_antisymm (aux h hx) (aux h (h.2.1 hx)), }}},
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
end
 
-- 3ª demostración
example
  (h : equivalence R)
  : particion {a : set X | ∃ s : X, a = clase R s} :=
begin
  split,
  { simp,
    intro y,
    use [clase R y,
         ⟨by use y,
          ⟨h.1 y, λ x hx, le_antisymm (aux h hx) (aux h (h.2.1 hx))⟩⟩], },
  { simp,
    intros x hx,
    have h1 : x ∈ clase R x := h.1 x,
    rw ← hx at h1,
    exact set.not_mem_empty x h1, },
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>

Soluciones con Isabelle/HOL
theory El_conjunto_de_las_clases_de_equivalencia_es_una_particion
imports Main
begin
 
definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"
  where "clase R x = {y. R x y}"
 
definition particion :: "('a set) set ⇒ bool" where
  "particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"
 
lemma
  fixes   R :: "'a ⇒ 'a ⇒ bool"
  assumes "equivp R"
  shows   "particion (⋃x. {clase R x})" (is "particion ?P")
proof (unfold particion_def; intro conjI)
  show "(∀x. ∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C))"
  proof (intro allI)
    fix x
    have "clase R x ∈ ?P"
      by auto
    moreover have "x ∈ clase R x"
      using assms clase_def equivp_def
      by (metis CollectI)
    moreover have "∀C∈?P. x ∈ C ⟶ clase R x = C"
    proof
      fix C
      assume "C ∈ ?P"
      then obtain y where "C = clase R y"
        by auto
      show "x ∈ C ⟶ clase R x = C"
      proof
        assume "x ∈ C"
        then have "R y x"
          using ‹C = clase R y› assms clase_def
          by (metis CollectD)
        then show "clase R x = C"
          using assms ‹C = clase R y› clase_def equivp_def
          by metis
      qed
    qed
    ultimately show "∃B∈?P. x ∈ B ∧ (∀C∈?P. x ∈ C ⟶ B = C)"
      by blast
  qed
next
  show "{} ∉ ?P"
  proof
    assume "{} ∈ ?P"
    then obtain x where "{} = clase R x"
      by auto
    moreover have "x ∈ clase R x"
      using assms clase_def equivp_def
      by (metis CollectI)
    ultimately show False
      by simp
  qed
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>

Soluciones →