如何将 Agda 中的两个自然数与标准库（如 N -> N -> Bool）进行比较？

Question

我可以通过手动编写比较器来比较两个自然数：

is-≤ : ℕ → ℕ → Bool
is-≤ zero _ = true
is-≤ (suc _) zero = false
is-≤ (suc x) (suc y) = is-≤ x y

不过，我希望标准库中有类似的东西，所以我不会每次都写。

我能够找到_≤_ 运算符in Data.Nat，但它是一种参数化类型，它基本上包含一个特定数字小于另一个的“证明”（类似于_≡_）。有没有办法使用它或其他方法来了解哪个数字小于另一个“运行时”（例如返回相应的Bool）？

我要解决的更大的问题：

1. 作为我任务的一部分，我正在编写一个readNat : List Char → Maybe (ℕ × List Char) 函数。它尝试从列表的开头读取自然数；稍后将成为sscanf 的一部分。
2. 我想实现 digit : Char → Maybe ℕ 帮助函数，它会解析一个十进制数字。
3. 为此，我想将primCharToNat c 与primCharToNat '0'、primCharToNat '1' 进行比较并决定是返回None 还是(primCharToNat c) ∸ (primCharToNat '0')

Answer 1

@gallais 在 cmets 中提出的解决方案：

open import Data.Nat using (ℕ; _≤?_)
open import Data.Bool using (Bool)
open import Relation.Nullary using (Dec)

is-≤ : ℕ → ℕ → Bool
is-≤ a b with a ≤? b
... | Dec.yes _ = Bool.true
... | Dec.no _ = Bool.false

这里我们匹配_≤_ 可以使用with 子句判定的证明。可以在更复杂的功能中类似地使用它。

cmets 中@user3237465 对此答案的建议：您还可以使用简写⌊_⌋（\clL/\clR 或\lfloor/\rfloor）其中does this exact pattern matching 并消除对is-≤ 的需要：

open import Data.Nat using (ℕ; _≤?_)
open import Data.Bool using (Bool)
open import Relation.Nullary.Decidable using (⌊_⌋)

is-≤ : ℕ → ℕ → Bool
is-≤ a b = ⌊ a ≤? b ⌋

另一种方法是使用compare，它还提供更多信息（例如两个数字之间的差异）：

open import Data.Nat using (ℕ; compare)
open import Data.Bool using (Bool)
open import Relation.Nullary using (Dec)

is-≤' : ℕ → ℕ → Bool
is-≤' a b with compare a b
... | Data.Nat.greater _ _ = Bool.false
... | _ = Bool.true

is-≤3' : ℕ → Bool
is-≤3' a with 3 | compare a 3
... | _ | Data.Nat.greater _ _ = Bool.false
... | _ | _ = Bool.true

请注意，compareing 出于某种原因使用常量值 requires extra caution。