1

我想知道如何在以下情况下重新排序目标：

lemma "P=Q"
  proof (rule iffI, (*here I would like to swap goal order*), rule ccontr)
oops

我想要一个不涉及更改引理语句的解决方案。我意识到这一点prefer并且defer可以用于应用风格的证明，但我希望有一种可以在proof (...)零件中使用的方法。

编辑：

正如 Andreas Lochbihler 所说，rule iffI[rotated]在上面的例子中写作是有效的。但是，在不改变引理陈述的情况下，是否可以在以下情况下交换目标顺序？

lemma "P==>Q" "Q==>P"
  proof ((*here I would like to swap goal order*), rule ccontr)
oops

这个例子可能看起来做作，但我觉得可能存在不方便改变引理的陈述的情况，或者在之前没有应用诸如iffI.

4

1 回答 1

2

子目标的顺序由您应用的规则的假设顺序决定。因此，交换规则的假设就足够了，例如，使用如下iffI所示的属性[rotated]

proof(rule iffI[rotated], rule ccontr)

一般来说，没有证明方法可以改变目标的顺序。如果您正在考虑将其与更复杂的证明自动化一起使用auto，我强烈建议您不要做这些事情。具有大量自动化的证明脚本应该独立于目标的顺序工作。否则，当证明自动化设置中的某些内容发生变化时，您的证明将很容易损坏。

然而，一些低级证明策略允许使用明确的目标寻址（主要是那些以 结尾的_tac）。例如，

proof(rule iffI, rule_tac [2] ccontr)

将ccontr规则应用于第二个子目标而不是第一个子目标。

于 2017-09-19T17:30:41.677 回答