Agda大序数(2) 良构序数

交流Q群: 893531731
目录: NonWellFormed.html
本文源码: WellFormed.lagda.md
高亮渲染: WellFormed.html

{-# OPTIONS --without-K --safe #-}
{-# OPTIONS --overlapping-instances #-}

module NonWellFormed.WellFormed where

前置

本章在内容上延续上一章.

open import NonWellFormed.Ordinal
open NonWellFormed.Ordinal.≤-Reasoning

标准库依赖大部分都在上一章出现过. 注意 Agda 有构造子重载, ℕ 的 zero 和 suc 与 Ord 的同名, 但只要类型明确就没有问题. _↩︎_ 表示存在左逆, 其强度介于等价和同构之间. MonoSequence₁ 是函数对序关系的单调性.

open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt)
open import Data.Nat as ℕ using (ℕ; zero; suc; z≤n)
open import Data.Nat.Properties as ℕ using (m≤n⇒m<n∨m≡n)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂; ∃-syntax)
open import Function using (_∘_; _↩_; it)
open import Relation.Binary.Definitions using (Monotonic₁)
open import Relation.Binary.PropositionalEquality as Eq
  using (_≡_; _≢_; refl; sym; cong; subst)

良构

我们说序列 f : ℕ → Ord 单调, 如果 f 保持 ℕ.< 到 Ord.<.

monoSequence : (ℕ → Ord) → Set
monoSequence = Monotonic₁ ℕ._<_ _<_

由于要作为 instance参数, 形式上做了一层 record 封装.

record MonoSequence (f : ℕ → Ord) : Set where
  constructor wrap
  field unwrap : monoSequence f

fm<fn : ∀ {f} → ⦃ MonoSequence f ⦄ → monoSequence f
fm<fn = MonoSequence.unwrap it

由单调序列的极限构成的序数我们称为良构序数. 注意这是递归定义, 序列的每一项也要求良构. 平凡地, 零以及良构序数的后继也是良构序数.

WellFormed : Ord → Set
WellFormed zero    = ⊤
WellFormed (suc α) = WellFormed α
WellFormed (lim f) = (∀ {n} → WellFormed (f n)) × MonoSequence f

以下 instance 用于从良构极限序数推出其序列每一项良构以及序列单调.

instance
  wf⇒wf : ∀ {f} → ⦃ WellFormed (lim f) ⦄ → ∀ {n} → WellFormed (f n)
  wf⇒wf ⦃ wf ⦄ = proj₁ wf

  wf⇒mono : ∀ {f} → ⦃ WellFormed (lim f) ⦄ → MonoSequence f
  wf⇒mono ⦃ wf ⦄ = proj₂ wf

有限序数与 `ω`

我们看几个简单的例子. 把 ℕ 嵌入到 Ord 可以得到有限序数 ⌜n⌝.

⌜_⌝ : ℕ → Ord
⌜ zero ⌝ = zero
⌜ suc n ⌝ = suc ⌜ n ⌝

定义 ω 为嵌入函数 ⌜_⌝ 的极限.

ω : Ord
ω = lim ⌜_⌝

简单的归纳法即可证明任意有限序数良构.

⌜_⌝-wellFormed : ∀ n → WellFormed ⌜ n ⌝
⌜ zero ⌝-wellFormed  = tt
⌜ suc n ⌝-wellFormed = ⌜ n ⌝-wellFormed

引理 ⌜_⌝ 是单调的.
证明即证 m < n 蕴含 ⌜m⌝ < ⌜n⌝. 只需考虑 n 是后继的情况, 即 m < suc n, 拆开分别讨论 m < n 和 m = n 并用归纳假设即可. ∎

⌜⌝-monoSequence : MonoSequence ⌜_⌝
⌜⌝-monoSequence = wrap mono where
  mono : monoSequence ⌜_⌝
  mono {m} {suc n} (ℕ.s≤s m≤n) with (m≤n⇒m<n∨m≡n m≤n)
  ... | inj₁ m<n  = begin-strict ⌜ m ⌝ <⟨ mono m<n ⟩ ⌜ n ⌝ <⟨ <s ⟩ suc ⌜ n ⌝ ∎
  ... | inj₂ refl = begin-strict ⌜ m ⌝ <⟨ <s ⟩ suc ⌜ m ⌝ ∎

以上两条引理说明 ω 是良构序数.

ω-wellFormed : WellFormed ω
ω-wellFormed = (λ {n} → ⌜ n ⌝-wellFormed) , ⌜⌝-monoSequence

`ω` 的性质

引理 ω 大于任意有限序数.

instance
  n≤ω : ∀ {n} → ⌜ n ⌝ ≤ ω
  n≤ω = f≤l

引理 ω 严格大于任意有限序数.

z<ω : zero < ω
z<ω = <-≤-trans z<s (n≤ω {1})

s<ω : ∀ {α} → α < ω → suc α < ω
s<ω {α} ((n , d) , ≤) = (suc n , inj₁ tt) , ≤-trans (s≤s ≤) s∸≤

instance
  n<ω : ∀ {n} → ⌜ n ⌝ < ω
  n<ω {zero}  = z<ω
  n<ω {suc n} = s<ω n<ω

以下引理将 monoSequence 的 f m < f n 结论特化到 f n < f (suc n), 因为它在接下来的证明中经常用到.

fn<fsn : ∀ {f n} → ⦃ MonoSequence f ⦄ → f n < f (suc n)
fn<fsn ⦃ wrap mono ⦄ = mono (ℕ.s≤s ℕ.≤-refl)

引理单调序列的第 n 项不会小于 n 自身.

⌜n⌝≤fn : ∀ {f n} → ⦃ MonoSequence f ⦄ → ⌜ n ⌝ ≤ f n
⌜n⌝≤fn {f} {zero}  = z≤
⌜n⌝≤fn {f} {suc n} = begin
  suc ⌜ n ⌝          ≤⟨ s≤s ⌜n⌝≤fn ⟩
  suc (f n)          ≤⟨ <⇒s≤ fn<fsn ⟩
  f (suc n)          ∎

我们称单调序列的极限为单调极限序数, 它比良构极限序数更宽泛, 但足以证明一些良好的性质. 如:

引理 ω 是最小的单调极限序数.

ω≤l : ∀ {f} → ⦃ MonoSequence f ⦄ → ω ≤ lim f
ω≤l = l≤ λ n → ≤f⇒≤l ⌜n⌝≤fn

等价性

引理 ⌜_⌝ 是自然数到良构序数的单射.

⌜⌝-injective : ∀ {m n} → ⌜ m ⌝ ≡ ⌜ n ⌝ → m ≡ n
⌜⌝-injective {zero}  {zero}  eq = refl
⌜⌝-injective {suc m} {suc n} eq = cong suc (⌜⌝-injective (suc-injective eq))

引理小于 ω 的良构序数被 ⌜_⌝ 满射.

⌜⌝-surjective : ∀ {α} → ⦃ WellFormed α ⦄ → α < ω → ∃[ n ] α ≡ ⌜ n ⌝
⌜⌝-surjective {zero} _ = 0 , refl
⌜⌝-surjective {suc α} s<ω with ⌜⌝-surjective (<-trans <s s<ω)
... | n , refl = suc n , refl
⌜⌝-surjective {lim f} l<ω = ⊥-elim (<⇒≱ l<ω ω≤l)

推论小于 ω 的良构序数与自然数等价.

∃[<ω]wf↩ℕ : (∃[ α ] α < ω × WellFormed α) ↩ ℕ
∃[<ω]wf↩ℕ = record
  { to        = λ (α , <ω , wf) → proj₁ (⌜⌝-surjective ⦃ wf ⦄ <ω)
  ; from      = λ n → ⌜ n ⌝ , n<ω , ⌜ n ⌝-wellFormed
  ; to-cong   = λ{ refl → refl }
  ; from-cong = λ{ refl → refl }
  ; inverseˡ  = λ n → ⌜⌝-injective (sym (proj₂ (⌜⌝-surjective ⦃ ⌜ n ⌝-wellFormed ⦄ n<ω)))
  }

单调极限序数的性质

引理任意单调极限序数严格大于零.

z<l : ∀ {f} → ⦃ MonoSequence f ⦄ → zero < lim f
z<l = <-≤-trans z<ω ω≤l

f<l 是上一章 f≤l 的 _<_ 版, 它要求 f 单调.

f<l : ∀ {f n} → ⦃ MonoSequence f ⦄ → f n < lim f
f<l = <-≤-trans fn<fsn f≤l

引理单调序列在其极限内有任意大的项.
证明

对于零, 我们有 f 1 大于它.
对于后继序数 suc α, 由归纳假设我们有 f n 大于 α, 由传递性有 f (suc n) 大于 suc α.
对于极限序数 lim g, 存在 f n 大于 lim g. ∎

∃[n]<fn : ∀ {α f} → ⦃ MonoSequence f ⦄ → α < lim f → ∃[ n ] α < f n
∃[n]<fn {zero} {f} _ = 1 , ≤-<-trans z≤ fn<fsn
∃[n]<fn {suc α} {f} s<l with ∃[n]<fn (<-trans <s s<l)
... | n , <f = suc n , (begin-strict
  suc α                 ≤⟨ <⇒s≤ <f ⟩
  f n                   <⟨ fn<fsn ⟩
  f (suc n)             ∎)
∃[n]<fn {lim g} ((n , d) , l<f) = n , d , l<f

推论两个单调极限序数的序关系可以反演到它们的序列项.
证明由 lim f ≤ lim g 有 f n < f (suc n) ≤ lim g, 套入上一条即得. ∎

module _ {f g} ⦃ mf : MonoSequence f ⦄ ⦃ mg : MonoSequence g ⦄ where
  ∃[m]fn<gm : lim f ≤ lim g → ∀ n → ∃[ m ] f n < g m
  ∃[m]fn<gm (l≤ fn≤l) n = ∃[n]<fn (begin-strict
    f n                            <⟨ fn<fsn ⟩
    f (suc n)                      ≤⟨ fn≤l (suc n) ⟩
    lim g                          ∎)

推论可以将 s<ω 的结论一般化到任意单调极限序数.
证明由 ∃[n]<fn, 存在 n 使得 α < f n, 即 suc α ≤ f n, 又 f n < f (suc n) < lim f, 由传递性即证. ∎

<l⇒s<l : ∀ {α f} → ⦃ MonoSequence f ⦄ → α < lim f → suc α < lim f
<l⇒s<l {α} {f} ⦃ mono ⦄ < with ∃[n]<fn <
... | n , <f = begin-strict suc α ≤⟨ <⇒s≤ <f ⟩ f n <⟨ f<l ⟩ lim f ∎

引理上一条的逆否命题成立.
证明与 ∃[m]fn<gm 类似的思路. ∎

l≤s⇒l≤ : ∀ {f α} → ⦃ MonoSequence f ⦄ → lim f ≤ suc α → lim f ≤ α
l≤s⇒l≤ {f} {α} ⦃ mono ⦄ (l≤ fn≤s) = l≤ λ n → <s⇒≤ (begin-strict
  f n       <⟨ fn<fsn ⟩
  f (suc n) ≤⟨ fn≤s (suc n) ⟩
  suc α     ∎)

推论后继无限序数的直接前驱也是无限序数.
证明这是上一条的直接推论. ∎

ω≤s⇒ω≤ : ∀ {α} → ω ≤ suc α → ω ≤ α
ω≤s⇒ω≤ ω≤s = l≤s⇒l≤ ⦃ ⌜⌝-monoSequence ⦄ ω≤s

≤-单调

还有一种更弱的单调序列, 叫做非严格单调.

≤-monoSequence : (ℕ → Ord) → Set
≤-monoSequence = Monotonic₁ ℕ._≤_ _≤_

事实非严格单调蕴含严格单调.

<⇒≤-mono : ∀ {f} → ⦃ MonoSequence f ⦄ → ≤-monoSequence f
<⇒≤-mono ⦃ wrap mono ⦄ ≤ with m≤n⇒m<n∨m≡n ≤
... | inj₁ < = <⇒≤ (mono <)
... | inj₂ refl = ≤-refl

事实非严格单调序列的极限与起始无关.
证明这可看作是上一章 l≈ls 的推广, 用类似思路可证. ∎

module _ {f h} (≤-mono : ≤-monoSequence f) (incr : ∀ n → n ℕ.< h n) where
  l≈l∘ : lim f ≈ lim (f ∘ h)
  l≈l∘ = l≤ (λ { ℕ.zero   → ≤f⇒≤l {n = 0} (≤-mono z≤n)
              ; (ℕ.suc n) → ≤f⇒≤l (≤-mono (incr n)) })
      , l≤ λ n → ≤f⇒≤l (≤-mono (ℕ.<⇒≤ (incr (h n))))

良构序数的性质

良构序数允许我们建立内涵等词与序关系的联系. 如:

引理非零良构序数大于零.

≢z⇒>z : ∀ {α} → ⦃ WellFormed α ⦄ → α ≢ zero → α > zero
≢z⇒>z {zero}  z≢z = ⊥-elim (z≢z refl)
≢z⇒>z {suc α} _   = inj₁ tt , z≤
≢z⇒>z {lim f} _   = z<l

引理外延等于零的良构序数就是零.

≈z⇒≡z : ∀ {α} → ⦃ WellFormed α ⦄ → α ≈ zero → α ≡ zero
≈z⇒≡z {zero}  _         = refl
≈z⇒≡z {suc α} (s≤z , _) = ⊥-elim (s≰z s≤z)
≈z⇒≡z {lim f} (l≤z , _) = ⊥-elim (<⇒≱ z<l l≤z)

引理小于等于零的良构序数就是零.

≤z⇒≡z : ∀ {α} → ⦃ WellFormed α ⦄ → α ≤ zero → α ≡ zero
≤z⇒≡z ≤z = ≈z⇒≡z (≤z , z≤)

良构序数还允许我们证明貌似要排中律才能得到的结果. 如:

引理良构序数要么是零, 要么大于零.

≡z⊎>z : ∀ α → ⦃ WellFormed α ⦄ → α ≡ zero ⊎ α > zero
≡z⊎>z zero    = inj₁ refl
≡z⊎>z (suc α) = inj₂ z<s
≡z⊎>z (lim f) = inj₂ (z<l)

引理良构序数要么有限, 要么无限.

<ω⊎≥ω : ∀ α → ⦃ WellFormed α ⦄ → α < ω ⊎ α ≥ ω
<ω⊎≥ω zero     = inj₁ z<ω
<ω⊎≥ω (suc α) with <ω⊎≥ω α
... | inj₁ <ω  = inj₁ (s<ω <ω)
... | inj₂ ≥ω  = inj₂ (≤⇒≤s ≥ω)
<ω⊎≥ω (lim f)  = inj₂ ω≤l

经典序数

在良构序数的基础上加入排中律可以得到经典序数, 可证 _≤_ 的线序性. 这部分内容与主线无关, 且非 --safe, 我们把它放在了独立的一章.