在 Isabelle/Isar 中使用时累积结果

Question

有时在证明中我发现自己需要累积结果，但也需要使用最后的结果，所以我最终为此使用了“also then”：

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

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

鉴于此，我有两个问题：

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

Answer 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 是足够长的子项时，好处才会变得明显。