如何查看Isabelle“证明”的分步推理

Question

我最近开始学习Isabelle，但我找不到一个重要问题的答案：一个人怎么能看到Isabelle找到的“证明”的逐步推理？我对“自动”或“通过爆炸使用Theorem_A”这样的行不满意，我想检查逐步推演。当然，我了解了Isar的“证明”，但是1. Sledgehammer不能总是找到这样的Isar证明，并且2.甚至Isar证明也不能总是给出循序渐进的推理。例如，由Sledgehammer生成的我的一个定理的Isar证明如下所示：

     proof -
  have "... here is my formula ...."
    using My_Theorem_1 My_axiom_2 by blast
  thus ?thesis
    by metis
qed

当然，不能像伊莎贝尔（Isabelle）和伊萨尔（Isar）的发烧友那样将这种证明称为“人类可读证明”。现在我的问题是：是否可以从伊莎贝尔（Isabelle）发现的“证明”逐步生成推论？或者至少有可能将“自动”之类的“证明”转换为Isar证明？需要逐步演绎的情况是例如存在性定理的证明，它们通常提供有用的显式构造。我浏览了一些教程，但找不到答案...

Answer 1

首先，我将解释为什么您的问题通常不像您认为的那么重要。然后我会回答您的实际问题。

伊莎贝尔的设计，使您不必“信任”的证明方法（如simp，auto，metis在所有）。所有证明都必须经过Isabelle的推理内核，因为该内核是Isabelle中唯一可以产生定理的部分：如果您信任（相对较小的）内核，则可以信任所有证明方法。证明方法直接或间接调用内核导出的函数来操纵定理。

内核包含反映Isabelle / Pure公理的功能，我认为这是自然推论。然后，您具有对象逻辑（在大多数情况下为HOL），定义和typedef的公理。所有Isabelle定理都有证明，这些证明基本上是由这些推理步骤组成的证明树。

因此，您要查找的“逐步”证明就是这棵树，它被称为证明对象或证明术语。这些东西的问题在于它们非常大且非常不可读（请参阅Russell和Whitehead 撰写的Principia Mathematica，以了解它们的大小和不可读性）。我认为您可以告诉Isabelle以某种方式生成这些证明条款，但我不知道如何生成。我确实找到了Stefan Berghofer的一组幻灯片。

我不明白为什么您会说您所举的例子难以理解。读者可以隐藏一些细节，是的，但是几乎所有普通的数学证明也是如此。blast并且metis不要魔术 blast是一阶表格证明者，metis是分辨率证明者。如果blast并且metis可以在一个步骤中证明某事，则数学家可能也不会在该步骤上做更多详细说明。

至于具有存在性的显式构造：Isabelle / HOL 不是一种构造逻辑。从经典证明中提取程序是正在进行的研究，并且非常困难。如果您想在Isabelle / HOL中进行某些事物的显式构造，我的建议不是证明存在性，而是直接证明您的显式构造。如果您可以通过一步证明您的存在auto，我敢打赌，构造非常简单。

Answer 2

您可以使用以下方法查看事实的内部证明条款：

prf lemma_name

例如，以下来自Pure的引理

thm Pure.conjunction_imp
> (PROP ?A &&& PROP ?B ? PROP ?C) ? (PROP ?A ? PROP ?B ? PROP ?C)

具有作为其证明词输出：

prf Pure.conjunction_imp
> equal_intr ? _ ? _ ? (??(H: _) (Ha: _) Hb: _. H ? (conjunctionI ? _ ? _ ? Ha ? Hb)) ?
  (??(H: _) Ha: _. H ? (conjunctionD1 ? _ ? _ ? Ha) ? (conjunctionD2 ? _ ? _ ? Ha))

使用full_prf，输出将变得更加冗长。

Manuel Eberl的答案中引用的幻灯片提供了有关符号含义的更多信息。即使不理解证明λ术语，prf术语也很清楚地揭示了证明引理的事实。

在默认的HOL会话中，输出将看起来很无聊，因为内部校样部分未编译到会话映像中（请参见Makarius的帖子）。对于所需的输出，您必须切换到HOL-Proofs会话。（在jEdit中：从理论面板中选择HOL-Proofs，然后重新启动jEdit。特殊会话映像的构建应自动开始。（...在理论上，它应该像这样工作...我只是尝试构建HOL- Isabelle2015的证明会议，但在我的计算机上花费了无限长的时间...））