# Concatenation of lists

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-08.

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 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-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)