形式化大数数学 (2.1 - 良构树序数的性质)

形式化大数数学 (2.1 - 良构树序数的性质)

交流Q群: 893531731
本文源码: Properties.lagda.md
高亮渲染: Properties.html

上一篇我们定义了良构树序数并证明了一些基本性质, 本文将继续讨论它的更多性质.

{-# OPTIONS --safe --cubical --lossy-unification #-}
module WellFormed.Properties where
open import WellFormed.Base

序数运算

我们先定义关于序数运算的一些性质.

约定 2-1-0 我们用

private variable
  A : Type
  F : A → A

定义 2-1-1 我们说 A 上的一个运算 F : A → A 保持 A 上的一个二元关系 \sim, 当且仅当对任意序数 x, y 都有 x \sim y \to F(x) \sim F(y).

_preserves_ : (A → A) → (A → A → Type) → Type
F preserves _~_ = ∀ {x y} → x ~ y → F x ~ F y

事实 2-1-2 如果 F 保持 \lt, 那么 F 保持 \leq.

map-pres≤ : F preserves _<_ → F preserves _≤_
map-pres≤ pres (inl p)    = <→≤ (pres p)
map-pres≤ pres (inr refl) = inr refl

定义 2-1-3 我们说 A 上的一个运算 F : A → A 单射 A 上的一个二元关系 \sim, 当且仅当对任意序数 x, y 都有 F(x) \sim F(y) \to x \sim y.

_injects_ : (A → A) → (A → A → Type) → Type
F injects _~_ = ∀ {x y} → F x ~ F y → x ~ y

事实 2-1-4 如果 F 单射 = 且单射 \lt, 那么 F 单射 \leq.

map-inj≤ : F injects _≡_ → F injects _<_ → F injects _≤_
map-inj≤ inj inj< (inl p) = inl (inj< p)
map-inj≤ inj inj< (inr p) = inr (inj p)

一些约定

记法 2-1-5 隐参版极限构造子: 它们与原版的区别在于良构条件为隐式参数, 从而允许从上下文自动推断出它们, 而不用一一显式写出.

lim- : (f : Seq) {w : wf f} → Ord
lim- f {w} = lim f ⦃ w ⦄

如果我们有 a 通往 \lim f 的序列第 n 项的路径 r, 那么我们把 a 通往 \lim f 的路径记作 \text{rd}[n](r).

rd[_] : (n : ℕ) {w : wf f} → Road a (f n) → Road a (lim f ⦃ w ⦄)
rd[_] n = lim {n = n} ⦃ _ ⦄

如果我们有 a 小于 \lim f 的序列第 n 项的证明 r, 那么我们把 a 小于 \lim f 的证明记作 \text{<}[n](r).

<[_] : (n : ℕ) {w : wf f} → a < f n → a < lim f ⦃ w ⦄
<[_] n = map rd[ n ]

约定 2-1-6 鉴于路径关系与子树关系的高度可互换性, 我们今后在自然语言中会适当地混淆两者, 例如把路径的构造说成是子树关系的证明, 或反之. 读者应该理解为是调用了上一篇的引理进行了两者的转换.

树序数的归纳定义允许我们快速判定一个序数是否是极限序数.

定义 2-1-7 极限序数谓词: 它仅在遇到极限序数时为真. 该谓词是可判定的.

isLim : Ord → Type
isLim zero = ⊥
isLim (suc a) = ⊥
isLim (lim f) = ⊤

记法 2-1-8 极限序数的基本列: 如果 a 是极限序数, 那么我们用 a[n] 表示其基本列的第 n 项. 由序数的定义有 a[n] < a[n^+].

_[_] : (a : Ord) → ⦃ isLim a ⦄ → Seq
_[_] (lim f) = f

[]-wf : ⦃ _ : isLim a ⦄ → a [ n ] < a [ suc n ]
[]-wf {lim f} = it

定义 2-1-9 自然数到序数的嵌入 \text{fin} : ℕ → \text{Ord}

\text{fin}(n) := \text{suc}^n(0)

其中后继函数的上标 n 表示迭代 n 次.

open import Lower public using (_∘ⁿ_)
fin : Seq
fin n = (suc ∘ⁿ n) zero

非形式地, 后文中我们把 \text{fin} 视作类型强转 (coercion).

约定 2-1-10 数字字面量既可以表示自然数, 也可以表示序数. Agda 使用字面量重载功能实现该约定.

open import Agda.Builtin.FromNat public
instance
  nNat = Number ℕ   ∋ record { Constraint = λ _ → ⊤ ; fromNat = λ n → n }
  nOrd = Number Ord ∋ record { Constraint = λ _ → ⊤ ; fromNat = λ n → fin n }

一些引理

事实 2-1-11 构造子的单射性

suc-inj : suc a ≡ suc b → a ≡ b
suc-inj refl = refl

lim-inj : {wff : wf f} {wfg : wf g} → Ord.lim f ⦃ wff ⦄ ≡ lim g ⦃ wfg ⦄ → f ≡ g
lim-inj refl = refl

事实 2-1-12 极限路径的反演: 如果 b 小于极限序数 a, 那么存在一个自然数 n 使得 b 小于 a[n].

lim-inv-rd : ⦃ _ : isLim a ⦄ → Road b a → Σ[ n ∈ ℕ ] Road b (a [ n ])
lim-inv-rd (lim r) = _ , r

lim-inv : ⦃ _ : isLim a ⦄ → b < a → Σ[ n ∈ ℕ ] b < a [ n ]
lim-inv r with lim-inv-rd (set r)
... | n , r = n , ∣ r ∣₁

鉴于互递归证明的特性, 我们有时会先声明定理, 然后再证明其所需的引理, 最后再证明定理本身.

互递归 2-1-13

\begin{aligned} (1)& \quad a < a^+ \\ (2)& \quad 0 ≤ a \end{aligned} 

z<s-rd : Road 0 (suc a)
z≤ : 0 ≤ a

z<s : 0 < suc a
z<s = ∣ z<s-rd ∣₁

引理 2-1-14 极限序数必然大于零.
证明 由引理 2-1-13-(2) 和定理 2-0-48 即证. ∎

z<l : {w : wf f} → 0 < lim f ⦃ w ⦄
z<l {f} {w} = begin-strict
  0               ≤⟨ z≤ ⟩
  f 0             <⟨ f<l ⟩
  lim- f          ∎ where open SubTreeReasoning

定理 2-1-13-(1) 0 < a^+.
证明 对 a 归纳.

z<s-rd {(zero)} = zero
z<s-rd {suc a} = suc z<s-rd
z<s-rd {lim f} = suc (set z<l)

定理 2-1-13-(2) 0 ≤ a.
证明 对 a 归纳. 零的情况由自反性, 后继的情况由2-1-13-(1), 极限的情况由引理 2-1-14 即得. ∎

z≤ {(zero)} = inr refl
z≤ {suc _}  = inl z<s
z≤ {lim _}  = inl z<l

互递归 2-1-17

<→s≤-rd : Road a b → NSRoad (suc a) b
s<s-rd : suc preserves Road

<→s≤ : a < b → suc a ≤ b
<→s≤ = rec isProp≤ (ns→≤ ∘ <→s≤-rd)

s<s : suc preserves _<_
s<s = map s<s-rd

定理 2-1-17-(1) a < b \to a^+ ≤ b.
证明 对路径 r : a < b 归纳.

<→s≤-rd zero = inr refl
<→s≤-rd (suc r) = inl (s<s-rd r)
<→s≤-rd {a} (lim {f} {n} r) = inl $ begin-strict
  suc a           <⟨ s<s-rd r ⟩
  suc (f n)       ≤⟨ <→s≤-rd (set it) ⟩
  f (suc n)       <⟨ f<l-rd ⟩
  lim f           ∎ where open RoadReasoning

定理 2-1-17-(2) 后继运算保持 <.
证明 对路径 r : a < b 归纳, 要证 a^+ < b^+.

s<s-rd zero = zero
s<s-rd (suc r) = suc (s<s-rd r)
s<s-rd {x} (lim {f} {n} r) = suc $ begin-strict
  suc x           <⟨ s<s-rd r ⟩
  suc (f n)       ≤⟨ <→s≤-rd (set it) ⟩
  f (suc n)       <⟨ f<l-rd ⟩
  lim f           ∎ where open RoadReasoning

定理 2-1-18 后继运算单射 <.
证明 对路径 r : a^+ < b^+ 归纳, 要证 a < b.

s<s-inj-rd : suc injects Road
s<s-inj-rd zero = zero
s<s-inj-rd (suc r) = rd-trans zero r

s<s-inj : suc injects _<_
s<s-inj = map s<s-inj-rd

推论 2-1-19 后继运算保持 \leq, 且单射 \leq.
证明 由事实 2-1-2 和定理 2-1-17-(2) 可证保持; 由事实 2-1-4, 事实 2-1-11 和定理 2-1-18 可证单射. ∎

s≤s : suc preserves _≤_
s≤s = map-pres≤ s<s

s≤s-inj : suc injects _≤_
s≤s-inj = map-inj≤ suc-inj s<s-inj

定理 2-1-20 定理 2-1-17-(1) 的逆命题 a^+ ≤ b → a < b 成立.
证明 对 b 归纳, 且讨论 r : a^+ ≤ b.

s≤→<-rd : NSRoad (suc a) b → Road a b
s≤→<-rd {b = suc b} (inl r)       = suc (s<s-inj-rd r)
s≤→<-rd {b = suc b} (inr refl)    = zero
s≤→<-rd {b = lim f} (inl (lim r)) = lim (rd-trans zero r)

s≤→< : suc a ≤ b → a < b
s≤→< (inl r)    = map (s≤→<-rd ∘ inl) r
s≤→< (inr refl) = zero₁

定理 2-1-21 后继运算在极限序数下封闭.
证明 要证对任意 b 小于极限序数 a 都有 b^+ < a. 讨论 r : b < a, 只能有 r = \lim(r') : b < a, 且 r' : b < a[n]. 由定理 2-1-17 即传递性即得 b^+ < a[n]^+ ≤ a. ∎

s<l-rd : ⦃ _ : isLim a ⦄ → Road b a → Road (suc b) a
s<l-rd {a} {b} (lim {n} r) = begin-strict
  suc b           <⟨ s<s-rd r ⟩
  suc (a [ n ])   ≤⟨ <→s≤-rd f<l-rd ⟩
  a               ∎ where open RoadReasoning

s<l : ⦃ _ : isLim a ⦄ → b < a → suc b < a
s<l = map s<l-rd

定理 2-1-22 直接前驱在极限序数上封闭.
证明 要证对任意极限序数 a ≤ b^+ 有 a ≤ b. 讨论 a ≤ b^+.

l≤p-rd : ⦃ _ : isLim a ⦄ → NSRoad a (suc b) → NSRoad a b
l≤p-rd {lim f} (inl zero)    = inr refl
l≤p-rd {lim f} (inl (suc r)) = inl r

l≤p : ⦃ _ : isLim a ⦄ → a ≤ suc b → a ≤ b
l≤p {lim f} (inl r) = ns→≤ (l≤p-rd (inl (set r)))

ω的性质

定义 2-1-23 由定义 2-1-9, 显然 \text{fin} 是良构序列, 我们把 \lim(\text{fin}) 记作 \omega.

instance
  fin-wf : wf fin
  fin-wf = zero₁

ω : Ord
ω = lim fin

引理 2-1-24 有限序数 n 都小于 \omega.
证明 对 n 归纳.

n<ω : fin n < ω
n<ω {n = zero}  = z<l
n<ω {n = suc n} = s<l n<ω

引理 2-1-25 任意基本列的第 n 项大于等于 n.
证明 对 n 归纳.

n≤fn : ∀ f → ⦃ _ : wf f ⦄ → fin n ≤ f n
n≤fn {n = zero} f   = z≤
n≤fn {n = suc n} f  = begin
  fin (suc n)         ≤⟨ s≤s (n≤fn f) ⟩
  suc (f n)           ≤⟨ <→s≤ it ⟩
  f (suc n)           ∎ where open SubTreeReasoning

推论 2-1-26 任意基本列的第 n^+ 项大于 n.
证明 n ≤ f(n) < f(n^+). ∎

n<fs : ∀ f n → ⦃ _ : wf f ⦄ → fin n < f (suc n)
n<fs f _ = ≤-<-trans (n≤fn f) it

引理 2-1-27 没有极限序数小于 \omega.
证明 假设有这样的序数 a. 由事实 2-1-12, 存在 n 使得 a < n. 但由引理 2-1-25 又有 n ≤ a[n] < a. 由传递性有 n < n, 违反 < 的反自反性. ∎

l≮ω : ⦃ isLim a ⦄ → a ≮ ω
l≮ω a@{lim f} r = let n , r = lim-inv r in <-irrefl refl $ begin-strict
  fin n               ≤⟨ n≤fn f ⟩
  a [ n ]             <⟨ f<l ⟩
  a                   <⟨ r ⟩
  fin n               ∎ where open SubTreeReasoning

引理 2-1-28 忽略非同株, \omega 是最小的极限序数.
证明 对任意与 \omega 同株的极限序数 a, 由推论 2-0-34, 讨论 \omega 与 a 的大小关系. 若 a < \omega, 由引理 2-1-27 可得矛盾. 所以只能有 ω ≤ a. ∎

ω≤l : ⦃ isLim a ⦄ → ω < b → a < b → ω ≤ a
ω≤l {lim f} r s with <-connex r s
... | inl r           = inl r
... | inr (inr refl)  = inr refl
... | inr (inl r)     = ⊥-elim $ l≮ω r

引理 2-1-29 \text{fin} 单射 =.
证明 对 m, n 归纳即得. ∎

fin-inj : fin m ≡ fin n → m ≡ n
fin-inj {(zero)} {(zero)} eq = refl
fin-inj {suc m}  {suc n}  eq = cong suc $ fin-inj $ suc-inj eq

引理 2-1-30 \text{fin} 满射 \omega.
证明 要证对任意 a < ω 都存在 n 使得 n = a. 对 a 归纳.

fin-suj : a < ω → Σ[ n ∈ ℕ ] fin n ≡ a
fin-suj {(zero)} r  = 0 , refl
fin-suj {suc _}  r  with fin-suj (<-trans zero₁ r)
... | n , refl      = suc n , refl
fin-suj {lim f}  r  = ⊥-elim $ <-irrefl refl $ begin-strict
  ω                   ≤⟨ ω≤l zero₁ (<-trans r zero₁) ⟩
  lim f               <⟨ r ⟩
  ω                   ∎ where open SubTreeReasoning

定理 2-1-31 ℕ 与小于 \omega 的序数同构.
证明 \text{fin} 提供了正映射, 引理 2-1-30 提供了逆映射. 结合引理 2-1-29 可以说明它们互逆. ∎

ℕ≡ω : ℕ ≡ Σ Ord (_< ω)
ℕ≡ω = pathToEq $ isoToPath $ iso
  (λ n → fin n , n<ω)
  (λ (a , a<ω) → fst (fin-suj a<ω))
  (λ a → ΣPathP $ eqToPath (snd $ fin-suj _) , toPathP (squash₁ _ _))
  (λ n → eqToPath $ fin-inj $ snd $ fin-suj _)
  where open import Cubical.Foundations.Isomorphism