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

Question

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

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

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

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

我试图解决的更大问题:

作为我作业的一部分，我正在写一个 readNat : List Char → Maybe (ℕ × List Char)功能。它尝试从列表的开头读取自然数；稍后将成为 sscanf 的一部分.

我要实现 digit : Char → Maybe ℕ将解析单个十进制数字的辅助函数。

为此，我想比较 primCharToNat c与 primCharToNat '0' , primCharToNat '1'并决定是否返回None或 (primCharToNat c) ∸ (primCharToNat '0')

Answer 1

@gallais 在评论中提出的解决方案:

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 来决定-条款。人们可以在更复杂的功能中类似地使用它。

@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

请注意 compare使用常数值 requires extra caution因为某些原因。