Proofs of take n xs ++ drop n xs = xs

José A. Alonso

14-08-2024

Lists

In Lean4, the functions

    take : Nat → List α → Nat
    drop : Nat → List α → Nat
    (++) : List α → List α → List α

are defined such that

(take n xs) is the list consisting of the first n elements of xs. For example,
```
take 2 [3,5,1,9,7] = [3,5]
```
(drop n xs) is the list containing all elements of xs except the first n elements. For example,
```
drop 2 [3,5,1,9,7] = [1,9,7]
```
(xs ++ ys) is the list obtained by concatenating xs and ys. For example,
```
[3,5] ++ [1,9,7] = [3,5,1,9,7]
```

These functions are characterized by the following lemmas:

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_succ_cons : drop (n + 1) (x :: xs) = drop n xs
nil_append     : [] ++ ys = ys
cons_append    : (x :: xs) ++ y = x :: (xs ++ ys)

Prove that

take n xs ++ drop n xs = xs

To do this, complete the following Lean4 theory:

import Mathlib.Data.List.Basic
import Mathlib.Tactic
open List Nat

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

example : take n xs ++ drop n xs = xs :=
by sorry

Proofs of the equality length(xs ++ ys) = length(xs) + length(ys)

José A. Alonso

07-08-2024

Lists

In Lean, the functions

    length : List α → Nat
    (++)   : List α → List α → List α

are defined such that

(length xs) is the length of xs. For example,
```
length [2,3,5,3] = 4
```
(xs ++ ys) is the list obtained by concatenating xs and ys. For example.
```
[1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]
```

These functions are characterized by the following lemmas:

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

To prove that

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

To that end, complete the following Lean4 theory

import Mathlib.Tactic
open List

variable {α : Type}
variable (xs ys : List α)

example :
  length (xs ++ ys) = length xs + length ys :=
by sorry

Asociatividad de la concatenación de listas

José A. Alonso

31-07-2024

Listas

En Lean4 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 Lean4:

import Mathlib.Data.List.Basic
open List

variable {α : Type}
variable (xs ys zs : List α)

-- 1ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as HI
  . calc [] ++ (ys ++ zs)
         = ys ++ zs                := nil_append (ys ++ zs)
       _ = ([] ++ ys) ++ zs        := congrArg (. ++ zs) (nil_append ys).symm
  . calc (a :: as) ++ (ys ++ zs)
         = a :: (as ++ (ys ++ zs)) := cons_append a as (ys ++ zs)
       _ = a :: ((as ++ ys) ++ zs) := congrArg (a :: .) HI
       _ = (a :: (as ++ ys)) ++ zs := (cons_append a (as ++ ys) zs).symm

-- 2ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  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]

-- 3ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as HI
  . calc [] ++ (ys ++ zs)
         = ys ++ zs                := by exact rfl
       _ = ([] ++ ys) ++ zs        := by exact 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

-- 4ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  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) := congrArg (a :: .) HI
       _ = (a :: (as ++ ys)) ++ zs := by simp
       _ = ((a :: as) ++ ys) ++ zs := by simp

-- 5ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as
  . simp
  . exact (append_assoc (a :: as) ys zs).symm

-- 6ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction' xs with a as HI
  . -- ⊢ [] ++ (ys ++ zs) = ([] ++ ys) ++ zs
    rw [nil_append]
    -- ⊢ ys ++ zs = ([] ++ ys) ++ zs
    rw [nil_append]
  . -- a : α
    -- as : List α
    -- HI : as ++ (ys ++ zs) = as ++ ys ++ zs
    -- ⊢ (a :: as) ++ (ys ++ zs) = ((a :: as) ++ ys) ++ zs
    rw [cons_append]
    -- ⊢ a :: (as ++ (ys ++ zs)) = ((a :: as) ++ ys) ++ zs
    rw [HI]
    -- ⊢ a :: ((as ++ ys) ++ zs) = ((a :: as) ++ ys) ++ zs
    rw [cons_append]
    -- ⊢ a :: ((as ++ ys) ++ zs) = (a :: (as ++ ys)) ++ zs
    rw [cons_append]

-- 7ª demostración
-- ===============

lemma conc_asoc_1 (xs ys zs : List α) :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by
  induction xs with
  | nil => calc
    [] ++ (ys ++ zs)
        = ys ++ zs         := by rw [nil_append]
      _ = ([] ++ ys) ++ zs := by rw [nil_append]
  | cons a as HI => 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 := congrArg (. ++ zs) (cons_append a as ys)

-- 8ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs  :=
(append_assoc xs ys zs).symm

-- 9ª demostración
-- ===============

example :
  xs ++ (ys ++ zs) = (xs ++ ys) ++ zs :=
by simp

-- Lemas usados
-- ============

-- variable (x : α)
-- #check (append_assoc xs ys zs : (xs ++ ys) ++ zs = xs ++ (ys ++ zs))
-- #check (cons_append x xs ys : (x :: xs) ++ ys = x :: (xs ++ ys))
-- #check (cons_inj x : x :: xs = x :: ys ↔ xs = ys)
-- #check (nil_append xs : [] ++ xs = xs)

Pruebas de length (replicate n x) = n

José A. Alonso

29-07-2024

Listas

En Lean4 están definidas las funciones length y replicate tales que

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

Demostrar que

length (replicate n x) = n

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

import Mathlib.Data.List.Basic
open Nat
open List

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

example :
  length (replicate n x) = n :=
by sorry

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

José A. Alonso

27-07-2024

Límites

En Lean4, una sucesión \(u_0, u_1, u_2, ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es \(u_n\).

En Lean4, 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| < ε

y que la sucesión \(u\) es no decreciente por

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

Demostrar con Lean4 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 Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}
variable (a : ℝ)

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 :=
by sorry

Las sucesiones divergentes positivas no tienen límites finitos

José A. Alonso

26-07-2024

Límites

En Lean4, una sucesión \(u_0, u_1, u_2, ...\) 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| < ε

La sucesión \(u\) diverge positivamente cuando, para cada número real \(A\), se puede encontrar un número natural \(m\) tal que si \(n ≥ m\), entonces \(uₙ > 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 Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable {u : ℕ → ℝ}

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) :=
by sorry

Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u

José A. Alonso

25-07-2024

Límites

En Lean4, una sucesión \(u_0, u_1, u_2, u_3 ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es el término \(u_n\).

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \(u_0, u_2, u_4, u_6, ...\) se ha obtenido con la función de extracción \(f\) tal que \(f(n) = 2n\).

En Lean4, se puede definir que \(f\) es una función de extracción por

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

que a es un límite de u por

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

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

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

que la sucesión u es de Cauchy por

   def suc_cauchy (u : ℕ → ℝ) :=
     ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε

Demostrar con Lean4 que si \(u\) es una sucesión de Cauchy y \(a\) es un punto de acumulación de \(u\), entonces \(a\) es el límite de \(u\).

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

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Nat

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

example
  (hu : suc_cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
by sorry

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

José A. Alonso

16-07-2024

Límites

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(f\) tal que \(f(n) = 2n\).

En Lean4, se puede definir que \(f\) es una función de extracción por

   def extraccion (f : ℕ → ℕ) :=
     ∀ n m, n < m → f n < f 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 : ℝ) :=
     ∃ f, extraccion f ∧ limite (u ∘ f) a

Demostrar con Lean4 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 Lean4:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

open Nat

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

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

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

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

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

example
  (hu : convergente u)
  (ha : punto_acumulacion u a)
  : limite u a :=
by sorry

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

José A. Alonso

15-07-2024

Límites

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_3, u_4, u_6, ... \] se ha obtenido con la función de extracción \(φ\) tal que \(φ(n) = 2n\).

En Lean4, 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 con Lean4 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 Lean4:

import Mathlib.Data.Real.Basic
open Nat

variable {u v : ℕ → ℝ}
variable {a : ℝ}
variable {φ : ℕ → ℕ}

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

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

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

example
  (hv : subsucesion v u)
  (ha : limite u a)
  : limite v a :=
by sorry

Si a es un punto de acumulación de u, entonces (∀ε>0)(∀n∈ℕ)(∃k≥n)[u(k)−a| < ε]

José A. Alonso

14-07-2024

Límites

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión \[ u_0, u_2, u_4, u_6, ... \] se ha obtenido con la función de extracción \(φ\) tal que \(φ(n) = 2n\).

En Lean4, se puede definir que \(φ\) es una función de extracción por

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

También se puede definir que \(a\) es un límite de \(u\) por

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

Los puntos de acumulación de una sucesión son los límites de sus subsucesiones. En Lean4 se puede definir por

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

Demostrar que si \(a\) es un punto de acumulación de \(u\), entonces \[ (∀ ε > 0)(∀ n ∈ ℕ)(∃ k ≥ n)[|u(k) - a| < ε \]

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

import Mathlib.Data.Real.Basic
open Nat

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

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

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

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

example
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ n, ∃ k ≥ n, |u k - a| < ε :=
by sorry