伊德里斯“没有改变类型”用完全相同的类型重写答案

【问题标题】：Idris "did not change type" for rewrite with exact same type伊德里斯“没有改变类型”用完全相同的类型重写
【发布时间】：2021-04-09 19:34:15
【问题描述】：

上下文我正在尝试为Vect 编写++ 的一个版本，编译器可以推断出生成的Vect 具有预期的内容。

详细信息我很难理解为什么第二次重写不起作用

import Data.Vect
import Data.Nat

infixl 9 ++:

public export
(++:) : {0 r, r' : Nat} -> Vect r Nat -> Vect r' Nat -> Vect (r' + r) Nat
(++:) [] y = rewrite plusZeroRightNeutral r' in y
(++:) {r = S rr} (x :: xs) y = rewrite plusSuccRightSucc r' rr in x :: (xs ++: y)

我有意以相反的顺序在签名中添加了向量长度，以使 API 更易于使用。我看到了

"tmp.idr" 8L, 254C written
Error: While processing right hand side of ++:. Rewriting by S (r' + rr) = r' + S rr did not change type Vect (r' + S rr) Nat.

/src/tmp.idr:8:32--8:82
   |
 8 | (++:) {r = S rr} (x :: xs) y = rewrite plusSuccRightSucc r' rr in x :: (xs ++: y)

我不明白为什么 r' + S rr 等于 S (r' + rr) 的证明不会重写 r' + S rr。这是我没有重写时的错误

"tmp.idr" 8L, 219C written
Error: While processing right hand side of ++:. Can't solve constraint between: S (plus r' rr) and plus r' (S rr).

/src/tmp.idr:8:32--8:47
   |
 8 | (++:) {r = S rr} (x :: xs) y = x :: (xs ++: y)
   |                                ^^^^^^^^^^^^^^^

【问题讨论】：

标签： proof idris

【解决方案1】：

这很简单，因为rewrite 以相反的顺序工作。所以如果目标是goal，但你有a，你需要一个证明goal = a，而不是a = goal。（我发现这总是很令人困惑，因为后台的replace 需要a = goal，但我猜这是因为rewrite 重写了目标项。）所以sym 这应该可以工作：

(++:) {r = S rr} (x :: xs) y = rewrite sym $ plusSuccRightSucc r' rr in x :: (xs ++: y)

【讨论】：