严格良序与最小元搜索

可以直接阅读本章，也可以通过阅读指南和依赖地图选择其他路线。

设自然数的一个性质至少对一个数成立。那么它对一个最小的数成立：见证之中必有最小者。对于一般的严格良序，本章采用从已知见证出发的下降论证：若仍有严格更小的元素满足该性质，就移到那里重复；若没有，当前元素即为最小。序的良基性保证这样的下降不可能永远继续，因此过程会停在某个最小见证处。

本章把这个论证推广成对任意严格良序成立的定理，而不只对自然数。两块序数据承担证明。其一，两个元素的比较有三种结果：严格小于、相等、严格大于；把这三种结果表示为显式数据，证明便可按情形推理，这正说明极小见证一旦找到便唯一，因为两个极小见证不可能彼此严格更小。其二，良基性表述为每个元素的可及性证书，正是这些证书逐层下传，使下降得以在类型论中执行。本章的这个证明还使用一个经典成分：每一步都判定是否仍存在更小的见证，这个单纯存在性问题由所问层级上的排中律裁决。其余部分，包括结果的唯一性，都是构造性的。

本章先定义比较数据，再把序定律一并陈述，然后证明「是极小元」是命题且极小见证存在，最后把自然数上的严格序组装成实例，使搜索在那里具体可用。

序的载体与序关系本身不必处在同一宇宙层级：关系可以取值于固定层级 ℓₚ，而载体住在任意层级。这种区分只关乎一般性，与搜索的数学无关；下文的最小元论证从不比较层级。

随后真正工作的是两个数学概念。良基性通过可及性谓词 Acc 表述：一个元素可及，意思是每个严格更小的元素也依次可及；每个元素都可及时，关系是良基的。正是这些可及性证书为搜索的递归下降提供许可。三歧性则是使极小见证唯一的比较数据。自然数上的序已经同时具备这两个概念，因此它的实例只需组装而无需另证。

{-# OPTIONS --cubical --safe --guardedness #-}

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.WellOrder.Base {ℓₚ : Level} where

搜索还必须与不完整的信息共处。假设只说见证的集合「仅仅非空」，即 ∥_∥₁ 的一个居民；而每一步下降所问的「是否仍有严格更小的见证」同样是单纯存在陈述。这两处都不交出被选定的见证，也不需要交出：命题截断之所以能消去，是因为目标「作为极小元」是命题，而这一点将在本章证明。排中律恰好用来把每个这样的存在问题变成证明或反驳的两路判定。

open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
open import Cubical.Data.Nat using ( ℕ )
open import Cubical.Data.Nat.Order using ( _<_; <-trans; ¬m<m; <-wellfounded; _≟_ )
import Cubical.Data.Nat.Order as NatOrder
import Cubical.HITs.PropositionalTruncation as PT

这个逻辑情形决定了证明的次序。在消去任一截断之前，先证明固定一点上的极小性是命题，并证明极小见证的总类型也是命题。三歧性给出任意两个候选之间的路径，而与极小性冲突的严格比较则被排除。只有完成这段唯一性论证之后，下降过程才能消耗仅仅非空的假设。

open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
open import Cubical.Data.Sigma using ( Σ≡Prop )
open import Cubical.Foundations.HLevels using ( isProp×; isPropΠ )
open import Cubical.Relation.Nullary using ( isProp¬ ) renaming ( ¬_ to ¬ᵗ_ )
import Cubical.Data.Empty as Empty

判定 (若存在) 返回证明或反驳之一。带两个构造子的二元和恰好给出这种裁决的形状，它将承载排中律递交给下降过程的那个选择。

open import Cubical.Data.Sum using ( _⊎_; inl; inr )

作为数据的三歧

比较严格良序的两个元素有三种可能结果，后续证明需要按出现的结果分情形推理。因此我们把比较表示为带三个构造子的归纳类型，各构造子携带自己的证据：一个方向严格关系的证明、一个相等，或另一方向的证明。由于三个选项是构造子标签而非嵌套的和类型，证明可以直接检查比较并指出自己所在的情形。三个类型各自可处于自己的宇宙层级，比较类型落在三者的最大层级。

三个构造子 lt、eq、gt 对应三种结果。相等分支携带载体元素之间路径 a ≡ b 的证明，而不是只返回一个报告相等的标签。对自然数例子，这个类型将通过把库中对 a ≟ b 的三路判定逐构造子翻译来填充。

data Tri {ℓ₁ ℓ₂ ℓ₃ : Level} (A : Type ℓ₁) (B : Type ℓ₂) (C : Type ℓ₃)
       : Type (ℓ-max ℓ₁ (ℓ-max ℓ₂ ℓ₃)) where
  lt : A → Tri A B C
  eq : B → Tri A B C
  gt : C → Tri A B C

束

严格良序不只是一个关系：它是一个关系连同使最小元搜索得以运作的定律。我们把关系、三歧性、非自反性、传递性与良基性收进载体 A 上的单一记录 SWO。为这个接口命名，使后续构造不依赖任何具体序的构造方式；本章稍后给出的自然数序与其他实例都提供同样的五个字段。载体与关系可处于不同宇宙层级：A 住在层级 ℓc，关系取值于 Type ℓₚ。由于这种关系值的类型本身位于高一层宇宙，记录位于 ℓ-max ℓc (ℓ-suc ℓₚ)。

前两个字段是关系及其三歧性。对任意两个元素 a 与 b，tri∙ 返回比较数据：a <∙ b、路径 a ≡ b、或 b <∙ a。三歧性正是稍后极小元唯一性的来源，因为两个候选不可能彼此严格更小。

record SWO {ℓc : Level} (A : Type ℓc) : Type (ℓ-max ℓc (ℓ-suc ℓₚ)) where
  field
    _<∙_   : A → A → Type ℓₚ
    tri∙   : (a b : A) → Tri (a <∙ b) (a ≡ b) (b <∙ a)
    irr∙   : (a : A) → ¬ᵗ a <∙ a

其余三个字段是序定律。irr∙ 说没有元素小于自身，trans∙ 是传递性，而 wf∙ 断言 A 的每个元素对该关系都是可及的。可及性是良基递归背后的归纳原理：给定 a 处的 acc rs，函数 rs 对每个更小的元素给出可及性数据。正是这份逐层下传的供给使搜索中的下降得以终止。

    trans∙ : (a b c : A) → a <∙ b → b <∙ c → a <∙ c
    wf∙    : WellFounded _<∙_

极小元

固定 A 上的一个严格良序 w。对取值于命题的谓词 P，元素 a 是 P 的极小元，当它满足 P 且没有满足 P 的元素严格位于其下。「是极小元」是命题，「极小元」这个类型整体也是：给定两个，三歧排除两个严格情形并强制相等。这两条命题性事实是本章的关键，因为命题值的目标可以吸收命题截断。正是这一点将让下文的搜索把仅仅非空的子集变成真正的极小元。

定义把 P 取为 hProp 值的族：每根纤维连同「它是命题」的证书一起打包。⟨ P a ⟩ 投影出底层类型，于是 IsLeast P a 是一个二元组：a 满足 P 的见证，加上一个函数，它把每个其他见证 b 连同其证书 ⟨ P b ⟩ 送到对 b <∙ a 的反驳。注意最小性约束只要求在实际满足谓词的元素上成立；子集之外的元素可以位于任何位置。

module _ {ℓc : Level} {A : Type ℓc} (w : SWO {ℓc} A) where
  open SWO w

  IsLeast : {ℓ'' : Level} → (A → hProp ℓ'') → A → Type (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
  IsLeast P a = ⟨ P a ⟩ × ((b : A) → ⟨ P b ⟩ → ¬ᵗ b <∙ a)

  isPropIsLeast : {ℓ'' : Level} (P : A → hProp ℓ'') (a : A) → isProp (IsLeast P a)

IsLeast P a 的两个分量都是命题：第一个由打包进 P a 的证书保证，第二个是因为取值于命题的否定值函数是命题。于是借助「命题的二元组仍是命题」把配对闭合，IsLeast P a 是命题。对极小元的整体类型，Σ≡Prop 在第二分量是命题时，只要两个二元组的第一分量相等就识别它们；这一化归正是辅助函数 decide 所执行的。

  isPropIsLeast P a = isProp× (snd (P a)) (isPropΠ λ b → isPropΠ λ _ → isProp¬ _)

  isPropLeastOf : {ℓ'' : Level} (P : A → hProp ℓ'')
                → isProp (Σ[ a ∈ A ] IsLeast P a)
  isPropLeastOf P (m , pm , minm) (m' , pm' , minm') =
    Σ≡Prop (isPropIsLeast P) (decide (tri∙ m m'))

为比较两个极小元 m 与 m'，decide 检查 tri∙ m m'。若 m <∙ m'，则 m' 是极小元而 m 满足谓词，于是 m 不应严格小于 m'：矛盾，经由 Empty.rec，它从不可能情形导出任何目标。对称情形类似。剩下的情形中比较本身交出路径 e : m ≡ m'，直接返回即可。结合 Σ≡Prop，这证明了 isPropLeastOf：P 的极小见证类型是命题，故极小性一旦存在便唯一。

    where
    decide : Tri (m <∙ m') (m ≡ m') (m' <∙ m) → m ≡ m'
    decide (lt m<m') = Empty.rec (minm' m pm m<m')
    decide (eq e)    = e
    decide (gt m'<m) = Empty.rec (minm m' pm' m'<m)

现在给出搜索本身。它取所问层级上的排中律、谓词 P，以及见证子集的单纯居民，返回真正的二元组：极小见证连同其最小性数据。论证沿良序下降：从任一初始见证出发，问是否有严格更小的元素仍满足 P。若有，就在那里递归；由于每次递归严格向下移动且可及性逐层下传，这会终止。若无，则当前元素按定义即为极小。每一步都需要对由任意谓词构造的命题作经典判定，这正是排中律进入的唯一位置；陈述本身与序定律仍是构造性的。

假设中截断的消去是合法的，因为目标 Σ[ a ∈ A ] IsLeast P a 已被 isPropLeastOf 证明为命题。于是可从仅仅非空的子集中提取某个初始见证 a₀ 及其证书，然后开始下降 go a₀ (wf∙ a₀) pa₀：作为束一部分的可及性数据 wf∙ a₀ 正是递归的燃料。注意初始见证是任意的；产出极小元的是下降过程，而非起点的选取。

  leastOf : {ℓ'' : Level} → LEM (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))
          → (P : A → hProp ℓ'')
          → ∥ Σ[ a ∈ A ] ⟨ P a ⟩ ∥₁ → Σ[ a ∈ A ] IsLeast P a
  leastOf {ℓ''} lem P =
    PT.rec (isPropLeastOf P) (λ { (a₀ , pa₀) → go a₀ (wf∙ a₀) pa₀ })

辅助函数 go 接收元素 a、其可及性数据、以及 a 满足 P 的证书，返回一个极小见证。每一步它构造命题 Smaller：是否「仅仅存在」一个严格位于 a 之下且仍满足 P 的元素。由于它的底层类型是命题截断，它是一个 hProp，排中律因此适用；层级簿记保证判定恰好在所涉数据所在的层级作出。

    where
    go : (a : A) → Acc _<∙_ a → ⟨ P a ⟩ → Σ[ m ∈ A ] IsLeast P m
    go a (acc rs) pa = decide (lem (Smaller , squash₁))
      where
      Smaller : Type (ℓ-max ℓc (ℓ-max ℓₚ ℓ''))

把 lem 用于 Smaller 得到证明或反驳，decide 把两种裁决都变成极小见证。肯定情形中，截断陈述再次消去到命题值的目标，交出真正的元素 b，严格小于 a 且满足 P b；递归借助可及性函数 rs 在 b 处继续，而 rs 恰好在 a 之下的元素上有定义。这就是下降步，正是可及性数据保证它不会无限继续。

      Smaller = ∥ Σ[ b ∈ A ] ((b <∙ a) × ⟨ P b ⟩) ∥₁
      decide : Smaller ⊎ (Smaller → Empty.⊥) → Σ[ m ∈ A ] IsLeast P m
      decide (inl q) = PT.rec (isPropLeastOf P)
        (λ { (b , (b<a , pb)) → go b (rs b b<a) pb }) q
      decide (inr ¬q) = a , (pa , λ b pb b<a → ¬q ∣ b , (b<a , pb) ∣₁)

自然数，良序化

自然数上的通常严格序满足束的全部四条定律，其良基性对上侧自然数作归纳即得。本节组装 natOrder : SWO {ℓ-zero} ℕ；一个具体使用处 L.Choice.FiniteStageOrders 调用 leastOf natOrder，从以自然数编号的有限层中挑出见证某性质的最早层。关于通常的序，库中已有全部所需材料，因此这个束只需组装而无需另行证明：关系、非自反性、传递性与良基性直接取自库，三歧性则是库的三路判定程序、其答案按本章构造子重新命名。

剩下的一步是真正的调整。自然数上的序处在最底宇宙层级，而束的关系取值于固定层级 ℓₚ；因此每次比较都要用 Lift 包一层，它只改变类型所在的层级，不改变其居民。

liftAcc 把可及性数据从原本的序搬运到其抬升副本。给定 n 处的 acc r，它返回某个函数的 acc：该函数从抬升序中位于 n 之下的 m 出发，先用 lower 拆开抬升的证明，再在 m 处递归。这是对可及性参数的结构递归，与稍后驱动 leastOf 的模式相同。注意 Lift 的两个宇宙参数：源层级保持为零，只有目标层级是 ℓₚ。

liftAcc : (n : ℕ) → Acc _<_ n → Acc (λ a b → Lift {ℓ-zero} {ℓₚ} (a < b)) n
liftAcc n (acc r) = acc (λ m h → liftAcc m (r m (lower h)))

natOrder : SWO {ℓ-zero} ℕ
natOrder = record
  { _<∙_   = λ a b → Lift (a < b)

有了抬升后的可及性，natOrder 逐字段填入。关系把 a 与 b 送到 Lift (a < b)；非自反性拆开假设并应用库的 ¬m<m；传递性拆开两个证明，用库的 <-trans 复合，再把结果重新抬升；良基性对每个 n 给出 liftAcc n (<-wellfounded n)。这里没有为自然数序证明任何新数学，只做了层级调整和向束字段名的改写。

  ; tri∙   = triOf
  ; irr∙   = λ a h → ¬m<m (lower h)
  ; trans∙ = λ a b c h k → lift (<-trans (lower h) (lower k))
  ; wf∙    = λ n → liftAcc n (<-wellfounded n) }
  where

三歧字段是 where 块中的 triOf。库的判定程序 a ≟ b 返回库自己的三路类型 NatOrder.Trichotomy a b 的值，其构造子 lt、eq、gt 携带与本章 Tri 相同的三种证据。于是 fromNat 逐构造子映射：任一方向的严格性证明被抬升，而相等性原样通过，因为自然数的相等无需层级调整。

  triOf : (a b : ℕ) → Tri (Lift (a < b)) (a ≡ b) (Lift (b < a))
  triOf a b = fromNat (a ≟ b)
    where
    fromNat : NatOrder.Trichotomy a b → Tri (Lift (a < b)) (a ≡ b) (Lift (b < a))
    fromNat (NatOrder.lt h) = lt (lift h)

fromNat 的三个子句完成翻译。合起来读可见为何改名就足够：库的比较数据与本章的形状相同，差别只在两个严格性类型所在的层级。填上这个字段后，natOrder 便是完整组装的束，前面各节的结论对它适用：给定排中律，ℕ 上每个非空的命题值谓词都有唯一的最小见证。

    fromNat (NatOrder.eq h) = eq h
    fromNat (NatOrder.gt h) = gt (lift h)

小结

现在，严格良序可以作为一个结构整体传递、以三歧作比较，并搜索最小见证。SWO 把关系连同四条定律收在一起，leastOf 从任何仅仅非空的子集中取出极小见证，且由 isPropLeastOf 提供的路径保证唯一。自然数实例 natOrder 支持在自然数索引上搜索，例如后续章节从 L 的有限层中挑选见证某性质的最早层。排中律只在搜索每一步下降所问的判定处进入；束的定义、其定律与自然数序本身仍是构造性的。