阿格达:为什么我无法在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

笔记:

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

感谢您的完整回答。对我来说，要点是： 1）如果存在证明相等的表达式，则只能在 refl 上进行模式匹配。2）匹配时会丢失信息，可以使用≡替换来避免这种情况。顺便说一下，我用`data _divides_ (d : ℤ) : ℤ → Set where div : ∀{kn} → k * d ≡ n → d 划分 n` 替换了可分性的定义，这对我的目标更好，并证明更容易写。 (2认同)