pattern-matching - Agda：为什么我无法在 refl 上进行模式匹配？

Question

我试图证明整数的可分性。首先，我试图证明可分性是反射性的。

∣-refl : ∀{n} → n ∣ n

因为我根据减法定义了除法...

data _∣_ : ℤ → ℤ → Set where
  0∣d : ∀{d} → zero ∣ d
  n-d∣d : ∀{n d} → (n - d) ∣ d → n ∣ d

...如果我使用以下事实似乎很容易n-n=0：

∣-refl {n} with n-n≡0 n 
... | refl = n-d∣d 0∣d

但是 Agda 拒绝在 refl 上进行模式匹配。即使没有其他可能的范式n-n=0 n。我已经用其他功能证明了这一点。我只需要使用n-n=0.

C:\Users\ebolnme\Desktop\agda\Integers.agda:118,7-11
n + neg n != zero of type ℤ
when checking that the pattern refl has type n + neg n ≡ zero

笔记：

• a - b定义为a + (neg b)
• 我已经证明了n-n≡0 : (n : ℤ) → n - n ≡ zero

Answer 1