Concatenation of lists

Content created by Egbert Rijke, Fredrik Bakke and Viktor Yudov.

Created on 2023-04-08.
Last modified on 2024-05-05.

module lists.concatenation-lists where
Imports 
open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.sets
open import foundation.universe-levels

open import foundation-core.coproduct-types

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)

TODO: Concats

in-concat-left :
  {l : Level} {A : UU l} (l1 l2 : list A)
  {a : A} → a ∈-list l1 → a ∈-list (concat-list l1 l2)
in-concat-left _ _ (is-head a _) =
  is-head a _
in-concat-left _ l2 (is-in-tail a x l1 in-l1) =
  is-in-tail a x (concat-list l1 l2) (in-concat-left l1 l2 in-l1)

in-concat-right :
  {l : Level} {A : UU l} (l1 l2 : list A)
  {a : A} → a ∈-list l2 → a ∈-list (concat-list l1 l2)
in-concat-right nil l2 in-l2 = in-l2
in-concat-right (cons x l1) l2 in-l2 =
  is-in-tail _ x (concat-list l1 l2) (in-concat-right l1 l2 in-l2)

in-concat-list :
  {l : Level} {A : UU l} (l1 l2 : list A)
  {a : A} → a ∈-list (concat-list l1 l2) → (a ∈-list l1) + (a ∈-list l2)
in-concat-list nil l2 {a} in-list = inr in-list
in-concat-list (cons x l1) l2 {.x} (is-head .x _) = inl (is-head x l1)
in-concat-list (cons x l1) l2 {a} (is-in-tail .a .x _ in-list)
  with in-concat-list l1 l2 in-list
... | inl in-l1 = inl (is-in-tail a x l1 in-l1)
... | inr in-l2 = inr in-l2

Recent changes