1

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

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

其中Excluded Middle如下。

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的“案例分析”，包括策略的使用left，right如果我的证明到目前为止还有意义的话。

提前感谢您的任何建议和建议！

4

1 回答 1

2

你可以EM : forall P : Prop, P \/ ~ P用任何命题来实例化（我用P下面的例子来实例化它并立即破坏它），因为 EM它本质上是一个函数，它接受一个任意的命题并返回一个orP的证明。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.
于 2017-07-06T09:14:16.787 回答