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

Question

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

is-? : ? ? ? ? Bool
is-? zero _ = true
is-? (suc _) zero = false
is-? (suc x) (suc y) = is-? x y

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

我可以在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在评论中建议的解决方案：

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）来进行这种精确的模式匹配，并消除对以下内容的需要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，具有恒定值的ing 需要格外小心。