Idris 交互式证明器不会根据假设执行重写

Question

（我知道交互式证明器现在已被弃用，取而代之的是精化器反射，但我还没有时间更新。很快！）

我目前在证明者中有以下假设（以及其他假设）：

x : Nat
c : Nat
m : Nat
lte : LTE c m
pma : x + (m - c) = (x + m) - c
p : Part (S c) (plus x (minus m c))

pma 是使用我自己编写的函数创建的，给定自然数 x, y, z 和 z ≤ y 的证明产生 x + (y - z) = (x + y) - z 的证明.

Part n x 是将自然数 x 分成 n 部分（每部分都是一个自然数）的分区类型，其中顺序很重要。

我想做的是使用 pma 重写 p 的类型以产生新的假设：

p' : Part (S c) (minus (plus x m) c)

不过，我试过了：

let p' = rewrite pma in p

还有：

let p' = rewrite (sym pma) in p

因为我永远记不起 rewrite 是哪种方式，在这两种情况下我都得到了：

rewrite did not change type letty

我哪里出错了？我认为这可能是因为 plus 和 + 之间以及 minus 和 - 之间存在一些差异，但我很确定我之前在证明中互换使用它们.我遗漏的表达式之间还有其他区别吗？

我正在使用 Idris 版本 0.9.18-，如果有帮助的话。

Answer 1

您可以使用 pma : x + (m - c) = (x + m) - c 到 rewrite 键入 E1 + (E2 - E3) 的类型，以便选择 E1、E2 和 E3。但是，你有

p : Part (S c) (plus x (minus m c))

不是那种形式。但它是形式的 P (E1 + (E2 - E3))。所以我们需要提升

的平等性

E1 + (E2 - E3) ~> (E1 + E2) - E3

到

P (E1 + (E2 - E3)) ~> P ((E1 + E2) - E3)

这正是 replace 所做的：

replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y
replace Refl prf = prf

所以在你的特定情况下，给定

pma : x + (m - c) = (x + m) - c

然后

replace {Part (S c)} pma : Part (S c) (x + (m - c)) -> Part (S c) ((x + m) - c)

特别是，

replace {Part (S c)} pma p : Part (S c) ((x + m) - c)

Idris interactive prover won't perform rewrite on an assumption