在 Idris 中替换等式证明中的子表达式

Question

作为 Idris 的一个练习，我试图证明这个属性：

multCancel : (a:Nat) -> (b:Nat) -> (c:Nat) -> (S a) * b = (S a) * c -> b = c

我得出的结论是，作为一个中间步骤，我需要证明这样的事情：

lemma1 : {x:Nat} -> {y:Nat} -> {z:Nat} -> (x + x) + (x * z) = (y + y) + (y * z) -> (x * (S (S z))) = (y * (S (S z)))
lemma1 {x=x} {y=y} {z=z} prf = ?todo

当然，我已经证明了：

plusDouble : (a:Nat) -> (a + a) = a*2
plusDouble a =
  rewrite multCommutative a 2 in
  rewrite plusZeroRightNeutral a in Refl

所以我相信我基本上只需要将(x + x) 替换为(x*2)，然后调用分配性即可证明lemma1。我不知道如何进行此替换。 我以为我可以简单地做一些类似

的事情

rewrite plusDouble x in ...

但这显然行不通，因为我要替换的子表达式在 prf 和目标中。

有一些通用的方法吗？或者在这种特殊情况下您会推荐什么？

Answer 1

重写功能在后台使用replace : (x = y) -> P x -> P y；它正在弄清楚P 应该是什么（据我所知）。

要将x + x 替换为x*2，您可以使用等式x + x = x*2。要将x*2 替换为x + x，您可以使用等式x*2 = x + x；在你的情况下是sym prf。你需要两个替换来实现两者。

当重写工具（或推理）无法弄清楚时，您可以显式提供P，例如replace {P = \x' => x' + (x * z) = (y + y) + (y * z)} (plusDouble x) prf。当您需要重写 x + x 的某些站点但不是全部时，这特别有用。

Answer 2

好的，所以我发现我不必总是使用重写规则来简化目标，而是可以扩展它以匹配我作为参数得到的证明。