Skip to main content

Posts about Lists

RSS feed (Lists, en)

Canal RSS (Listas, es)

Also available in:

Español (Listas)

Equivalence of reverse definitions

Discrete Structures/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

Discrete Structures/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)

Discrete Structures/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…