---
title: "严格良序与最小元搜索"
module: L.WellOrder.Base
lang: zh
site: "Bedrock"
description: "严格良序与最小元搜索"
stage: "典范良序与选择公理"
reading_order: 73
canonical: https://bedrock.institute/zh/L.WellOrder.Base.html
html: L.WellOrder.Base.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/WellOrder/Base.lagda.md
prerequisites: [Base.Prelude, Base.Classical]
routes: [canonical-order]
translations: [https://bedrock.institute/en/L.WellOrder.Base.md, https://bedrock.institute/ja/L.WellOrder.Base.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 严格良序与最小元搜索

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

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

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

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

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

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

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

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

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

```agda
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
```

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

```agda
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
```

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

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

## 作为数据的三歧

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

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

```agda
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`。三歧性正是稍后极小元唯一性的来源，因为两个候选不可能彼此严格更小。

```agda
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` 对每个更小的元素给出可及性数据。正是这份逐层下传的供给使搜索中的下降得以终止。

```agda
    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` 的反驳。注意最小性约束只要求在实际满足谓词的元素上成立；子集之外的元素可以位于任何位置。

```agda
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` 所执行的。

```agda
  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` 的极小见证类型是命题，故极小性一旦存在便唯一。

```agda
    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₀` 正是递归的燃料。注意初始见证是任意的；产出极小元的是下降过程，而非起点的选取。

```agda
  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`，排中律因此适用；层级簿记保证判定恰好在所涉数据所在的层级作出。

```agda
    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` 之下的元素上有定义。这就是下降步，正是可及性数据保证它不会无限继续。

```agda
      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` 的两个宇宙参数：源层级保持为零，只有目标层级是 `ℓₚ`。

```agda
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)`。这里没有为自然数序证明任何新数学，只做了层级调整和向束字段名的改写。

```agda
  ; 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` 逐构造子映射：任一方向的严格性证明被抬升，而相等性原样通过，因为自然数的相等无需层级调整。

```agda
  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` 便是完整组装的束，前面各节的结论对它适用：给定排中律，`ℕ` 上每个非空的命题值谓词都有唯一的最小见证。

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

## 小结

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