Agda 2.5.1.2 模式匹配失败

Question

给定以下数据类型，它对两个自然数之间经过验证的比较进行编码：

open import Agda.Builtin.Nat

data Compare : Nat -> Nat -> Set where
  LT : {m : Nat} {n : Nat} -> Compare m (suc (m + n))
  EQ : {m : Nat} -> Compare m m
  GT : {m : Nat} {n : Nat} -> Compare (suc (m + n)) m

以下代码正确比较数字并计算它们的差值：

comparehelper : {m : Nat} {n : Nat} -> (Compare m n) -> Compare (suc m) (suc n)
comparehelper LT = LT
comparehelper EQ = EQ
comparehelper GT = GT

compare : (m : Nat) (n : Nat) -> Compare m n
compare 0 0 = EQ
compare (suc _) 0 = GT
compare 0 (suc _) = LT
compare (suc m) (suc n) = comparehelper (compare m n)

differencehelper : {m : Nat} {n : Nat} -> (Compare m n) -> Nat
differencehelper (LT {n = difflt1}) = suc difflt1
differencehelper EQ = 0
differencehelper (GT {n = difflt1}) = suc difflt1

difference : Nat -> Nat -> Nat
difference m n = differencehelper (compare m n)

但是下面的代码显然在功能上是相同的（模式匹配失败类型检查):

compare' : (m : Nat) (n : Nat) -> Compare m n
compare' 0 0 = EQ
compare' (suc _) 0 = GT
compare' 0 (suc _) = LT
compare' (suc m) (suc n) with compare' m n
... | LT = LT
... | EQ = EQ
... | GT = GT

difference' : Nat -> Nat -> Nat
difference' m n with compare' m n
... | LT {n = difflt1} = suc difflt1
... | EQ = 0
... | GT {n = difflt1} = suc difflt1

行为差异的解释是什么？正如问题中所述，我是运行 Agda 2.5.1.2.

Answer 1

这里的问题是 Compare m n 类型值的模式匹配优化了 m 和 n 的模式。

因此 ... 所代表的方案 compare' (suc m) (suc n) 不再有效。您必须使用精致的图案重复左侧，例如

compare' (suc m) (suc n) with compare' m n
compare' (suc m) (suc .(suc m + _)) | LT = LT
compare' (suc m) (suc .m)           | EQ = EQ
compare' (suc .(suc m + _)) (suc m) | GT = GT

我在这里对范围内但未明确命名的变量使用下划线（它们分别是 LT 和 GT 的隐式参数）。它们没有命名但在模式中是必需的这一事实可能是一个很好的线索，表明它们可能应该是 LT 和 GT 构造函数的显式参数。

或者，如果您不关心模式，您可以使用下划线（可以代表任何模式，包括点线）并写：

compare' (suc _) (suc _) | LT = LT
compare' (suc _) (suc _) | EQ = EQ
compare' (suc _) (suc _) | GT = GT

正如@asr 提到的，较新版本的 Agda 将支持您当前的模式匹配，因为 dot patterns have been made optional.

Agda 2.5.1.2 模式匹配失败

Failure in pattern matching in Agda 2.5.1.2

pattern-matching

agda