在这种情况下，为什么 rewrite 不会改变表达式的类型？

Question

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

rewrite prf in expr

如果我们有prf : x = y，并且expr 所需的类型是x 的某个属性，rewrite ... in 语法将在所需的expr 类型中搜索x 并将其替换为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 的下一个答案

将 plus y k 重写为 plus k y 并没有改变 letty 类型

我猜 rewrite 只是为了改变结果表达式的类型。因此，它在 let 表达式的主体中不起作用，而仅在它的“in”部分中起作用。这是正确的吗？

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

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

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)

Answer 2

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

  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