Concatenation of lists

module lists.concatenation-lists where

Imports

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import group-theory.monoids

open import lists.lists

Idea

Two lists can be concatenated to form a single list.

Definition

concat-list : {l : Level} {A : UU l} → list A → (list A → list A)
concat-list {l} {A} = fold-list id (λ a f → (cons a) ∘ f)

Properties

List concatenation is associative and unital

Concatenation of lists is an associative operation and nil is the unit for list concatenation.

associative-concat-list :
  {l1 : Level} {A : UU l1} (x y z : list A) →
  Id (concat-list (concat-list x y) z) (concat-list x (concat-list y z))
associative-concat-list nil y z = refl
associative-concat-list (cons a x) y z =
  ap (cons a) (associative-concat-list x y z)

left-unit-law-concat-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (concat-list nil x) x
left-unit-law-concat-list x = refl

right-unit-law-concat-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (concat-list x nil) x
right-unit-law-concat-list nil = refl
right-unit-law-concat-list (cons a x) =
  ap (cons a) (right-unit-law-concat-list x)

list-Monoid : {l : Level} (X : Set l) → Monoid l
list-Monoid X =
  pair
    ( pair (list-Set X) (pair concat-list associative-concat-list))
    ( pair nil (pair left-unit-law-concat-list right-unit-law-concat-list))

`snoc`-law for list concatenation

snoc-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) (a : A) →
  snoc (concat-list x y) a ＝ concat-list x (snoc y a)
snoc-concat-list nil y a = refl
snoc-concat-list (cons b x) y a = ap (cons b) (snoc-concat-list x y a)

The length of a concatenation of two lists is the sum of the length of the two lists

length-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id (length-list (concat-list x y)) ((length-list x) +ℕ (length-list y))
length-concat-list nil y = inv (left-unit-law-add-ℕ (length-list y))
length-concat-list (cons a x) y =
  ( ap succ-ℕ (length-concat-list x y)) ∙
  ( inv (left-successor-law-add-ℕ (length-list x) (length-list y)))

An `η`-rule for lists

eta-list :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (concat-list (head-list x) (tail-list x)) x
eta-list nil = refl
eta-list (cons a x) = refl

eta-list' :
  {l1 : Level} {A : UU l1} (x : list A) →
  Id (concat-list (remove-last-element-list x) (last-element-list x)) x
eta-list' nil = refl
eta-list' (cons a nil) = refl
eta-list' (cons a (cons b x)) = ap (cons a) (eta-list' (cons b x))

Heads and tails of concatenated lists

head-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( head-list (concat-list x y))
     ( head-list (concat-list (head-list x) (head-list y)))
head-concat-list nil nil = refl
head-concat-list nil (cons x y) = refl
head-concat-list (cons a x) y = refl

tail-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( tail-list (concat-list x y))
     ( concat-list (tail-list x) (tail-list (concat-list (head-list x) y)))
tail-concat-list nil y = refl
tail-concat-list (cons a x) y = refl

last-element-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( last-element-list (concat-list x y))
     ( last-element-list
       ( concat-list (last-element-list x) (last-element-list y)))
last-element-concat-list nil nil = refl
last-element-concat-list nil (cons b nil) = refl
last-element-concat-list nil (cons b (cons c y)) =
  last-element-concat-list nil (cons c y)
last-element-concat-list (cons a nil) nil = refl
last-element-concat-list (cons a nil) (cons b nil) = refl
last-element-concat-list (cons a nil) (cons b (cons c y)) =
  last-element-concat-list (cons a nil) (cons c y)
last-element-concat-list (cons a (cons b x)) y =
  last-element-concat-list (cons b x) y

remove-last-element-concat-list :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( remove-last-element-list (concat-list x y))
     ( concat-list
       ( remove-last-element-list (concat-list x (head-list y)))
       ( remove-last-element-list y))
remove-last-element-concat-list nil nil = refl
remove-last-element-concat-list nil (cons a nil) = refl
remove-last-element-concat-list nil (cons a (cons b y)) = refl
remove-last-element-concat-list (cons a nil) nil = refl
remove-last-element-concat-list (cons a nil) (cons b y) = refl
remove-last-element-concat-list (cons a (cons b x)) y =
  ap (cons a) (remove-last-element-concat-list (cons b x) y)

tail-concat-list' :
  {l1 : Level} {A : UU l1} (x y : list A) →
  Id ( tail-list (concat-list x y))
     ( concat-list
       ( tail-list x)
       ( tail-list (concat-list (last-element-list x) y)))
tail-concat-list' nil y = refl
tail-concat-list' (cons a nil) y = refl
tail-concat-list' (cons a (cons b x)) y =
  ap (cons b) (tail-concat-list' (cons b x) y)