open import 1Lab.Prelude
open import Data.Dec
open import Data.Nat using (0≤x; s≤s)
open import Data.Fin using (Fin; fzero; fsuc)
open import Data.Sum

open import StringLab.Order.Trichotomous
open import StringLab.Data.List.Factor
open import StringLab.Data.List

import Data.Fin as Fin
import Data.Nat as Nat

module StringLab.Data.List.Lexicographic {o ℓ} (A : Trichotomous o ℓ) where

Lexicographic orders on lists🔗

open Trichotomous A

Let $A$ be a strict total order. We define the lexicographic ordering on $A^{*}$ inductively:

For every $x, x s,$ $[] < x : : x s .$
If $x < y$ $(x : : x s) < (y : : ys) .$
If $x = y$ and $x s < ys,$ then $x : : x s < y : : ys .$

data _≺_ : List ⌞ A ⌟ → List ⌞ A ⌟ → Type (o ⊔ ℓ) where
  ≺-nil : ∀ {x xs} → [] ≺ (x ∷ xs)
  ≺-∷-head : ∀ {x y xs ys} → x < y → (x ∷ xs) ≺ (y ∷ ys)
  ≺-∷-tail : ∀ {x y xs ys} → x ≡ y → xs ≺ ys → (x ∷ xs) ≺ (y ∷ ys)

infix 6 _≺_

Next, we define some useful accessors.

≺-head-≤ : ∀ {x y xs ys} → (x ∷ xs) ≺ (y ∷ ys) → x ≤ y
≺-head-≤ (≺-∷-head x<y) = inl x<y
≺-head-≤ (≺-∷-tail x=y p) = inr x=y

≺-uncons : ∀ {x y xs ys} → (x ∷ xs) ≺ (y ∷ ys) → x < y ⊎ (x ≡ y × xs ≺ ys)
≺-uncons (≺-∷-head x<y) = inl x<y
≺-uncons (≺-∷-tail x=y xs<ys) = inr (x=y , xs<ys)

≺-untail : ∀ {x y xs ys} → x ≡ y → x ∷ xs ≺ y ∷ ys → xs ≺ ys
≺-untail x=y (≺-∷-head x<y) = absurd (<-irrefl' x<y x=y)
≺-untail x=y (≺-∷-tail _ xs<ys) = xs<ys

We can also provide versions of these lemmas that use our Nonempty API.

≺-head-nonempty
  : ∀ {xs ys : List ⌞ A ⌟}
  → (x y : ⌞ A ⌟)
  → Nonempty xs → Nonempty ys
  → head x xs < head y ys → xs ≺ ys
≺-head-nonempty {xs = x ∷ xs} {ys = y ∷ ys} _ _ _ _ x<y = ≺-∷-head x<y

Lexicographic orderings are transitive.

≺-trans : ∀ {xs ys zs} → xs ≺ ys → ys ≺ zs → xs ≺ zs

The proof is a straightforward induction.

≺-trans ≺-nil (≺-∷-head x) =
  ≺-nil
≺-trans ≺-nil (≺-∷-tail x q) =
  ≺-nil
≺-trans (≺-∷-head x<y) (≺-∷-head y<z) =
  ≺-∷-head (<-trans x<y y<z)
≺-trans (≺-∷-head x<y) (≺-∷-tail y=z ys<zs) =
  ≺-∷-head (subst _ y=z x<y)
≺-trans (≺-∷-tail x=y p) (≺-∷-head y<z) =
  ≺-∷-head (subst _ (sym x=y) y<z)
≺-trans (≺-∷-tail x=y xs<ys) (≺-∷-tail y=z ys<zs) =
  ≺-∷-tail (x=y ∙ y=z) (≺-trans xs<ys ys<zs)

Moreover, lexicographic orderings are trichotomous.

≺-tri : ∀ (xs ys : List ⌞ A ⌟) → Tri _≺_ xs ys

The proof is quite ugly, and reduces down to a giant case bash.

≺-tri [] [] = eq (λ ()) refl (λ ())
≺-tri [] (x ∷ ys) = lt ≺-nil (∷≠[] ∘ sym) (λ ())
≺-tri (x ∷ xs) [] = gt (λ ()) ∷≠[] ≺-nil
≺-tri (x ∷ xs) (y ∷ ys) with <-tri x y
... | lt x<y x≠y y≮x =
  lt (≺-∷-head x<y) (x≠y ∘ ∷-head-inj) ([ y≮x , x≠y ∘ sym ] ∘ ≺-head-≤)
... | gt x≮y x≠y y<x =
  gt ([ x≮y , x≠y ] ∘ ≺-head-≤) (x≠y ∘ ∷-head-inj) (≺-∷-head y<x)
... | eq x≮y x=y y≮x with ≺-tri xs ys
... | lt xs<ys xs≠ys ys≮xs =
  lt (≺-∷-tail x=y xs<ys) (xs≠ys ∘ ∷-tail-inj) (ys≮xs ∘ ≺-untail (sym x=y))
... | eq xs≮ys xs=ys ys≮xs =
  eq (xs≮ys ∘ ≺-untail x=y) (ap₂ _∷_ x=y xs=ys) (ys≮xs ∘ ≺-untail (sym x=y))
... | gt xs≮ys xs≠ys ys<xs =
  gt (xs≮ys ∘ ≺-untail x=y) (xs≠ys ∘ ∷-tail-inj) (≺-∷-tail (sym x=y) ys<xs)

Finally, the lexicographic ordering is a proposition; IE: all witnesses of the lexicographic order are equal.

≺-is-prop : ∀ {xs ys} → is-prop (xs ≺ ys)
≺-is-prop ≺-nil ≺-nil =
  refl
≺-is-prop (≺-∷-head x<y) (≺-∷-head x<y') =
  ap ≺-∷-head (<-is-prop x<y x<y')
≺-is-prop (≺-∷-head x<y) (≺-∷-tail x=y _) =
  absurd (<-irrefl' x<y x=y)
≺-is-prop (≺-∷-tail x=y xs<ys) (≺-∷-head x<y) =
  absurd (<-irrefl' x<y x=y)
≺-is-prop (≺-∷-tail x=y xs<ys) (≺-∷-tail x=y' xs<ys') =
  ap₂ ≺-∷-tail (Ob-is-set _ _ x=y x=y') (≺-is-prop xs<ys xs<ys')

instance
  H-Level-≺ : ∀ {xs ys n} → H-Level (xs ≺ ys) (suc n)
  H-Level-≺ = prop-instance ≺-is-prop

In other words, lexicographic orderings are trichotomous orders.

Lex-trichotomous : Trichotomous o (o ⊔ ℓ)
Lex-trichotomous .Trichotomous.Ob = List ⌞ A ⌟
Lex-trichotomous .Trichotomous._<_ = _≺_
Lex-trichotomous .Trichotomous.<-trans = ≺-trans
Lex-trichotomous .Trichotomous.<-tri = ≺-tri
Lex-trichotomous .Trichotomous.<-is-prop = ≺-is-prop

open Trichotomous Lex-trichotomous
  renaming
    ( _≤_ to _≼_
    ; ¬≥→< to ¬≽→≺
    ; <→¬≥ to ≺→¬≽
    ; ≤-<-trans to ≼-≺-trans
    ; <-≤-trans to ≺-≼-trans
    ; <-irrefl to ≺-irrefl
    ; <-irrefl' to ≺-irrefl'
    ; <-asym to ≺-asym
    ; <-linear to ≺-linear
    ; <-conn to ≺-conn
    ; Dec-≤ to Dec-≼
    ; Dec-< to Dec-≺
    )
  using ()
  public

Note that the non-strict order has a bottom element.

≼-bot : ∀ {xs} → [] ≼ xs
≼-bot {xs = []} = inr refl
≼-bot {xs = x ∷ xs} = inl ≺-nil

Basic properties of lexicographic orderings🔗

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

⊏ˡ-≺ : ∀ {xs ys} → xs ⊏ˡ ys → xs ≺ ys
⊏ˡ-≺ {xs = []} {ys = []} xs⊏ys = absurd (⊏ˡ-strict-bot [] xs⊏ys)
⊏ˡ-≺ {xs = []} {ys = x ∷ ys} xs⊏ys = ≺-nil
⊏ˡ-≺ {xs = x ∷ xs} {ys = []} xs⊏ys = absurd (⊏ˡ-strict-bot (x ∷ xs) xs⊏ys)
⊏ˡ-≺ {xs = x ∷ xs} {ys = y ∷ ys} xs⊏ys =
  ≺-∷-tail (⊏ˡ-head xs⊏ys) $
  ⊏ˡ-≺ (⊏ˡ-tail xs⊏ys)

Moreover, the lexicographic ordering is jointly asymmetric and jointly transitive with the left factor relation.

≺-⊒ˡ-asym : ∀ {xs ys} → xs ≺ ys → ¬ (ys ⊑ˡ xs)
≺-⊑ˡ-trans : ∀ {xs ys us} → ys ≺ us → us ⊑ˡ xs → ys ≺ xs
≺-⊏ˡ-trans : ∀ {xs ys us} → ys ≺ us → us ⊏ˡ xs → ys ≺ xs
⊑ˡ-≺-trans : ∀ {us xs ys} → us ⊑ˡ xs → xs ≺ ys → us ≺ ys
⊏ˡ-≺-trans : ∀ {us xs ys} → us ⊏ˡ xs → xs ≺ ys → us ≺ ys

These proofs are not very informative, so we will hide the details from all but the most brave readers.

≺-⊒ˡ-asym {xs = xs} {ys = ys} xs<ys ys⊑xs with xs ≡? ys
... | yes xs=ys = absurd (≺-irrefl' xs<ys xs=ys)
... | no ¬xs=ys =
  ≺-asym xs<ys $ ⊏ˡ-≺ $
  [ (λ ys=xs → absurd (¬xs=ys (sym ys=xs))) , id ] (⊑ˡ-strengthen ys⊑xs)


≺-⊑ˡ-trans {xs = []} {ys = ys} {us = u ∷ us} ys≺us us⊑xs = absurd (⊑ˡ-strict-bot us⊑xs)
≺-⊑ˡ-trans {xs = x ∷ xs} {ys = []} {us = u ∷ us} ≺-nil us⊑xs = ≺-nil
≺-⊑ˡ-trans {xs = x ∷ xs} {ys = y ∷ ys} {us = u ∷ us} (≺-∷-head y<u) us⊑xs =
  ≺-∷-head (subst (y <_) (⊑ˡ-head us⊑xs) y<u)
≺-⊑ˡ-trans {xs = x ∷ xs} {ys = y ∷ ys} {us = u ∷ us} (≺-∷-tail y=u ys≺us) us⊑xs =
  ≺-∷-tail (y=u ∙ ⊑ˡ-head us⊑xs) (≺-⊑ˡ-trans ys≺us (⊑ˡ-tail us⊑xs))

≺-⊏ˡ-trans ys≺us us⊏xs = ≺-⊑ˡ-trans ys≺us (⊏ˡ-weaken us⊏xs)

⊑ˡ-≺-trans {us = []} {ys = y ∷ ys} us⊑xs xs≺ys =
  ≺-nil
⊑ˡ-≺-trans {us = u ∷ us} {ys = y ∷ ys} us⊑xs ≺-nil =
  absurd (⊑ˡ-strict-bot us⊑xs)
⊑ˡ-≺-trans {us = u ∷ us} {ys = y ∷ ys} us⊑xs (≺-∷-head x<y) =
  ≺-∷-head (subst (_< y) (sym (⊑ˡ-head us⊑xs)) x<y)
⊑ˡ-≺-trans {us = u ∷ us} {ys = y ∷ ys} us⊑xs (≺-∷-tail x=y xs≺ys) =
  ≺-∷-tail (⊑ˡ-head us⊑xs ∙ x=y) (⊑ˡ-≺-trans (⊑ˡ-tail us⊑xs) xs≺ys)

⊏ˡ-≺-trans us⊏xs xs≺ys = ⊑ˡ-≺-trans (⊏ˡ-weaken us⊏xs) xs≺ys

Lexicographic ordering and concatenation🔗

If $x = y,$ then $x s < ys$ if and only if $x : : x s < y : : ys .$

≺-∷-extend : ∀ {x y xs ys} → x ≡ y → (xs ≺ ys) ≃ (x ∷ xs ≺ y ∷ ys)
≺-∷-extend x=y = prop-ext! (≺-∷-tail x=y) (≺-untail x=y)

We can extend this result to concatenations via an easy induction.

++-pres-≺l-≃
  : ∀ {ys zs} (ws xs : List ⌞ A ⌟)
  → ws ≡ xs
  → (ys ≺ zs) ≃ (ws ++ ys ≺ xs ++ zs)
++-pres-≺l-≃ {ys} {zs} [] [] ws=xs = id≃
++-pres-≺l-≃ {ys} {zs} [] (x ∷ xs) ws=xs = absurd ([]≠∷ ws=xs)
++-pres-≺l-≃ {ys} {zs} (x ∷ ws) [] ws=xs = absurd (∷≠[] ws=xs)
++-pres-≺l-≃ {ys} {zs} (w ∷ ws) (x ∷ xs) ws=xs =
  ys ≺ zs                     ≃⟨ ++-pres-≺l-≃ ws xs (∷-tail-inj ws=xs) ⟩≃
  ws ++ ys ≺ xs ++ zs         ≃⟨ ≺-∷-extend (∷-head-inj ws=xs) ⟩≃
  w ∷ ws ++ ys ≺ x ∷ xs ++ zs ≃∎

Equivalences are great, but a bit clunky to work with, so we provide named versions of both directions of the previous equivalence.

≺-++-extendl
  : ∀ {ys zs} (ws xs : List ⌞ A ⌟)
  → ws ≡ xs
  → (ys ≺ zs) → (ws ++ ys ≺ xs ++ zs)
≺-++-extendl ws xs ws=xs = Equiv.to (++-pres-≺l-≃ ws xs ws=xs)

≺-++-restrictl
  : ∀ {ys zs} (ws xs : List ⌞ A ⌟)
  → ws ≡ xs
  → (ws ++ ys ≺ xs ++ zs) → (ys ≺ zs)
≺-++-restrictl ws xs ws=xs = Equiv.from (++-pres-≺l-≃ ws xs ws=xs)

_ = _⋉_

We can extend this to ⋉ via duality.

≺-⋉-extendl
  : ∀ {ys zs} (ws xs : List ⌞ A ⌟)
  → ws ≡ xs
  → (ys ≺ zs) ≃ (ws ⋉ ys ≺ xs ⋉ zs)
≺-⋉-extendl {ys = ys} {zs = zs} ws xs ws=xs =
  ys ≺ zs                             ≃⟨ ++-pres-≺l-≃ (reverse ws) (reverse xs) (ap reverse ws=xs) ⟩≃
  reverse ws ++ ys ≺ reverse xs ++ zs ≃˘⟨ path→equiv (ap₂ _≺_ (⋉-exchangel [] ws ys) (⋉-exchangel [] xs zs)) ⟩≃˘
  ws ⋉ ys ≺ xs ⋉ zs                   ≃∎

We can slightly generalize the previous results: $x : : x s < y : : ys$ if and only if $x < y$ or $x = y \land x s < ys .$

≺-∷-examine : ∀ {x y xs ys} → (x ∷ xs ≺ y ∷ ys) ≃ (x < y ⊎ (x ≡ y × xs ≺ ys))
≺-∷-examine =
  prop-ext
    (hlevel 1)
    (disjoint-⊎-is-prop (hlevel 1) (hlevel 1) λ (x<y , x=y , _) → <-irrefl' x<y x=y)
    ≺-uncons
    [ ≺-∷-head , uncurry ≺-∷-tail ]

We can also describe how lexicographic orderings behave when you append rather than prepend, but it is decidedly more complicated.

Warning

Note that we need to ensure that $w s$ is not a prefix of $x s$ and $x s$ is not a prefix of $w s$ to get an equivalence; this condition is easily overlooked!

++-pres-≺r-≃
  : ∀ {ws xs : List ⌞ A ⌟} (ys zs : List ⌞ A ⌟)
  → ¬ (ws ⊑ˡ xs) → ¬ (xs ⊑ˡ ws)
  → (ws ≺ xs) ≃ (ws ++ ys ≺ xs ++ zs)

The proof is a giant inductive equivalence chase.

++-pres-≺r-≃ {[]} {xs} ys zs ¬ws⊑xs ¬xs⊑ws =
  absurd (¬ws⊑xs (xs , refl))
++-pres-≺r-≃ {w ∷ ws} {[]} ys zs ¬ws⊑xs ¬xs⊑ws =
  absurd (¬xs⊑ws (w ∷ ws , refl))
++-pres-≺r-≃ {w ∷ ws} {x ∷ xs} ys zs ¬ws⊑xs ¬xs⊑ws =
    w ∷ ws ≺ x ∷ xs
  ≃⟨ ≺-∷-examine ⟩≃
    w < x ⊎ (w ≡ x × ws ≺ xs)
  ≃⟨ ⊎-apr (Σ-ap id≃ (λ w=x → ++-pres-≺r-≃ ys zs (¬ws⊑xs ∘ ⊑ˡ-∷-extendl w=x) (¬xs⊑ws ∘ ⊑ˡ-∷-extendl (sym w=x)))) ⟩≃
    w < x ⊎ (w ≡ x × ws ++ ys ≺ xs ++ zs)
  ≃˘⟨ ≺-∷-examine ⟩≃˘
    w ∷ ws ++ ys ≺ x ∷ xs ++ zs
  ≃∎

We can relax the preconditions of the previous result if we only need a single direction of the equivalence.

Warning

Note the directions of the prefixes flip!

≺-++-extendr
  : ∀ {ws xs : List ⌞ A ⌟} (ys zs : List ⌞ A ⌟)
  → ¬ (ws ⊑ˡ xs)
  → ws ≺ xs
  → ws ++ ys ≺ xs ++ zs
≺-++-restrictr
  : ∀ {ws xs : List ⌞ A ⌟} (ys zs : List ⌞ A ⌟)
  → ¬ (xs ⊑ˡ ws)
  → ws ++ ys ≺ xs ++ zs
  → ws ≺ xs

We proceed by brute force induction, using our hypotheses to avoid the problematic cases where we’d need to prove that something is lex smaller than the empty list.

≺-++-extendr {ws} {xs} ys zs ¬ws⊑xs ≺-nil =
  absurd (¬ws⊑xs ⊑ˡ-bot)
≺-++-extendr {ws} {xs} ys zs ¬ws⊑xs (≺-∷-head w<x) =
  ≺-∷-head w<x
≺-++-extendr {ws} {xs} ys zs ¬ws⊑xs (≺-∷-tail w=x ws≺xs) =
  ≺-∷-tail w=x (≺-++-extendr ys zs (¬ws⊑xs ∘ ⊑ˡ-∷-extendl w=x) ws≺xs)

≺-++-restrictr {[]} {[]} ys zs ¬xs⊑ws ws++ys≺xs++zs =
  absurd (¬xs⊑ws ⊑ˡ-bot)
≺-++-restrictr {[]} {x ∷ xs} ys zs ¬xs⊑ws ws++ys≺xs++zs =
  ≺-nil
≺-++-restrictr {x ∷ ws} {[]} ys zs ¬xs⊑ws ws++ys≺xs++zs =
  absurd (¬xs⊑ws ⊑ˡ-bot)
≺-++-restrictr {w ∷ ws} {x ∷ xs} ys zs ¬xs⊑ws (≺-∷-head w<x) =
  ≺-∷-head w<x
≺-++-restrictr {w ∷ ws} {x ∷ xs} ys zs ¬xs⊑ws (≺-∷-tail w=x ws++ys≺xs++zs) =
  ≺-∷-tail w=x (≺-++-restrictr ys zs (¬xs⊑ws ∘ ⊑ˡ-∷-extendl (sym w=x)) ws++ys≺xs++zs)

These are versions of the previous lemma that are easier to use when zs is empty.

≺-nil-nonempty
  : ∀ {zs : List ⌞ A ⌟}
  → ⦃ Nonempty zs ⦄
  → [] ≺ zs
≺-nil-nonempty {zs = z ∷ zs} = ≺-nil

≺-++-injl
  : ∀ {xs ys zs : List ⌞ A ⌟}
  → xs ≺ ys
  → xs ≺ ys ++ zs
≺-++-injl ≺-nil = ≺-nil
≺-++-injl (≺-∷-head x<y) = ≺-∷-head x<y
≺-++-injl (≺-∷-tail x=y xs≺ys) = ≺-∷-tail x=y (≺-++-injl xs≺ys)

≺-++-injr
  : ∀ {xs ys zs : List ⌞ A ⌟}
  → ⦃ Nonempty zs ⦄
  → xs ≡ ys
  → xs ≺ ys ++ zs
≺-++-injr {xs = []} xs=ys = Equiv.to (++-pres-≺l-≃ [] _ xs=ys) ≺-nil-nonempty
≺-++-injr {xs = x ∷ xs} {ys = []} xs=ys =
  absurd (∷≠[] xs=ys)
≺-++-injr {xs = x ∷ xs} {ys = y ∷ ys} xs=ys =
  ≺-∷-tail (∷-head-inj xs=ys) (≺-++-injr (∷-tail-inj xs=ys))

≺-++-projl
  : ∀ {xs ys zs : List ⌞ A ⌟}
  → ¬ (xs ⊑ˡ zs)
  → xs ≺ zs
  → xs ++ ys ≺ zs
≺-++-projl ¬xs⊑zs ≺-nil = absurd (¬xs⊑zs ⊑ˡ-bot)
≺-++-projl ¬xs⊑zs (≺-∷-head x<z) = ≺-∷-head x<z
≺-++-projl ¬xs⊑zs (≺-∷-tail x=z xs≺zs) = ≺-∷-tail x=z (≺-++-projl (¬xs⊑zs ∘ ⊑ˡ-∷-extendl x=z) xs≺zs)

Lex orderings and Levi’s lemma🔗

Next, we prove a lex-ordering version of Levi’s lemma¹: if $x s < ys + zs,$ then either:

$x s \leq ys$
$ys$ is a proper left prefix of $x s,$ and the corresponding right factor is lex smaller than $zs .$

≺-split-++
  : ∀ (xs ys zs : List ⌞ A ⌟)
  → xs ≺ ys ++ zs
  → xs ≼ ys ⊎ (Σ[ ys⊏xs ∈ ys ⊏ˡ xs ] ⊏ˡ-factor ys⊏xs ≺ zs)

Like most results in this file, the proof reduces to a giant case bash.

≺-split-++ [] [] zs xs≺ys+zs = inl (inr refl)
≺-split-++ (x ∷ xs) [] zs xs≺ys+zs = inr (⊏ˡ-bot , xs≺ys+zs)
≺-split-++ [] (y ∷ ys) zs xs≺ys+zs = inl (inl ≺-nil)
≺-split-++ (x ∷ xs) (y ∷ ys) zs (≺-∷-head x<y) = inl (inl (≺-∷-head x<y))
≺-split-++ (x ∷ xs) (y ∷ ys) zs (≺-∷-tail x=y xs≺ys+zs) with ≺-split-++ xs ys zs xs≺ys+zs
... | inl (inl xs≺ys) = inl (inl (≺-∷-tail x=y xs≺ys))
... | inl (inr xs=ys) = inl (inr (ap₂ _∷_ x=y xs=ys))
... | inr (ys⊏xs , us≺zs) = inr (⊏ˡ-∷-extendl (sym x=y) ys⊏xs , us≺zs)

A slightly sharper version of the previous lemma lets us determine if a lex smaller list is a prefix, or if there is some element that is smaller.

≺-find-<
  : ∀ {xs ys : List ⌞ A ⌟}
  → xs ≺ ys
  → (xs ⊏ˡ ys)
  ⊎ Σ[ us ∈ List ⌞ A ⌟ ] Σ[ us⊏xs ∈ us ⊏ˡ xs ] Σ[ us⊏ys ∈ us ⊏ˡ ys ] (us⊏xs .fst < us⊏ys .fst)

As is usual, the proof follows from some straightforward induction.

≺-find-< {xs = []} ≺-nil = inl ⊏ˡ-bot
≺-find-< {xs = x ∷ xs} (≺-∷-head x<y) = inr ([] , ⊏ˡ-bot , ⊏ˡ-bot , x<y)
≺-find-< {xs = x ∷ xs} (≺-∷-tail x=y xs≺ys) with ≺-find-< xs≺ys
... | inl xs⊏ys =
  inl (⊏ˡ-∷-extendl x=y xs⊏ys)
... | inr (us , us⊏xs , us⊏ys , x'<y') =
  inr (x ∷ us , (⊏ˡ-∷-extendl refl us⊏xs) , ⊏ˡ-∷-extendl x=y us⊏ys , x'<y')

Note that we can eliminate a lot of these cases if we already know that $ys$ is a proper left prefix of $x s .$

≺-++-restrict-⊏ˡ
  : {xs ys zs : List ⌞ A ⌟}
  → (ys⊏xs : ys ⊏ˡ xs)
  → xs ≺ ys ++ zs
  → ⊏ˡ-factor ys⊏xs ≺ zs
≺-++-restrict-⊏ˡ {xs = xs} {ys = []} {zs = zs} ys⊏xs@(u , us , ys+us=xs) xs≺ys+zs =
  ≼-≺-trans (inr ys+us=xs) xs≺ys+zs
≺-++-restrict-⊏ˡ {xs = xs} {ys = y ∷ ys} {zs = zs} ys⊏xs ≺-nil =
  absurd (⊏ˡ-strict-bot (y ∷ ys) ys⊏xs)
≺-++-restrict-⊏ˡ {xs = xs} {ys = y ∷ ys} {zs = zs} ys⊏xs (≺-∷-head x<y) =
  absurd (<-irrefl' x<y (sym (⊏ˡ-head ys⊏xs)))
≺-++-restrict-⊏ˡ {xs = xs} {ys = y ∷ ys} {zs = zs} ys⊏xs (≺-∷-tail _ xs≺ys+zs) =
  ≺-++-restrict-⊏ˡ (⊏ˡ-tail ys⊏xs) xs≺ys+zs

The previous lemmas gave us a good picture of how lex orderings decompose into left factors. This leads to a natural question: how do lex orderings relate to right factors? The next result gives a partial answer to this question: if $x s$ is a proper right factor of $ys,$ then either:

Every right factor of $u s$ is lex larger than $ys .$
There is some nonempty right factor of $x s$ with $u s$ lex smaller than $ys .$

≺-on-suffixes
  : ∀ (xs ys : List ⌞ A ⌟)
  → xs ⊏ʳ ys
  → (∀ us → ⦃ Nonempty us ⦄ → us ⊑ʳ xs → ys ≺ us)
  ⊎ (Σ[ us ∈ List ⌞ A ⌟ ] (Nonempty us × us ⊑ʳ xs × us ≺ ys))

The proof is yet another induction, though this one is of particular interest. When viewed from a computational angle, this proof is essentially checking if a word is Lyndon. This is important enough to warrant close inspection.

If $x s$ is empty, then there are no nonempty right factors, so condition (1) is trivially true.

≺-on-suffixes [] ys []⊏ys = inl λ where
  (u ∷ us) us⊏[] → absurd (⊑ʳ-strict-bot us⊏[])

If $x s$ is nonempty, then the situation is more interesting. We begin by checking if $x s$ is lex lesser than $ys;$ if it is, then condition (2) holds. Note that $x s = ys$ contradicts our hypothesis that $x s$ is a proper right factor, so this leaves the case where $ys < x s .$ If this is the case,, then we recurse on the tail of $x s .$

Clearly, this algorithm is $O (n^{2}) .$ We could do better by computing a suffix array, but this project is already quite large! Moreover, we don’t ever need to check if a word is Lyndon directly in code that we intend to run; this result is only used for proving properties.

≺-on-suffixes (x ∷ xs) ys xs⊏ys with ≺-tri (x ∷ xs) ys
... | lt xs≺ys _ _ =
  inr (x ∷ xs , nonempty , ⊑ʳ-refl , xs≺ys)
... | eq _ xs=ys _ =
  absurd (⊏ʳ-irrefl' xs⊏ys xs=ys)
... | gt _ _ ys≺xs with ≺-on-suffixes xs ys (⊏ʳ-∷-shrinkl xs⊏ys)
... | inl p = inl λ where
  us us⊏x∷xs →
    case ⊑ʳ-∷-inversion us⊏x∷xs of λ where
      (inl us=x∷xs) → subst (ys ≺_) (sym us=x∷xs) ys≺xs
      (inr us⊏xs) → p us us⊏xs
... | inr (us , us-ne , us⊑xs , us≺ys) =
  inr (us , us-ne , ⊑ʳ-∷-extendr us⊑xs , us≺ys)

Atoms🔗

Like factors, we can neatly the lex order of atomic elements. These results are all repackaging the same idea: if something is lex smaller than an atom, then it is either empty, or another atom that is smaller.

≺-atom
  : ∀ {xs : List ⌞ A ⌟} {y : ⌞ A ⌟}
  → xs ≺ y ∷ []
  → Empty xs ⊎ Σ[ ne ∈ Nonempty xs ] (head⁺ xs ⦃ ne ⦄ < y)
≺-atom {xs = xs} {y = y} ≺-nil = inl empty
≺-atom {xs = xs} {y = y} (≺-∷-head x<y) = inr (nonempty , x<y)

≺-atom-nonempty
  : ∀ {xs : List ⌞ A ⌟} {y : ⌞ A ⌟}
  → ⦃ _ : Nonempty xs ⦄
  → xs ≺ y ∷ []
  → head⁺ xs < y
≺-atom-nonempty {xs = x ∷ xs} (≺-∷-head x<y) = x<y

atom-≺
  : ∀ {x : ⌞ A ⌟} {ys : List ⌞ A ⌟}
  → x ∷ [] ≺ ys
  → Σ[ ne ∈ Nonempty ys ] (x ≤ head⁺ ys ⦃ ne ⦄)
atom-≺ {ys = ys} (≺-∷-head x) = nonempty , inl x
atom-≺ {ys = ys} (≺-∷-tail x ≺-nil) = nonempty , inr x

Drop🔗

If if the head of $x s$ is smaller than the $i th$ element of $ys,$ then $x s$ is smaller than drop i ys.

head-drop-≺
  : ∀ {xs : List ⌞ A ⌟} {ys : List ⌞ A ⌟}
  → ⦃ _ : Nonempty xs ⦄
  → (i : Fin (length ys))
  → head⁺ xs < (ys ! i)
  → xs ≺ drop (Fin.to-nat i) ys
head-drop-≺ {xs = x ∷ xs} {ys = y ∷ ys} fzero x<ys[i] =
  ≺-∷-head x<ys[i]
head-drop-≺ {xs = x ∷ xs} {ys = y ∷ ys} (fsuc i) x<ys[i] =
  head-drop-≺ i x<ys[i]

A sort of converse is also true: if the $i th$ element of $x s$ is smaller than the head of $ys,$ then drop i xs is smaller than $ys .$

drop-head-≺
  : ∀ (xs : List ⌞ A ⌟) (ys : List ⌞ A ⌟)
  → ⦃ _ : Nonempty ys ⦄
  → (i : Fin (length xs))
  → (xs ! i) < head⁺ ys
  → drop (Fin.to-nat i) xs ≺ ys
drop-head-≺ (x ∷ xs) (y ∷ ys) fzero xs[i]<y =
  ≺-∷-head xs[i]<y
drop-head-≺ (x ∷ xs) (y ∷ ys) (fsuc i) xs[i]<y =
  drop-head-≺ xs (y ∷ ys) i xs[i]<y

Lex orderings and powers🔗

If $x s$ is not a prefix of $ys$ and $x s < ys,$ then $x^{n} < ys .$ Note that this is a general form of ≺-++-extendr.

powers-≺
  : ∀ (xs : List ⌞ A ⌟) (n : Nat) (ys : List ⌞ A ⌟)
  → ¬ (xs ⊑ˡ ys) → xs ≺ ys
  → powers xs n [] ≺ ys
powers-≺ xs zero (y ∷ ys) ¬xs⊑ys xs≺ys = ≺-nil
powers-≺ xs (suc n) (y ∷ ys) ¬xs⊑ys xs≺ys = ≺-++-projl ¬xs⊑ys xs≺ys

What a great lemma!↩︎