The minimal bad sequence argument, slightly generalized.
module MinimalBadSeq where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; _≢_; sym; trans; cong; cong-app; subst)
-- open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _∸_; _≤_; s≤s; z≤n; _<_)
open import Data.Nat.Properties
-- Don't use the library version of ≤-<-connex.
using (≤-reflexive; ≤-refl; ≤-trans; <-trans; <-irrefl; <⇒≤; <-transʳ;
≤⇒≯; n∸n≡0; ∸-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 (_∈_; Satisfiable)
open import Function using (_∘_; id)
open import Miscellaneous
open import Classical
open import WQO
private
variable
A : Set
“Induction step” of the construction of MBS.
module MinSeqStep (𝕤 : A → ℕ) (P : (ℕ → A) → Set) (P-nonempty : Satisfiable P) where
𝕤P : (ℕ → ℕ) → Set
𝕤P = (𝕤 ∘_) [ P ] -- 𝕤P g = Σ[ f ∈ (ℕ → A) ] (f ∈ P × 𝕤 ∘ f ≡ g)
𝕤P-nonempty : Satisfiable 𝕤P
𝕤P-nonempty = nonempty-image (𝕤 ∘_) P P-nonempty
record MinSeqAt (n : ℕ) : Set where
field
seq : ℕ → A
member : seq ∈ P
minimal : (g : ℕ → A) → g ∈ P → 𝕤 (seq n) ≤ 𝕤 (g n)
minSeqAt : (n : ℕ) → MinSeqAt n
minSeqAt n = record
{ seq = f
; member = f∈P
; minimal = f-minimal
}
where
l𝕤P : Σ[ f₁ ∈ (ℕ → ℕ) ] (f₁ ∈ 𝕤P × ((g₁ : ℕ → ℕ) → g₁ ∈ 𝕤P → f₁ n ≤ g₁ n))
l𝕤P = leastSeqAt 𝕤P-nonempty n
f₁ = proj₁ l𝕤P
f₁∈𝕤P = proj₁ (proj₂ l𝕤P)
f = proj₁ f₁∈𝕤P
f∈P : f ∈ P
f∈P = proj₁ (proj₂ f₁∈𝕤P)
𝕤∘f≡f₁ : 𝕤 ∘ f ≡ f₁
𝕤∘f≡f₁ = proj₂ (proj₂ f₁∈𝕤P)
f₁-minimal : (g₁ : ℕ → ℕ) → g₁ ∈ 𝕤P → f₁ n ≤ g₁ n
f₁-minimal = proj₂ (proj₂ l𝕤P)
f-minimal : (g : ℕ → A) → g ∈ P → 𝕤 (f n) ≤ 𝕤 (g n)
f-minimal g g∈P rewrite cong-app 𝕤∘f≡f₁ n = f₁-minimal g₁ g₁∈𝕤P
where
g₁ = 𝕤 ∘ g
g₁∈𝕤P : g₁ ∈ 𝕤P
g₁∈𝕤P = member-image (𝕤 ∘_) P g∈P
The constructon of the minimal “bad” sequence is relativized to the
predicate P. We construct the minimal sequence with respect to P, which
is known to be nonempty.
module MBS-helper (𝕤 : A → ℕ) (P : (ℕ → A) → Set) (P-nonempty : Satisfiable P) where
open MinSeqStep 𝕤
P′ : ℕ → (ℕ → A) → Set
P′-nonempty : (n : ℕ) → Satisfiable (P′ n)
mbs-helper : (n : ℕ) → MinSeqAt (P′ n) (P′-nonempty n) n
-- Σ[ f ∈ (ℕ → A) ] f ∈ P′ n × ((g : ℕ → A) → g ∈ P′ n → 𝕤 (f n) ≤ 𝕤 (g n))
mbs-helper-seq : ℕ → ℕ → A
mbs-helper-member : (n : ℕ) → mbs-helper-seq n ∈ P
P′ zero = P
P′ (suc n) g = g ∈ P × AgreeUpTo n (mbs-helper-seq n) g
P′-nonempty 0 = P-nonempty
P′-nonempty (suc n) = mbs-helper-seq n , mbs-helper-member n , agreeUpTo-reflexive n (mbs-helper-seq n)
mbs-helper n = minSeqAt (P′ n) (P′-nonempty n) n
mbs-helper-seq n = MinSeqAt.seq (mbs-helper n)
mbs-helper-member zero = MinSeqAt.member (mbs-helper zero)
mbs-helper-member (suc n) = proj₁ (MinSeqAt.member (mbs-helper (suc n)))
mbs-helper-minimal : (n : ℕ) (g : ℕ → A) → g ∈ P′ n → 𝕤 (mbs-helper-seq n n) ≤ 𝕤 (g n)
mbs-helper-minimal n = MinSeqAt.minimal (mbs-helper n)
mbs-helper-agreeUpTo : (m n : ℕ) → m ≤ n → AgreeUpTo m (mbs-helper-seq m) (mbs-helper-seq n)
mbs-helper-agreeUpTo .zero zero z≤n = agreeUpTo-reflexive zero (mbs-helper-seq zero)
mbs-helper-agreeUpTo m (suc n) m≤1+n with ≤-suc m≤1+n
... | inj₁ m≤n = agreeUpTo-transitive (mbs-helper-agreeUpTo m n m≤n)
(agreeUpTo-≤ (mbs-helper-agreeUpTo-step n) m≤n)
where
mbs-helper-agreeUpTo-step : (n : ℕ)
→ AgreeUpTo n (mbs-helper-seq n) (mbs-helper-seq (suc n))
mbs-helper-agreeUpTo-step n = proj₂ (MinSeqAt.member (mbs-helper (suc n)))
... | inj₂ refl = agreeUpTo-reflexive (suc n) (mbs-helper-seq (suc n))
mbs : ℕ → A
mbs n = mbs-helper-seq n n
In general, the minimal sequence relativized to P need not itself
satisfy P. We need the condition we call “initial segment property” for
the mbs to satisfy P.
mbs-member : InitialSegmentProperty P → mbs ∈ P
mbs-member isp = isp mbs (λ (n : ℕ) →
mbs-helper-seq n ,
mbs-helper-member n ,
λ {m : ℕ} (m≤n : m ≤ n) → mbs-helper-agreeUpTo m n m≤n ≤-refl)
The predicate “bad” is closed under subsequence, as well as satisfying
the initial segment property.
module _ (_≼_ : A → A → Set) where
Bad = ¬_ ∘ (Good _≼_)
subseq-bad : {f : ℕ → A} → Bad f → (r : ℕ → ℕ) → Increasing _<_ r → Bad (f ∘ r)
subseq-bad {f} f-bad r r-increasing (i , j , i<j , fri≼frj) =
f-bad (r i , r j , r-increasing i j i<j , fri≼frj)
Bad-isp : InitialSegmentProperty {A} Bad
Bad-isp f h f-good = contra
where
i j : ℕ
i = proj₁ f-good
j = proj₁ (proj₂ f-good)
i<j : i < j
i<j = proj₁ (proj₂ (proj₂ f-good))
fi≼fj : f i ≼ f j
fi≼fj = proj₂ (proj₂ (proj₂ f-good))
g : ℕ → A
g = proj₁ (h j)
g-bad : Bad g
g-bad = proj₁ (proj₂ (h j))
h₁ : AgreeUpTo j f g
h₁ = proj₂ (proj₂ (h j))
fi≡gi : f i ≡ g i
fi≡gi = h₁ (<⇒≤ i<j)
fj≡gj : f j ≡ g j
fj≡gj = h₁ ≤-refl
gi≼gj : g i ≼ g j
gi≼gj rewrite sym fi≡gi | sym fj≡gj = fi≼fj
contra : ⊥
contra = g-bad (i , j , i<j , gi≼gj)
We restrict attention to sequences that can be obtained from a
subsequence of a given sequence f by taking a “substructure” of each
term in the subsequence. This predicate satisfies the initial segment
property.
module _ {A : Set} (_⊑_ : A → A → Set) where
Sub-⊑-isp : (f : ℕ → A) → InitialSegmentProperty (Sub _⊑_ f)
Sub-⊑-isp f g h = r , r-increasing , r-witness
where
S : ℕ → (ℕ → ℕ) → Set
S n s = Increasing _<_ s × ((m : ℕ) → m ≤ n → g m ⊑ f (s m))
S-nonempty : (n : ℕ) → Satisfiable (S n)
S-nonempty n = s₁ , s₁-increasing , h₃
where
g₁ : ℕ → A
g₁ = proj₁ (h n)
g₁∈Sub-⊑f : g₁ ∈ Sub _⊑_ f
g₁∈Sub-⊑f = proj₁ (proj₂ (h n))
s₁ : ℕ → ℕ
s₁ = proj₁ g₁∈Sub-⊑f
s₁-increasing : Increasing _<_ s₁
s₁-increasing = proj₁ (proj₂ g₁∈Sub-⊑f)
h₁ : (m : ℕ) → g₁ m ⊑ f (s₁ m)
h₁ = proj₂ (proj₂ g₁∈Sub-⊑f)
h₂ : AgreeUpTo n g g₁
h₂ = proj₂ (proj₂ (h n))
h₃ : (m : ℕ) → m ≤ n → g m ⊑ f (s₁ m)
h₃ m m≤n rewrite h₂ m≤n = h₁ m
minS : (n : ℕ) → Σ[ s ∈ (ℕ → ℕ) ] (s ∈ S n × ((s′ : ℕ → ℕ) → s′ ∈ S n → s n ≤ s′ n))
minS n = leastSeqAt (S-nonempty n) n
t : ℕ → ℕ → ℕ
t n = proj₁ (minS n)
tn∈Sn : (n : ℕ) → t n ∈ S n
tn∈Sn n = proj₁ (proj₂ (minS n))
tn-increasing : (n : ℕ) → Increasing _<_ (t n)
tn-increasing n = proj₁ (tn∈Sn n)
tn-witness : (n m : ℕ) → m ≤ n → g m ⊑ f (t n m)
tn-witness n = proj₂ (tn∈Sn n)
m<n⇒tn∈Sm : (n m : ℕ) → m < n → t n ∈ S m
m<n⇒tn∈Sm n m m<n =
tn-increasing n , λ m₁ m₁≤m → proj₂ (tn∈Sn n) m₁ (≤-trans m₁≤m (<⇒≤ m<n))
r : ℕ → ℕ
r n = t n n
r-increasing : Increasing _<_ r
r-increasing m n m<n = <-transʳ tmm≤tnm tnm<tnn
where
tmm≤tnm : t m m ≤ t n m
tmm≤tnm = proj₂ (proj₂ (minS m)) (t n) (m<n⇒tn∈Sm n m m<n)
tnm<tnn : t n m < t n n
tnm<tnn = tn-increasing n m n m<n
r-witness : (n : ℕ) → g n ⊑ f (r n)
r-witness n = tn-witness n n ≤-refl
Sub-⊑-reflexive : Reflexive _⊑_ → (f : ℕ → A) → f ∈ Sub _⊑_ f
Sub-⊑-reflexive ⊑-reflexive f = id , id-increasing , λ n → ⊑-reflexive
Sub-⊑-transitive : Transitive _⊑_ → {f g k : ℕ → A}
→ g ∈ Sub _⊑_ f
→ k ∈ Sub _⊑_ g
-------------
→ k ∈ Sub _⊑_ f
Sub-⊑-transitive ⊑-transitive (r₁ , r₁-increasing , h₁) (r₂ , r₂-increasing , h₂) =
r₁ ∘ r₂ ,
subseq-increasing _<_ r₁ r₂ r₁-increasing r₂-increasing ,
λ n → ⊑-transitive (h₂ n) (h₁ (r₂ n))
The predicate we use is the conjunction of “bad” and the above
predicate. So, given a bad sequence f, we construct the minimal bad
sequence that can be obtained from a subsequence of f by taking
substructures.
module MBS {A : Set} (𝕤 : A → ℕ) (_≼_ : A → A → Set)
(_⊑_ : A → A → Set) (⊑-reflexive : Reflexive _⊑_)
{f : ℕ → A} (f-bad : ¬ Good _≼_ f) where
Bad-Sub-⊑ : (ℕ → A) → Set
Bad-Sub-⊑ = λ (g : ℕ → A) → ¬ Good _≼_ g × Sub _⊑_ f g
Bad-Sub-⊑-nonempty : Satisfiable Bad-Sub-⊑
Bad-Sub-⊑-nonempty = f , f-bad , Sub-⊑-reflexive _⊑_ ⊑-reflexive f
open MBS-helper {A} 𝕤 Bad-Sub-⊑ Bad-Sub-⊑-nonempty public
mbs-bad-sub-⊑-member : mbs ∈ Bad-Sub-⊑
mbs-bad-sub-⊑-member = mbs-member (ISP-closed-∩ (¬_ ∘ (Good _≼_)) (Sub _⊑_ f)
(Bad-isp _≼_) (Sub-⊑-isp _⊑_ f))
mbs-bad : ¬ Good _≼_ mbs
mbs-bad = proj₁ mbs-bad-sub-⊑-member
mbs-sub-⊑ : mbs ∈ Sub _⊑_ f
mbs-sub-⊑ = proj₂ mbs-bad-sub-⊑-member
mbs-bad-sub-⊑-minimal-zero : (g : ℕ → A) → g ∈ Bad-Sub-⊑ → 𝕤 (mbs 0) ≤ 𝕤 (g 0)
mbs-bad-sub-⊑-minimal-zero = mbs-helper-minimal 0
mbs-bad-sub-⊑-minimal-suc : (n : ℕ) (g : ℕ → A)
→ g ∈ Bad-Sub-⊑ → AgreeUpTo n mbs g → 𝕤 (mbs (suc n)) ≤ 𝕤 (g (suc n))
mbs-bad-sub-⊑-minimal-suc n g h₁ h₂ = mbs-helper-minimal (suc n) g (h₁ , h)
where
h : AgreeUpTo n (mbs-helper-seq n) g
h {m} m≤n = trans (sym (mbs-helper-agreeUpTo m n m≤n ≤-refl)) (h₂ m≤n)
A general form of the minimal bad sequence argument. If mbs is the
minimal bad sequence (with respect to our predicate), then any sequence
that can be obtained by taking a “proper” substructure of each term of a
subsequence of mbs must be good, provided that the binary relation ≼ in
question is “monotone” on the right argument with respect to the
substructure relation ⊑.
_⊏_ : A → A → Set
x ⊏ y = x ⊑ y × x ≢ y
⊏⇒⊑ : (x y : A) → x ⊏ y → x ⊑ y
⊏⇒⊑ x y (x⊑y , x≢y) = x⊑y
module Sub-⊑-⊏
(⊏-𝕤-< : {x y : A} → x ⊏ y → 𝕤 x < 𝕤 y)
(≼-⊑-≼ : {x y z : A} → x ≼ y → y ⊑ z → x ≼ z)
(⊑-transitive : Transitive _⊑_)
where
⊏-transitive : {x y z : A} → x ⊏ y → y ⊏ z → x ⊏ z
⊏-transitive {x} {y} {z} x⊏y@(x⊑y , x≢y) y⊏z@(y⊑z , y≢z) =
⊑-transitive x⊑y y⊑z ,
λ x≡z → <-irrefl (cong 𝕤 x≡z) (<-trans (⊏-𝕤-< x⊏y) (⊏-𝕤-< y⊏z))
Sub-⊑-⊏-0 : (ℕ → A) → (ℕ → A) → Set
Sub-⊑-⊏-0 k g =
Σ[ r ∈ (ℕ → ℕ) ] Increasing _<_ r × ((n : ℕ) → g n ⊑ k (r n)) × g 0 ⊏ k (r 0)
Sub-⊑-⊏-0⇒Sub-⊑ : (k g : ℕ → A) → Sub-⊑-⊏-0 k g → Sub _⊑_ k g
Sub-⊑-⊏-0⇒Sub-⊑ k g (r , r-increasing , hn , h0) = r , r-increasing , hn
Sub-⊑-⊏-0-mbs⇒Good : (g : ℕ → A) → g ∈ Sub-⊑-⊏-0 mbs → Good _≼_ g
Sub-⊑-⊏-0-mbs⇒Good g (r , r-increasing , hn , h0) = g-good
where
g∈Sub-⊑ : g ∈ Sub _⊑_ mbs
g∈Sub-⊑ = (r , r-increasing , hn)
g-good : Good _≼_ g
g-good with r 0 in eq
... | zero = ¬¬-elim not-g-bad
where
not-g-bad : ¬ ¬ Good _≼_ g
not-g-bad g-bad = ≤⇒≯ h≤ h>
where
h≤ : 𝕤 (mbs 0) ≤ 𝕤 (g 0)
h≤ = mbs-bad-sub-⊑-minimal-zero g
(g-bad ,
Sub-⊑-transitive _⊑_ ⊑-transitive {f} {mbs} {g}
(proj₂ mbs-bad-sub-⊑-member)
g∈Sub-⊑)
h> : 𝕤 (g 0) < 𝕤 (mbs 0)
h> = ⊏-𝕤-< h0
... | suc p = i ∸ (suc p) , j ∸ (suc p) , i∸1+p<j∸1+p , gi∸1+p≼gj∸1+p
where
g′ = switch′ mbs (λ n → g (n ∸ (suc p))) p
g′sucp≡g0 : g′ (suc p) ≡ g 0
g′sucp≡g0 rewrite ≤-<-connex-> (suc p) p (s≤s ≤-refl) | n∸n≡0 (suc p) = refl
r′ = switch′ id (λ n → r (n ∸ (suc p))) p
r′-≤ : (n : ℕ) → n ≤ p → r′ n ≡ n
r′-≤ = switch′-≤ id (λ n → r (n ∸ (suc p))) p
-- r′-> : (n : ℕ) → p < n → r′ n ≡ r (n ∸ (suc p)) -- not used
-- r′-> = switch′-> id (λ n → r (n ∸ (suc p))) p
r′-increasing : Increasing _<_ r′
r′-increasing m n m<n with ≤-<-connex m p | ≤-<-connex n p
... | inj₁ m≤p | inj₁ n≤p = m<n
... | inj₁ m≤p | inj₂ n>p =
≤-trans (s≤s m≤p)
(≤-trans (≤-reflexive (sym eq))
(increasing-≤ r r-increasing 0 (n ∸ (suc p)) z≤n))
... | inj₂ m>p | inj₁ n≤p = ⊥-elim (≤⇒≯ (<⇒≤ (<-transʳ n≤p m>p)) m<n)
... | inj₂ m>p | inj₂ n>p =
r-increasing (m ∸ (suc p)) (n ∸ (suc p)) (∸-monoˡ-< m<n m>p)
g′-≤ : (n : ℕ) → n ≤ p → g′ n ≡ mbs n
g′-≤ = switch′-≤ mbs (λ n → g (n ∸ (suc p))) p
g′-> : (n : ℕ) → p < n → g′ n ≡ g (n ∸ (suc p))
g′-> = switch′-> mbs (λ n → g (n ∸ suc p)) p
h₁ : AgreeUpTo p mbs g′
h₁ = agreeUpTo-symmetric p g′ mbs (λ {n : ℕ} → g′-≤ n)
h₂ : (n : ℕ) → g′ n ⊑ mbs (r′ n)
h₂ n with ≤-<-connex n p
... | inj₁ n≤p = ⊑-reflexive
... | inj₂ n>p = hn (n ∸ (suc p))
g′∈Sub-⊑ : g′ ∈ Sub _⊑_ mbs
g′∈Sub-⊑ = r′ , r′-increasing , h₂
not-g′-bad : ¬ ¬ Good _≼_ g′
not-g′-bad g′-bad = ≤⇒≯ h≤ h>
where
h≤ : 𝕤 (mbs (suc p)) ≤ 𝕤 (g′ (suc p))
h≤ = mbs-bad-sub-⊑-minimal-suc p g′
(g′-bad ,
Sub-⊑-transitive _⊑_ ⊑-transitive {f} {mbs} {g′}
(proj₂ mbs-bad-sub-⊑-member) g′∈Sub-⊑)
h₁
h> : 𝕤 (g′ (suc p)) < 𝕤 (mbs (suc p))
h> rewrite g′sucp≡g0 | eq = ⊏-𝕤-< h0
g′-good : Good _≼_ g′
g′-good = ¬¬-elim not-g′-bad
i j : ℕ
i = proj₁ g′-good
j = proj₁ (proj₂ g′-good)
i<j : i < j
i<j = proj₁ (proj₂ (proj₂ g′-good))
g′i≼g′j : g′ i ≼ g′ j
g′i≼g′j = proj₂ (proj₂ (proj₂ g′-good))
p<i : p < i
p<i = case-⊎ (λ i≤p → ⊥-elim (¬i≤p i≤p))
(λ i>p → i>p)
(≤-<-connex i p)
where
¬i≤p : i ≤ p → ⊥
¬i≤p i≤p =
mbs-bad (r′ i , r′ j , r′-increasing i j i<j , mbsr′i≼mbsr′j)
where
mbsr′i≼mbsr′j : mbs (r′ i) ≼ mbs (r′ j)
mbsr′i≼mbsr′j = subst (λ z → mbs z ≼ mbs (r′ j)) (sym (r′-≤ i i≤p))
(subst (_≼ mbs (r′ j)) (g′-≤ i i≤p) (≼-⊑-≼ g′i≼g′j (h₂ j)))
p<j : p < j
p<j = <-trans p<i i<j
gi∸1+p≼gj∸1+p : g (i ∸ (suc p)) ≼ g (j ∸ (suc p))
gi∸1+p≼gj∸1+p =
subst (_≼ g (j ∸ (suc p))) (g′-> i p<i) (subst (g′ i ≼_) (g′-> j p<j) g′i≼g′j)
i∸1+p<j∸1+p : i ∸ (suc p) < j ∸ (suc p)
i∸1+p<j∸1+p = ∸-monoˡ-< i<j p<i
Sub-⊏⇒Sub-⊑ : (g k : ℕ → A) → k ∈ Sub _⊏_ g → k ∈ Sub _⊑_ g
Sub-⊏⇒Sub-⊑ g k h = Sub-mono _⊏_ _⊑_ g ⊏⇒⊑ k h
Sub-⊏⇒Sub-⊑-⊏-0 : (g k : ℕ → A) → k ∈ Sub _⊏_ g → k ∈ Sub-⊑-⊏-0 g
Sub-⊏⇒Sub-⊑-⊏-0 g k (r , r-increasing , h) =
r , r-increasing , (λ n → ⊏⇒⊑ (k n) (g (r n)) (h n)) , h 0
Sub-⊏-transitive : {d g k : ℕ → A} → g ∈ Sub _⊏_ d → k ∈ Sub _⊏_ g → k ∈ Sub _⊏_ d
Sub-⊏-transitive {d} {g} {k} = Sub-⊑-transitive _⊏_ ⊏-transitive {d} {g} {k}
Sub-⊏-mbs⇒VeryGood : (g : ℕ → A) → g ∈ Sub _⊏_ mbs → VeryGood _≼_ g
Sub-⊏-mbs⇒VeryGood g (s , s-increasing , h) r r-increasing =
Sub-⊑-⊏-0-mbs⇒Good (g ∘ r)
(s ∘ r ,
subseq-increasing _<_ s r s-increasing r-increasing ,
(λ n → ⊏⇒⊑ (g (r n)) (mbs (s (r n))) (h (r n))) ,
h (r 0))