open import 1Lab.Prelude
open import 1Lab.Reflection.Regularity
open import 1Lab.Function.Embedding

open import Data.Wellfounded.Base
open import Data.Nat
open import Data.Sum

open import Meta.Invariant hiding (empty)

open import StringLab.Data.List
open import StringLab.Data.Dec

open import StringLab.Order.Trichotomous

import Data.Nat as Nat

module StringLab.Data.List.Factor where

Factors🔗

private variable
  ℓ : Level
  A B S : Type ℓ

A word $x s : A^{*}$ is a factor of a word $ys : A^{*}$ if there merely exists $u s, v s : A^{*}$ such that $u s x s v s = ys .$

Note that mere existence is required to make this a proposition: there are multiple ways to witness $[]$ as a factor of a non-empty list.

_⊑_ : List A → List A → Type _
_⊑_ {A = A} xs ys = ∥ Σ[ us ∈ List A ] Σ[ vs ∈ List A ] us ++ xs ++ vs ≡ ys ∥

A word $x s : A^{*}$ is a left factor of a word $ys : A^{*},$ denoted $x s ⊑^{l} ys,$ if there exists some $u s : A^{*}$ such that $x s u s = ys .$

_⊑ˡ_ : List A → List A → Type _
_⊑ˡ_ {A = A} xs ys = Σ[ us ∈ List A ] xs ++ us ≡ ys

Conversely, a word $x s : A^{*}$ is a right factor of a word $ys : A^{*},$ denoted $x s ⊑^{r} ys,$ if there exists some $u s : A^{*}$ such that $u s x s = ys .$

_⊑ʳ_ : List A → List A → Type _
_⊑ʳ_ {A = A} xs ys = Σ[ us ∈ List A ] us ++ xs ≡ ys

A word $x s : A^{*}$ is a proper left factor of $ys : A^{*},$ denoted $x s ⊏^{l} ys,$ if there exists a non-empty word $u s : A^{+}$ such that $u s x s = ys .$

Likewise, a word $x s : A^{*}$ is a proper right factor of $ys : A^{*},$ denoted $x s ⊏^{r},$ if there exists a non-empty word $u s : A^{+}$ such that $x s u s = ys .$

_⊏ˡ_ : List A → List A → Type _
_⊏ˡ_ {A = A} xs ys =
  Σ[ u ∈ A ] Σ[ us ∈ List A ] xs ++ (u ∷ us) ≡ ys

_⊏ʳ_ : List A → List A → Type _
_⊏ʳ_ {A = A} xs ys =
  Σ[ u ∈ A ] Σ[ us ∈ List A ] (u ∷ us) ++ xs ≡ ys

Note

Left factors are more commonly known as prefixes, and right factors as suffixes. We choose the left/right factor terminology to emphasize the algebraic nature of factorisations.

infix 6 _⊑ˡ_ _⊑ʳ_ _⊏ˡ_ _⊏ʳ_

Convienence functions🔗

We start by defining some nicer names for left factor corresponding to a right factor, and vice versa.

⊑ˡ-factor : ∀ {xs ys : List A} → xs ⊑ˡ ys → List A
⊑ˡ-factor = fst

⊑ʳ-factor : ∀ {xs ys : List A} → xs ⊑ʳ ys → List A
⊑ʳ-factor = fst

⊑ˡ-dual-⊑ʳ : ∀ {xs ys : List A} → (p : xs ⊑ˡ ys) → ⊑ˡ-factor p ⊑ʳ ys
⊑ˡ-dual-⊑ʳ {xs = xs} (vs , p) = xs , p

⊑ʳ-dual-⊑ˡ : ∀ {xs ys : List A} → (p : xs ⊑ʳ ys) → ⊑ʳ-factor p ⊑ˡ ys
⊑ʳ-dual-⊑ˡ {xs = xs} (vs , p) = xs , p

Note that the corresponding right factor of a proper left factor may not be proper, and vice versa for proper right factors.

⊏ˡ-factor : ∀ {xs ys : List A} → xs ⊏ˡ ys → List A
⊏ˡ-factor (u , us , _) = u ∷ us

⊏ˡ-dual-⊑ʳ : {xs ys : List A} → (p : xs ⊏ˡ ys) → ⊏ˡ-factor p ⊑ʳ ys
⊏ˡ-dual-⊑ʳ {xs = xs} (u , us , p) = xs , p

⊏ʳ-factor : ∀ {xs ys : List A} → xs ⊏ʳ ys → List A
⊏ʳ-factor (u , us , _) = u ∷ us

⊏ʳ-dual-⊑ˡ : {xs ys : List A} → (p : xs ⊏ʳ ys) → ⊏ʳ-factor p ⊑ˡ ys
⊏ʳ-dual-⊑ˡ {xs = xs} (u , us , p) = xs , p

However, the corresponding right/left factors of proper left/right factors are always non-empty

⊏ˡ-factor-nonempty
  : ∀ {xs ys : List A}
  → (xs⊏ys : xs ⊏ˡ ys)
  → Nonempty (⊏ˡ-factor xs⊏ys)
⊏ˡ-factor-nonempty xs⊏ys = nonempty

⊏ʳ-factor-nonempty
  : ∀ {xs ys : List A}
  → (xs⊏ys : xs ⊏ʳ ys)
  → Nonempty (⊏ʳ-factor xs⊏ys)
⊏ʳ-factor-nonempty xs⊏ys = nonempty

This also gives us a method for constructing proper factors.

++-nonempty-⊏ˡ
  : ∀ (xs ys zs : List A)
  → Nonempty ys
  → xs ++ ys ≡ zs
  → xs ⊏ˡ zs
++-nonempty-⊏ˡ xs (y ∷ ys) zs _ p = y , ys , p


++-nonempty-⊏ʳ
  : ∀ (xs ys zs : List A)
  → Nonempty xs
  → xs ++ ys ≡ zs
  → ys ⊏ʳ zs
++-nonempty-⊏ʳ (x ∷ xs) ys zs _ p = x , xs , p

The following are also clearly factorisations.

⊑ˡ-++-inl
  : ∀ (xs ys : List A)
  → xs ⊑ˡ xs ++ ys
⊑ˡ-++-inl xs ys = ys , refl

⊏ˡ-++-inl
  : ∀ (xs ys : List A)
  → ⦃ _ : Nonempty ys ⦄
  → xs ⊏ˡ xs ++ ys
⊏ˡ-++-inl xs (y ∷ ys) = y , ys , refl

⊑ʳ-++-inr
  : ∀ (xs ys : List A)
  → ys ⊑ʳ xs ++ ys
⊑ʳ-++-inr xs ys = xs , refl

⊏ʳ-++-inr
  : ∀ (xs ys : List A)
  → ⦃ _ : Nonempty xs ⦄
  → ys ⊏ʳ xs ++ ys
⊏ʳ-++-inr (x ∷ xs) ys = x , xs , refl

We also have corresponding versionns of these lemmas for fused reverse-and-add, though we only include the version we need for the time being.

⊑ʳ-⋉-inr :  ∀ (xs ys : List A) → xs ⊑ʳ ys ⋉ xs
⊑ʳ-⋉-inr xs ys = reverse ys , sym (⋉-exchangel [] ys xs)

Strengthening and weakening🔗

Clearly, proper left/right factors are left/right factors.

⊏ʳ-weaken : ∀ {xs ys : List A} → xs ⊏ʳ ys → xs ⊑ʳ ys
⊏ʳ-weaken (u , us , p) = (u ∷ us) , p

⊏ˡ-weaken : ∀ {xs ys : List A} → xs ⊏ˡ ys → xs ⊑ˡ ys
⊏ˡ-weaken (u , us , p) = (u ∷ us) , p

Moreover, a left/right factor of $ys$ is either a proper factor, or equal to $ys .$ Note that this does not require decidable equality; just check the length of the other list.

⊑ˡ-strengthen : ∀ {xs ys : List A} → xs ⊑ˡ ys → (xs ≡ ys) ⊎ (xs ⊏ˡ ys)
⊑ˡ-strengthen ([] , p) = inl (sym (++-idr _) ∙ p)
⊑ˡ-strengthen (u ∷ us , p) = inr (u , us , p)

⊑ʳ-strengthen : ∀ {xs ys : List A} → xs ⊑ʳ ys → (xs ≡ ys) ⊎ (xs ⊏ʳ ys)
⊑ʳ-strengthen ([] , p) = inl p
⊑ʳ-strengthen (u ∷ us , p) = inr (u , us , p)

We can also mediate between proper right factors of non-empty lists, and factors of the tails of those lists.

⊑ʳ-consr
  : ∀ {xs : List A} {y : A} {ys : List A}
  → xs ⊑ʳ ys
  → xs ⊏ʳ (y ∷ ys)
⊑ʳ-consr {y = y} (us , p) = y , us , ap (y ∷_) p

⊏ʳ-tailr
  : ∀ {xs ys : List A}
  → xs ⊏ʳ ys
  → xs ⊑ʳ tail ys
⊏ʳ-tailr (u , us , p) = us , ap tail p

Dual results hold for left factors and snoc.

⊏ˡ-snocr
  : ∀ {xs : List A} {ys : List A} {y : A}
  → xs ⊑ˡ ys
  → xs ⊏ˡ (ys ∷r y)
⊏ˡ-snocr {xs = xs} {ys = ys} {y = y} (us , p) =
  head y us ,
  tail (us ∷r y) ,
  path
  where
    path : xs ++ head y us ∷ tail (us ∷r y) ≡ ys ∷r y
    path =
      xs ++ head y us ∷ tail (us ∷r y) ≡⟨ ap (xs ++_) (head-tail-∷ y us) ⟩≡
      xs ++ us ∷r y                    ≡˘⟨ ++-assoc xs us (y ∷ []) ⟩≡˘
      (xs ++ us) ∷r y                  ≡⟨ ap (_∷r y) p ⟩≡
      ys ∷r y                          ∎

⊏ˡ-initr
  : ∀ {xs ys : List A}
  → xs ⊏ˡ ys
  → xs ⊑ˡ init ys
⊏ˡ-initr {xs = xs} {ys = ys} (u , us , p) =
  init (u ∷ us) ,
  path
  where
    path : xs ++ init (u ∷ us) ≡ init ys
    path =
      xs ++ init (u ∷ us) ≡˘⟨ init-nonempty-++ xs (u ∷ us) ⟩≡˘
      init (xs ++ u ∷ us) ≡⟨ ap init p ⟩≡
      init ys             ∎

In fact, we can precisely characterise proper left/right factors as left/right factors whose corresponding right/left factor is nonempty.

⊏ˡ≃⊑ˡ-nonempty
  : ∀ {A : Type ℓ}
  → (xs ys : List A)
  → (xs ⊏ˡ ys) ≃ (Σ[ p ∈ xs ⊑ˡ ys ] Nonempty (⊑ˡ-factor p))

⊏ʳ≃⊑ʳ-nonempty
  : ∀ {A : Type ℓ}
  → (xs ys : List A)
  → (xs ⊏ʳ ys) ≃ (Σ[ p ∈ xs ⊑ʳ ys ] Nonempty (⊑ʳ-factor p))

This is surprisingly annoying to prove: the easiest way is to chain a series of equivalences that reassociate quantifiers, and then invoke nonempty≃∷.

⊏ˡ≃⊑ˡ-nonempty {A = A} xs ys =
  Σ[ u ∈ A ] Σ[ us ∈ List A ] xs ++ u ∷ us ≡ ys
    ≃⟨ Σ-assoc ⟩≃
  Σ[ uus ∈ (A × List A) ] xs ++ uus .fst ∷ uus .snd ≡ ys
    ≃⟨ Σ-ap (nonempty≃∷ e⁻¹) (λ (u , us) → path→equiv (lemma u us)) ⟩≃
  Σ (Σ (List A) Nonempty) (λ (us , _) → xs ++ us ≡ ys)
    ≃˘⟨ Σ-assoc ⟩≃˘
  Σ[ us ∈ List A ] (Nonempty us × xs ++ us ≡ ys)
    ≃⟨ Σ-ap id≃ (λ _ → ×-swap) ⟩≃
  Σ[ us ∈ List A ] (xs ++ us ≡ ys × Nonempty us)
    ≃⟨ Σ-assoc ⟩≃
  Σ[ p ∈ xs ⊑ˡ ys ] Nonempty (p .fst) ≃∎
  where
    lemma : ∀ u us → _
    lemma u us =
      ap₂ _≡_ (ap₂ (λ u us → xs ++ u ∷ us) (sym (transport-refl _)) (sym (transport-refl _ ∙ transport-refl _))) refl

The case for right factors is nearly identical and equally as tedious, so we omit the details.

⊏ʳ≃⊑ʳ-nonempty {A = A} xs ys =
  Σ[ u ∈ A ] Σ[ us ∈ List A ] u ∷ us ++ xs ≡ ys
    ≃⟨ Σ-assoc ⟩≃
  Σ[ uus ∈ (A × List A) ] uus .fst ∷ uus .snd ++ xs ≡ ys
    ≃⟨ Σ-ap (nonempty≃∷ e⁻¹) (λ (u , us) → path→equiv (lemma u us)) ⟩≃
  Σ (Σ (List A) Nonempty) (λ (us , _) → us ++ xs ≡ ys)
    ≃˘⟨ Σ-assoc ⟩≃˘
  Σ[ us ∈ List A ] (Nonempty us × us ++ xs ≡ ys)
    ≃⟨ Σ-ap id≃ (λ _ → ×-swap) ⟩≃
  Σ[ us ∈ List A ] (us ++ xs ≡ ys × Nonempty us)
    ≃⟨ Σ-assoc ⟩≃
  Σ[ p ∈ xs ⊑ʳ ys ] Nonempty (p .fst) ≃∎
  where
    lemma : ∀ u us → _
    lemma u us =
      ap₂ _≡_ (ap₂ (λ u us → u ∷ us ++ xs) (sym (transport-refl _)) (sym (transport-refl _ ∙ transport-refl _))) refl

Bottom elements🔗

The empty list is a bottom element for all the factorization orders.

⊑ˡ-bot : ∀ {xs : List A} → [] ⊑ˡ xs
⊑ˡ-bot {xs = xs} = xs , refl

⊏ˡ-bot : ∀ {x : A} {xs : List A} → [] ⊏ˡ (x ∷ xs)
⊏ˡ-bot {x = x} {xs = xs} = x , xs , refl

⊑ʳ-bot : ∀ {xs : List A} → [] ⊑ʳ xs
⊑ʳ-bot {xs = xs} = xs , ++-idr xs

⊏ʳ-bot : ∀ {x : A} {xs : List A} → [] ⊏ʳ (x ∷ xs)
⊏ʳ-bot {x = x} {xs = xs} = x , xs , ++-idr (x ∷ xs)

There are no proper left or right factors of the empty list.

⊑ˡ-strict-bot : ∀ {x : A} {xs : List A} → ¬ (x ∷ xs ⊑ˡ [])
⊑ˡ-strict-bot (us , p) = absurd (∷≠[] p)

⊏ˡ-strict-bot : ∀ (xs : List A) → ¬ (xs ⊏ˡ [])
⊏ˡ-strict-bot xs (u , us , p) = absurd (∷≠[] (++-zeror xs (u ∷ us) p))

⊑ʳ-strict-bot : ∀ {x : A} {xs : List A} → ¬ (x ∷ xs ⊑ʳ [])
⊑ʳ-strict-bot {x = x} {xs = xs} (us , p) = absurd (∷≠[] (++-zeror us (x ∷ xs) p))

⊏ʳ-strict-bot : ∀ (xs : List A) → ¬ (xs ⊏ʳ [])
⊏ʳ-strict-bot xs (u , us , p) = absurd (∷≠[] p)

There are many ways we can repackage this fact: the following list is not exhaustive, and covers all the cases we will need.

empty-not-⊏ʳ-empty
  : ∀ {xs ys : List A}
  → Empty xs → Empty ys
  → ¬ (xs ⊏ʳ ys)
empty-not-⊏ʳ-empty {xs = []} {ys = []} _ _ = ⊏ʳ-strict-bot []

⊏ʳ-nonempty
  : ∀ {xs : List A}
  → Nonempty xs
  → [] ⊏ʳ xs
⊏ʳ-nonempty {xs = x ∷ xs} _ = ⊏ʳ-bot

nonempty-⊏ˡ
  : ∀ {xs ys : List A}
  → xs ⊏ˡ ys
  → Nonempty ys
nonempty-⊏ˡ {ys = []} xs⊏ys = absurd (⊏ˡ-strict-bot _ xs⊏ys)
nonempty-⊏ˡ {ys = y ∷ ys} xs⊏ys = nonempty

nonempty-⊏ʳ
  : ∀ {xs ys : List A}
  → xs ⊏ʳ ys
  → Nonempty ys
nonempty-⊏ʳ {ys = []} xs⊏ys = absurd (⊏ʳ-strict-bot _ xs⊏ys)
nonempty-⊏ʳ {ys = y ∷ ys} xs⊏ys = nonempty

Monotonicity🔗

If $ys$ has a nonempty left/right factor $x s,$ then $ys$ must also be nonempty.

nonempty-⊑ˡ-stable
  : ∀ {xs : List A} {ys : List A}
  → ⦃ _ : Nonempty xs ⦄
  → xs ⊑ˡ ys
  → Nonempty ys
nonempty-⊑ˡ-stable {xs = x ∷ xs} {ys = []} (us , p) =
  absurd (∷≠[] p)
nonempty-⊑ˡ-stable {xs = x ∷ xs} {ys = y ∷ ys} (us , p) =
  nonempty

nonempty-⊑ʳ-stable
  : ∀ {xs : List A} {ys : List A}
  → ⦃ _ : Nonempty xs ⦄
  → xs ⊑ʳ ys
  → Nonempty ys
nonempty-⊑ʳ-stable {xs = x ∷ xs} {ys = []} (us , p) =
  absurd (∷≠[] (++-zeror us (x ∷ xs) p))
nonempty-⊑ʳ-stable {xs = x ∷ xs} {ys = y ∷ ys} (us , p) =
  nonempty

Lengths of factors🔗

If $x s$ is a proper left factor of $ys,$ then the length of $x s$ is strictly smaller than the length of $ys .$

⊏ˡ-length-<
  : ∀ {xs ys : List A}
  → xs ⊏ˡ ys
  → length xs Nat.< length ys
⊏ˡ-length-< {xs = xs} {ys = ys} (u , us , xs+us=ys) =
  ≤-trans (+-≤l (suc (length xs)) (length us)) $
  ≤-refl' 1+∣xs∣+∣us∣=∣ys∣
  where
    1+∣xs∣+∣us∣=∣ys∣ : 1 + length xs + length us ≡ length ys
    1+∣xs∣+∣us∣=∣ys∣ =
      1 + length xs + length us   ≡˘⟨ +-sucr (length xs) (length us) ⟩≡˘
      length xs + (1 + length us) ≡⟨⟩
      length xs + length (u ∷ us) ≡˘⟨ length-++ xs (u ∷ us) ⟩≡˘
      length (xs ++ u ∷ us)       ≡⟨ ap length xs+us=ys ⟩≡
      length ys                   ∎

Extending factors🔗

We can extend left prefixes on the left, and right prefixes on the right.

⊑ˡ-++-extendl
  : ∀ {ws xs ys zs : List A}
  → ws ≡ xs → ys ⊑ˡ zs → (ws ++ ys) ⊑ˡ (xs ++ zs)
⊑ˡ-++-extendl {ws = ws} {ys = ys} p (us , q) =
  us , ++-assoc ws ys us ∙ ap₂ _++_ p q

⊏ˡ-++-extendl
  : ∀ {ws xs ys zs : List A}
  → ws ≡ xs → ys ⊏ˡ zs → (ws ++ ys) ⊏ˡ (xs ++ zs)
⊏ˡ-++-extendl {ws = ws} {ys = ys} p (u , us , q) =
  u , us , ++-assoc ws ys (u ∷ us) ∙ ap₂ _++_ p q

⊑ʳ-++-extendr
  : ∀ {ws xs ys zs : List A}
  → ws ⊑ʳ xs → ys ≡ zs → (ws ++ ys) ⊑ʳ (xs ++ zs)
⊑ʳ-++-extendr {ws = ws} {ys = ys} (us , p) q =
  us , sym (++-assoc us ws ys) ∙ ap₂ _++_ p q

⊏ʳ-++-extendr
  : ∀ {ws xs ys zs : List A}
  → ws ⊏ʳ xs → ys ≡ zs → (ws ++ ys) ⊏ʳ (xs ++ zs)
⊏ʳ-++-extendr {ws = ws} {ys = ys} (u , us , p) q =
  u , us , sym (++-assoc (u ∷ us) ws ys) ∙ ap₂ _++_ p q

As corollaries, we get can extend left/right prefixes with a single element on the left/right, resp.

⊑ˡ-∷-extendl
  : ∀ {x y : A} {xs ys : List A}
  → x ≡ y → xs ⊑ˡ ys → (x ∷ xs) ⊑ˡ (y ∷ ys)
⊑ˡ-∷-extendl p q = ⊑ˡ-++-extendl (ap (_∷ []) p) q

⊏ˡ-∷-extendl
  : ∀ {x y : A} {xs ys : List A}
  → x ≡ y → xs ⊏ˡ ys → (x ∷ xs) ⊏ˡ (y ∷ ys)
⊏ˡ-∷-extendl p q = ⊏ˡ-++-extendl (ap (_∷ []) p) q

⊑ʳ-∷r-extendr
  : ∀ {x y : A} {xs ys : List A}
  → xs ⊑ʳ ys → x ≡ y → (xs ∷r x) ⊑ʳ (ys ∷r y)
⊑ʳ-∷r-extendr p q = ⊑ʳ-++-extendr p (ap (_∷ []) q)

⊏ʳ-∷r-extendr
  : ∀ {x y : A} {xs ys : List A}
  → xs ⊏ʳ ys → x ≡ y → (xs ∷r x) ⊏ʳ (ys ∷r y)
⊏ʳ-∷r-extendr p q = ⊏ʳ-++-extendr p (ap (_∷ []) q)

We also have extension lemmata for fused reverse-and-concatenate.

⊑ʳ-⋉-extendr
  : ∀ {ws xs ys zs : List A}
  → ws ⊑ˡ xs → ys ≡ zs → (ws ⋉ ys) ⊑ʳ (xs ⋉ zs)
⊑ʳ-⋉-extendr {ws = ws} {xs = xs} {ys = ys} {zs = zs} (vs , p) ys=zs =
  reverse vs ,
  ⋉-exchanger vs [] (ws ⋉ ys)
  ∙ ⋉-assocl vs ws ys
  ∙ ap₂ (_⋉_) p ys=zs

Next, we prove a battery of rather tedious inversion lemmas. These sorts of lemmas are (understandably) often omitted in informal accounts of the subject, but we are being completely formal, so a bit of elbow grease is required. Luckily, none of them are particularly hard, so we shall gloss over the proofs.

We begin by charaterising left factors of non-empty lists. In particular, if $x s$ is a nonempty factor of a nonempty list $ys,$ then their first elements must be equal, and their tails must be factors.

⊑ˡ-head
  : {xs ys : List A}
  → ⦃ _ : Nonempty xs ⦄ → ⦃ _ : Nonempty ys ⦄
  → xs ⊑ˡ ys → head⁺ xs ≡ head⁺ ys
⊑ˡ-head {xs = x ∷ xs} {ys = y ∷ ys} (us , p) = ∷-head-inj p

⊑ˡ-tail
  : {xs ys : List A}
  → xs ⊑ˡ ys → tail xs ⊑ˡ tail ys
⊑ˡ-tail {xs = []} {ys = ys} _ = ⊑ˡ-bot
⊑ˡ-tail {xs = x ∷ xs} {ys = []} (us , p) = absurd (∷≠[] p)
⊑ˡ-tail {xs = x ∷ xs} {ys = y ∷ ys} (us , p) = us , ∷-tail-inj p

⊏ˡ-head
  : ∀ {xs ys : List A}
  → ⦃ _ : Nonempty xs ⦄ → ⦃ _ : Nonempty ys ⦄
  → xs ⊏ˡ ys → head⁺ xs ≡ head⁺ ys
⊏ˡ-head {xs = x ∷ xs} {ys = y ∷ ys} (u , us , p) = ∷-head-inj p

⊏ˡ-tail
  : ∀ {xs ys : List A}
  → ⦃ _ : Nonempty xs ⦄ → ⦃ _ : Nonempty ys ⦄
  → xs ⊏ˡ ys
  → tail xs ⊏ˡ tail ys
⊏ˡ-tail {xs = x ∷ xs} {ys = y ∷ ys} (u , us , p) = u , us , ∷-tail-inj p

We also have analogous lemmas for right factors and init/last.

⊑ʳ-last :
  ∀ {xs ys : List A}
  → ⦃ _ : Nonempty xs ⦄ → ⦃ _ : Nonempty ys ⦄
  → xs ⊑ʳ ys → last⁺ xs ≡ last⁺ ys
⊑ʳ-last {xs = x ∷ xs} {ys = y ∷ ys} (us , p) =
  last xs x                ≡˘⟨ last-nonempty-++ us (x ∷ xs) x x ⟩≡˘
  last ⌜ us ++ x ∷ xs ⌝ x  ≡⟨ ap! p ⟩≡
  last (y ∷ ys) x          ≡⟨⟩
  last ys y                ∎

⊑ʳ-init : ∀ {xs ys : List A} → xs ⊑ʳ ys → init xs ⊑ʳ init ys
⊑ʳ-init {xs = []} {ys = ys} xs⊑ys = ⊑ʳ-bot
⊑ʳ-init {xs = x ∷ xs} {ys = []} xs⊑ys = absurd (⊑ʳ-strict-bot xs⊑ys)
⊑ʳ-init {xs = x ∷ xs} {ys = y ∷ ys} (us , p) =
  us , (sym (init-nonempty-++ us (x ∷ xs)) ∙ ap init p)

⊏ʳ-last
  : ∀ {xs ys : List A}
  → ⦃ _ : Nonempty xs ⦄ → ⦃ _ : Nonempty ys ⦄
  → xs ⊏ʳ ys → last⁺ xs ≡ last⁺ ys
⊏ʳ-last (u , us , p) = ⊑ʳ-last (u ∷ us , p)

⊏ʳ-init
  : ∀ {xs ys : List A}
  → ⦃ Nonempty xs ⦄ → ⦃ Nonempty ys ⦄
  → xs ⊏ʳ ys → init xs ⊏ʳ init ys
⊏ʳ-init {xs = x ∷ xs} {ys = y ∷ ys} (u , us , p) =
  u , us , sym (init-nonempty-++ (u ∷ us) (x ∷ xs)) ∙ ap init p

Moreover, if $x s$ is a (proper) right factor of $ys,$ then the tail of $x s$ is a (proper) right factor of the tail of $ys .$

⊑ʳ-tail
  : ∀ {xs ys : List A}
  → xs ⊑ʳ ys → tail xs ⊑ʳ tail ys
⊏ʳ-∷-tail
  : ∀ {xs ys : List A}
  → ⦃ _ : Nonempty xs ⦄ → ⦃ _ : Nonempty ys ⦄
  → xs ⊏ʳ ys → tail xs ⊏ʳ tail ys

The proof is easy, but tedious. Dedicated readers can click “read more” to see the details.

⊑ʳ-tail {xs = []} {ys = ys} xs⊑ys = ⊑ʳ-bot
⊑ʳ-tail {xs = x ∷ xs} {ys = []} xs⊑ys = absurd (⊑ʳ-strict-bot xs⊑ys)
⊑ʳ-tail {xs = x ∷ xs} {ys = y ∷ ys} (us , p) =
  tail (us ∷r x) , us+xs=ys
  where
    us+xs=ys : tail (us ∷r x) ++ xs ≡ ys
    us+xs=ys =
      tail (us ∷r x) ++ xs ≡˘⟨ tail-nonempty-++ (us ∷r x) xs ⟩≡˘
      tail (us ∷r x ++ xs) ≡⟨ ap tail (++-assoc us (x ∷ []) xs) ⟩≡
      tail (us ++ x ∷ xs)  ≡⟨ ap tail p ⟩≡
      ys                   ∎

⊏ʳ-∷-tail {xs = x ∷ xs} {ys = y ∷ ys} (u , us , p) = head x us , tail (us ∷r x) , us+xs=ys
  where
    us+xs=ys : head x us ∷ tail (us ∷r x) ++ xs ≡ ys
    us+xs=ys =
      head x us ∷ tail (us ∷r x) ++ xs ≡⟨ ap (_++ xs) (head-tail-∷ x us) ⟩≡
      us ∷r x ++ xs                    ≡⟨ ++-assoc us (x ∷ []) xs ⟩≡
      us ++ x ∷ xs                     ≡⟨ ∷-tail-inj p ⟩≡
      ys                               ∎

We can repackage some of these inversion lemmas in forms that are more ergonomic in some situations.

⊑ʳ-∷-inversion
  : ∀ {us : List ⌞ A ⌟} {x : ⌞ A ⌟} {xs : List ⌞ A ⌟}
  → us ⊑ʳ x ∷ xs
  → (us ≡ x ∷ xs) ⊎ us ⊑ʳ xs
⊑ʳ-∷-inversion ([] , p) = inl p
⊑ʳ-∷-inversion (v ∷ vs , p) = inr (vs , ∷-tail-inj p)

⊏ʳ-∷-shrinkl
  : ∀ {u : ⌞ A ⌟} {us : List ⌞ A ⌟} {xs : List ⌞ A ⌟}
  → u ∷ us ⊏ʳ xs
  → us ⊏ʳ xs
⊏ʳ-∷-shrinkl {u = u} {us = us} (v , vs , p) =
  v ,
  vs ∷r u ,
  ap (v ∷_) (++-assoc vs (u ∷ []) us) ∙ p

⊑ʳ-∷-extendr
  : ∀ {us : List ⌞ A ⌟} {x : ⌞ A ⌟} {xs : List ⌞ A ⌟}
  → us ⊑ʳ xs
  → us ⊑ʳ (x ∷ xs)
⊑ʳ-∷-extendr {x = x} (vs , p) = (x ∷ vs , ap (x ∷_) p)

Factorisations as orders🔗

The left/right factorisation relations are reflexive.

⊑ˡ-refl' : ∀ {xs  ys : List A} → xs ≡ ys → xs ⊑ˡ ys
⊑ˡ-refl' p = [] , ++-idr _ ∙ p

⊑ˡ-refl : ∀ {xs : List A} → xs ⊑ˡ xs
⊑ˡ-refl {xs = xs} = [] , ++-idr _

⊑ʳ-refl' : ∀ {xs  ys : List A} → xs ≡ ys → xs ⊑ʳ ys
⊑ʳ-refl' p = [] , p

⊑ʳ-refl : ∀ {xs : List A} → xs ⊑ʳ xs
⊑ʳ-refl {xs = xs} = [] , refl

Conversely, the proper factor relations are irreflexive.

⊏ˡ-irrefl' : ∀ {xs ys : List A} → xs ⊏ˡ ys → xs ≠ ys
⊏ʳ-irrefl' : ∀ {xs ys : List A} → xs ⊏ʳ ys → xs ≠ ys

This follows from some easy algebra: if they were reflexive, – then there would be some nonempty $u s$ such that $u s + (-)$ had a fixpoint.

⊏ˡ-irrefl' {ys = ys} (u , us , p) xs=ys =
  ++-no-fixl _ (u ∷ us) (ap (_++ u ∷ us) (sym xs=ys) ∙ p)

⊏ʳ-irrefl' (u , us , p) xs=ys =
  ++-no-fixr (u ∷ us) _ (ap (u ∷ us ++_) (sym xs=ys) ∙ p)

The more general form of irreflexivity can be annoying to use, so we repackage the result into a friendlier form.

⊏ˡ-irrefl : ∀ {xs : List A} → ¬ (xs ⊏ˡ xs)
⊏ˡ-irrefl xs⊏xs = ⊏ˡ-irrefl' xs⊏xs refl

⊏ʳ-irrefl : ∀ {xs : List A} → ¬ (xs ⊏ʳ xs)
⊏ʳ-irrefl xs⊏xs = ⊏ʳ-irrefl' xs⊏xs refl

The (proper) factorisation relations are not only (ir)reflexive, they are transitive! This follows from some easy algebra in all cases.

⊑ˡ-trans : ∀ {xs ys zs : List A} → xs ⊑ˡ ys → ys ⊑ˡ zs → xs ⊑ˡ zs
⊑ˡ-trans (us , p) (vs , q) =
  us ++ vs , sym (++-assoc _ us vs) ∙ ap (_++ vs) p ∙ q

⊑ʳ-trans : ∀ {xs ys zs : List A} → xs ⊑ʳ ys → ys ⊑ʳ zs → xs ⊑ʳ zs
⊑ʳ-trans (us , p) (vs , q) =
  vs ++ us , ++-assoc vs us _ ∙ ap (vs ++_) p ∙ q

⊏ˡ-trans : ∀ {xs ys zs : List A} → xs ⊏ˡ ys → ys ⊏ˡ zs → xs ⊏ˡ zs
⊏ˡ-trans (u , us , p) (v , vs , q) =
  u , (us ++ v ∷ vs) , sym (++-assoc _ (u ∷ us) (v ∷ vs)) ∙ ap (_++ v ∷ vs) p ∙ q

⊏ʳ-trans : ∀ {xs ys zs : List A} → xs ⊏ʳ ys → ys ⊏ʳ zs → xs ⊏ʳ zs
⊏ʳ-trans (u , us , p) (v , vs , q) =
  v , (vs ++ u ∷ us) , ++-assoc (v ∷ vs) (u ∷ us) _ ∙ ap (v ∷ vs ++_) p ∙ q

We also have joint transitivity of the proper and non-proper factorisation relations.

⊏ˡ-⊑ˡ-trans : ∀ {xs ys zs : List A} → xs ⊏ˡ ys → ys ⊑ˡ zs → xs ⊏ˡ zs
⊑ˡ-⊏ˡ-trans : ∀ {xs ys zs : List A} → xs ⊑ˡ ys → ys ⊏ˡ zs → xs ⊏ˡ zs
⊏ʳ-⊑ʳ-trans : ∀ {xs ys zs : List A} → xs ⊏ʳ ys → ys ⊑ʳ zs → xs ⊏ʳ zs
⊑ʳ-⊏ʳ-trans : ∀ {xs ys zs : List A} → xs ⊑ʳ ys → ys ⊏ʳ zs → xs ⊏ʳ zs

These all follow from our previous transitivity lemmas.

⊏ˡ-⊑ˡ-trans {xs = xs} {ys = ys} {zs = zs} xs⊏ys ys⊑zs =
  Equiv.from (⊏ˡ≃⊑ˡ-nonempty xs zs) $
    ⊑ˡ-trans (⊏ˡ-weaken xs⊏ys) ys⊑zs ,
    auto

⊑ˡ-⊏ˡ-trans {xs = xs} {ys = ys} {zs = zs} xs⊑ys ys⊏zs =
  Equiv.from (⊏ˡ≃⊑ˡ-nonempty xs zs) $
    ⊑ˡ-trans xs⊑ys (⊏ˡ-weaken ys⊏zs) ,
    auto

⊏ʳ-⊑ʳ-trans {xs = xs} {ys = ys} {zs = zs} xs⊏ys ys⊑zs =
  Equiv.from (⊏ʳ≃⊑ʳ-nonempty xs zs) $
    ⊑ʳ-trans (⊏ʳ-weaken xs⊏ys) ys⊑zs ,
    auto

⊑ʳ-⊏ʳ-trans {xs = xs} {ys = ys} {zs = zs} xs⊑ys ys⊏zs =
  Equiv.from (⊏ʳ≃⊑ʳ-nonempty xs zs) $
    ⊑ʳ-trans xs⊑ys (⊏ʳ-weaken ys⊏zs) ,
    auto

The proper left/right factor relations are jointly asymmetric with both non-proper factorisation relations.

⊏ˡ-⊑ˡ-asym
  : ∀ {xs ys : List A}
  → xs ⊏ˡ ys
  → ys ⊑ˡ xs
  → ⊥
⊏ˡ-⊑ʳ-asym
  : ∀ {xs ys : List A}
  → xs ⊏ˡ ys
  → ys ⊑ʳ xs
  → ⊥
⊏ʳ-⊑ˡ-asym
  : ∀ {xs ys : List A}
  → xs ⊏ʳ ys
  → ys ⊑ˡ xs
  → ⊥
⊏ʳ-⊑ʳ-asym
  : ∀ {xs ys : List A}
  → xs ⊏ʳ ys
  → ys ⊑ʳ xs
  → ⊥

All these follow from fixpoint arguments.

⊏ʳ-⊑ˡ-asym {ys = ys} (u , us , p) (vs , q) =
  ++-no-fix (u ∷ us) ys vs (inl nonempty) (ap (u ∷ us ++_) q ∙ p)

⊏ˡ-⊑ʳ-asym {ys = ys} (u , us , p) (vs , q) =
  ++-no-fix vs ys (u ∷ us) (inr nonempty) (sym (++-assoc vs ys (u ∷ us)) ∙ ap (_++ u ∷ us) q ∙ p)

⊏ʳ-⊑ʳ-asym {xs = xs} {ys = ys} (u , us , p) (vs , q) =
  ++-no-fixr (u ∷ us ++ vs) ys $
  (u ∷ us ++ vs) ++ ys ≡⟨ ++-assoc (u ∷ us) vs ys ⟩≡
  u ∷ us ++ vs ++ ys   ≡⟨ ap (u ∷ us ++_) q ⟩≡
  u ∷ us ++ xs         ≡⟨ p ⟩≡
  ys                   ∎

⊏ˡ-⊑ˡ-asym {xs = xs} {ys = ys} (u , us , p) (vs , q) =
  ++-no-fixl xs (u ∷ us ++ vs) $
  xs ++ u ∷ us ++ vs ≡˘⟨ ++-assoc xs (u ∷ us) vs ⟩≡˘
  (xs ++ u ∷ us) ++ vs ≡⟨ ap (_++ vs) p ⟩≡
  ys ++ vs             ≡⟨ q ⟩≡
  xs                   ∎

Non-joint asymmetry follows immediately from weakening

⊏ˡ-asym
  : ∀ {xs ys : List A}
  → xs ⊏ˡ ys → ys ⊏ˡ xs
  → ⊥
⊏ˡ-asym xs⊏ys ys⊏xs = ⊏ˡ-⊑ˡ-asym xs⊏ys (⊏ˡ-weaken ys⊏xs)

⊏ʳ-asym
  : ∀ {xs ys : List A}
  → xs ⊏ʳ ys → ys ⊏ʳ xs
  → ⊥
⊏ʳ-asym xs⊏ys ys⊏xs = ⊏ʳ-⊑ʳ-asym xs⊏ys (⊏ʳ-weaken ys⊏xs)

Levi’s lemma🔗

The next obvious step is to prove antisymmetry of the factorisation relations. This is slightly tricker than the other cases, so we will take a slight detour to prove Levi’s lemma (Levi 1944): if two words $a s + b s = x s + ys,$ then there is some list $u s$ that characterises their overlap. In more succinct terms, the free monoid is equidivisible.

++-equidiv
  : ∀ {ℓ} {A : Type ℓ}
  → (as bs xs ys : List A)
  → as ++ bs ≡ xs ++ ys
  → Σ[ us ∈ List A ] ((as ≡ xs ++ us × us ++ bs ≡ ys) ⊎ (as ++ us ≡ xs × bs ≡ us ++ ys))

The proof is somewhat obvious, but contains algorithmic content. We proceed by induction down $a s$ and $x s;$ when one of them is empty, we simply returun the other list.

++-equidiv [] bs xs ys as+bs=xs+ys =
  xs , inr (refl , as+bs=xs+ys)
++-equidiv (a ∷ as) bs [] ys as+bs=xs+ys =
  a ∷ as , inl (refl , as+bs=xs+ys)

If the are both non-empty, we just recurse.

++-equidiv (a ∷ as) bs (x ∷ xs) ys as+bs=xs+ys with ++-equidiv as bs xs ys (∷-tail-inj as+bs=xs+ys)
... | us , inl (as=xs+us , us+bs=ys) =
  us , inl (ap₂ _∷_ (∷-head-inj as+bs=xs+ys) as=xs+us , us+bs=ys)
... | us , inr (as+us=xs , bs=us+ys) =
  us , (inr (ap₂ _∷_ (∷-head-inj as+bs=xs+ys) as+us=xs , bs=us+ys))

Levi’s lemma has some extremely useful corollaries. First, observe that if $x s$ and $ys$ are both left/right factors of some common word $zs,$ then either $x s$ is a proper left/right factor of $ys,$ $ys$ is a proper left/right of $x s,$ or $x s = ys .$

⊑ˡ-equidiv
  : ∀ {xs ys zs : List A}
  → xs ⊑ˡ zs
  → ys ⊑ˡ zs
  → Tri _⊏ˡ_ xs ys

⊑ʳ-equidiv
  : ∀ {xs ys zs : List A}
  → xs ⊑ʳ zs
  → ys ⊑ʳ zs
  → Tri _⊏ʳ_ xs ys

The argument is quite elegant: by definition, $x s + u s = ys + v s$ for some $u s, v s .$ We then invoke Levi’s lemma to find their overlap: if the overlap is empty, then we immediately know that $x s = ys .$ Moreover, we can deduce if $x s$ is a proper left factor of $ys$ or vice-versa by the direction the overlap extends in!

⊑ˡ-equidiv {xs = xs} {ys = ys} {zs = zs} (us , p) (vs , q)
  with ++-equidiv xs us ys vs (p ∙ sym q)
... | [] , inl (xs=ys+[] , _) =
  eq (flip ⊏ˡ-irrefl' xs=ys) xs=ys (flip ⊏ˡ-irrefl' (sym xs=ys))
  where
    xs=ys : xs ≡ ys
    xs=ys = xs=ys+[] ∙ ++-idr ys
... | [] , inr ([]+xs=ys , _) =
  eq (flip ⊏ˡ-irrefl' xs=ys) xs=ys (flip ⊏ˡ-irrefl' (sym xs=ys))
  where
    xs=ys : xs ≡ ys
    xs=ys = sym (++-idr xs) ∙ []+xs=ys
... | w ∷ ws , inl (xs=ys+ws , _) =
  gt (⊏ˡ-asym ys⊏xs) (⊏ˡ-irrefl' ys⊏xs ∘ sym) ys⊏xs
  where
    ys⊏xs : ys ⊏ˡ xs
    ys⊏xs = w , ws , sym xs=ys+ws
... | w ∷ ws , inr (xs+ws=ys , _) =
  lt xs⊏ys (⊏ˡ-irrefl' xs⊏ys) (⊏ˡ-asym xs⊏ys)
  where
    xs⊏ys : xs ⊏ˡ ys
    xs⊏ys = w , ws , xs+ws=ys

The right case follows the same line of argument, so we omit the details.

⊑ʳ-equidiv {xs = xs} {ys = ys} {zs = zs} (us , p) (vs , q)
  with ++-equidiv us xs vs ys (p ∙ sym q)
... | [] , inl (_ , xs=ys) =
  eq (flip ⊏ʳ-irrefl' xs=ys) xs=ys (flip ⊏ʳ-irrefl' (sym xs=ys))
... | [] , inr (_ , xs=ys) =
  eq (flip ⊏ʳ-irrefl' xs=ys) xs=ys (flip ⊏ʳ-irrefl' (sym xs=ys))
... | w ∷ ws , inl (_ , ws+xs=ys) =
  lt xs⊏ys (⊏ʳ-irrefl' xs⊏ys) (⊏ʳ-asym xs⊏ys)
  where
    xs⊏ys : xs ⊏ʳ ys
    xs⊏ys = w , ws , ws+xs=ys
... | w ∷ ws , inr (_ , xs=ws+ys) =
  gt (⊏ʳ-asym ys⊏xs) (⊏ʳ-irrefl' ys⊏xs ∘ sym) ys⊏xs
  where
    ys⊏xs : ys ⊏ʳ xs
    ys⊏xs = w , ws , sym xs=ws+ys

We can whittle Levi’s lemma down to an even finer point: if $x s$ is a proper left/right factor of $ys + zs,$ then $x s$ is either:

A proper left/right factor of $zs .$
Equal to $zs .$
Properly left/right factored by $zs,$ and the corresponding right/left factor is a proper left/right factor of $ys .$

⊏ˡ-split-++
  : ∀ {A : Type ℓ} (xs ys zs : List A)
  → xs ⊏ˡ ys ++ zs
  → (xs ⊏ˡ ys) ⊎ (xs ≡ ys) ⊎ (Σ[ ys⊏xs ∈ ys ⊏ˡ xs ] ⊏ˡ-factor ys⊏xs ⊏ˡ zs)
⊏ʳ-split-++
  : ∀ {A : Type ℓ} (xs ys zs : List A)
  → xs ⊏ʳ ys ++ zs
  → (xs ⊏ʳ zs) ⊎ (xs ≡ zs) ⊎ (Σ[ zs⊏xs ∈ zs ⊏ʳ xs ] ⊏ʳ-factor zs⊏xs ⊏ʳ ys)

We shall present the proof for right factors. By definition, if $x s$ is a proper left factor of $ys + zs,$ then there is some nonempty $u s$ such that $u s + x s = ys + zs .$ Once we apply Levi’s lemma, the rest of the proof essentially becomes definition unfolding.

⊏ʳ-split-++ xs ys zs (u , us , us+xs=ys+zs)
  with ++-equidiv (u ∷ us) xs ys zs us+xs=ys+zs
... | [] , inl (_ , xs=zs) =
  inr (inl xs=zs)
... | [] , inr (_ , xs=zs) =
  inr (inl xs=zs)
... | w ∷ ws , inl (_ , ws+xs=zs) =
  inl (w , ws , ws+xs=zs)
... | w ∷ ws , inr (us+ws=ys , xs=ws+zs) =
  inr (inr ((w , ws , sym xs=ws+zs) , u , us , us+ws=ys))

The left factor case is equivalent, though marginally more tedious.

⊏ˡ-split-++ xs ys zs (u , us , xs+us=ys+zs)
  with ++-equidiv xs (u ∷ us) ys zs xs+us=ys+zs
... | [] , inl (xs=ys , _) =
  inr (inl (xs=ys ∙ ++-idr ys))
... | [] , inr (xs=ys , _) =
  inr (inl (sym (++-idr xs) ∙ xs=ys))
... | w ∷ ws , inl (xs=ys+ws , ws+us=zs) =
  inr (inr ((w , ws , sym xs=ys+ws) , u , us , ws+us=zs))
... | w ∷ ws , inr (xs+ws=ys , _) =
  inl (w , ws , xs+ws=ys)

Asymmetry🔗

Now that we have Levi’s lemma and its corollaries, antisymmetry is easy.

⊑ˡ-antisym : ∀ {xs ys : List A} → xs ⊑ˡ ys → ys ⊑ˡ xs → xs ≡ ys
⊑ʳ-antisym : ∀ {xs ys : List A} → xs ⊑ʳ ys → ys ⊑ʳ xs → xs ≡ ys

Suppose that $x s$ and $ys$ are left/right factors of one another. In particular, this means that $x s$ and $ys$ are both factors of $ys .$ By equidivisibility, we have that $x s = ys,$ or one of $x s$ or $ys$ is a proper factor of the other. Joint asymmetry rules out those two cases, which lets us deduce that $x s = ys$

⊑ˡ-antisym {xs = xs} {ys = ys} xs⊑ys ys⊑xs
  with ⊑ˡ-equidiv xs⊑ys ⊑ˡ-refl
... | lt xs⊏ys _ _ = absurd (⊏ˡ-⊑ˡ-asym xs⊏ys ys⊑xs)
... | eq _ xs=ys _ = xs=ys
... | gt _ _ ys⊏xs = absurd (⊏ˡ-⊑ˡ-asym ys⊏xs xs⊑ys)

⊑ʳ-antisym {xs = xs} {ys = ys} xs⊑ys ys⊑xs
  with ⊑ʳ-equidiv xs⊑ys ⊑ʳ-refl
... | lt xs⊏ys _ _ = absurd (⊏ʳ-⊑ʳ-asym xs⊏ys ys⊑xs)
... | eq _ xs=ys _ = xs=ys
... | gt _ _ ys⊏xs = absurd (⊏ʳ-⊑ʳ-asym ys⊏xs xs⊑ys)

Uniqueness of left and right factors🔗

Note that we do not require mere existence in the definition of left/right factor. This is because there is only one such $u s$ that witnesses a list as a left/right factor!

⊑ˡ-unique
  : ∀ {xs ys : List A}
  → (p q : xs ⊑ˡ ys)
  → ⊑ˡ-factor p ≡ ⊑ˡ-factor q

⊑ʳ-unique
  : ∀ {xs ys : List A}
  → (p q : xs ⊑ʳ ys)
  → ⊑ʳ-factor p ≡ ⊑ʳ-factor q

Like many things, these are essentially restatements of Levi’s lemma. We shall focus our attention on the left-factor case. Suppose that $x s + u s = ys = x s + v s .$ If we apply Levi’s lemma to this equation, we can immediately see that the only possible outcome is that $u s = v s;$ any other case results in a fixpoint of concatenation.

⊑ˡ-unique {xs = xs} {ys = ys} (us , p) (vs , q)
  with ++-equidiv xs us xs vs (p ∙ sym q)
... | [] , (inl (_ , us=vs)) = us=vs
... | [] , (inr (_ , us=vs)) = us=vs
... | w ∷ ws , inl (xs=xs+ws , _) =
  absurd (++-no-fixl xs (w ∷ ws) (sym xs=xs+ws))
... | w ∷ ws , inr (xs+ws=xs , _) =
  absurd (++-no-fixl xs (w ∷ ws) (xs+ws=xs))

A dual argument works for right factors.

⊑ʳ-unique {xs = xs} {ys = ys} (us , p) (vs , q)
  with ++-equidiv us xs vs xs (p ∙ sym q)
... | [] , (inl (us=vs , _)) = us=vs ∙ ++-idr vs
... | [] , (inr (us=vs , _)) = sym (++-idr us) ∙ us=vs
... | w ∷ ws , inl (_ , ws+xs=xs) =
  absurd (++-no-fixr (w ∷ ws) xs ws+xs=xs)
... | w ∷ ws , inr (_ , xs=ws+xs) =
  absurd (++-no-fixr (w ∷ ws) xs (sym xs=ws+xs))

If $A$ is a set, then we can prove that _⊑ˡ_ and _⊑ʳ_ are both propositions.

⊑ˡ-is-prop
  : ∀ {xs ys : List A}
  → is-set A
  → is-prop (xs ⊑ˡ ys)
⊑ˡ-is-prop A-set p q =
  Σ-prop-path (λ _ → ListPath.List-is-hlevel zero A-set _ _)
    (⊑ˡ-unique p q)

⊑ʳ-is-prop
  : ∀ {xs ys : List A}
  → is-set A
  → is-prop (xs ⊑ʳ ys)
⊑ʳ-is-prop A-set p q =
  Σ-prop-path (λ _ → ListPath.List-is-hlevel zero A-set _ _)
    (⊑ʳ-unique p q)

Atoms🔗

Recall that an atomic element in a monoid is one that cannot be written as a product of two non-invertible elements. When specialized to the free monoid, this precisely describes singleton lists.

We have a handful of useful results detailing factors of atomic elements, but they are all repackaged forms of the same idea: namely, that the only factors of a singleton list are the empty list and itself.

⊑ʳ-atom
  : ∀ {xs : List A} {y : A}
  → xs ⊑ʳ y ∷ []
  → Empty xs ⊎ xs ≡ y ∷ []
⊑ʳ-atom {xs = []} {y = y} xs⊑y =
  inl empty
⊑ʳ-atom {xs = x ∷ []} {y = y} xs⊑y =
  inr (ap (_∷ []) (⊑ʳ-last xs⊑y))
⊑ʳ-atom {xs = x ∷ x' ∷ xs} {y = y} xs⊑y =
  absurd (⊑ʳ-strict-bot (⊑ʳ-init xs⊑y))

⊏ʳ-atom
  : ∀ {xs : List A} {y : A}
  → xs ⊏ʳ y ∷ []
  → Empty xs
⊏ʳ-atom {xs = []} {y = y} p = empty
⊏ʳ-atom {xs = x ∷ xs} {y = y} p =
  absurd (⊏ʳ-strict-bot (init (x ∷ xs)) (⊏ʳ-init p))

nonempty-¬⊏ʳ-atom
  : ∀ {xs : List A} {y : A}
  → Nonempty xs
  → ¬ (xs ⊏ʳ y ∷ [])
nonempty-¬⊏ʳ-atom ne xs⊏y = Equiv.to empty≃¬nonempty (⊏ʳ-atom xs⊏y) ne

We also take the time to observe that the atom last xs of a non-empty list is a factor of x ∷ xs.

last-nonempty-⊏ʳ
  : ∀ (x : A) (xs : List A)
  → ⦃ _ : Nonempty xs ⦄
  → last⁺ xs ∷ [] ⊏ʳ x ∷ xs
last-nonempty-⊏ʳ x (x' ∷ xs) =
  x , init (x' ∷ xs) , ap (x ∷_) (init-last-∷r xs x')

Relating left and right factors🔗

A word $x s$ is a right factor of $ys$ if and only if the reverse of $x s$ is a left factor of the reverse of $ys .$

⊑ʳ≃reverse-⊑ˡ
  : ∀ (xs ys : List A)
  → (xs ⊑ʳ ys) ≃ (reverse xs ⊑ˡ reverse ys)

The proof is essentially “reverse is an anti-isomorphism”.

⊑ʳ≃reverse-⊑ˡ xs ys =
  Σ-ap reverse-≃ λ us →
    us ++ xs ≡ ys                         ≃⟨ ap reverse , equiv→cancellable reverse-is-equiv ⟩≃
    reverse (us ++ xs) ≡ reverse ys       ≃⟨ ∙-pre-equiv (sym (reverse-++ us xs)) ⟩≃
    reverse xs ++ reverse us ≡ reverse ys ≃∎

We can extend this result to proper factors by recalling that proper factors are precisely factors whose other half is non-empty.

⊏ʳ≃reverse-⊏ˡ
  : ∀ (xs ys : List A)
  → (xs ⊏ʳ ys) ≃ (reverse xs ⊏ˡ reverse ys)
⊏ʳ≃reverse-⊏ˡ xs ys =
  xs ⊏ʳ ys                                              ≃⟨ ⊏ʳ≃⊑ʳ-nonempty xs ys ⟩≃
  (Σ[ p ∈ xs ⊑ʳ ys ] Nonempty (p .fst))                 ≃⟨ Σ-ap (⊑ʳ≃reverse-⊑ˡ xs ys) (λ xs⊑ys → reverse-nonempty (xs⊑ys .fst) e⁻¹) ⟩≃
  (Σ[ p ∈ reverse xs ⊑ˡ reverse ys ] Nonempty (p .fst)) ≃˘⟨ ⊏ˡ≃⊑ˡ-nonempty (reverse xs) (reverse ys) ⟩≃˘
  reverse xs ⊏ˡ reverse ys                              ≃∎

A similar argument lets us deduce that left factors are the same as reversed right factors.

⊑ˡ≃reverse-⊑ʳ
  : ∀ (xs ys : List A)
  → (xs ⊑ˡ ys) ≃ (reverse xs ⊑ʳ reverse ys)
⊑ˡ≃reverse-⊑ʳ xs ys =
  Σ-ap reverse-≃ λ us →
    xs ++ us ≡ ys                         ≃⟨ ap reverse , equiv→cancellable reverse-is-equiv ⟩≃
    reverse (xs ++ us) ≡ reverse ys       ≃⟨ ∙-pre-equiv (sym (reverse-++ xs us)) ⟩≃
    reverse us ++ reverse xs ≡ reverse ys ≃∎

Deciding if a list is a factor🔗

If $A$ has decidable equality, then we have an easy, efficient algorithm for checking if lists are left factors of one another: simply start checking from the head of the list.

instance
  Dec-⊑ˡ
    : ∀ {xs ys : List A}
    → ⦃ _ : Discrete A ⦄
    → Dec (xs ⊑ˡ ys)
  Dec-⊑ˡ {xs = []} {ys = ys} = yes (ys , refl)
  Dec-⊑ˡ {xs = x ∷ xs} {ys = []} = no (∷≠[] ∘ snd)
  Dec-⊑ˡ {xs = x ∷ xs} {ys = y ∷ ys} with x ≡? y
  ... | yes x=y =
    invmap
      (Σ-map₂ (ap₂ _∷_ x=y))
      (Σ-map₂ ∷-tail-inj)
      (holds? (xs ⊑ˡ ys))
  ... | no ¬x=y = no (¬x=y ∘ ∷-head-inj ∘ snd)

Deciding if a list is a right factor is a bit tricker. We are using linked lists as our main datastructure of choice, so they have an inherent leftward bias. There isn’t a good choice here; any solution that tries to use lengths will also end up eating a $Θ (n)$ cost, and accessing the last element is also $Θ (n) .$ Therefore, the best option is to reverse the lists, and check if it is a right factor.

  Dec-⊑ʳ
    : ∀ {xs ys : List A}
    → ⦃ _ : Discrete A ⦄
    → Dec (xs ⊑ʳ ys)
  Dec-⊑ʳ {xs = xs} {ys = ys} =
    Equiv→Dec (⊑ʳ≃reverse-⊑ˡ xs ys)
      (holds? (reverse xs ⊑ˡ reverse ys))

Well-foundedness🔗

Both the proper left and proper right factor relations are well-founded. This is a critical fact for the correctness of many algorithms, as it lets us prove that the actually terminate.

In a surprising role-reversal, the proof for right factors is easier! This ends up boiling down to the fact that we need make calls on increasingly smaller tails of lists, which lines up with the natural direction of structural induction over lists. From an algorithmic perspective, this is also the preferable iteration order: we don’t need to traverse the entire list to start working, which means that any algorithms that use right-factor induction are naturally online.

⊏ʳ-wf : Wf {A = List A} _⊏ʳ_
⊏ʳ-wf xs = go xs xs ⊑ʳ-refl
  module ⊏ʳ-wf where
    go : (xs ys : List A) → .(ys ⊑ʳ xs) → Acc _⊏ʳ_ ys
    go xs [] p = acc (λ zs zs⊏[] → absurd (⊏ʳ-strict-bot zs zs⊏[]))
    go [] (y ∷ ys) p = absurd (⊑ʳ-strict-bot p)
    go (x ∷ xs) (y ∷ ys) p = acc λ zs zs⊏y∷ys →
      go xs zs (⊏ʳ-tailr (⊏ʳ-⊑ʳ-trans zs⊏y∷ys p))

Left factors are much more troublesome, and require us to reverse a list. The fundamental issue here is that we need to shrink the list from starting from the final element, which just does not line up with structural recursion over lists. Reversing a list fixes this, but does make the proof much clunkier.

⊏ˡ-wf : Wf {A = List A} _⊏ˡ_
⊏ˡ-wf xs = go (reverse xs) xs (⊑ˡ-refl' (sym (reverse-reverse xs)))
  module ⊏˘ˡ-wf where
    go : (xs ys : List A) → .(ys ⊑ˡ reverse xs) → Acc _⊏ˡ_ ys
    go xs [] p = acc λ zs zs⊏[] → absurd (⊏ˡ-strict-bot zs zs⊏[])
    go [] (y ∷ ys) p = absurd (⊑ˡ-strict-bot p)
    go (x ∷ xs) (y ∷ ys) p = acc λ zs zs⊏y∷ys →
      go xs zs $ᵢ
        ⊑ˡ-trans (⊏ˡ-initr (⊏ˡ-⊑ˡ-trans zs⊏y∷ys p)) $
        ⊑ˡ-refl' (init-nonempty-⋉ xs (x ∷ []))

Fixpoints🔗

We can repackage our prior fixpoint lemmas as statements about factors; this is essentially a restatement of irreflexivity.

⊑ʳ-no-fixl
  : ∀ (xs ys : List A)
  → Nonempty ys
  → ¬ (xs ++ ys ⊑ʳ xs)
⊑ʳ-no-fixl xs ys ne (vs , p) = ++-no-fix vs xs ys (inr ne) p

⊑ʳ-no-fixr
  : ∀ (xs ys : List A)
  → ⦃ Nonempty xs ⦄
  → ¬ (xs ++ ys ⊑ʳ ys)
⊑ʳ-no-fixr xs ys (vs , p) =
  ++-no-fixr (vs ++ xs) ys ⦃ ++-nonemptyr vs xs auto ⦄ (++-assoc vs xs ys ∙ p)

Factors of concatenations🔗

If $w s + ys$ is a proper right factor of $x s + zs$ and $∣ ys ∣=∣ zs ∣,$ then $w s$ is a proper right factor of $x s .$

⊏ʳ-++-restrictl
  : ∀ {ws xs : List A}
  → (ys zs : List A)
  → length ys ≡ length zs
  → (ws ++ ys) ⊏ʳ (xs ++ zs) → ws ⊏ʳ xs

The proof is a bit of straightforward algebra that hinges on the following observation from earlier: if $∣ w s + ys ∣=∣ x s + zs ∣$ and $∣ ys ∣=∣ zs ∣,$ then $∣ w s ∣=∣ x s ∣ .$ Once we have this, the proof is reduced to shuffling around a take.

⊏ʳ-++-restrictl {ws = ws} {xs = xs} ys zs ys-zs-same-len (u , us , p) =
  ++-nonempty-⊏ʳ (u ∷ us) ws xs nonempty $
    u ∷ us ++ ws                                               ≡˘⟨ take-all (length (u ∷ us ++ ws)) (u ∷ us ++ ws) ≤-refl ⟩≡˘
    take (length (u ∷ us ++ ws)) (u ∷ us ++ ws)                ≡˘⟨ take-++l (length (u ∷ us ++ ws)) (u ∷ us ++ ws) ys ≤-refl ⟩≡˘
    take ⌜ length (u ∷ us ++ ws) ⌝ ((u ∷ us ++ ws) ++ ys)      ≡⟨ ap! us+ws-xs-same-len ⟩≡
    take (length xs) ((u ∷ us ++ ws) ++ ys)                    ≡⟨ ap (take (length xs)) (++-assoc (u ∷ us) ws ys) ⟩≡
    take (length xs) (u ∷ us ++ ws ++ ys)                      ≡⟨ ap (take (length xs)) p ⟩≡
    take (length xs) (xs ++ zs)                                ≡⟨ take-++l (length xs) xs zs ≤-refl ⟩≡
    take (length xs) xs                                        ≡⟨ take-all (length xs) xs ≤-refl ⟩≡
    xs                                                         ∎
  where
    us+ws-xs-same-len : length (u ∷ us ++ ws) ≡ length xs
    us+ws-xs-same-len =
      length-++-cancelr (u ∷ (us ++ ws)) xs ys zs
        (ap length (++-assoc (u ∷ us) ws ys ∙ p))
        ys-zs-same-len

A similar strategy lets us conclude that if $∣ w s ∣=∣ x s ∣$ and $w s + ys$ is a proper right factor of $x s + zs,$ then $ys$ is a proper right factor of $zs .$

⊏ʳ-++-restrictr
  : ∀ {ys zs : List A}
  → (ws xs : List A)
  → length ws ≡ length xs
  → (ws ++ ys) ⊏ʳ (xs ++ zs) → ys ⊏ʳ zs
⊏ʳ-++-restrictr {ys = ys} {zs = zs} ws xs ws-xs-same-len (u , us , p) =
  ++-nonempty-⊏ʳ (drop (length ws) (u ∷ us ++ ws)) ys zs
    (drop-nonempty (length ws) (u ∷ us ++ ws) (s≤s len-ws≤len-us+ws)) $
      drop (length ws) (u ∷ us ++ ws) ++ ys     ≡˘⟨ drop-++r (length ws) (u ∷ us ++ ws) ys (≤-sucr len-ws≤len-us+ws) ⟩≡˘
      drop ⌜ length ws ⌝ ((u ∷ us ++ ws) ++ ys) ≡⟨ ap! ws-xs-same-len ⟩≡
      drop (length xs) ((u ∷ us ++ ws) ++ ys)   ≡⟨ ap (drop (length xs)) (++-assoc (u ∷ us) ws ys) ⟩≡
      drop (length xs) (u ∷ us ++ ws ++ ys)     ≡⟨ ap (drop (length xs)) p ⟩≡
      drop (length xs) (xs ++ zs)               ≡⟨ drop-++r (length xs) xs zs ≤-refl ⟩≡
      drop (length xs) xs ++ zs                 ≡⟨ ap (_++ zs) (drop-all (length xs) xs ≤-refl) ⟩≡
      zs                                        ∎
    where
      len-ws≤len-us+ws : length ws ≤ length (us ++ ws)
      len-ws≤len-us+ws =
        ≤-trans (+-≤r (length us) (length ws)) $
        ≤-refl' (sym (length-++ us ws))

We also have a curious little result that relates right and left factors. Namely, if $x s$ is a proper right factor of $ys + zs,$ and $ys$ is a left factor of $x s,$ then the corresponding left factor of $x s$ is a right factor of $zs .$

⊏ʳ-++-restrictr-⊑ˡ
  : ∀ (xs ys zs : List A)
  → xs ⊏ʳ ys ++ zs
  → (p : ys ⊑ˡ xs)
  → p .fst ⊏ʳ zs

The theorem statement is honestly harder than the proof, which gives way after a bit of algebra.

⊏ʳ-++-restrictr-⊑ˡ xs ys zs (u , us , us+xs=ys+zs) (vs , ys+vs=xs) = vs⊏zs
  where
    us+ys+vs=ys+zs : u ∷ us ++ ys ++ vs ≡ ys ++ zs
    us+ys+vs=ys+zs =
      u ∷ us ++ ys ++ vs ≡⟨ ap (u ∷ us ++_) ys+vs=xs ⟩≡
      u ∷ us ++ xs       ≡⟨ us+xs=ys+zs ⟩≡
      ys ++ zs           ∎

    ys+vs⊏ys+zs : ys ++ vs ⊏ʳ ys ++ zs
    ys+vs⊏ys+zs = u , us , us+ys+vs=ys+zs

    vs⊏zs : vs ⊏ʳ zs
    vs⊏zs = ⊏ʳ-++-restrictr ys ys refl ys+vs⊏ys+zs

Factors of powers🔗

Clearly, $x s$ is a proper left factor of $x s^{k + 1} + ys$ if $ys$ is nonempty.

⊏ˡ-powers-inl
  : ∀ (xs : List A) (k : Nat) (ys : List A)
  → ⦃ Nonempty ys ⦄
  → xs ⊏ˡ powers xs (suc k) ys
⊏ˡ-powers-inl xs k ys =
  ⊏ˡ-++-inl xs (powers xs k ys) ⦃ powers-nonemptyr xs k ys auto ⦄

Conversly, $ys$ is a proper right factor of $x s^{k + 1} + ys$ if $x s$ is nonempty.

⊏ʳ-powers-inr
  : ∀ (xs : List A) (k : Nat) (ys : List A)
  → ⦃ Nonempty xs ⦄
  → ys ⊏ʳ powers xs (suc k) ys
⊏ʳ-powers-inr xs zero ys = ⊏ʳ-++-inr xs ys
⊏ʳ-powers-inr xs (suc k) ys =
  ⊏ʳ-trans (⊏ʳ-powers-inr xs k ys) $
  ⊏ʳ-++-inr xs (powers xs (suc k) ys)

Factors of `drop`🔗

If we remove a non-zero number of element from $x s,$ then we get a proper right factor.

drop-suc-⊏ʳ : ∀ (n : Nat) (xs : List A) → ⦃ Nonempty xs ⦄ → drop (suc n) xs ⊏ʳ xs
drop-suc-⊏ʳ zero (x ∷ xs) = x , [] , refl
drop-suc-⊏ʳ (suc n) (x ∷ []) = x , [] , refl
drop-suc-⊏ʳ (suc n) (x ∷ x' ∷ xs) =
  ⊏ʳ-trans (drop-suc-⊏ʳ n (x' ∷ xs)) $
  ⊏ʳ-++-inr (x ∷ []) (x' ∷ xs)

References

Levi, F. W. 1944. “On Semigroups.” Bulletin of the Calcutta Mathematical Society 36: 141–46.

Factors of drop🔗

References

Factors of `drop`🔗