How to make use of a hypothesis containing forall in Coq?

Question

I am trying to prove the equivalence of P \/ Q and ~ P -> Q, under the assumption of Excluded Middle,

Theorem eq_of_or :
  excluded_middle ->
  forall P Q : Prop,
    (P \/ Q) <-> (~ P -> Q).

where the Excluded Middle is the following.

Definition excluded_middle := forall P : Prop, P \/ ~ P.

Actually, the proof of one direction does not require the Excluded Middle. In my attempt at proving the other direction, I get stuck when I am trying to utilize the Excluded Middle among the hypotheses,

Proof.
  intros EM P Q. split.
  { intros [H | H]. intros HNP. 
    - unfold not in HNP. exfalso.
      apply HNP. apply H.
    - intros HNP. apply H. }
  { intros H. unfold excluded_middle in EM.
    unfold not in EM. unfold not in H.
  }

where the current environment is the following:

1 subgoal
EM : forall P : Prop, P \/ (P -> False)
P, Q : Prop
H : (P -> False) -> Q
______________________________________(1/1)
P \/ Q

I understand that under such circumstance, what we need to do next is to do something like the "case analysis" of P, including the use of tactics left and right, if my proof makes sense till now.

Thanks in advance for any advice and suggestion!

Anton Trunov Anton Trunov · Accepted Answer · 2017-07-06T09:14:16

You can instantiate EM : forall P : Prop, P \/ ~ P with any proposition (I instantiated it with P below and destructed it immediately), since EM is essentially a function that takes an arbitrary proposition P and returns a proof of either P or ~ P.

Theorem eq_of_or' :
  excluded_middle ->
  forall P Q : Prop, (~ P -> Q) -> P \/ Q.
Proof.
  intros EM P Q.
  destruct (EM P) as [p | np].     (* <- the key part is here *)
  - left. apply p.
  - right.
    apply (H np).
    (* or, equivalently, *)
    Undo.
    apply H.
    apply np.
    Undo 2.
    (* we can also combine two `apply` into one: *)
    apply H, np.
Qed.

How to make use of a hypothesis containing forall in Coq?

1 Answers