如何在 Coq 中使用包含 forall 的假设？

Question

我试图证明 P \/ Q 和 ~ P -> Q 的等价性，在排除中间的假设下，

Theorem eq_of_or :
  excluded_middle ->
  forall P Q : Prop,
    (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

我明白了，在这种情况下，我们接下来要做的就是像P的"case analysis"一样，包括使用战术left和right，如果到目前为止，我的证明是有道理的。

在此先感谢您的任何意见和建议！

Answer 1

你可以用任何命题实例化EM : forall P : Prop, P \/ ~ P（我在下面用P实例化它并立即销毁它），因为 EM 本质上是一个函数，它采用任意命题 P 和 returns 证明 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.

如何在 Coq 中使用包含 forall 的假设？

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

coq

coq-tactic