Skip to main content

Proofs of "flatten (mirror a) = reverse (flatten a)"

Binary trees

The tree corresponding to

    3
   / \
  2   4
 / \
1   5

can be represented by the term

Node 3 (Node 2 (Leaf 1) (Leaf 5)) (Leaf 4)

using the datatype defined by

   inductive Tree' (α : Type) : Type
     | Leaf : α → Tree' α
     | Node : α → Tree' α → Tree' α → Tree' α

The mirror image of the previous tree is

  3
 / \
4   2
   / \
  5   1

and the list obtained by flattening it (traversing it in infix order) is

[4, 3, 5, 2, 1]

The definition of the function that calculates the mirror image is

   def mirror : Tree' α → Tree' α
     | Leaf x     => Leaf x
     | Node x l r => Node x (mirror r) (mirror l)

and the one that flattens the tree is

   def flatten : Tree' α → List α
     | Leaf x     => [x]
     | Node x l r => (flatten l) ++ [x] ++ (flatten r)

Prove that

   flatten (mirror a) = reverse (flatten a)

To do this, complete the following Lean4 theory:

import Mathlib.Tactic

open List

variable {α : Type}

set_option pp.fieldNotation false

inductive Tree' (α : Type) : Type
  | Leaf : α → Tree' α
  | Node : α → Tree' α → Tree' α → Tree' α

namespace Tree'

variable (a l r : Tree' α)
variable (x : α)

def mirror : Tree' α → Tree' α
  | Leaf x     => Leaf x
  | Node x l r => Node x (mirror r) (mirror l)

def flatten : Tree' α → List α
  | Leaf x     => [x]
  | Node x l r => (flatten l) ++ [x] ++ (flatten r)

example :
  flatten (mirror a) = reverse (flatten a) :=
by sorry

Read more…

Proofs that the mirror function of binary trees is involutive

Binary trees

The tree corresponding to

    3
   / \
  2   4
 / \
1   5

can be represented by the term

Node 3 (Node 2 (Leaf 1) (Leaf 5)) (Leaf 4)

using the datatype defined by

   inductive Tree' (α : Type) : Type
     | Leaf : α → Tree' α
     | Node : α → Tree' α → Tree' α → Tree' α

The mirror image of the previous tree is

  3
 / \
4   2
   / \
  5   1

whose term is

Node 3 (Leaf 4) (Node 2 (Leaf 5) (Leaf 1))

The definition of the function that calculates the mirror image is

   def mirror : Tree' α → Tree' α
     | (Leaf x)     => Leaf x
     | (Node x l r) => Node x (mirror r) (mirror l)

Prove that the mirror function is involutive; that is,

   mirror (mirror a) = a

To do this, complete the following Lean4 theory:

import Mathlib.Tactic

variable {α : Type}

set_option pp.fieldNotation false

inductive Tree' (α : Type) : Type
  | Leaf : α → Tree' α
  | Node : α → Tree' α → Tree' α → Tree' α

namespace Tree'

variable (a l r : Tree' α)
variable (x : α)

def mirror : Tree' α → Tree' α
  | (Leaf x)     => Leaf x
  | (Node x l r) => Node x (mirror r) (mirror l)

example :
  mirror (mirror a) = a :=
by sorry

end Tree'

Read more…

Equivalence of reverse definitions

Lists

In Lean4, the function

    reverse : List α → List α

is defined such that (reverse xs) is the list obtained by reversing the order of elements in xs, such that the first element becomes the last, the second element becomes the second to last, and so on, resulting in a new list with the same elements but in the opposite sequence. For example,

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

Its definition is

    def reverseAux : List α → List α → List α
      | [],    ys => ys
      | x::xs, ys => reverseAux xs (x::ys)

    def reverse (xs : List α) : List α :=
      reverseAux xs []

The following lemmas characterize its behavior:

    reverseAux_nil : reverseAux [] ys = ys
    reverseAux_cons : reverseAux (x::xs) ys = reverseAux xs (x::ys)

An alternative definition is

    def reverse2 : List α → List α
      | []        => []
      | (x :: xs) => reverse2 xs ++ [x]

Prove that the two definitions are equivalent; that is,

    reverse xs = reverse2 xs

To do this, complete the following Lean4 theory:

import Mathlib.Data.List.Basic
open List

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

example : reverse xs = reverse2 xs :=
by sorry

Read more…

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

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

Read more…

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

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

Read more…

Asociatividad de la concatenación de listas

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)

Read more…

Pruebas de length (replicate n x) = n

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

Read more…

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

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

Read more…

Las sucesiones divergentes positivas no tienen límites finitos

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

Read more…

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

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

Read more…