General properties of well-quasiorders.

```
module WQO where

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; subst)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; s≤s; z≤n; _<_)
open import Data.Nat.Properties
  using (≤-refl; ≤-trans; <-trans; <-irrefl; m≤n+m; +-monoˡ-<)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂ ; ∃; Σ-syntax; ∃-syntax; ∃₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) renaming ([_,_]′ to case-⊎)
open import Relation.Nullary using (¬_)
open import Data.Unit using (⊤; tt)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Unary using (_∈_; _⊆_)
open import Function using (_∘_; id)
open import Data.Maybe using (Maybe; just; nothing)

open import Miscellaneous

open import Classical
```

Definitions of quasiorder and well-quasiorder.
```
Reflexive : {A : Set} → (A → A → Set) → Set
Reflexive _≼_ = ∀ {x} → x ≼ x

Transitive : {A : Set} → (A → A → Set) → Set
Transitive _≼_ = ∀ {x y z} → x ≼ y → y ≼ z → x ≼ z

record IsQO {A : Set} (_≼_ : A → A → Set) : Set where
  field
    reflexive : Reflexive _≼_ -- (x : A) → x ≼ x
    transitive : Transitive _≼_ -- {x y z : A} → x ≼ y → y ≼ z → x ≼ z

open IsQO

Good : {A : Set} (_≼_ : A → A → Set) → (ℕ → A) → Set
Good _≼_ f = ∃₂ (λ i j → i < j × f i ≼ f j)
```

A sequence is very good if every subsequence of it is good.
```
VeryGood : {A : Set} (_≼_ : A → A → Set) → (ℕ → A) → Set
VeryGood _≼_ f = (r : ℕ → ℕ) → Increasing _<_ r → Good _≼_ (f ∘ r)

veryGood-extensional : {A : Set} {_≼_ : A → A → Set} (f g : ℕ → A)
  → ((n : ℕ) → f n ≡ g n)
  → VeryGood _≼_ f
  ----------------
  → VeryGood _≼_ g
veryGood-extensional {A} {_≼_} f g f≐g f-veryGood r r-increasing = i , j , i<j , grigrj
  where
  h : ∃₂ (λ i j → i < j × f (r i) ≼ f (r j))
  h = f-veryGood r r-increasing
  i = proj₁ h
  j = proj₁ (proj₂ h)
  i<j = proj₁ (proj₂ (proj₂ h))
  frifrj : f (r i) ≼ f (r j)
  frifrj = proj₂ (proj₂ (proj₂ h))
  grigrj : g (r i) ≼ g (r j)
  grigrj = subst (λ z → z ≼ g (r j)) (f≐g (r i)) (subst (λ z → f (r i) ≼ z) (f≐g (r j)) frifrj)

veryGood⇒good : {A : Set} (_≼_ : A → A → Set) (f : ℕ → A) → VeryGood _≼_ f → Good _≼_ f
veryGood⇒good _≼_ f f-veryGood = f-veryGood id id-increasing

subseq-veryGood : {A : Set} (_≼_ : A → A → Set) (f : ℕ → A) (r : ℕ → ℕ)
  → VeryGood _≼_ f
  → Increasing _<_ r
  ----------------------
  → VeryGood _≼_ (f ∘ r)
subseq-veryGood _≼_ f r f-veryGood r-increasing r₁ r₁-increasing
  = f-veryGood (r ∘ r₁) r∘r₁-increasing
  where
  r∘r₁-increasing : Increasing _<_ (r ∘ r₁)
  r∘r₁-increasing = subseq-increasing _<_ r r₁ r-increasing r₁-increasing
```

The following form of reasoning is used repeatedly, but it's often cumbersome to identify P and prove that 
it's closed under subsequence, so I usually won't bother invoking this lemma.
```agda
ClosedUnderSubseq : {A : Set} (P : (ℕ → A) → Set) → Set
ClosedUnderSubseq {A} P = (f : ℕ → A) (r : ℕ → ℕ) → Increasing _<_ r → P f → P (f ∘ r)

lemma-good-veryGood : {A : Set} {_≼_ : A → A → Set} (P : (ℕ → A) → Set)
  → ClosedUnderSubseq P
  → ((f : ℕ → A) → P f → Good _≼_ f)
  → (f : ℕ → A)
  → P f 
  → VeryGood _≼_ f
lemma-good-veryGood {A} P P-closed h f Pf r r-increasing = h (f ∘ r) (P-closed f r r-increasing Pf)

AlmostFull : {A : Set} (_≼_ : A → A → Set) → Set
AlmostFull _≼_ = ∀ f → Good _≼_ f

⇒-almostFull : {A : Set} (_≼₁_ _≼₂_ : A → A → Set)
  → ((x y : A) → (x ≼₁ y) → (x ≼₂ y))
  → AlmostFull _≼₁_
  → AlmostFull _≼₂_
⇒-almostFull _≼₁_ _≼₂_ h ≼₁-almostFull f with ≼₁-almostFull f
... | i , j , i<j , fi≼₁fj = i , j , i<j , h (f i) (f j) fi≼₁fj

record IsWQO {A : Set} (_≼_ : A → A → Set) : Set where
  field
    isQO : IsQO _≼_
    almostFull : AlmostFull _≼_

open IsWQO
```

Some consequences.
```
module _ {A : Set} (_≼_ : A → A → Set) (f : ℕ → A) where
  almostFull-veryGood : AlmostFull _≼_ → VeryGood _≼_ f
  almostFull-veryGood h r r-increasing = h (f ∘ r)

  Nonterminal : ℕ → Set
  Nonterminal m = ∃[ n ] m < n × f m ≼ f n

  Terminal : ℕ → Set
  Terminal m = (n : ℕ) → m < n → ¬ f m ≼ f n

  notTerminal⇒Nonterminal : (m : ℕ) → ¬ (Terminal m) → Nonterminal m
  notTerminal⇒Nonterminal m h = ¬¬-elim (λ k → h (λ n m<n fm≼fn → k (n , m<n , fm≼fn)))

  veryGood⇒∀∞-nonterminal : VeryGood _≼_ f → ∃[ n ] ((x : ℕ) → n < x → Nonterminal x)
  veryGood⇒∀∞-nonterminal h = n , λ x n<x → notTerminal⇒Nonterminal x (λ tx → h₃ (x , n<x , tx))
    where
    ∀∞-nonterminal-aux : Σ[ n ∈ ℕ ] (¬ (Σ[ x ∈ ℕ ] (n < x × Terminal x)))
    ∀∞-nonterminal-aux = ¬∀⟶∃¬ h₁
      where
      h₁ : ¬ ((n : ℕ) → Σ[ x ∈ ℕ ] (n < x × Terminal x))
      h₁ h₂ = r-terminal i (r j) ri<rj gi≼gj
        where
        r : ℕ → ℕ
        r zero = proj₁ (h₂ zero)
        r (suc n) with h₂ (r n)
        ... | x , rn<x , tx = x -- proj₁ (h₂ (r n))
        r-increasing : Increasing _<_ r -- (i j : ℕ) → i < j → r i < r j
        r-increasing i (suc j) i<1+j with ≤-suc i<1+j | h₂ (r j)
        ... | inj₁ i<j  | y , rj<y , ty = <-trans (r-increasing i j i<j) rj<y
        ... | inj₂ refl | y , ri<y , ty = ri<y
        r-terminal : (x : ℕ) → Terminal (r x)
        r-terminal zero = proj₂ (proj₂ (h₂ zero))
        r-terminal (suc x) = proj₂ (proj₂ (h₂ (r x)))
        g : ℕ → A
        g = f ∘ r
        g-good : Good _≼_ g
        g-good = h r r-increasing
        i = proj₁ g-good
        j = proj₁ (proj₂ g-good)
        i<j : i < j
        i<j = proj₁ (proj₂ (proj₂ g-good))
        ri<rj : r i < r j
        ri<rj = r-increasing i j i<j
        gi≼gj : g i ≼ g j
        gi≼gj = proj₂ (proj₂ (proj₂ g-good))
    n = proj₁ ∀∞-nonterminal-aux
    h₃ : ¬ (Σ[ x ∈ ℕ ] (n < x × Terminal x))
    h₃ = proj₂ ∀∞-nonterminal-aux

  veryGood⇒ascendingSubseq : Transitive _≼_ → VeryGood _≼_ f
    → Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × Increasing _≼_ (f ∘ r))
  veryGood⇒ascendingSubseq ≼-transitive f-veryGood
    with veryGood⇒∀∞-nonterminal f-veryGood
  ... | s , s<x⟶ntx = r , r-increasing , f∘r-increasing
    where
    -- s<x⟶ntx : (x : ℕ) → s < x → Nonterminal x
    -- r, r-helper, s<r are mutually recursive
    r : ℕ → ℕ
    r-helper : (n : ℕ) → Nonterminal (r n)
    s<r : (n : ℕ) → s < r n
    r zero = suc s
    r (suc n) = proj₁ (r-helper n)
    r-helper n = s<x⟶ntx (r n) (s<r n)
    s<r zero = ≤-refl
    s<r (suc n) = <-trans (s<r n) (proj₁ (proj₂ (r-helper n)))
    r-increasing-step : (n : ℕ) → r n < r (suc n)
    r-increasing-step n = proj₁ (proj₂ (r-helper n))
    r-increasing : Increasing _<_ r
    r-increasing m (suc n) m<1+n with ≤-suc m<1+n
    ... | inj₁ m<n = <-trans (r-increasing m n m<n) (r-increasing-step n)
    ... | inj₂ refl = r-increasing-step n
    f∘r-increasing-step : (n : ℕ) → f (r n) ≼ f (r (suc n))
    f∘r-increasing-step n = proj₂ (proj₂ (r-helper n))
    f∘r-increasing : Increasing _≼_ (f ∘ r)
    f∘r-increasing m (suc n) m<1+n with ≤-suc m<1+n
    ... | inj₁ m<n = ≼-transitive (f∘r-increasing m n m<n) (f∘r-increasing-step n)
    ... | inj₂ refl = f∘r-increasing-step n

  ∀∞-nonterminal : IsWQO _≼_ → ∃[ n ] ((x : ℕ) → n < x → Nonterminal x)
  ∀∞-nonterminal h = veryGood⇒∀∞-nonterminal (almostFull-veryGood (almostFull h))

  ascendingSubseq : IsWQO _≼_
    → Σ[ r ∈ (ℕ → ℕ) ] (Increasing _<_ r × Increasing _≼_ (f ∘ r))
  ascendingSubseq h =
    veryGood⇒ascendingSubseq (transitive (isQO h)) (almostFull-veryGood (almostFull h))
```

Maybe: maybe we should prove a more general lemma about unions?
```
module M {A : Set} (_≼_ : A → A → Set) where
  _≼′_ : Maybe A → Maybe A → Set
  just x  ≼′ just y  = x ≼ y
  just x  ≼′ nothing = ⊥
  nothing ≼′ just y  = ⊥
  nothing ≼′ nothing = ⊤ -- ??

  maybe-almostFull : AlmostFull _≼_ → AlmostFull _≼′_
  maybe-almostFull ≼-almostFull f = f-good
    where
    Inf = (k : ℕ) → Σ[ l ∈ ℕ ] k < l × f l ≡ nothing
    Cof = Σ[ k ∈ ℕ ] ((l : ℕ) → k < l → f l ≢ nothing)
    h₁ : Inf ⊎ Cof
    h₁ = infinite-or-cofinite-¬ (λ z → f z ≡ nothing)
    f-good : Good _≼′_ f
    f-good with h₁
    ... | inj₁ inf = i , j , i<j , fi≼′fj
      where
      i j : ℕ
      i = proj₁ (inf zero)
      j = proj₁ (inf i) 
      i<j : i < j
      i<j = proj₁ (proj₂ (inf i))
      fi≡nothing : f i ≡ nothing
      fi≡nothing = proj₂ (proj₂ (inf zero))
      fj≡nothing : f j ≡ nothing
      fj≡nothing = proj₂ (proj₂ (inf i))
      fi≼′fj : f i ≼′ f j
      fi≼′fj rewrite fi≡nothing | fj≡nothing = tt
    ... | inj₂ cof = i + suc k , j + suc k , i+1+k<j+1+k , fi+1+k≼′fj+1+k
      where
      k = proj₁ cof
      cof′ : (l : ℕ) → k < l → ∃[ x ] f l ≡ just x
      cof′ l k<l with f l in eq
      ... | just x = x , refl
      ... | nothing = ⊥-elim (proj₂ cof l k<l eq)
      g : (n : ℕ) → ∃[ x ] f (n + suc k) ≡ just x
      g n = cof′ (n + suc k) (m≤n+m (suc k) n)
      f′ : ℕ → A
      f′ n = proj₁ (g n)
      f-f′ : (n : ℕ) → f (n + suc k) ≡ just (f′ n)
      f-f′ n = proj₂ (g n)
      f′-good : Good _≼_ f′
      f′-good = ≼-almostFull f′
      i j : ℕ
      i = proj₁ f′-good
      j = proj₁ (proj₂ f′-good)
      i<j : i < j
      i<j = proj₁ (proj₂ (proj₂ f′-good))
      f′i≼f′j : f′ i ≼ f′ j
      f′i≼f′j = proj₂ (proj₂ (proj₂ f′-good))
      i+1+k<j+1+k : i + suc k < j + suc k
      i+1+k<j+1+k = +-monoˡ-< (suc k) i<j
      fi+1+k≼′fj+1+k : f (i + suc k) ≼′ f (j + suc k)
      fi+1+k≼′fj+1+k rewrite f-f′ i | f-f′ j = f′i≼f′j
```

Dixon's lemma
```
prodSeq : {A B : Set} → (ℕ → A) → (ℕ → B) → (ℕ → A × B)
prodSeq f g n = f n , g n

prodOrder : {A B : Set} → (A → A → Set) → (B → B → Set) → A × B → A × B → Set
prodOrder _≼₁_ _≼₂_ x y = (proj₁ x ≼₁ proj₁ y) × (proj₂ x ≼₂ proj₂ y)

prod-reflexive : {A B : Set} (_≼₁_ : A → A → Set) (_≼₂_ : B → B → Set)
  → Reflexive _≼₁_
  → Reflexive _≼₂_
  → Reflexive (prodOrder _≼₁_ _≼₂_)
prod-reflexive _≼₁_ _≼₂_ h₁ h₂ = h₁ , h₂

prod-transitive : {A B : Set} (_≼₁_ : A → A → Set) (_≼₂_ : B → B → Set)
  → Transitive _≼₁_
  → Transitive _≼₂_
  → Transitive (prodOrder _≼₁_ _≼₂_)
prod-transitive _≼₁_ _≼₂_ h₁ h₂ xy yz = (h₁ (proj₁ xy) (proj₁ yz)) , h₂ (proj₂ xy) (proj₂ yz)

prod-isQO : {A B : Set} (_≼₁_ : A → A → Set) (_≼₂_ : B → B → Set)
  → IsQO _≼₁_
  → IsQO _≼₂_
  ----------------------------
  → IsQO (prodOrder _≼₁_ _≼₂_)

prod-isQO _≼₁_ _≼₂_ h₁ h₂ = 
  record
    { reflexive = prod-reflexive _≼₁_ _≼₂_ (reflexive h₁) (reflexive h₂)
    ; transitive = prod-transitive _≼₁_ _≼₂_ (transitive h₁) (transitive h₂)
    }

prod-veryGood : {A B : Set} {_≼₁_ : A → A → Set} {_≼₂_ : B → B → Set}
  {f : ℕ → A} {g : ℕ → B}
  → Transitive _≼₁_ -- unsatisfactorily lacking symmetry
  → VeryGood _≼₁_ f
  → VeryGood _≼₂_ g
  ----------------------------------------------
  → VeryGood (prodOrder _≼₁_ _≼₂_) (prodSeq f g)
prod-veryGood {_≼₁_ = _≼₁_} {_≼₂_ = _≼₂_} {f = f} {g = g} 
  ≼₁-transitive f-veryGood g-veryGood r r-increasing
  = r₁ i , r₁ j , r₁-increasing i j i<j , ( frr₁i≼₁frr₁j , grr₁i≼₂grr₁j )
  where
  _≼_ = prodOrder _≼₁_ _≼₂_
  f∘r-veryGood : VeryGood _≼₁_ (f ∘ r)
  f∘r-veryGood = subseq-veryGood _≼₁_ f r f-veryGood r-increasing
  f∘r-ascendingSubseq : 
    Σ[ r₁ ∈ (ℕ → ℕ) ] Increasing _<_ r₁ × Increasing _≼₁_ (f ∘ r ∘ r₁)
  f∘r-ascendingSubseq = 
    veryGood⇒ascendingSubseq _≼₁_ (f ∘ r) ≼₁-transitive f∘r-veryGood
  r₁ : ℕ → ℕ
  r₁ = proj₁ f∘r-ascendingSubseq
  r₁-increasing : Increasing _<_ r₁
  r₁-increasing = proj₁ (proj₂ f∘r-ascendingSubseq)
  f∘r∘r₁-increasing : Increasing _≼₁_ (f ∘ r ∘ r₁)
  f∘r∘r₁-increasing = proj₂ (proj₂ f∘r-ascendingSubseq)
  r∘r₁-increasing : Increasing _<_ (r ∘ r₁)
  r∘r₁-increasing = subseq-increasing _<_ r r₁ r-increasing r₁-increasing
  g∘r∘r₁-good : Good _≼₂_ (g ∘ r ∘ r₁)
  g∘r∘r₁-good = g-veryGood (r ∘ r₁) r∘r₁-increasing
  i j : ℕ
  i = proj₁ g∘r∘r₁-good
  j = proj₁ (proj₂ g∘r∘r₁-good)
  i<j : i < j
  i<j = proj₁ (proj₂ (proj₂ g∘r∘r₁-good))
  grr₁i≼₂grr₁j : g (r (r₁ i)) ≼₂ g (r (r₁ j))
  grr₁i≼₂grr₁j = proj₂ (proj₂ (proj₂ g∘r∘r₁-good))
  frr₁i≼₁frr₁j : f (r (r₁ i)) ≼₁ f (r (r₁ j))
  frr₁i≼₁frr₁j = f∘r∘r₁-increasing i j i<j

prod-isWQO : {A B : Set} (_≼₁_ : A → A → Set) (_≼₂_ : B → B → Set)
  → IsWQO _≼₁_
  → IsWQO _≼₂_
  -------------------------------------
  → IsWQO {A × B} (prodOrder _≼₁_ _≼₂_)
prod-isWQO {A} {B} _≼₁_ _≼₂_ h₁ h₂ = 
  record
    { isQO = prod-isQO _≼₁_ _≼₂_ (isQO h₁) (isQO h₂)
    ; almostFull = ≼-almostFull
    }
  where
  _≼_ = prodOrder _≼₁_ _≼₂_
  ≼-almostFull : (f : ℕ → A × B) → Good _≼_ f
  ≼-almostFull f = f₁f₂-good
    where
    f₁ : ℕ → A
    f₁ n = proj₁ (f n)
    f₂ : ℕ → B
    f₂ n = proj₂ (f n)
    f₁-veryGood : VeryGood _≼₁_ f₁
    f₁-veryGood = almostFull-veryGood _≼₁_ f₁ (almostFull h₁)
    f₂-veryGood : VeryGood _≼₂_ f₂
    f₂-veryGood = almostFull-veryGood _≼₂_ f₂ (almostFull h₂)
    f₁f₂-veryGood : VeryGood (prodOrder _≼₁_ _≼₂_) (prodSeq f₁ f₂)
    f₁f₂-veryGood = 
      prod-veryGood {_≼₁_ = _≼₁_} {_≼₂_ = _≼₂_} {f = f₁} {g = f₂}
        (transitive (isQO h₁)) f₁-veryGood f₂-veryGood
    f₁f₂-good : Good (prodOrder _≼₁_ _≼₂_) (prodSeq f₁ f₂)
    f₁f₂-good = veryGood⇒good (prodOrder _≼₁_ _≼₂_) (prodSeq f₁ f₂) f₁f₂-veryGood
```