-- Needed for some proof automation.
{-# OPTIONS --no-require-unique-meta-solutions #-}
open import 1Lab.Prelude
open import 1Lab.Function.Embedding

open import Data.Dec
open import Data.Nat
open import Data.Fin using (Fin; fsuc; fzero)
open import Data.Sum

import Data.Fin as Fin

open import StringLab.Equiv

module StringLab.Data.List where

private variable
  ℓ ℓ' ℓ'' : Level
  A B C D T F : Type ℓ

Basic operations on lists🔗

If we wish to prove things about strings, then we will need to start by defining strings! This is an extremely consequential moment: at the end of the day, mechanized mathematics is programming, and we have to contend with the same engineering tradeoffs we encounter when doing “normal” software engineering. In fact, the engineering tradeoffs are even more severe, as we need to worry about performance and ease of proof.

With this in mind, we opt to define strings as singly-linked lists. This choice may seem somewhat unorthodox, but is the best option for the following reasons:

1. Agda is a pure, total functional language; this means that we do not have any mutable state, and every data structure is persistent (Driscoll et al. 1986). Notably, it is impossible to build a persistent array with $O(1)$ random access (see Demaine et al. (Demaine, Langerman, and Price 2010)).
2. With point (1) in mind, our only option is to use some sort of balanced tree¹. This is where mathematical concerns come into the picture: the more complicated the data structure, the harder reasoning about it will be. Moreover, most of the algorithms we care about are single passes over a list that do not actually require random access, so all of this work would be for nought! Therefore, we opt to use the simplest balanced tree of them all: the persistent singly linked list.

Persistent singly linked lists have some major upsides, and one glaring problem. First, let’s consider the pros.

1. Access to the front of the string is $O(1)\text{.}$
2. We can share memory across strings. EG: if we have a string $abc\text{,}$ we can form the two strings $xabc$ and $yabc\text{,}$ and only store the suffix $abc$ once. Moreover, adding an element on to the front of a string is $O(1)$
3. Induction over strings is very easy: we do not need to worry about balance at all.

Now, for the problem: random access is $O(n)\text{.}$ In particular, accessing the last element of a string is extremely expensive. This unfortunate fact will drive a lot of our algorithmic choices down the line.

With that discussion out of the way, we can actually define singly linked lists. Luckily, this is already done in the 1Lab, and we can just re-use the definition².

open import Data.List hiding (reverse) public

However, the 1Lab’s list module is rather sparse, so we will need to do quite a bit ourselves.

{-# DISPLAY _++_ xs (x ∷ []) = xs ∷r x #-}

Paths🔗

We begin by proving some basic results about equality types of lists. Note that we are using homotopy type theory, so there are potentially many ways for two things to be equal!

However, this is not the case for the empty list: there is exactly a single equality between the empty list and itself.

empty-loop-is-contr : is-contr (Path (List A) [] [])
empty-loop-is-contr .centre = refl
empty-loop-is-contr .paths = J (λ { [] p → refl ≡ p ; (x ∷ xs) p → Lift _ ⊤ }) refl

This means that the identity type xs ≡ [] is a proposition; either a list is empty, at which point [] ≡ [] is contractible or the list is non-empty, at which point x ∷ xs ≡ [] is an empty type.

empty-path-is-prop : ∀ {xs : List A} → is-prop (xs ≡ [])
empty-path-is-prop {xs = []} = is-contr→is-prop empty-loop-is-contr
empty-path-is-prop {xs = x ∷ xs} p = absurd (∷≠[] p)

instance
  H-Level-empty-path : ∀ {xs : List A} → H-Level (xs ≡ []) 
  H-Level-empty-path = prop-instance empty-path-is-prop
  {-# OVERLAPS H-Level-empty-path #-}

Inversion lemmas🔗

Two cons cells are equal precisely when the head and the tail are equal.

opaque
  ∷-inversion : ∀ {x y : A} {xs ys : List A} → (x ∷ xs ≡ y ∷ ys) ≃ (x ≡ y × xs ≡ ys)
  ∷-inversion = Iso→Equiv $
    ⟨ ∷-head-inj , ∷-tail-inj ⟩ , iso (uncurry (ap₂ _∷_))
      (λ _ → refl)
      (J (λ { [] p → absurd (∷≠[] p) ; (y ∷ ys) p → ap₂ _∷_ (ap (head _) p) (ap tail p) ≡ p }) refl)

Proof automation🔗

Empty and nonempty lists🔗

Our next move is to declare a pair of predicates that classify empty and non-empty lists, respectively. These are both marked as instances to aid with some proof automation³.

data Empty {A : Type ℓ} : List A → Type ℓ where
  empty : Empty []

data Nonempty {A : Type ℓ} : List A → Type ℓ where
  nonempty : ∀ {x : A} {xs : List A} → Nonempty (x ∷ xs)

Both Empty and Nonempty are propositions.

Empty-is-prop : ∀ {xs : List A} → is-prop (Empty xs)
Empty-is-prop empty empty = refl

Nonempty-is-prop : ∀ {xs : List A} → is-prop (Nonempty xs)
Nonempty-is-prop nonempty nonempty = refl

Moreover, both Empty [] and Nonempty (x ∷ xs) are inhabited, so they must be contractible.

Empty-is-contr : is-contr (Empty {A = A} [])
Empty-is-contr = is-prop∙→is-contr Empty-is-prop empty

Nonempty-is-contr : ∀ (x : A) (xs : List A) → is-contr (Nonempty (x ∷ xs))
Nonempty-is-contr x xs = is-prop∙→is-contr Nonempty-is-prop nonempty

data UnlessEmpty {A : Type ℓ} (C : Type ℓ') : List A → Type (ℓ ⊔ ℓ') where
  was-empty : UnlessEmpty C []
  wasnt-empty : ∀ {xs} → C → UnlessEmpty C xs

data UnlessCons {A : Type ℓ} (C : Type ℓ') : List A → Type (ℓ ⊔ ℓ') where
  was-cons : ∀ {x xs} → UnlessCons C (x ∷ xs)
  wasnt-cons : ∀ {xs} → C → UnlessCons C xs

instance
  UnlessEmpty-Empty
    : UnlessEmpty {A = A} C []
  UnlessEmpty-Empty = was-empty
  {-# OVERLAPS UnlessEmpty-Empty #-}

  UnlessEmpty-Default
    : ∀ {xs : List A}
    → ⦃ _ : C ⦄
    → UnlessEmpty C xs
  UnlessEmpty-Default ⦃ c ⦄ = wasnt-empty c
  {-# INCOHERENT UnlessEmpty-Default #-}

  UnlessCons-Cons
    : ∀ {x : A} {xs : List A}
    → UnlessCons {A = A} C (x ∷ xs)
  UnlessCons-Cons = was-cons
  {-# OVERLAPS UnlessCons-Cons #-}

  UnlessCons-Default
    : ∀ {xs : List A}
    → ⦃ _ : C ⦄
    → UnlessCons C xs
  UnlessCons-Default ⦃ c ⦄ = wasnt-cons c
  {-# INCOHERENT UnlessCons-Default #-}

instance
  H-Level-Nonempty
    : ∀ {xs : List A} {n} ⦃ _ : UnlessCons ( ≤ n) xs ⦄ → H-Level (Nonempty xs) n
  H-Level-Nonempty ⦃ was-cons ⦄ = basic-instance  (Nonempty-is-contr _ _)
  H-Level-Nonempty ⦃ wasnt-cons (s≤s 0≤x) ⦄ = prop-instance Nonempty-is-prop

  H-Level-Empty
    : ∀ {xs : List A} {n} ⦃ _ : UnlessEmpty ( ≤ n) xs ⦄ → H-Level (Empty xs) n
  H-Level-Empty ⦃ was-empty ⦄ = basic-instance  Empty-is-contr
  H-Level-Empty ⦃ wasnt-empty (s≤s 0≤x) ⦄ = prop-instance Empty-is-prop

A non-empty list cannot be empty, and vice versa.

nonempty≃¬empty : ∀ {xs : List A} → Nonempty xs ≃ (¬ Empty xs)
nonempty≃¬empty {xs = []} =
  is-empty→≃ (λ ()) (_$ empty)
nonempty≃¬empty {xs = x ∷ xs} =
  is-contr→≃ (hlevel ) (is-prop∙→is-contr (Π-is-hlevel  (λ ())) (λ ()))

empty≃¬nonempty : ∀ {xs : List A} → Empty xs ≃ (¬ Nonempty xs)
empty≃¬nonempty {xs = []} =
  is-contr→≃ (hlevel ) (is-prop∙→is-contr (Π-is-hlevel  (λ ())) (λ ()))
empty≃¬nonempty {xs = x ∷ xs} =
  is-empty→≃ (λ ()) (_$ nonempty)

Finally, both Empty and Nonempty can be characterised via path types.

Empty-lens : ∀ {xs : List A} → Empty xs ≃ (xs ≡ [])
Empty-lens {xs = []} =
  is-contr→≃ Empty-is-contr empty-loop-is-contr
Empty-lens {xs = x ∷ xs} =
  is-empty→≃ (Equiv.to nonempty≃¬empty nonempty) ∷≠[]

Nonempty-lens
  : ∀ {A : Type ℓ} {xs : List A}
  → Nonempty xs ≃ (Σ[ u ∈ A ] Σ[ us ∈ List A ] xs ≡ u ∷ us)
Nonempty-lens {xs = []} =
  is-empty→≃ (Equiv.to empty≃¬nonempty empty) (λ (u , us , p) → absurd (∷≠[] (sym p)))
Nonempty-lens {xs = x ∷ xs} =
  is-contr→≃
    (Nonempty-is-contr x xs)
    (contr (x , xs , refl) λ (u , us , p) →
      J (λ { [] p → absurd (∷≠[] p)
           ; (u ∷ us) p → (x , xs , refl) ≡ (u , us , p)
           })
        refl
        p)

nonempty≃∷
  : {A : Type ℓ}
  → (Σ[ xs ∈ List A ] Nonempty xs) ≃ (A × List A)
nonempty≃∷ {A = A} =
  Σ[ xs ∈ List A ] Nonempty xs                             ≃⟨ Σ-ap id≃ (λ _ → Nonempty-lens) ⟩≃
  Σ[ xs ∈ List A ] Σ[ u ∈ A ] Σ[ us ∈ List A ] xs ≡ u ∷ us ≃⟨ Σ-swap₂ ∙e Σ-ap id≃ (λ _ → Σ-swap₂) ⟩≃
  Σ[ u ∈ A ] Σ[ us ∈ List A ] Σ[ xs ∈ List A ] xs ≡ u ∷ us ≃⟨ Σ-ap id≃ (λ u → Σ-contract (λ us → singleton-is-contr (u ∷ us))) ⟩≃
  A × List A ≃∎

We can obviously decide if a list is (non)empty.

instance
  Dec-Empty : ∀ {xs : List A} → Dec (Empty xs)
  Dec-Empty {xs = []} = yes empty
  Dec-Empty {xs = x ∷ xs} = no λ ()

  Dec-Nonempty : ∀ {xs : List A} → Dec (Nonempty xs)
  Dec-Nonempty {xs = []} = no λ ()
  Dec-Nonempty {xs = x ∷ xs} = yes nonempty

empty? : ∀ (xs : List A) → Empty xs ⊎ Nonempty xs
empty? [] = inl empty
empty? (x ∷ xs) = inr nonempty

We can give a nice characterisation of when concatenations are non-empty.

++-nonemptyl : ∀ (xs ys : List A) → Nonempty xs → Nonempty (xs ++ ys)
++-nonemptyl xs ys nonempty = nonempty

++-nonemptyr : ∀ (xs ys : List A) → Nonempty ys → Nonempty (xs ++ ys)
++-nonemptyr [] ys ys-ne = ys-ne
++-nonemptyr (x ∷ xs) ys ys-ne = nonempty

++-not-both-empty
  : ∀ (xs ys : List A)
  → Nonempty (xs ++ ys) ≃ (¬ (Empty xs × Empty ys))
++-not-both-empty [] [] =
  is-empty→≃ (λ ()) (_$ (empty , empty))
++-not-both-empty [] (x ∷ ys) =
  is-contr→≃ (hlevel ) (Π-is-hlevel  (λ ()))
++-not-both-empty (x ∷ xs) ys =
  is-contr→≃ (hlevel ) (Π-is-hlevel  (λ ()))

++-nonempty
  : ∀ (xs ys : List A)
  → Nonempty (xs ++ ys)
  ≃ ((Nonempty xs × Empty ys) ⊎ (Empty xs × Nonempty ys) ⊎ (Nonempty xs × Nonempty ys))
++-nonempty xs ys =
  Nonempty (xs ++ ys)
    ≃⟨ ++-not-both-empty xs ys ⟩≃
  ¬ (Empty xs × Empty ys)
    ≃⟨ Dec→demorgan≃ ⟩≃
  ¬ Empty xs × Empty ys ⊎ Empty xs × ¬ Empty ys ⊎ ¬ Empty xs × ¬ Empty ys
    ≃˘⟨ ⊎-ap (×-apl (λ _ → nonempty≃¬empty)) (⊎-ap (×-apr (λ _ → nonempty≃¬empty)) (Σ-ap nonempty≃¬empty (λ _ → nonempty≃¬empty))) ⟩≃˘
  ((Nonempty xs × Empty ys) ⊎ (Empty xs × Nonempty ys) ⊎ (Nonempty xs × Nonempty ys))
    ≃∎

instance
  Empty-[] : Empty {A = A} []
  Empty-[] = empty
  {-# INCOHERENT Empty-[] #-}

  NonEmpty-∷ : ∀ {x : A} {xs : List A} → Nonempty (x ∷ xs)
  NonEmpty-∷ = nonempty
  {-# INCOHERENT NonEmpty-∷ #-}

  NonEmpty-++-∷r
    : ∀ {xs ys : List A} {y : A}
    → Nonempty (xs ++ y ∷ ys)
  NonEmpty-++-∷r {xs = xs} {ys = ys} {y = y} = ++-nonemptyr xs (y ∷ ys) nonempty
  {-# OVERLAPPABLE NonEmpty-++-∷r #-}

  NonEmpty-++-lr
    : ∀ {xs ys : List A}
    → ⦃ _ : Nonempty ys ⦄
    → Nonempty ((xs ++ ys) ++ [])
  NonEmpty-++-lr {xs = xs} {ys = ys} ⦃ ne ⦄ = ++-nonemptyl (xs ++ ys) [] (++-nonemptyr xs ys ne)
  {-# OVERLAPPABLE NonEmpty-++-lr #-}
  -- All out of good rules, let's just give up.

Heads and tails of lists🔗

If $xs$ is non-empty, then the tail of $xs++ys$ is $\mathrm{tail}xs++ys\text{.}$

tail-nonempty-++ : ∀ (xs ys : List A) ⦃ _ : Nonempty xs ⦄ → tail (xs ++ ys) ≡ tail xs ++ ys
tail-nonempty-++ (x ∷ xs) ys = refl

tail-nonempty-∷r : ∀ (xs : List A) (x : A) ⦃ _ : Nonempty xs ⦄ → tail (xs ∷r x) ≡ tail xs ∷r x
tail-nonempty-∷r xs x = tail-nonempty-++ xs (x ∷ [])

Conversely, the head of $xs++ys$ is the head of $xs\text{,}$ defaulting to the head of $ys\text{.}$

head-++ : ∀ (def : A) (xs ys : List A) → head def (xs ++ ys) ≡ head (head def ys) xs
head-++ def [] ys = refl
head-++ def (x ∷ xs) ys = refl

Length🔗

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

length-++ : ∀ (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-++ [] ys = refl
length-++ (x ∷ xs) ys = ap suc (length-++ xs ys)

length-conj : ∀ (xs ys : List A)→ length (xs ++ ys) ≡ length (ys ++ xs)
length-conj xs ys =
  length (xs ++ ys)     ≡⟨ length-++ xs ys ⟩≡
  length xs + length ys ≡⟨ +-commutative (length xs) (length ys) ⟩≡
  length ys + length xs ≡˘⟨ length-++ ys xs ⟩≡˘
  length (ys ++ xs)     ∎

The following lemma is a useful combination of results: if the length of $ws++ys$ is equal to the length of $xs++zs\text{,}$ and $\mid ys\mid =\mid zs\mid \text{,}$ then $\mid xs\mid =\mid zs\mid \text{.}$

length-++-cancelr
  : ∀ (ws xs ys zs : List A)
  → length (ws ++ ys) ≡ length (xs ++ zs)
  → length ys ≡ length zs
  → length ws ≡ length xs
length-++-cancelr ws xs ys zs p q =
  +-inj (length ys) (length ws) (length xs) $
    length ys + length ws ≡⟨ +-commutative (length ys) (length ws) ⟩≡
    length ws + length ys ≡˘⟨ length-++ ws ys ⟩≡˘
    length (ws ++ ys)     ≡⟨ p ⟩≡
    length (xs ++ zs)     ≡⟨ length-++ xs zs ⟩≡
    length xs + length zs ≡⟨ +-commutative (length xs) (length zs) ⟩≡
    length zs + length xs ≡⟨ ap (_+ length xs) (sym q) ⟩≡
    length ys + length xs ∎

We also have a corresponding lemma for cancelling on the left.

length-++-cancell
  : ∀ (ws xs ys zs : List A)
  → length (ws ++ ys) ≡ length (xs ++ zs)
  → length ws ≡ length xs
  → length ys ≡ length zs

Luckily, the proof is much shorter, as we can appeal to the previous lemma.

length-++-cancell ws xs ys zs p q =
  length-++-cancelr ys zs ws xs
    (length-conj ys ws ∙ p ∙ length-conj xs zs)
    q

Reversing lists and duality🔗

One of the defining features of the free monoid is that is about as far from a group as one can get: the only invertible element is the empty word!

++-zerol : ∀ (xs ys : List A) → xs ++ ys ≡ [] → xs ≡ []
++-zerol [] ys p = refl
++-zerol (x ∷ xs) ys p = absurd (∷≠[] p)

++-zeror : ∀ (xs ys : List A) → xs ++ ys ≡ [] → ys ≡ []
++-zeror [] ys p = p
++-zeror (x ∷ xs) ys p = absurd (∷≠[] p)

++-zero-lens : ∀ (xs ys : List A) → (xs ++ ys ≡ []) ≃ (xs ≡ [] × ys ≡ [])
++-zero-lens xs ys =
  prop-ext! ⟨ ++-zerol xs ys , ++-zeror xs ys ⟩ (uncurry (ap₂ _++_))

However, lists do have something that almost acts like an inverse. Namely, we can reverse a list⁴. Crucially, reverse is an involution: this is an extremely powerful reasoning principle, as it lets us obtain dual theorems “for free”.

Unfortunately, reversing a singly-linked list is $\Theta (n)\text{.}$ Moreover, it completely ruins any sharing. It is also somewhat annoying to reason if one isn’t careful; it is very easy to make reversal not ammenable to structural induction over lists!

With these pitfalls in mind, we start by defining a fused reverse-and-concatenate operation, which we denote $x⋉y\text{;}$ the mnemonic is that $x$ gets “flipped” during the concatenation. Wew can then define reverse as $x⋉[]$ ⁵.

_⋉_ : List A → List A → List A
[] ⋉ ys = ys
(x ∷ xs) ⋉ ys = xs ⋉ (x ∷ ys)

reverse : List A → List A
reverse xs = xs ⋉ []

infix  _⋉_
{-# INJECTIVE_FOR_INFERENCE _⋉_ #-}
{-# DISPLAY _⋉_ xs [] = reverse xs #-}

Our fused reverse-and-concatenation operation interacts nicely with concatenation.

⋉-assocl : ∀ (xs ys zs : List A) → xs ⋉ (ys ⋉ zs) ≡ (ys ++ xs) ⋉ zs
⋉-assocl xs [] zs = refl
⋉-assocl xs (y ∷ ys) zs = ⋉-assocl xs ys (y ∷ zs)

⋉-assocr : ∀ (xs ys zs : List A) → (xs ⋉ ys) ⋉ zs ≡ ys ⋉ (xs ++ zs)
⋉-assocr [] ys zs = refl
⋉-assocr (x ∷ xs) ys zs = ⋉-assocr xs (x ∷ ys) zs

⋉-exchanger : ∀ (xs ys zs : List A) → (xs ⋉ ys) ++ zs ≡ xs ⋉ (ys ++ zs)
⋉-exchanger [] ys zs = refl
⋉-exchanger (x ∷ xs) ys zs = ⋉-exchanger xs (x ∷ ys) zs

⋉-exchangel : ∀ (xs ys zs : List A) → xs ++ (ys ⋉ zs) ≡ (xs ++ reverse ys) ++ zs
⋉-exchangel [] ys zs = sym (⋉-exchanger ys [] zs)
⋉-exchangel (x ∷ xs) ys zs = ap (x ∷_) (⋉-exchangel xs ys zs)

We can specialise these lemmas to deduce that reverse is an antihomomorphism.

reverse-++ : ∀ (xs ys : List A) → reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ xs ys =
  (xs ++ ys) ⋉ []        ≡˘⟨ ⋉-assocl ys xs [] ⟩≡˘
  ys ⋉ (xs ⋉ [])         ≡˘⟨ ⋉-exchanger ys [] (xs ⋉ []) ⟩≡˘
  (ys ⋉ []) ++ (xs ⋉ []) ∎

Moreover, reverse is an involution. As mentioned earlier, this lets us prove quite a few results via duality-style arguments.

reverse-reverse : ∀ (xs : List A) → reverse (reverse xs) ≡ xs
reverse-reverse xs = ⋉-assocr xs [] [] ∙ ++-idr xs

reverse-is-equiv : is-equiv (reverse {A = A})
reverse-is-equiv = is-involutive→is-equiv reverse-reverse

reverse-≃ : List A ≃ List A
reverse-≃ = reverse , reverse-is-equiv

reverse-cancel : ∀ {xs ys : List A} → (reverse xs ≡ reverse ys) ≃ (xs ≡ ys)
reverse-cancel = (ap reverse , equiv→cancellable reverse-is-equiv) e⁻¹

We can also characterise how reverse interacts with ⋉, cons, and snoc.

reverse-⋉ : ∀ (xs ys : List A) → reverse (xs ⋉ ys) ≡ reverse ys ++ xs
reverse-⋉ xs ys =
  (xs ⋉ ys) ⋉ []    ≡⟨ ⋉-assocr xs ys [] ⟩≡
  ys ⋉ (xs ++ [])   ≡⟨ ap (ys ⋉_) (++-idr xs) ⟩≡
  ys ⋉ ([] ++ xs)   ≡˘⟨ ⋉-exchanger ys [] xs ⟩≡˘
  (ys ⋉ []) ++ xs ∎

reverse-∷ : ∀ (x : A) (xs : List A) → reverse (x ∷ xs) ≡ reverse xs ∷r x
reverse-∷ x xs = reverse-++ (x ∷ []) xs

reverse-∷r : ∀ (xs : List A) (x : A) → reverse (xs ∷r x) ≡ x ∷ reverse xs
reverse-∷r xs x = reverse-++ xs (x ∷ [])

Reversing empty and nonempty lists🔗

We then proceed to prove a battery of lemmas that describe how empty and nonempty lists interact with reversal.

⋉-nonemptyr : ∀ (xs ys : List A) → ⦃ Nonempty ys ⦄ → Nonempty (xs ⋉ ys)
⋉-nonemptyr [] (y ∷ ys) = nonempty
⋉-nonemptyr (x ∷ xs) (y ∷ ys) = ⋉-nonemptyr xs (x ∷ y ∷ ys)

⋉-nonemptyl : ∀ (xs ys : List A) → ⦃ Nonempty xs ⦄ → Nonempty (xs ⋉ ys)
⋉-nonemptyl (x ∷ xs) ys = ⋉-nonemptyr xs (x ∷ ys)

⋉-++-nonempty
  : ∀ (xs ys : List A)
  → Nonempty (xs ⋉ ys) ≃ Nonempty (xs ++ ys)
⋉-++-nonempty [] ys = id≃
⋉-++-nonempty (x ∷ xs) ys =
  prop-ext! (λ _ → nonempty) (λ _ → ⋉-nonemptyl (x ∷ xs) ys)

⋉-++-empty
  : ∀ (xs ys : List A)
  → Empty (xs ⋉ ys) ≃ Empty (xs ++ ys)
⋉-++-empty xs ys =
  empty≃¬nonempty
  ∙e Π-dom≃ (⋉-++-nonempty xs ys e⁻¹)
  ∙e empty≃¬nonempty e⁻¹

reverse-nonempty
  : ∀ (xs : List A)
  → Nonempty (reverse xs) ≃ Nonempty xs
reverse-nonempty xs =
  ⋉-++-nonempty xs [] ∙e path→equiv (ap Nonempty (++-idr xs))

reverse-empty
  : ∀ (xs : List A)
  → Empty (reverse xs) ≃ Empty xs
reverse-empty xs =
  ⋉-++-empty xs [] ∙e path→equiv (ap Empty (++-idr xs))

⋉-nonempty
  : ∀ (xs ys : List A)
  → Nonempty (xs ⋉ ys)
  ≃ ((Nonempty xs × Empty ys) ⊎ (Empty xs × Nonempty ys) ⊎ (Nonempty xs × Nonempty ys))
⋉-nonempty xs ys =
  ⋉-++-nonempty xs ys
  ∙e ++-nonempty xs ys

-- Fall back on the concatenation proof automation for `_⋉_`{.Agda}.
instance
  NonEmpty-reverse-∷
    : ∀ {xs ys : List A}
    → ⦃ Nonempty (xs ++ ys) ⦄
    → Nonempty (xs ⋉ ys)
  NonEmpty-reverse-∷ ⦃ ne ⦄ = Equiv.from (⋉-++-nonempty _ _) ne
  {-# INCOHERENT NonEmpty-reverse-∷ #-}

We also take the time to describe the heads and tails of reversed lists.

head-⋉ : ∀ (def : A) (xs ys : List A) → head def (xs ⋉ ys) ≡ head (head def ys) (reverse xs)
head-⋉ def xs ys =
  head def (xs ⋉ ys)              ≡⟨ ap (head def) (⋉-exchangel [] xs ys) ⟩≡
  head def (reverse xs ++ ys)     ≡⟨ head-++ def (reverse xs) ys ⟩≡
  head (head def ys) (reverse xs) ∎

tail-⋉ : ∀ (xs ys : List A) → ⦃ _ : Nonempty xs ⦄ → tail (xs ⋉ ys) ≡ tail (reverse xs) ++ ys
tail-⋉ (x ∷ xs) ys =
  tail ((x ∷ xs) ⋉ ys)          ≡⟨ ap tail (⋉-exchangel [] (x ∷ xs) ys) ⟩≡
  tail (reverse (x ∷ xs) ++ ys) ≡⟨ tail-nonempty-++ (reverse (x ∷ xs)) ys ⟩≡
  tail (reverse (x ∷ xs)) ++ ys ∎

As mentioned above, duality is a powerful reasoning principle, and lets us get quite a few proofs “for free”. A nice example of duality in action is the following lemma, which characterizes the equality type of a snoc cell.

∷r-lens : ∀ {xs ys : List A} {x y : A} → (xs ∷r x ≡ ys ∷r y) ≃ (xs ≡ ys × x ≡ y)
∷r-lens {xs = xs} {ys = ys} {x = x} {y = y} =
  xs ∷r x ≡ ys ∷r y                     ≃˘⟨ reverse-cancel ⟩≃˘
  reverse (xs ∷r x) ≡ reverse (ys ∷r y) ≃⟨ ∙-pre-equiv (sym (reverse-∷r xs x)) ∙e ∙-post-equiv (reverse-∷r ys y) ⟩≃
  x ∷ reverse xs ≡ y ∷ reverse ys       ≃⟨ ∷-inversion ⟩≃
  x ≡ y × reverse xs ≡ reverse ys       ≃⟨ ×-apr (λ _ → reverse-cancel) ⟩≃
  x ≡ y × xs ≡ ys                       ≃⟨ ×-swap ⟩≃
  xs ≡ ys × x ≡ y                       ≃∎

∷r-last-inj : ∀ {xs ys : List A} {x y : A} → xs ∷r x ≡ ys ∷r y → x ≡ y
∷r-last-inj p = snd (Equiv.to ∷r-lens p)

∷r-init-inj : ∀ {xs ys : List A} {x y : A} → xs ∷r x ≡ ys ∷r y → xs ≡ ys
∷r-init-inj p = fst (Equiv.to ∷r-lens p)

Reversing a list preserves its length.

length-⋉ : ∀ (xs ys : List A) → length (xs ⋉ ys) ≡ length xs + length ys
length-⋉ [] ys = refl
length-⋉ (x ∷ xs) ys = length-⋉ xs (x ∷ ys) ∙ +-sucr (length xs) (length ys)

Take and drop🔗

If we truncate the length of a list $xs$ to a length larger that $\mid xs\mid \text{,}$ then we get the original list.

take-all : ∀ (n : Nat) (xs : List A) → length xs ≤ n → take n xs ≡ xs
take-all zero [] xs≤n = refl
take-all (suc n) [] xs≤n = refl
take-all (suc n) (x ∷ xs) xs≤n = ap (x ∷_) (take-all n xs (≤-peel xs≤n))

Dually, if we drop the more elements than a list contains, then we get the empty list.

drop-all : ∀ (n : Nat) (xs : List A) → length xs ≤ n → drop n xs ≡ []
drop-all zero [] xs≤n = refl
drop-all (suc n) [] xs≤n = refl
drop-all (suc n) (x ∷ xs) xs≤n = drop-all n xs (≤-peel xs≤n)

If we truncate $xs++ys$ to $n\le \mid xs\mid$ elements, then it is the same as truncating $xs\text{.}$

take-++l : ∀ (n : Nat) (xs ys : List A) → n ≤ length xs → take n (xs ++ ys) ≡ take n xs
take-++l zero xs ys n≤xs = refl
take-++l (suc n) (x ∷ xs) ys (s≤s n≤xs) = ap (x ∷_) (take-++l n xs ys n≤xs)

We also have an analogous result for drop.

drop-++r : ∀ (n : Nat) (xs ys : List A) → n ≤ length xs → drop n (xs ++ ys) ≡ drop n xs ++ ys
drop-++r zero xs ys n≤xs = refl
drop-++r (suc n) (x ∷ xs) ys n≤xs = drop-++r n xs ys (≤-peel n≤xs)

Accessing the $i\text{th}$ index of $xs$ is the same as removing $i<\mid xs\mid$ element from the front, and then getting the head.

drop-head
  : ∀ (xs : List A)
  → (i : Fin (length xs))
  → head (xs ! i) (drop (Fin.to-nat i) xs) ≡ (xs ! i)
drop-head (x ∷ xs) fzero = refl
drop-head (x ∷ xs) (fsuc i) = drop-head xs i

If we remove $i<\mid xs\mid$ elements from $xs\text{,}$ then the result is nonempty.

drop-to-nat-nonempty
  : ∀ (xs : List A)
  → (i : Fin (length xs))
  → Nonempty (drop (Fin.to-nat i) xs)
drop-to-nat-nonempty (x ∷ xs) fzero = nonempty
drop-to-nat-nonempty (x ∷ xs) (fsuc i) = drop-to-nat-nonempty xs i

More generally, if we remove less elements than the length of $xs$ for $xs$ noempty, then drop n xs is nonempty.

drop-nonempty
  : ∀ (n : Nat) (xs : List A)
  → ⦃ _ : Nonempty xs ⦄
  → n < length xs
  → Nonempty (drop n xs)
drop-nonempty zero xs n<xs = auto
drop-nonempty (suc n) (x ∷ x' ∷ xs) (s≤s n<xs) = drop-nonempty n (x' ∷ xs) n<xs

Powers of a list🔗

Powers of lists are an extremely important concept, and will pop up constantly during the results of our development. Moreover, we compute powers of lists in the course of some algorithms, so it behooves us to spend some time optimizing.

In particular, we define a fused power-and-concatenate operation⁶ power, which computes $x^n+y$ in a single shot; this makes reasoning more difficult, but the sharing benefits are worth the annoyance.

powers : List A → Nat → List A → List A
powers xs zero ys = ys
powers xs (suc n) ys = xs ++ powers xs n ys

We also define an optimized version of powers{Agda} that takes powers of a single character.

replicate : A → Nat → List A → List A
replicate x zero xs = xs
replicate x (suc n) xs = x ∷ replicate x n xs

Taking powers of the empty list and concatenating $xs$ is the identity.

powers-[] : ∀ (n : Nat) (xs : List A) → powers [] n xs ≡ xs
powers-[] zero xs = refl
powers-[] (suc n) xs = powers-[] n xs

The following pair of results are simple lemmas that let us move around concatenations through fused power-and-concatenations.

powers-pulll
  : ∀ (xs : List A) (n : Nat) (ys : List A)
  → powers xs n (xs ++ ys) ≡ powers xs (suc n) ys
powers-pulll xs zero ys = refl
powers-pulll xs (suc n) ys = ap (xs ++_) (powers-pulll xs n ys)

powers-pushr
  : ∀ (xs : List A) (n : Nat) (ys zs : List A)
  → powers xs n (ys ++ zs) ≡ powers xs n ys ++ zs
powers-pushr xs zero ys zs = refl
powers-pushr xs (suc n) ys zs =
  xs ++ powers xs n (ys ++ zs) ≡⟨ ap (xs ++_) (powers-pushr xs n ys zs) ⟩≡
  xs ++ powers xs n ys ++ zs   ≡˘⟨ ++-assoc xs (powers xs n ys) zs ⟩≡˘
  (xs ++ powers xs n ys) ++ zs ∎

Note that $x+x^n=x^n+x\text{.}$ In general, powers are the only situation where lists are commutative.

powers-comm : ∀ (xs : List A) (n : Nat) → xs ++ powers xs n [] ≡ powers xs n [] ++ xs
powers-comm xs n =
  sym (powers-pulll xs n [])
  ∙ ap (powers xs n) (++-idr xs)
  ∙ powers-pushr xs n [] xs

While we are at it, we may as well describe how ⋉ interacts with powers.

powers-⋉-interchange
  : ∀ (xs : List A) (n : Nat) (ys : List A) (zs : List A)
  → powers xs n ys ⋉ zs ≡ ys ⋉ powers (reverse xs) n zs
powers-⋉-interchange xs zero ys zs = refl
powers-⋉-interchange xs (suc n) ys zs =
  (xs ++ powers xs n ys) ⋉ zs                   ≡˘⟨ ⋉-assocl (powers xs n ys) xs zs ⟩≡˘
  powers xs n ys ⋉ (xs ⋉ zs)                    ≡⟨ powers-⋉-interchange xs n ys (xs ⋉ zs) ⟩≡
  ys ⋉ powers (reverse xs) n ⌜ xs ⋉ zs ⌝        ≡⟨ ap! (⋉-exchangel [] xs zs) ⟩≡
  ys ⋉ powers (reverse xs) n (reverse xs ++ zs) ≡⟨ ap (ys ⋉_) (powers-pulll (reverse xs) n zs) ⟩≡
  ys ⋉ (reverse xs ++ powers (reverse xs) n zs) ∎

Moreover, we get the usual formulae for exponentials.

powers-powers
  : ∀ (xs : List A) (n : Nat) (k : Nat) (ys : List A)
  → powers xs (n + k) ys ≡ powers xs n (powers xs k ys)
powers-powers xs zero k ys = refl
powers-powers xs (suc n) k ys = ap (xs ++_) (powers-powers xs n k ys)

Powers are computed via concatenations, so length interacts nicely with them.

length-powers
  : ∀ (xs : List A) (n : Nat) (ys : List A)
  → length (powers xs n ys) ≡ (length xs * n) + length ys
length-powers xs zero ys =
  sym (ap (_+ length ys) (*-zeror (length xs)))
length-powers xs (suc n) ys =
  length (xs ++ powers xs n ys)           ≡⟨ length-++ xs (powers xs n ys) ⟩≡
  length xs + length (powers xs n ys)     ≡⟨ ap (length xs +_) (length-powers xs n ys) ⟩≡
  length xs + (length xs * n + length ys) ≡⟨ +-associative (length xs) (length xs * n) (length ys) ⟩≡
  (length xs + length xs * n) + length ys ≡˘⟨ ap (_+ length ys) (*-sucr (length xs) n) ⟩≡˘
  length xs * suc n + length ys           ∎

The following lemma illustrates that truncation behaves somewhat like a root-finding operation.

powers-take
  : (xs : List A) (ys : List A) (d n : Nat)
  → .⦃ _ : Positive n ⦄
  → d * n ≡ length ys
  → powers xs n [] ≡ ys
  → xs ≡ take d ys
powers-take xs ys d (suc n) p q = xs-take-ys where

  d-length : d ≡ length xs
  d-length = *-injr (suc n) d (length xs) $
    d * suc n                     ≡⟨ p ⟩≡
    length ys                     ≡˘⟨ ap length q ⟩≡˘
    length (powers xs (suc n) []) ≡⟨ length-powers xs (suc n) [] ⟩≡
    length xs * suc n +          ≡⟨ +-zeror (length xs * suc n) ⟩≡
    length xs * suc n ∎

  xs-take-ys : xs ≡ take d ys
  xs-take-ys =
    xs                              ≡˘⟨ take-length xs ⟩≡˘
    take ⌜ length xs ⌝ xs           ≡⟨ ap! (sym d-length) ⟩≡
    take d xs                       ≡˘⟨ take-++l d xs (powers xs n []) (≤-refl' d-length) ⟩≡˘
    take d ⌜ powers xs (suc n) [] ⌝ ≡⟨ ap! q ⟩≡
    take d ys                       ∎

We also have the usual battery of non-emptyness lemmas.

powers-nonemptyl
  : ∀ (xs : List A) (k : Nat) (ys : List A)
  → .⦃ _ : Positive k ⦄
  → Nonempty xs
  → Nonempty (powers xs k ys)
powers-nonemptyl xs (suc k) ys ne = ++-nonemptyl xs (powers xs k ys) ne

powers-nonemptyr
  : ∀  (xs : List A) (k : Nat) (ys : List A)
  → Nonempty ys
  → Nonempty (powers xs k ys)
powers-nonemptyr xs zero ys ne =
  ne
powers-nonemptyr xs (suc k) ys ne =
  ++-nonemptyr xs (powers xs k ys) (powers-nonemptyr xs k ys ne)

Head and Tail🔗

We can always get the first element of a non-empty list.

head⁺ : (xs : List A) → ⦃ Nonempty xs ⦄ → A
head⁺ (x ∷ xs) = x

The following technical lemma is very useful when doing computations!

head-tail-∷ : ∀ (x : A) (xs : List A) → head x xs ∷ tail (xs ∷r x) ≡ xs ∷r x
head-tail-∷ x [] = refl
head-tail-∷ x (y ∷ xs) = refl

Last and init🔗

As mentioned earlier, accessing the last element of a list is extremely expensive, and should be avoided at all cost in algorithmic contexts. However, it is still useful to be able to talk about the final element of a list when doing algebraic proofs.

We start by defining a version of last that takes in a default value for when the input list is empty.

last : List A → A → A
last [] def = def
last (x ∷ xs) def = last xs x

If we can prove that a list is non-empty, then we can omit this default element.

last⁺ : (xs : List A) → ⦃ Nonempty xs ⦄ → A
last⁺ (x ∷ xs) = last xs x

We also define init, which returns all but the last element.

init : List A → List A
init [] = []
init (x ∷ []) = []
init (x ∷ y ∷ xs) = x ∷ (init (y ∷ xs))

Though init computes on cons-cells, we can prove that it removes a single snoc cell. Unfortunately, it has to walk through the entire list to do this, completely destroying sharing in the process. Needless to say, init is reserved solely for non-computational contexts!

init-∷r : (xs : List A) (x : A) → init (xs ∷r x) ≡ xs
init-∷r [] x = refl
init-∷r (y ∷ []) x = refl
init-∷r (y ∷ z ∷ xs) x = ap (y ∷_) (init-∷r (z ∷ xs) x)

We can also give an analogous characterisation of last.

last-∷r : (xs : List A) (x y : A) → last (xs ∷r x) y ≡ x
last-∷r [] x y = refl
last-∷r (x' ∷ []) x y = refl
last-∷r (x' ∷ x'' ∷ xs) x y = last-∷r (x'' ∷ xs) x x'

Note that last and head are dual.

last-head-reverse : ∀ (xs : List A) (x : A) → last xs x ≡ head x (reverse xs)
last-head-reverse [] x = refl
last-head-reverse (y ∷ []) x = refl
last-head-reverse (y ∷ z ∷ xs) x =
  last (z ∷ xs) y           ≡⟨ last-head-reverse (z ∷ xs) y ⟩≡
  head y (reverse (z ∷ xs)) ≡˘⟨ head-⋉ x (z ∷ xs) (y ∷ []) ⟩≡˘
  head x (xs ⋉ z ∷ y ∷ [])  ∎

A similar duality holds between init and tail.

init-reverse-tail : ∀ (xs : List A) → init (reverse xs) ≡ reverse (tail xs)
init-reverse-tail [] = refl
init-reverse-tail (x ∷ []) = refl
init-reverse-tail (x ∷ y ∷ xs) =
  init (reverse (x ∷ y ∷ xs))  ≡⟨ ap init (reverse-∷ x (y ∷ xs)) ⟩≡
  init (reverse (y ∷ xs) ∷r x) ≡⟨ init-∷r (reverse (y ∷ xs)) x ⟩≡
  reverse (y ∷ xs)              ∎

We have a dual version of head-tail-∷; this could be proved via duality, but its easy enough to do via brute-force induction.

init-last-∷r : ∀ (xs : List A) (x : A) → init (x ∷ xs) ∷r last xs x ≡ x ∷ xs
init-last-∷r [] x = refl
init-last-∷r (y ∷ []) x = refl
init-last-∷r (y ∷ z ∷ xs) x = ap (x ∷_) (init-last-∷r (z ∷ xs) y)

If $ys$ is nonempty, then we can commute init and last through concatenations.

init-nonempty-++
  : ∀ (xs ys : List A)
  → ⦃ Nonempty ys ⦄
  → init (xs ++ ys) ≡ xs ++ init ys
init-nonempty-++ [] ys = refl
init-nonempty-++ (x ∷ []) (y ∷ ys) = refl
init-nonempty-++ (x ∷ x' ∷ xs) (y ∷ ys) = ap (x ∷_) (init-nonempty-++ (x' ∷ xs) (y ∷ ys))

last-nonempty-++
  : ∀ (xs ys : List A) (x y : A)
  → ⦃ Nonempty ys ⦄
  → last (xs ++ ys) x ≡ last ys y
last-nonempty-++ [] (y' ∷ ys) x y = refl
last-nonempty-++ (x' ∷ []) (y' ∷ ys) x y = refl
last-nonempty-++ (x' ∷ x'' ∷ xs) (y' ∷ ys) x y = last-nonempty-++ (x'' ∷ xs) (y' ∷ ys) x' y

As corollaries, we get analogous results about ⋉.

init-nonempty-⋉
  : ∀ (xs ys : List A)
  → ⦃ Nonempty ys ⦄
  → init (xs ⋉ ys) ≡ xs ⋉ init ys
init-nonempty-⋉ xs ys =
  init (xs ⋉ ys)          ≡⟨ ap init (⋉-exchangel [] xs ys) ⟩≡
  init (reverse xs ++ ys) ≡⟨ init-nonempty-++ (reverse xs) ys ⟩≡
  reverse xs ++ init ys   ≡˘⟨ ⋉-exchangel [] xs (init ys) ⟩≡˘
  xs ⋉ init ys            ∎

last-nonempty-⋉
  : ∀ (xs ys : List A) (x y : A)
  → ⦃ Nonempty ys ⦄
  → last (xs ⋉ ys) x ≡ last ys y
last-nonempty-⋉ xs ys x y =
  last ⌜ xs ⋉ ys ⌝ x        ≡⟨ ap! (⋉-exchangel [] xs ys) ⟩≡
  last (reverse xs ++ ys) x ≡⟨ last-nonempty-++ (reverse xs) ys x y ⟩≡
  last ys y ∎

Disjointness🔗

The empty list is distinct from concs and snoc cells.

[]≠∷ : ∀ {x : A} {xs : List A} → [] ≠ (x ∷ xs)
[]≠∷ = ∷≠[] ∘ sym

∷r≠[] : ∀ {xs : List A} {x : A} → (xs ∷r x) ≠ []
∷r≠[] {xs = xs} {x = x} p = ∷≠[] (sym (reverse-∷r xs x) ∙ ap reverse p)

The algebra of lists🔗

As computer scientists, our first impulse is to view singly-linked-lists purely from a data-structure perspective. However, lists have a very rich algebraic structure: they are the free monoid! With this in mind, we shall describe a bit of the algebra of lists.

Right identities in the free monoid are unique.

++-idr-unique : ∀ (xs ys : List A) → xs ++ ys ≡ xs → ys ≡ []
++-idr-unique [] ys p = p
++-idr-unique (x ∷ xs) ys p = ++-idr-unique xs ys (∷-tail-inj p)

Moreover, the free monoid is isomorphic to its dual via reverse, so left identities are also unique.

++-idl-unique : ∀ (xs ys : List A) → xs ++ ys ≡ ys → xs ≡ []
++-idl-unique xs ys p =
  Equiv.injective reverse-≃ $
  ++-idr-unique (reverse ys) (reverse xs) (sym (reverse-++ xs ys) ∙ ap reverse p)

More generally, any 2-sided identity is unique.

++-two-sided-id-unique
  : ∀ (xs ys zs : List A) → xs ++ ys ++ zs ≡ ys → xs ≡ [] × zs ≡ []
++-two-sided-id-unique xs [] zs p = ++-zerol xs zs p , ++-zeror xs zs p
++-two-sided-id-unique [] (y ∷ ys) zs p = refl , (++-idr-unique (y ∷ ys) zs p)
++-two-sided-id-unique (x ∷ xs) (y ∷ ys) zs p =
  ×-map₁ (λ xs∷y=[] → absurd (∷r≠[] xs∷y=[])) $
  ++-two-sided-id-unique (xs ∷r y) ys zs $
    xs ∷r y ++ ys ++ zs ≡⟨ ++-assoc xs (y ∷ []) (ys ++ zs) ⟩≡
    xs ++ y ∷ ys ++ zs  ≡⟨ ap tail p ⟩≡
    ys                  ∎

We can repackage these results as into some handly little technical lemmas: namely, prepending or appending a non-empty list has no fixpoints.

++-no-fixl
  : ∀ (xs : List A) (ys : List A)
  → ⦃ Nonempty ys ⦄
  → (xs ++ ys) ≠ xs
++-no-fixl xs (y ∷ ys) p = ∷≠[] (++-idr-unique xs (y ∷ ys) p)

++-no-fixr
  : ∀ (xs : List A) (ys : List A)
  → ⦃ Nonempty xs ⦄
  → (xs ++ ys) ≠ ys
++-no-fixr (x ∷ xs) ys p = ∷≠[] (++-idl-unique (x ∷ xs) ys p)

++-no-fix
  : ∀ (xs : List A) (ys : List A) (zs : List A)
  → Nonempty xs ⊎ Nonempty zs
  → (xs ++ ys ++ zs) ≠ ys
++-no-fix [] ys (z ∷ zs) (inr nonempty) p =
  ++-no-fixl ys (z ∷ zs) p
++-no-fix (x ∷ xs) ys zs ne p =
  ∷≠[] $ fst $ ++-two-sided-id-unique (x ∷ xs) ys zs p

Every element of the free monoid is left-cancellative. We will go about this in a somewhat non-standard way, and prove that $xs+ys=xs+zs$ is equivalent to $xs=xs\times ys=zs\text{.}$ The redundant loop is imporant here; we are working in homotopy type theory, so there may be homotopical information hiding in there!

++l-lens : ∀ (xs ys zs : List A) → (xs ++ ys ≡ xs ++ zs) ≃ (xs ≡ xs × ys ≡ zs)
++l-lens [] ys zs = lens-introl empty-loop-is-contr
++l-lens (x ∷ xs) ys zs =
  x ∷ xs ++ ys ≡ x ∷ xs ++ zs ≃⟨ ∷-inversion ⟩≃
  x ≡ x × xs ++ ys ≡ xs ++ zs ≃⟨ ×-apr (λ _ → ++l-lens xs ys zs) ⟩≃
  x ≡ x × xs ≡ xs × ys ≡ zs   ≃⟨ Σ-assoc ⟩≃
  (x ≡ x × xs ≡ xs) × ys ≡ zs ≃˘⟨ ×-apl (λ _ → ∷-inversion) ⟩≃˘
  x ∷ xs ≡ x ∷ xs × ys ≡ zs   ≃∎

We can use duality to prove that every element is also right-cancellative.

++r-lens : ∀ (xs ys zs : List A) → (xs ++ zs ≡ ys ++ zs) ≃ (xs ≡ ys × zs ≡ zs)
++r-lens xs ys zs =
  xs ++ zs ≡ ys ++ zs                                 ≃˘⟨ reverse-cancel ⟩≃˘
  reverse (xs ++ zs) ≡ reverse (ys ++ zs)             ≃⟨ ∙-pre-equiv (sym (reverse-++ xs zs)) ∙e ∙-post-equiv (reverse-++ ys zs) ⟩≃
  reverse zs ++ reverse xs ≡ reverse zs ++ reverse ys ≃⟨ ++l-lens (reverse zs) (reverse xs) (reverse ys) ⟩≃
  reverse zs ≡ reverse zs × reverse xs ≡ reverse ys   ≃⟨ Σ-ap reverse-cancel (λ _ → reverse-cancel) ⟩≃
  zs ≡ zs × xs ≡ ys                                   ≃⟨ ×-swap ⟩≃
  xs ≡ ys × zs ≡ zs                                   ≃∎

These proofs are slick, but don’t provide the nicest interface, so we prove some easy corollaries that package things up in a more user-friendly format.

++-cancell : ∀ (xs ys zs : List A) → (xs ++ ys) ≡ (xs ++ zs) → ys ≡ zs
++-cancell xs ys zs p = snd (Equiv.to (++l-lens xs ys zs) p)

++-cancelr : ∀ (xs ys zs : List A) → (xs ++ zs) ≡ (ys ++ zs) → xs ≡ ys
++-cancelr xs ys zs p = fst (Equiv.to (++r-lens xs ys zs) p)

A bit of reversal yoga lets us establish analogous results for fused reverse-and-concatenation.

⋉l-lens : ∀ (xs ys zs : List A) → (xs ⋉ ys ≡ xs ⋉ zs) ≃ (xs ≡ xs × ys ≡ zs)
⋉l-lens xs ys zs =
  xs ⋉ ys ≡ xs ⋉ zs                   ≃⟨ path→equiv (ap₂ _≡_ (⋉-exchangel [] xs ys) (⋉-exchangel [] xs zs)) ⟩≃
  reverse xs ++ ys ≡ reverse xs ++ zs ≃⟨ ++l-lens (reverse xs) ys zs ⟩≃
  reverse xs ≡ reverse xs × ys ≡ zs   ≃⟨ ×-apl (λ _ → reverse-cancel) ⟩≃
  xs ≡ xs × ys ≡ zs                   ≃∎

⋉-cancell : ∀ (xs ys zs : List A) → (xs ⋉ ys) ≡ (xs ⋉ zs) → ys ≡ zs
⋉-cancell xs ys zs p = snd (Equiv.to (⋉l-lens xs ys zs) p)