Isabelle 中的完整证明输出

Question

如果 Isabelle 没有找到引理的证明，是否有可能输出所有证明方法所做的所有事情，以达到他们无法进一步进行的子目标？这将帮助我了解他们在哪些方面卡住了，这将帮助我为他们指明正确的方向。

（对于已完成的证明，我会发现拥有一个完整的证明日志很有趣，该日志显示了为证明某些引理而执行的所有基本推理。）

Answer 1

这个问题听起来类似于我几天前回答的this one。该答案的部分内容也适用于此。无论如何，要具体回答这个问题：

不是真的。对于大多数基本的证明方法（rule 等，intro，fact，cases，induct）他们所做的事情相对简单，当他们失败时，几乎总是因为他们的规则试图申请与给定的目标/前提不一致。 （或者他们不知道首先应用哪个规则）

您可能正在考虑更多自动策略，例如 blast、force、simp 和 auto。他们中的大多数（blast、force、fastforce、fast、metis、meson、best 等）是“全有或全无”：他们要么解决子目标，要么他们什么都不做。因此，找出他们卡在哪里有点棘手，通常人们使用auto 进行这种探索：您申请auto，查看剩余的子目标，并考虑您可以按顺序添加哪些事实/参数分解更多。

simp 的情况类似，只是它比auto 少。 simp 是简化器，它使用术语重写、称为 simprocs 的自定义重写过程、某些求解器（例如，用于线性算术）以及其他一些方便的东西，例如拆分器，以摆脱 if 表达式。 auto 基本上是simp 结合经典推理，这使得它比simp 强大得多，但也更难预测。 （有时，auto 做得太多，从而将可证明的目标变成了不可证明的目标）

有一些跟踪工具（例如，简化器跟踪，在here 中有解释）。我认为还有一种方法可以追溯经典推理，但我似乎再也找不到了；也许我弄错了。无论如何，跟踪工具有时可以帮助解释意外行为，但我认为它们不是您想在这里使用的那种东西。更好的方法是了解这些方法尝试了哪些类型的事情，然后当 simp 或 auto 返回子目标时，您可以查看这些并确定您期望 simp 和 auto 下一步做什么以及为什么它没有这样做（通常是因为一些缺失的事实）并修复它。