Agda:为什么我不能在参考图上进行匹配？

Question

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

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

因为我定义了基于减法的可分性.

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

如果我使用...it的话，n-n=0看起来很容易

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

但Agda拒绝在参考书上进行模式匹配。即使没有其他正常形式的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

平等证明没什么可谈的。当您在构造函数上进行模式匹配时，它可以细化其他参数(及其类型)。在您的例子中，n-n≡0 n应该细化n - n，但是没有这样的表达式，并且Agda给出了这个(有点令人费解的)错误消息。

您可以通过在with中引入表达式来解决这个问题。

∣-refl : ∀ {n} → n ∣ n
∣-refl {n} with n - n | n-n≡0 n
... | ._ | refl = ?

我们可以更清楚地了解左手边，这很好地说明了细化是如何进行的：

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

但是，当您试图填写该定义的其余部分时：

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

类型检查器再次不同意。为什么呢？n-d∣d应该有(n - n) ∣ n → n ∣ n类型，0∣d应该有类型0 ∣ n。但是等等！我们不是刚刚证明了n - n是，事实上，0

模式匹配和它所导致的细化的原因之一是，它只发生过一次，右手侧完全不会受到它的影响(顺便说一句，这是我们拥有inspect机器的原因之一)。我们该怎么处理呢？

有一个名为subst的函数，它接受某种类型的P a，这证明了a ≡ b并给出了P b。注意，如果我们用λ x → x ∣ n代替P，用zero代替a，用n - n代替b，就会得到一个函数，它接受zero ∣ n并给出n - n ∣ n (当然，作为适当的证明)。

事实上：

∣-refl {n} = n-d∣d (subst (λ x → x ∣ n) (sym (n-n≡0 n)) 0∣d)

这个定义被接受：subst ... 0∣d的类型是n - n ∣ n，这是适合n-d∣d的输入。注意，我们还需要一个证明zero ≡ n - n，但我们有n - n ≡ zero -这里我们使用的事实是≡是对称的(sym)。

为了完整起见，以下是subst的定义

subst : ∀ {a p} {A : Set a} (P : A → Set p) {x y} →
  x ≡ y → P x → P y
subst _ refl p = p