coq - 弱排除中间意味着摩根定律的合取

Question

我目前正在阅读 Gert Smolka 的书Computational Type Theory and Interactive Theorem Proving with Coq，第 75 页上有一个练习 9.3.14.b 要求我证明“弱排中律”定义为:

Definition WXM : Prop := forall (X:Prop), ~X \/ ~~X.

暗示摩根定律的合取:

Definition MGC : Prop := forall (X Y:Prop), ~(X/\Y) -> ~X \/ ~Y.      (* <- always true *)

即

Lemma L1 : WXM -> MGC
Proof.
Admitted.

我已经尝试解决这个问题有一段时间了，但没有成功。假设WXM 和 ~(X/\Y) 对于一些 Prop X Y，面对目标 ~ X\/~Y，我做了一个案例 分析(在 X 和 Y 上应用 WXM)。在 4 个案例中，有 3 个是立即调度的，但我留下了第 4 个案例，并附加了 ~~X 和 ~~Y 的假设。 直观上 ~~X 和 ~~Y 表示 X 和 Y 是“弱真”，你会希望得出结论 X//Y 也是弱真(即，由于假设 ~( 而显示 ~~(X/\Y) 导致矛盾X/\Y))。然而，我无法下结论。 我不想放弃，但也想继续读这本书。有谁知道这个问题的答案吗？

Answer 1

这里不需要考虑这四种情况，因为人们已经否定了目标中的析取，从而在选择要证明哪个析取时可以使用一些术语。得到例如~Q 和 ~~Q 案例足以证明引理。

我不确定如何在不展示解决方案的情况下进一步解释这种直觉。

Goal
  (forall P : Prop, ~ P \/ ~ ~ P) ->
  (forall P Q : Prop, ~ (P /\ Q) -> ~ P \/ ~ Q).
Proof.
intros wlem P Q npq.
destruct (wlem Q) as [nq | nnq].
- right; trivial.
- left; intros p.
  apply nnq; intros q.
  apply npq; split; trivial.
Qed.