agda - 为什么 Agda 需要在这里进行模式匹配

Question

我有以下几点:

open import Agda.Builtin.Equality
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Sigma
open import Agda.Primitive

_×_ : {n m : Level} (A : Set n) (B : Set m) → Set (n ⊔ m)
X × Y = Σ X (λ _ → Y)

ℕ² : Set
ℕ² = ℕ × ℕ 

canonical : ℕ² → ℕ²
canonical (x , 0) = (x , 0)
canonical (0 , y) = (0 , y)
canonical (suc x , suc y) = canonical (x , y)

p1 : (a : ℕ) → (a , 0) ≡ canonical (a , 0) -- works
p1 a = refl

p2 : (a : ℕ) → (0 , a) ≡ canonical (0 , a) -- doesn't work
p2 a = refl

p3 : (a : ℕ) → (0 , a) ≡ canonical (0 , a) -- works
p3 0 = refl
p3 (suc a) = refl

当我尝试键入检查时，它 agda 响应 p2 中的错误

zero != fst (canonical (0 , a)) of type ℕ
when checking that the expression refl has type
(0 , a) ≡ canonical (0 , a)

为什么 Agda 要求我对一对的第二个元素进行模式匹配，就像在 p3 中一样？为什么 p1 类型检查而不是 p2？

Answer 1

Agda 通过模式匹配将所有定义编译为案例树，如 user manual page on function definitions 中所述。 .在您的情况下，案例树如下所示:

canonical xy = case xy of
  (x , y) -> case y of
    zero -> (x , 0)
    suc y -> case x of
      zero -> (0 , suc y)
      suc x -> canonical (x , y)

特别是，该函数仅在已知第二个参数是 zero 时才进行计算。或 suc .当发生这种情况时，Agda 通过为第二个子句提供浅灰色背景来提供温和的警告。您也可以通过打开 --exact-split 将其变成错误。标志(在文件顶部带有 {-# OPTIONS --exact-split #-} 编译指示。
如果您想了解更多关于案例树的翻译，我推荐我们的 paper on elaboration of dependent pattern matching .您可能还对 a possible solution to this problem 感兴趣(遗憾的是它没有进入 Agda 的主要版本)或 --rewriting flag它允许您添加计算规则 canonical (0 , y) = (0 , y)首先证明它，然后将其注册为重写规则。