0

有时在证明中我发现自己需要累积结果，但也需要使用最后的结果，所以我最终使用 " also then" 来达到这个目的：

proof
  have ...
  also then have ...
  also then have ...
  ultimately show ...
qed

我觉得有更多我不知道的惯用方法。另一方面，这可能是标准的做法，并受到社区的鼓励。

因此，鉴于此，我有两个问题：

  1. 不鼓励使用“ also then”？
  2. 如果是这样，我可以在使用它们时使用哪些替代方法来累积结果？
4

1 回答 1

1

我将从提供一些背景开始。你违反了 Isabelle 中称为计算推理的主题。计算推理在文档The Isabelle/Isar Reference Manual的第 1.2 小节中进行了描述。

两种最常见的计算推理模式是

  have "a R b" sorry
  also have "b R c" sorry
  also have "c R d" sorry
  finally have "a R d" by assumption

（其中R是传递关系，例如=，使用中缀表示法编写）和

  have P sorry
  moreover have Q  sorry
  moreover have R sorry
  ultimately have S by (rule assms(1))

命令喜欢also并moreover使用附加事实calculation来存储附加信息。例如，随着上述第一个示例中的计算继续进行，事实calculation以下列方式发生变化

  have "a R b" sorry
  also have "b R c" (*calculation: a R b*) sorry 
  also have "c R d" (*calculation: a R c*) sorry
  finally have "a R d" by assumption

在这种情况下，传递性规则R用于链接谓词。因此，最终目标可以通过假设来实现。模式的情况有所不同moreover ... ultimately：

  have P sorry
  moreover have Q (*calculation: P*) sorry
  moreover have R (*calculation: P, Q*) sorry
  ultimately have S (*P ⟹ Q ⟹ R ⟹ S*) by (rule assms(1))

在这种情况下，事实calculation只是累积了所有先前的结果。

计算推理的实现在文档The Isabelle/Isar Reference Manual的第 6.3 小节中进行了说明。但是，我省略了这篇文章中的细节。

我现在将尝试在上述内容的背景下回答您的问题。

不鼓励使用“also then”吗？

我相信这不一定是不鼓励的，并且在 AFP 中有一些使用这种模式的例子。但是，我可以想象，对于这种特定模式，这将是一个相当不常见的用例。

如果是这样，我可以在使用它们时使用哪些替代方法来累积结果？

我相信，如果您确实只需要累积结果（同时可能在间歇性步骤中使用它们），那么最好使用的模式是moreover ... ultimately. 但是，当然，这取决于“结果的积累”究竟是什么意思。

备注 1

我希望从上面的讨论中可以清楚地看出，与的also结合使用ultimately是非常非传统的。在大多数情况下，使用这种模式几乎没有意义。

备注 2

该模式also ... finally通常与缩写一起使用...：

  have "a R b" sorry
  also have "... R c" sorry
  also have "... R d" sorry
  finally have "a R d" by assumption

当然，只有在子条款足够长的情况下b，这些好处才会变得明显。c

于 2021-05-08T00:40:47.550 回答