Comment utiliser une hypothèse contenant forall dans Coq?

Question

Je suis en train de prouver l'équivalence des P \/ Q et ~ P -> Q, dans l'hypothèse de tiers exclu,

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

où le Moyen-exclus est le suivant.

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

En fait, la preuve d'une direction ne nécessite pas le milieu exclu. Dans ma tentative de prouver l'autre sens, je suis bloqué quand je suis en train d'utiliser le tiers exclu parmi les hypothèses,

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. 
    } 

où l'environnement actuel est le suivant:

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

Je comprends que dans de telles circonstances, ce que nous devons faire ensuite est de faire quelque chose comme "l'analyse de cas" de P, y compris l'utilisation de tactiques left et right, si ma preuve a du sens jusqu'à maintenant.

Merci d'avance pour tout conseil et suggestion!

Answer 1

Vous pouvez instancier EM : forall P : Prop, P \/ ~ P toute proposition (j'instancié avec P ci-dessous et DESTRUCTED immédiatement), puisque EM est essentiellement une fonction qui prend une proposition arbitraire P et renvoie une preuve de l'une ou P~ 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.