Agda:为什么我无法在 refl 上进行模式匹配? [英] Agda: Why am I unable to pattern match on refl?

问题描述

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

I'm trying to prove things about divisibility on integers. First I tried to prove that divisibility is reflective.

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

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

Because I defined divisibility based on subtraction...

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

...如果我使用 n-n=0 的事实似乎很容易:

...it seems easy if I use the fact that 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 的事实.

But Agda rejects to pattern match on refl. Even if there is no possible other normal form of n-n=0 n. I've proven this with an other function. I just have to use the fact that 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 ≡ 零

推荐答案

等式证明没什么好谈的.当您对构造函数进行模式匹配时，它可以优化其他参数(及其类型).在你的情况下，n-n≡0 n 应该改进 n - n，但没有这样的表达，Agda 给你这个(有点令人费解的)错误信息.

The equality proof has nothing to talk about. When you pattern match on a constructor, it can refine other arguments (and their types). In your case, n-n≡0 n should refine n - n, but there's no such expression and Agda gives you this (a bit puzzling) error message.

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

You can fix that by introducing the expression in a with:

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

我们可以更明确地说明左侧，这很好地展示了细化是如何发生的:

We can be more explicit about the left hand side, this nicely shows how the refinement happens:

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

<小时>

但是，当您尝试填写定义的其余部分时:

---

However, when you try to fill in the rest of the definition:

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

类型检查器再次不同意.为什么会这样?nd∣d 应该有一个类型 (n - n) ∣ n → n ∣ n 并且 0∣d 有一个类型 0∣ n.可是等等！我们不是刚刚表明 n - n 实际上是 0 吗?

The type checker disagrees yet again. Why is that so? n-d∣d should have a type (n - n) ∣ n → n ∣ n and 0∣d has a type 0 ∣ n. But wait! Didn't we just show that n - n is, in fact, 0?

模式匹配和它导致的细化的事情是它只发生一次，右侧根本不会受到它的影响(顺便说一下，这是我们拥有 <代码>检查机械).我们如何处理?

The thing with pattern matching and the refining it causes is that it happens only once, the right hand side won't be affected by it, at all (this is, by the way, one of the reasons we have the inspect machinery). How do we deal with it?

有一个名为 subst 的函数，它接受 P a 类型的东西，证明 a ≡ b 并给我们 Pb.请注意，如果我们用 λ x → x ∣ n 替换 P，zero 替换 a 和 n- n 对于 b，我们得到一个函数，它接受 zero ∣ n 并给我们 n - n ∣ n(对于合适的当然是证明).

There's a function called subst that takes something of type P a, a proof that a ≡ b and gives us P b. Notice that if we substitute λ x → x ∣ n for P, zero for a and n - n for b, we get a function that takes zero ∣ n and gives us n - n ∣ n (for suitable proof, of course).

事实上:

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

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

This definition is accepted: the type of subst ... 0∣d is n - n ∣ n, which is suitable input for n-d∣d. Notice that we also needed a proof that zero ≡ n - n, but we have n - n ≡ zero - here we use the fact that ≡ is symmetric (sym).

为了完整起见，这里是 subst 的定义:

For completeness' sake, here's the definition of subst:

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

这篇关于Agda:为什么我无法在 refl 上进行模式匹配?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！