为什么重写在这种情况下不改变表达式的类型？

Question

在 (*1) 中可以阅读下一个

rewrite prf in expr

If we have prf : x = y, and the required type for expr is some property of x, the rewrite ... in syntax will search for x in the required type of expr and replace it with y.

现在，我有下一段代码（您可以将其复制到编辑器并尝试 ctrl-l）

module Test

plusCommZ : y = plus y 0
plusCommZ {y = Z} = Refl
plusCommZ {y = (S k)} = cong $ plusCommZ {y = k}

plusCommS : S (plus y k) = plus y (S k)
plusCommS {y = Z} = Refl
plusCommS {y = (S j)} {k} = let ih = plusCommS {y=j} {k=k} in cong ih

plusComm : (x, y : Nat) -> plus x y = plus y x
plusComm Z y = plusCommZ
plusComm (S k) y =
  let
    ih = plusComm k y
    prfXeqY = sym ih
    expr = plusCommS {k=k} {y=y}
    -- res = rewrite prfXeqY in expr
  in ?hole

下面是洞的样子

- + Test.hole [P]
 `--          k : Nat
              y : Nat
             ih : plus k y = plus y k
        prfXeqY : plus y k = plus k y
           expr : S (plus y k) = plus y (S k)
     -----------------------------------------
      Test.hole : S (plus k y) = plus y (S k)

问题。 在我看来，注释行中的 expr（来自 *1）等于 S (plus y k) = plus y (S k)。 prf 等于 plus y k = plus k y，其中 x 是 plus y k，y 是 plus k y。并且重写应该在 expr（即 S (plus y k) = plus y (S k) 中搜索 x（即 plus y k），并且应该将 x 替换为 y（即用 plus k y). 结果 (res) 应该是 S (plus k y) = plus y (S k).

但这不起作用。

我有来自 idris 的下一个答案

rewriting plus y k to plus k y did not change type letty

我猜重写只是为了改变结果表达式的类型。因此，它不适用于 let 表达式的主体，而仅适用于 'in' 部分。这是正确的吗？

(*1) http://docs.idris-lang.org/en/latest/proofs/patterns.html

PS。教程中的示例工作正常。我只是想知道为什么我尝试使用重写的方式不起作用。

Answer 1

不幸的是，您没有提供导致您的代码行为异常的确切行，不知何故您一定做了一些奇怪的事情，因为根据您上面概述的推理，代码运行良好：

  let
    ih = plusComm k y -- plus k y = plus y k
    px = plusCommS {k=k} {y=y} -- S (plus y k) = plus y (S k)
    in rewrite ih in px

Answer 2

虽然文档中没有明确说明，rewrite 是对 Elab 战术脚本 (defined around here) 的语法糖调用。

为什么您的示例不起作用：未找到 "required type of expr"；仅使用 res = rewrite prfXeqY in expr，尚不清楚 res 应该具有哪种类型（即使是统一器 也可以 使用 let res = … in res 解决此问题。）如果您指定所需的类型，它按预期工作：

res = the (S (plus k y) = plus y (S k)) (rewrite prfXeqY in expr)

为什么重写在这种情况下不改变表达式的类型？

Why does rewrite not change the type of the expression in this case?

idris