Coqにforallを含む仮説を使用するにはどうすればよいですか？

Question

私は、除外された中東の仮定の下で、除外された中東は次の通りである

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

をP \/ Qと~ P -> Qの等価性を証明しようとしています。

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

実際、一方向の証明には除外された中間は必要ありません。他の方向を証明で私の試みで、私は仮説の中で除外中東を利用しようとしていたとき、私は動けなく、現在の環境は以下の通りです

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

：

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

私がいることを理解してそのような状況の下で私たちが次に行う必要があるのは、私の証拠が今まで意味をなさなければ、戦術leftとrightの使用を含む、Pの「ケース分析」のようなことをすることです。

アドバイスとアドバイスをお寄せいただきありがとうございます！

Answer 1

EMは、本質的に任意の命題Pをとり、P又は~ Pのいずれかの証拠を返す関数であるので、あなたは、（私は以下Pとそれをインスタンス化し、すぐに破壊）任意の命題とEM : forall P : Prop, 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.