如何在Idris中重写？

Question

我在伊德里斯写了以下命题:

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))这是预期的类型,以及伊德里斯可以完成的证明自动替换?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). 在这个问题中，我解释了一个重要的观点：从plus函数是如何编写的事实以及编译器可以在您看到的类型中执行模式匹配的事实，S (plus k (S j))这仅适用plus于(S k)and (S j)。类似的情况S n + m。

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

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

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 中的行为方式如下：

1. 接受Refl : left = right对象和expr : t。
2. 搜索left在t。
3. left用rightin替换所有出现的t。

在我们的例子中：

1. t 是 S (plus k (S j)) = S (S (plus k j))
2. Refl : plus k (S j) = plus (S k) j
   • left 是 plus k (S j)
   • right 是 plus (S k) j
3. 伊德里斯内容替换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))。