dependent-type - 重写在 Idris 中究竟是如何工作的？

Question

我在 Idris 中写了以下命题:

total
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m)
plusOneCommutes Z     k     = Refl
plusOneCommutes (S k) j     = 
 let inductiveHypothesis = plusOneCommutes k j in
   rewrite inductiveHypothesis in Refl

使用来自 Prelude.Nat 的灵感源代码，我理解为什么使用递归调用(在第二种情况下)作为归纳假设来证明这种情况是有意义的。然而，通过漏洞重写的细节，我并没有真正理解发生了什么以及为什么会这样。

如果我写:

plusOneCommutes (S k) j     = ?hole

我从编译器得到以下信息:

- + HolyGrail.hole [P]
 `--               k : Nat
                   j : Nat
     ------------------------------------------------------
      HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))

这似乎并不正确。根据 plusOneCommutes的签名这个洞应该有类型 (plus (S k) (S j)) = (plus (S (S k)) j) .

更进一步并引入归纳假设，如果我写:

plusOneCommutes (S k) j     = 
 let inductiveHypothesis = plusOneCommutes k j in
   ?hole

然后输入 hole变成:

 - + HolyGrail.hole [P]
  `--                    k : Nat
                         j : Nat
       inductiveHypothesis : k + S j = S k + j
      -------------------------------------------------------------------------
       HolyGrail.hole : S (plus k (S j))  = S (S (plus k j))

然后使用 inductiveHypothesis 给出的重写规则

 - + HolyGrail.hole [P]
  `--                    k : Nat
                         j : Nat
       inductiveHypothesis : k + S j = S k + j
             _rewrite_rule : k + S j = S k + j
      -------------------------------------------------------------------------
       HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j)

这导致 S (plus (S k) j) = S (S (plus k j))这是预期的类型，Idris 可以自动完成证明替换 ?hole与 Refl .

然后让我感到困惑的是我从签名中推断出的和编译器从漏洞中推断出的类型之间的意外差异。如果我自愿引入一个错误:

我收到以下消息:

 - + Errors (1)
  `-- HolyGrail.idr line 121 col 16:
      When checking right hand side of plusOneCommutes with expected type
              S k + S j = S (S k) + j

      Type mismatch between
              S (S (plus k j)) = S (S (plus k j)) (Type of Refl)
      and
              S (plus k (S j)) = S (S (plus k j)) (Expected type)

      Specifically:
              Type mismatch between
                      S (plus k j)
              and
                      plus k (S j)

Type mismatch...部分与上述步骤一致但不是 When checking ...部分给出了我期望的类型。

Answer 1

编译器的以下内容实际上是有道理的:

- + HolyGrail.hole [P]
 `--               k : Nat
                   j : Nat
     ------------------------------------------------------
      HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))

在 =的左侧您拥有的类型 n + S m .在 n 上进行模式匹配后你有 (S k)并且应该有 S k + S j类型为 plus (S k) (S j) .在 this question我解释了一个重要的点:从事实如何 plus函数已编写，事实上编译器可以在您看到的类型中执行模式匹配 S (plus k (S j))刚刚申请 plus至 (S k)和 (S j) .与 S n + m 类似的情况.

现在到 rewrite .在 Agda 编程语言中 rewrite只是 Refl 上模式匹配的语法糖.有时您可以替换 rewrite在 Idris 中使用模式匹配，但在这种情况下不是。

我们可以尝试做一些类似的事情。接下来考虑:

total
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m)
plusOneCommutes Z     k     = Refl
plusOneCommutes (S k) j     = case plusOneCommutes k j of
    prf => ?hole

编译器说下一个非常合理的事情:

- + HolyGrail.hole [P]
 `--               k : Nat
                   j : Nat
                 prf : k + S j = S k + j
     ------------------------------------------------------
      HolyGrail.hole : S (plus k (S j)) = S (S (plus k j))

prf是证明 k + S j = S k + j的东西这是有道理的。使用后 rewrite :

plusOneCommutes (S k) j     = case plusOneCommutes k j of
    prf => rewrite prf in ?hole

我们有:

- + HolyGrail.hole [P]
 `--               k : Nat
                   j : Nat
                 prf : k + S j = S k + j
       _rewrite_rule : k + S j = S k + j
     -------------------------------------------------------------------------
      HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j)

rewrite在 Idris 中的行为方式如下:

需要 Refl : left = right对象和 expr : t .

搜索 left在 t .

替换所有出现的 left与 right在 t .

在我们的例子中:

t是 S (plus k (S j)) = S (S (plus k j))

Refl : plus k (S j) = plus (S k) j

left是 plus k (S j)

right是 plus (S k) j

idris 替换 plus k (S j) (左)与 plus (S k) j (右)在 t我们得到 S (plus (S k) j) = S (S (plus k j)) . Idris 可以执行它所做的模式匹配。和 S (plus (S k) j)自然变成S (S (plus k j)) .