Coq：在没有 `contradiction` 策略的情况下证明 `P -> ~P -> Q`？

Question

我正在学习 Coq，我刚刚发现它很有建设性。

这是我可以证明“矛盾蕴含一切”的一种方法，它有效：

Theorem contradiction_implies_anything: forall P Q : Prop, P -> ~P -> Q.
Proof.
  intros P Q p not_p.
  contradiction.
  Qed.

请注意，没有 Q 是 构造的 ，所以我假设 contradiction 是内置在 Coq 证明引擎中的。在我看来，否则就必须证明 Q 是如何构造的，而任何 Q 都是不可能的，因此无法证明上面的定理。特别是我无法在以下（伪）代码中证明上面的定理：

intros P Q p not_p.
introduce P \/ Q. # here I have to construct Q, right?.. that's the point where Coq's "constructivity" becomes an obstruction
introduce ~P \/ Q. # same here
run case analysis on both and figure out that Q must be true.
Qed.

我说得对吗？

Answer 1

contradiction 在这里实际上不是必需的，主要原因有两个：

~ P 是 P -> False 的标准库符号，这意味着如果你有假设 P 和 ~ P，你可以应用 ~ P 到 P 得到 False.
标准库这样定义False：Inductive False : Prop :=.这意味着如果你destruct一个False类型的假设，结果是分析将有零个案。也就是说，你的证明就完成了！

所以，总而言之，你可以像这样证明你的定理：

Theorem contradiction_implies_anything: forall P Q : Prop, P -> ~P -> Q.
Proof.
  intros P Q p not_p.
  apply not_p in p.
  destruct p.
Qed.

Answer 2

在Coq中，否定定义如下：

Inductive False : Prop := 
  (* An inductive proposition with no constructors *). 
Definition not (P : Prop) : Prop := P -> False.

您证明的引理是以下更原始原理的结果：

Lemma exfalso (Q : Prop) : False -> Q.
Proof. intros contra. destruct contra. Qed.

直觉上，如果我们知道一个归纳命题 P 成立并且我们想证明其他一些 Q 也成立，我们需要做的就是考虑所有可能具有的构造函数已应用于建立 P。这就是 destruct 策略的作用。但是当P是False时，没有构造函数，所以我们什么都不用做。

我喜欢这种情况的事情如下：并不是这个过程构建了 Q 的证明，而是我们在那里展示了我们不必构建任何东西。

鉴于 exfalso，很容易用更原始的术语证明你的原始陈述（我建议你通过这个证明看看发生了什么！）：

Goal forall P Q : Prop, P -> ~P -> Q.
Proof.
intros P Q Hyes Hno.
apply exfalso. apply Hno. apply Hyes.
Qed.

Coq：在没有 `contradiction` 策略的情况下证明 `P -> ~P -> Q`？

Coq: proving `P -> ~P -> Q` without `contradiction` tactic?

coq

coq-tactic