Weak Excluded Middle Implies Morgan law for conjunction

user_5339728 0
Viewed 98

I am currently following the book Computational Type Theory and Interactive Theorem Proving with Coq by Gert Smolka and on page 75, there is exercise 9.3.14.b asking me to prove that the 'weak law of excluded middle' defined as:

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

implies the Morgan law for conjunction:

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

i.e.

Lemma L1 : WXM -> MGC
Proof.
Admitted.

I have been trying for solve this for a while now, but with no success. Assuming WXM and ~(X/\Y) for some Prop X Y, faced with the goal ~X \/ ~Y, I did a case analysis (applying WXM on X and Y). Out of the 4 cases, 3 are immediately dispatched but I am left with a 4th cases with additional assumptions ~~X and ~~Y. Intuitively ~~X and ~~Y are saying that X and Y are 'weakly true' and you would hope to conclude that X /\ Y is also weakly true (i.e. show ~~(X/\Y) leading to a contradiction thanks to the assumption ~(X/\Y)). However, I am not able to conclude. I don't want to give up but would also like to move on with the book. Does anyone have the answer to this?.

coq
1 Answers

One does not need to consider the four cases here, because one has negated disjuncts in the goal giving some terms to work with when one chooses which disjunct to prove. Getting e.g. ~ Q and ~ ~ Q cases is enough to prove the lemma.

I'm not sure how to explain this intuition further without just showing the solution.

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.
user_27475110
Related