0

我试图弄清楚如何在 Coq 中执行以下操作。假设我们已经证明了以下内容：

trans_lemma: a = b -> b = c -> a = c

我们想用它来推断

b = a -> c = b -> a = c。

无论我做什么，我似乎都无法让“应用 trans_lemma with ...”。看起来我需要重写 trans_lemma 中的方程，以便变量以相同的顺序匹配。是否有一些简单的方法可以做到这一点而无需修改引理，即我可以以某种方式在表达式中的方程上应用“对称”策略吗？

（我知道我可以通过使用一些介绍和重写来证明我想要什么而不使用引理，但我想知道是否有一种语法方式可以重用我已经拥有的结果。）

4

1 回答 1

2

你不能对你的引理应用一些会神奇地改变它的形状的东西。你可以在这里做的是介绍你的等式b = a，c =b然后应用你的引理，留下两个目标，可以很容易地通过 的对称性来证明=。

总的来说，我认为您无法按照您希望的方式将策略应用于术语。

现在还有一些额外的事情：

  • 如果=这里是 Coq 的等式，你实际上不需要引理，因为系统给了你传递性。

  • 你的引理应该是多态的：trans_lemma : forall {T} (a b c : T), a = b -> b = c -> c = d。也许您向我们展示这个是因为您在一个部分中，但是一旦您关闭了该部分，您可能应该推断出第二个目标。

（您可能还对重用Transitive来自 ... 的类型类感兴趣Coq.Classes.RelationClasses）

于 2012-12-27T23:21:57.500 回答