如何证明 Isabelle/HOL 引理中存在目标？
我想证明以下 Isabelle/HOL 定理：
lemma involution:
"∀P h. (∀x. ¬P x ⟶ P (h x)) ⟶ (∃x. P x ∧ P (h (h x)))"
但到目前为止我还没有找到正确的推理规则来证明它。我相信它直接来自推理规则应用程序，因为 metis 可以简单地证明它。
我的证明脚本只有以下内容：
apply (rule allI; rename_tac P; rule allI; rename_tac h; rule impI)
apply (rule exI; rule conjI)
让我有目标：
proof (prove)
goal (2 subgoals):
- ⋀P h. ∀x. ¬ P x ⟶ P (h x) ⟹
P (?x17 P h)
- ⋀P h. ∀x. ¬ P x ⟶ P (h x) ⟹
P (h (h (?x17 P h)))
之后我对如何继续感到非常困惑。我可能需要调用排中律，我尝试了以下两种方法：
P x \/ ~ P x(P x /\ ~ P (hx)) \/ ~(P x /\ ~P (hx))
无济于事。
我比 Isabelle/HOL 更熟悉 Coq，但即使在那里我也无法证明这一点（即使有额外的假设，即 P 的参数类型是存在的，并且 classic公理）。
任何线索将不胜感激。
I have the following Isabelle/HOL theorem I'd like to prove:
lemma involution:
"∀P h. (∀x. ¬P x ⟶ P (h x)) ⟶ (∃x. P x ∧ P (h (h x)))"
but I have so far not found the correct inference rules to prove it. I believe it follows from directly from inference rule applications since metis can prove it trivially.
My proof script has only the following:
apply (rule allI; rename_tac P; rule allI; rename_tac h; rule impI)
apply (rule exI; rule conjI)
leaving me with the goal:
proof (prove)
goal (2 subgoals):
- ⋀P h. ∀x. ¬ P x ⟶ P (h x) ⟹
P (?x17 P h)
- ⋀P h. ∀x. ¬ P x ⟶ P (h x) ⟹
P (h (h (?x17 P h)))
after which I'm quite stumped as to how to proceed. I may need some invocation of the law of excluded middle, I tried both:
P x \/ ~ P x(P x /\ ~ P (h x)) \/ ~(P x /\ ~P (h x))
to no avail.
I am more familiar with Coq than Isabelle/HOL but even there I could not prove it (even with the additional assumption that the argument type for P is inhabited, and the classic axiom).
Any clues would be much appreciated.
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
首先，正如您已经提到的，您的引理可以通过 Isabelle 的一些内置证明方法来简单地证明，例如 Isabelle2021-1 中的
blast。然而，由于我猜您正在寻找更具教学意义的答案，因此我将对此进行详细说明。在解决重要结果的证明之前，先用纸笔画出草图通常很有用。这是我想到的一个（也许还有一个更简单的，但出于说明目的，我认为这就足够了）：
我的证明是区分大小写的。让
a为任意但固定的值。然后，下表显示了要考虑的所有案例以及满足结论的相关证人：在上表中，
T、F和?分别代表True、False和“不关心”，虚线箭头表示前提∀x 的实例化。 ØP x ⟶ P (hx)，具体值为x。我们的证明草图到此结束。关于你的引理的 Isabelle/HOL 证明，我认为有一些评论是正确的：
由于最外面的全称量词是多余的，我将从引理语句中删除它们并使用自由变量。
*
_tac策略现在被认为已经过时，Isabelle/Isar（即结构化）证明比apply脚本更受青睐（除了实验阶段）证明）。请参阅Isabelle/Isar参考手册 了解更多详情。现在，请根据上面的证明草图在下面找到您的引理的结构化证明。出于教学目的，我尝试将证明分解为最基本的步骤，并在代码中包含内联注释以帮助读者：
First of all, as you already mentioned, your lemma can be trivially proved by some of the Isabelle's built-in proof methods, e.g.,
blastin Isabelle2021-1. However, since I guess you are looking for a more pedagogical answer, I'll elaborate a bit on it.Before tackling the proof of a non-trivial result, it's often useful to have a pen-and-paper proof sketch first. Here's the one I got off the top of my head (perhaps there's a simpler one, but for illustration purposes I think it will suffice):
My proof is by case distinction. Let
aby an arbitrary but fixed value. Then, the following table shows all the cases to consider and an associated witness that satisfies the conclusion:In the table above,
T,Fand?stands forTrue,Falseand "don't care" respectively, and a dashed arrow represents an instantiation of the premise∀x. ¬P x ⟶ P (h x)with a specific value ofx. This concludes our proof sketch.Regarding an Isabelle/HOL proof for your lemma, I think a few remarks are in order:
Since the outermost universal quantifiers are superfluous, I'll remove them from the lemma statement and use free variables instead.
*
_tactactics are considered obsolete nowadays, and Isabelle/Isar (i.e., structured) proofs are strongly preferred overapply-scripts (except for the experimental stages of a proof). Please refer to the Isabelle/Isar Reference Manual for further details.Now, please find below a structured proof for your lemma, based on the proof sketch above. For pedagogical purposes, I tried to break down the proof to the most elementary steps and included inline comments in the code in order to aid the reader: