coq 证明：战术荒谬，它是如何工作的？

Question

我试图理解 coq 中的证明。我很久以前在一个课程中写的，但现在我被荒谬的命令阻止了。这是证据：

Theorem Thm_2 : (~psi -> ~phi) -> (phi -> psi).
Proof.
intro.
intro.
cut (psi \/ ~psi).
intro.
elim H1.
intro.
exact H2.
intro.
absurd phi.
cut (~psi).
exact H.
exact H2.
exact H0.
apply classic.
Qed.

当我使用荒谬的 phi 策略时，我目前的目标是 psi。荒谬的命令将其转化为两个目标：~ phi 和 phi。我的问题是我不知道也不记得这一步背后的逻辑......

感谢您的帮助 ！（好像我不能在我的消息开头添加Hello...抱歉）

Answer 1

• 如果你能证明phi和~ phi，那么你就可以证明False（记住，~ phi := phi -> False）
• 如果你能证明False，那么你就可以证明任何事情，包括你当时的目标

因此absurd phi应用False消元法，并且您是否False通过证明phi和来证明~ phi。