# Reversing lists

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-08.

module lists.reversing-lists where

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

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

open import lists.concatenation-lists
open import lists.flattening-lists
open import lists.functoriality-lists
open import lists.lists


## Idea

The reverse of a list of elements in A lists the elements of A in the reversed order.

## Definition

reverse-list : {l : Level} {A : UU l} → list A → list A
reverse-list nil = nil
reverse-list (cons a l) = snoc (reverse-list l) a


## Properties

reverse-unit-list :
{l1 : Level} {A : UU l1} (a : A) →
Id (reverse-list (unit-list a)) (unit-list a)
reverse-unit-list a = refl

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

length-reverse-list :
{l1 : Level} {A : UU l1} (x : list A) →
Id (length-list (reverse-list x)) (length-list x)
length-reverse-list nil = refl
length-reverse-list (cons a x) =
( length-snoc-list (reverse-list x) a) ∙
( ap succ-ℕ (length-reverse-list x))

reverse-concat-list :
{l1 : Level} {A : UU l1} (x y : list A) →
Id
( reverse-list (concat-list x y))
( concat-list (reverse-list y) (reverse-list x))
reverse-concat-list nil y =
inv (right-unit-law-concat-list (reverse-list y))
reverse-concat-list (cons a x) y =
( ap (λ t → snoc t a) (reverse-concat-list x y)) ∙
( ( snoc-concat-list (reverse-list y) (reverse-list x) a))

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

reverse-flatten-list :
{l1 : Level} {A : UU l1} (x : list (list A)) →
Id
( reverse-list (flatten-list x))
( flatten-list (reverse-list (map-list reverse-list x)))
reverse-flatten-list nil = refl
reverse-flatten-list (cons a x) =
( reverse-concat-list a (flatten-list x)) ∙
( ( ap (λ t → concat-list t (reverse-list a)) (reverse-flatten-list x)) ∙
( inv
( flatten-snoc-list
( reverse-list (map-list reverse-list x))
( (reverse-list a)))))

reverse-reverse-list :
{l1 : Level} {A : UU l1} (x : list A) →
Id (reverse-list (reverse-list x)) x
reverse-reverse-list nil = refl
reverse-reverse-list (cons a x) =
( reverse-snoc-list (reverse-list x) a) ∙
( ap (cons a) (reverse-reverse-list x))

head-reverse-list :
{l1 : Level} {A : UU l1} (x : list A) →
head-list (reverse-list x) ＝ last-element-list x
head-reverse-list (cons a nil) = refl
head-reverse-list (cons a (cons b x)) =
( head-snoc-snoc-list (reverse-list x) b a) ∙

last-element-reverse-list :
{l1 : Level} {A : UU l1} (x : list A) →
Id (last-element-list (reverse-list x)) (head-list x)
last-element-reverse-list x =
( inv (head-reverse-list (reverse-list x))) ∙

tail-reverse-list :
{l1 : Level} {A : UU l1} (x : list A) →
Id (tail-list (reverse-list x)) (reverse-list (remove-last-element-list x))
tail-reverse-list nil = refl
tail-reverse-list (cons a nil) = refl
tail-reverse-list (cons a (cons b x)) =
( tail-snoc-snoc-list (reverse-list x) b a) ∙
( ap (λ t → snoc t a) (tail-reverse-list (cons b x)))

remove-last-element-reverse-list :
{l1 : Level} {A : UU l1} (x : list A) →
Id (remove-last-element-list (reverse-list x)) (reverse-list (tail-list x))
remove-last-element-reverse-list x =
( inv (reverse-reverse-list (remove-last-element-list (reverse-list x)))) ∙
( ( inv (ap reverse-list (tail-reverse-list (reverse-list x)))) ∙
( ap (reverse-list ∘ tail-list) (reverse-reverse-list x)))