如何在 Agda 中定义满足上下界约束的自然数类型？

2026-11-04数据小陈

可以用 record 保存自然数 x，以及 m ≤ x 和 x < n 的证明。数独中的数字 1 到 9 对应半开区间 [1, 10)，因此可以定义为 Range 1 10。

原问题中的 InRange m n x 也能表达区间约束：它是给定的 x 满足区间条件的证明。若要让类型的值直接携带数字，需要把 x 和证明放在一起。

为什么原来的 Range 会接受无效区间？

问题出在 rbase 的类型：

rbase : {m n : ℕ} → Range m (suc n)

它允许任意的 m 和 n，既不要求下界小于上界，也不要求提供一个位于区间内的数字。取 m = 3、n = 1，得到的就是 Range 3 2，所以 test = rbase 可以成立。

后面的 rsuc 无法补上这个约束，因为无效的值已经可以通过 rbase 直接构造。

Range 3 2 作为类型表达式可以合法存在。合理的区间定义应让它没有可构造的值，而不是要求这个类型表达式本身非法。

用 record 保存数字及边界证明

下面的定义使用 Agda 标准库中的自然数和序关系。字段 lower 和 upper 的类型可以依赖前面定义的 value，这是依赖 record 的用法。Agda record 文档

module BoundedNumbers where

open import Data.Nat.Base
  using (ℕ; _≤_; _<_; z≤n; s≤s)
open import Data.Nat.Properties using (≤-refl)

record Range (m n : ℕ) : Set where
  constructor bounded
  field
    value : ℕ
    lower : m ≤ value
    upper : value < n

SudokuNum : Set
SudokuNum = Range 1 10

one : SudokuNum
one = bounded 1
  (s≤s z≤n)
  (s≤s (s≤s z≤n))

nine : SudokuNum
nine = bounded 9
  (s≤s z≤n)
  ≤-refl

getValue : ∀ {m n} → Range m n → ℕ
getValue r = Range.value r

bounded 依次接收数字、下界证明和上界证明。上下界 m、n 可以从目标类型推断，无需手动传入。

标准库将 x < n 定义为 suc x ≤ n，所以：

one 的上界证明需要证明 2 ≤ 10，使用两次 s≤s 后归结为 0 ≤ 8。
nine 的上界证明需要证明 10 ≤ 10，可以直接使用 ≤-refl。

这些构造器和严格小于关系的定义可见 Data.Nat.Base。

取出数字时使用 Range.value r；需要边界证明时，可以分别使用 Range.lower r 和 Range.upper r，无需再次检查数字是否越界。

同样的定义也允许表示空区间。例如，构造 Range 3 2 的值时，必须同时提供 3 ≤ value 和 value < 2 的证明，而这两个条件无法同时满足。

输入数字时，怎样自动检查范围？

对于程序接收到的任意自然数，可以先判断两条不等式。检查成功时返回携带证明的 Range，失败时返回 nothing。

将下面的代码接在前面的模块中：

open import Data.Nat.Properties using (_≤?_; _<?_)
open import Data.Maybe.Base using (Maybe; just; nothing)
open import Relation.Nullary using (yes; no)

makeRange : (m n x : ℕ) → Maybe (Range m n)
makeRange m n x with m ≤? x | x <? n
... | yes lowerProof | yes upperProof =
  just (bounded x lowerProof upperProof)
... | no _ | _ = nothing
... | yes _ | no _ = nothing

readSudokuNum : ℕ → Maybe SudokuNum
readSudokuNum = makeRange 1 10

_≤?_ 和 _<?_ 返回可判定结果。匹配到 yes 时，分支中会得到对应关系的证明，可以直接传给 bounded。Data.Nat.Properties

这个接口可以把外部输入转换成受约束的数字，调用方再通过 just、nothing 处理成功或失败。

原来的 Boolean 版 InRange 是否正确？

在导入所需名称、调整好缩进后，这个定义可以使用：

open import Data.Nat.Base using (_≤ᵇ_; _<ᵇ_)
open import Data.Bool.Base using (T; _∧_)
open import Data.Unit.Base using (tt)

record InRange (m n x : ℕ) : Set where
  field
    inRange : T ((m ≤ᵇ x) ∧ (x <ᵇ n))

fiveProof : InRange 1 10 5
fiveProof = record { inRange = tt }

T 把 Boolean 结果转换成类型：T true 是有值的类型 ⊤，T false 是空类型 ⊥。Data.Bool.Base

对于 InRange 1 10 5，比较表达式可以计算为 true，所以字段可以填入 tt。对于越界的具体数字，表达式会计算为 false，此时无法提供这个字段的值。

这里的 5 是类型参数，fiveProof 保存的是区间条件的证明。若希望沿用这个谓词，并把数字一起保存，可以使用依赖对：

open import Data.Product.Base using (Σ; _,_)

BoolRange : ℕ → ℕ → Set
BoolRange m n = Σ ℕ (InRange m n)

five : BoolRange 1 10
five = 5 , fiveProof

Σ ℕ (InRange m n) 表示一对相互依赖的值：第一个是 x : ℕ，第二个是 InRange m n x 的证明。这样就把三参数的约束包装成了两参数的数字类型。

若后续经常需要分别使用上下界证明，前面使用 lower、upper 两个字段的写法会更直接。Boolean 写法同样能保证约束，只是在进行关系推理时，可能需要把 Boolean 条件的证明转换成 _≤_、_<_ 的证明。

数独也可以直接使用 Fin 9

如果目标只是表示九种数字，Fin 9 已经足够。它的自然数解释是 0 到 8，显示时加一即可：

open import Data.Fin.Base using (Fin; toℕ)
open import Data.Nat.Base using (suc)

SudokuIndex : Set
SudokuIndex = Fin 9

displayDigit : SudokuIndex → ℕ
displayDigit i = suc (toℕ i)

Fin 及 toℕ 的定义见 Data.Fin.Base。这种表示适合索引和枚举；若希望直接保存自然数，并在类型中明确保留任意上下界，可以使用 Range。

区间内的数字相加或取后继后，结果可能越界。此类操作需要重新检查范围，或者提供结果仍满足边界条件的证明。