替换 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*2) 替换 (x + x) 然后调用分配性来证明 lemma1 。我不知道如何进行此替换。我以为我可以简单地做一些像

rewrite plusDouble x in ...

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

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

Answer 1

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

Answer 2

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

要用 x*2 替换 x + x，您可以使用等式 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 但不是全部

的某些站点时，这特别有用。

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

Replace subexpression in equality proof in Idris

theorem-proving

dependent-type

idris