A proof of Higman’s lemma about finite sequences.
module Higman 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≤1+n) 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.List using (List; []; _∷_; _++_; length) open import Miscellaneous open import Classical open import WQO open import MinimalBadSeqSuffix relation, etc.
private variable
A B : Set
data _⊑_ : List A → List A → Set where
⊑-refl : {xs : List A} → xs ⊑ xs
_∷ʳ_ : {xs ys : List A} (y : A) → xs ⊑ ys → xs ⊑ (y ∷ ys)
⊑-reflexive : Reflexive (_⊑_ {A}) -- {xs : List A} → xs ⊑ xs
⊑-reflexive = ⊑-refl
⊑-transitive : {xs ys zs : List A} → xs ⊑ ys → ys ⊑ zs → xs ⊑ zs
⊑-transitive xs⊑ys ⊑-refl = xs⊑ys
⊑-transitive xs⊑ys (z ∷ʳ ys⊑zs) = z ∷ʳ (⊑-transitive xs⊑ys ys⊑zs)
⊑-length-≤ : {xs ys : List A} → xs ⊑ ys → length xs ≤ length ys
⊑-length-≤ ⊑-refl = ≤-refl
⊑-length-≤ (y ∷ʳ xs⊑ys) = m≤n⇒m≤1+n (⊑-length-≤ xs⊑ys)
⊏-length-< : {xs ys : List A} → (xs ⊑ ys × xs ≢ ys) → length xs < length ys
⊏-length-< (⊑-refl , xs≢xs) = ⊥-elim (xs≢xs refl)
⊏-length-< ((y ∷ʳ xs⊑ys) , xs≢ys) = s≤s (⊑-length-≤ xs⊑ys)
elem-⊑-elem : (x : A) (xs ys : List A) → x elem xs → xs ⊑ ys → x elem ys
elem-⊑-elem x xs .xs [x]elem[xs] ⊑-refl = [x]elem[xs]
elem-⊑-elem x xs (y ∷ ys) [x]elem[xs] (y ∷ʳ xs⊑ys) =
there (elem-⊑-elem x xs ys [x]elem[xs] xs⊑ys)
Sub-⊑-Sub-elem : (f g : ℕ → List A) (k : ℕ → A)
→ g ∈ Sub _⊑_ f
→ k ∈ Sub _elem_ g
----------------
→ k ∈ Sub _elem_ f
Sub-⊑-Sub-elem f g k (r , r-increasing , h₁) (s , s-increasing , h₂) =
r ∘ s ,
(subseq-increasing _<_ r s r-increasing s-increasing) ,
λ n → elem-⊑-elem (k n) (g (s n)) (f (r (s n))) (h₂ n) (h₁ (s n))
Subseq-mono : ((ℕ → B) → (ℕ → A) → Set) → Set
Subseq-mono P = ∀ f (r : ℕ → ℕ) (r-increasing : Increasing _<_ r)
→ P (f ∘ r) ⊆ P f
Sub-Sub-elem : Subseq-mono {B = List A} (Sub _elem_)
Sub-Sub-elem f r r-increasing (r₁ , r₁-increasing , h) =
r ∘ r₁ , (subseq-increasing _<_ r r₁ r-increasing r₁-increasing) , (λ n → h n)
The definition of the embedding relation.
The following definition from Data.List.Relation.Binary.Sublist.Heterogeneous.Core could be used instead.
data Sublist : REL (List A) (List B) (a ⊔ b ⊔ r) where
[] : Sublist [] []
_∷ʳ_ : ∀ {xs ys} → ∀ y → Sublist xs ys → Sublist xs (y ∷ ys)
_∷_ : ∀ {x xs y ys} → R x y → Sublist xs ys → Sublist (x ∷ xs) (y ∷ ys)module _ (_≼_ : A → A → Set) where
infixr 5 _∷_ _∷ʳ_
data Embedding : List A → List A → Set where
[] : Embedding [] []
_∷ʳ_ : ∀ {xs ys} → ∀ y → Embedding xs ys → Embedding xs (y ∷ ys)
_∷_ : ∀ {x xs y ys} → x ≼ y → Embedding xs ys → Embedding (x ∷ xs) (y ∷ ys)
embedding-reflexive : Reflexive _≼_ → Reflexive Embedding
embedding-reflexive h {[]} = []
embedding-reflexive h {x ∷ xs} = h ∷ embedding-reflexive h
embedding-transitive : Transitive _≼_ → Transitive Embedding
embedding-transitive h xsys [] with xsys
... | [] = []
embedding-transitive h xsys (y ∷ʳ yszs) = y ∷ʳ embedding-transitive h xsys yszs
embedding-transitive h (_ ∷ʳ xsys) (_ ∷ yszs) = _ ∷ʳ embedding-transitive h xsys yszs
embedding-transitive h (x≼y ∷ xsys) (y≼z ∷ yszs) = h x≼y y≼z ∷ embedding-transitive h xsys yszs
[]-Embedding : ∀ xs → Embedding [] xs
[]-Embedding [] = []
[]-Embedding (x ∷ xs) = x ∷ʳ []-Embedding xs
embedding-⊑-embedding : ∀ {xs ys zs} → Embedding xs ys → ys ⊑ zs → Embedding xs zs
embedding-⊑-embedding h ⊑-refl = h
embedding-⊑-embedding h (y ∷ʳ ys⊑zs) = y ∷ʳ embedding-⊑-embedding h ys⊑zs
elem-embedding : ∀ {x xs ys} → x elem xs → Embedding xs ys → ∃[ y ] y elem ys × x ≼ y
elem-embedding h (y ∷ʳ h₁) with elem-embedding h h₁
... | z , h₂ , x≼z = z , there h₂ , x≼z
elem-embedding here (_∷_ {y = y} h₁ h₂) = y , here , h₁
elem-embedding (there h) (h₁ ∷ h₂) with elem-embedding h h₂
... | z , h₃ , x≼z = z , there h₃ , x≼z
tail-⊏ : {x : A} {xs : List A} → xs ⊑ (x ∷ xs) × xs ≢ x ∷ xs
tail-⊏ {x} {xs} = x ∷ʳ ⊑-refl , λ ()
-- ++-Embedding : ∀ {xs ys us vs}
-- → Embedding xs ys
-- → Embedding us vs
-- ---------------------------------
-- → Embedding (xs ++ us) (ys ++ vs)
-- ++-Embedding [] h₂ = h₂
-- ++-Embedding (y ∷ʳ h₁) h₂ = y ∷ʳ ++-Embedding h₁ h₂
-- ++-Embedding (xy ∷ h₁) h₂ = xy ∷ ++-Embedding h₁ h₂
embedding-isQO : IsQO _≼_ → IsQO Embedding
embedding-isQO h =
record
{ reflexive = embedding-reflexive (IsQO.reflexive h)
; transitive = embedding-transitive (IsQO.transitive h)
}
sub-elem-veryGood-good : (f : ℕ → List A)
→ ((g : ℕ → A) → g ∈ Sub _elem_ f → VeryGood _≼_ g)
→ Good Embedding f
sub-elem-veryGood-good f h = ¬¬-elim not-f-bad
where
not-f-bad : ¬ ¬ Good Embedding f
not-f-bad f-bad = contra
where
open MBS {List A} length Embedding _⊑_ ⊑-reflexive {f} f-bad
contra : ⊥
contra = case-⊎ h₁ h₂ (em {∃[ i ] mbs i ≡ []})
where
h₁ : ∃[ i ] mbs i ≡ [] → ⊥
h₁ (i , mbsi≡[]) =
mbs-bad (i , suc i , ≤-refl ,
subst (λ z → Embedding z (mbs (suc i)))
(sym mbsi≡[])
([]-Embedding (mbs (suc i))))
h₂ : ¬ (∃[ i ] mbs i ≡ []) → ⊥
h₂ ¬∃i = mbs-bad (i , j , i<j , emb-mbsi-mbsj)
where
h₃ : (i : ℕ) → mbs i ≢ []
h₃ i mbsi≡[] = ¬∃i (i , mbsi≡[])
h₄ : (i : ℕ) → ∃₂ (λ x xs → mbs i ≡ x ∷ xs)
h₄ i with mbs i in eq
... | [] = ⊥-elim (h₃ i eq)
... | x ∷ xs = x , xs , refl
g₁ : ℕ → A
g₁ n = proj₁ (h₄ n)
g₂ : ℕ → List A
g₂ n = proj₁ (proj₂ (h₄ n))
mbs≡g₁∷g₂ : (n : ℕ) → mbs n ≡ g₁ n ∷ g₂ n
mbs≡g₁∷g₂ n = proj₂ (proj₂ (h₄ n))
g₁∈Sub-elem-mbs : g₁ ∈ Sub _elem_ mbs
g₁∈Sub-elem-mbs = id , id-increasing , h₅
where
h₅ : (n : ℕ) → g₁ n elem mbs n
h₅ n = subst (λ z → (proj₁ (h₄ n)) elem z) (sym (mbs≡g₁∷g₂ n))
(here {x = proj₁ (h₄ n)} {xs = proj₁ (proj₂ (h₄ n))})
g₁∈Sub-elem-f : g₁ ∈ Sub _elem_ f
g₁∈Sub-elem-f = Sub-⊑-Sub-elem f mbs g₁ mbs-sub-⊑ g₁∈Sub-elem-mbs
g₁-veryGood : VeryGood _≼_ g₁
g₁-veryGood = h g₁ g₁∈Sub-elem-f
open Sub-⊑-⊏ ⊏-length-< embedding-⊑-embedding ⊑-transitive
g₂∈Sub-⊏-mbs : g₂ ∈ Sub _⊏_ mbs
g₂∈Sub-⊏-mbs =
id , id-increasing ,
λ n → subst (g₂ n ⊏_) (sym (mbs≡g₁∷g₂ n)) (tail-⊏ {x = g₁ n} {xs = g₂ n})
g₂-veryGood : VeryGood Embedding g₂
g₂-veryGood = Sub-⊏-mbs⇒VeryGood g₂ g₂∈Sub-⊏-mbs
g₁g₂-veryGood : VeryGood (prodOrder _≼_ Embedding) (λ n → g₁ n , g₂ n)
g₁g₂-veryGood =
prod-veryGood {A = A} {B = List A} {_≼₁_ = _≼_} {_≼₂_ = Embedding} {g₁} {g₂}
g₁-veryGood g₂-veryGood
g₁g₂-good : Good (prodOrder _≼_ Embedding) (prodSeq g₁ g₂)
g₁g₂-good = veryGood⇒good (prodOrder _≼_ Embedding) (λ n → g₁ n , g₂ n) g₁g₂-veryGood
i j : ℕ
i = proj₁ g₁g₂-good
j = proj₁ (proj₂ g₁g₂-good)
i<j : i < j
i<j = proj₁ (proj₂ (proj₂ g₁g₂-good))
g₁i≼g₁j : g₁ i ≼ g₁ j
g₁i≼g₁j = proj₁ (proj₂ (proj₂ (proj₂ g₁g₂-good)))
emb-g₂i-g₂j : Embedding (g₂ i) (g₂ j)
emb-g₂i-g₂j = proj₂ (proj₂ (proj₂ (proj₂ g₁g₂-good)))
emb-g₁ig₂i-g₁jg₂j : Embedding (g₁ i ∷ g₂ i) (g₁ j ∷ g₂ j)
emb-g₁ig₂i-g₁jg₂j = g₁i≼g₁j ∷ emb-g₂i-g₂j
emb-mbsi-mbsj : Embedding (mbs i) (mbs j)
emb-mbsi-mbsj =
subst (λ z → Embedding z (mbs j)) (sym (mbs≡g₁∷g₂ i))
(subst (Embedding (g₁ i ∷ g₂ i)) (sym (mbs≡g₁∷g₂ j)) emb-g₁ig₂i-g₁jg₂j)
sub-elem-veryGood-veryGood : (f : ℕ → List A)
→ ((g : ℕ → A) → g ∈ Sub _elem_ f → VeryGood _≼_ g)
→ VeryGood Embedding f
sub-elem-veryGood-veryGood f h =
lemma-good-veryGood {A = List A} {_≼_ = Embedding} P P-closed sub-elem-veryGood-good f h
where
P : (ℕ → List A) → Set
P z = (g : ℕ → A) → g ∈ Sub _elem_ z → VeryGood _≼_ g
P-closed : ClosedUnderSubseq P
P-closed f r r-increasing Pf g g∈Sub-elem-f∘r = Pf g (Sub-Sub-elem f r r-increasing g∈Sub-elem-f∘r)
embedding-isWQO : IsWQO _≼_ → IsWQO Embedding
embedding-isWQO ≼-isWQO =
record
{ isQO = embedding-isQO (IsWQO.isQO ≼-isWQO)
; almostFull = embedding-almostFull
}
where
embedding-almostFull : (f : ℕ → List A) → Good Embedding f
embedding-almostFull f =
sub-elem-veryGood-good f (λ g _ → almostFull-veryGood _≼_ g (IsWQO.almostFull ≼-isWQO))