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

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 是 加 k y。而rewrite应该在expr中搜索x(即for plus y k)(即S (plus y k) = plus y (S 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

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

Answer 1

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

为什么您的示例不起作用:未找到“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)