LOGIC

LOGIC IN COQ

Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality".
From LF Require Export Tactics.

我们已经看到了许多事实主张（命题）的例子，以及证明其真实性的方法（证据）。特别是，我们广泛研究了等式命题（e1=e2）、含义（P→ Q） ，以及量化命题(∀ x、 P）。在本章中，我们将看到如何使用Coq进行其他常见形式的逻辑推理。

在深入讨论细节之前，让我们先谈谈Coq中数学语句的状态。回想一下，Coq是一种类型化语言，这意味着其世界中的每个合理表达式都有一个关联的类型。逻辑主张也不例外：我们可能试图在Coq中证明的任何陈述都有一种类型，即Prop，命题的类型。我们可以通过Check命令看到这一点：

Check (3 = 3) : Prop.

Check (forall n m : nat, n + m = m + n) : Prop.

请注意，所有语法形式良好的命题在Coq中都有类型Prop，无论它们是否为真。

简单地成为一个命题是一回事；可证明是另一回事！

Check 2 = 2 : Prop.

Check 3 = 2 : Prop.

Check forall n : nat, n = 2 : Prop.

事实上，命题不仅有类型：它们是一流的实体，可以像Coq世界中的任何其他事物一样进行操纵。

到目前为止，我们已经看到了命题可以出现的一个主要位置：在定理（引理和例子）声明中。

Theorem plus_2_2_is_4

Theorem plus_2_2_is_4 :
  2 + 2 = 4.
Proof. reflexivity.  Qed.

但命题可以用在许多其他方面。例如，我们可以使用定义为命题命名，就像我们为其他类型的表达式命名一样。

Definition plus_claim : Prop

Definition plus_claim : Prop := 2 + 2 = 4.
Check plus_claim : Prop.

我们以后可以在任何需要命题的情况下使用这个名称——例如，在定理声明中的声明。

Theorem plus_claim_is_true

Theorem plus_claim_is_true :
  plus_claim.
Proof. reflexivity.  Qed.

我们还可以编写参数化命题——也就是说，接受某种类型的参数并返回命题的函数。

例如，以下函数获取一个数字并返回一个命题，断言该数字等于三：

Definition is_three (n : nat) : Prop

Definition is_three (n : nat) : Prop :=
  n = 3.
Check is_three : nat -> Prop.

在Coq中，返回命题的函数被称为定义其参数的属性。

例如，这里有一个（多态）属性定义了人们熟悉的***函数的概念。

Definition injective {A B} (f : A -> B)

Definition injective {A B} (f : A -> B) :=
  forall x y : A, f x = f y -> x = y.

相等运算符=也是一个返回属性的函数。

表达式n=m是等式n m的语法糖（在Coq的标准库中使用符号机制定义）。由于eq可用于任何类型的元素，因此它也是多态的：

Check @eq : forall A : Type, A -> A -> Prop.

（请注意，我们编写了@eq而不是eq：eq的类型参数A声明为隐式，我们需要关闭此隐式参数的推断以查看eq的完整类型。）

Logical Connectives

Conjunction

命题A和命题B的连词或逻辑and写为A∧ B、 代表A和B都是真实的主张。

Example and_example : 3 + 4 = 7 /\ 2 * 2 = 4.

要证明连词，请使用拆分策略。它将生成两个子目标，每个子目标对应于语句的每个部分：

Proof.
  split.
  - (* 3 + 4 = 7 *) reflexivity.
  - (* 2 * 2 = 4 *) reflexivity.
Qed.

对于任何命题A和命题B，如果我们假设A为真，B为真，我们可以得出结论A∧ B也是正确的。

Lemma and_intro

Lemma and_intro : forall A B : Prop, A -> B -> A /\ B.
Proof.
  intros A B HA HB. split.
  - apply HA.
  - apply HB.
Qed.

由于将带有假设的定理应用于某个目标会产生与该定理的假设数量相同的子目标，因此我们可以应用和介绍来实现与拆分相同的效果。

Example and_example' : 3 + 4 = 7 /\ 2 * 2 = 4.
Proof.
  apply and_intro.
  - (* 3 + 4 = 7 *) reflexivity.
  - (* 2 + 2 = 4 *) reflexivity.
Qed.

Exercise: 2 stars, standard (and_exercise)

Example and_exercise :
  forall n m : nat, n + m = 0 -> n = 0 /\ m = 0.
Proof.
  (* FILL IN HERE *) Admitted.

Solution

证明连词陈述就到此为止。为了向另一个方向发展——也就是说，使用连接假设来帮助证明其他东西——我们采用了自毁策略。

如果证明上下文包含形式a的假设H∧ B、 将析构函数H写成[HA HB]将从上下文中删除H，并添加两个新假设：HA，声明A为真，HB，声明B为真。

Lemma and_example2

Lemma and_example2 :
  forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
Proof.
  (* WORKED IN CLASS *)
  intros n m H.
  destruct H as [Hn Hm].
  rewrite Hn. rewrite Hm.
  reflexivity.
Qed.

通常，我们在引入H时也可以对其进行解构，而不是先引入然后解构：

Lemma and_example2' :
  forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
Proof.
  intros n m [Hn Hm].
  rewrite Hn. rewrite Hm.
  reflexivity.
Qed.

你可能想知道为什么我们费心把两个假设n=0和m=0组合成一个连词，因为我们也可以用两个独立的前提来说明这个定理：

  forall n m : nat, n = 0 -> m = 0 -> n + m = 0.
Proof.
  intros n m Hn Hm.
  rewrite Hn. rewrite Hm.
  reflexivity.
Qed.

对于这个特定的定理，这两个公式都很好。但是理解如何使用连接词假设很重要，因为连接词通常产生于证明的中间步骤，尤其是在更大的发展中。下面是一个简单的例子：

Lemma and_example3

Lemma and_example3 :
  forall n m : nat, n + m = 0 -> n * m = 0.
Proof.
  (* WORKED IN CLASS *)
  intros n m H.
  apply and_exercise in H.
  destruct H as [Hn Hm].
  rewrite Hn. reflexivity.
Qed.

连接词的另一个常见情况是我们知道∧ 但在某些情况下，我们只需要A或B。在这种情况下，我们可以进行析构函数（可能作为介绍的一部分）并使用下划线模式来表示不需要的连接词应该被丢弃。

Lemma proj1

Lemma proj1 : forall P Q : Prop,
  P /\ Q -> P.
Proof.
  intros P Q HPQ.
  destruct HPQ as [HP _].
  apply HP.  Qed.

Exercise: 1 star, standard, optional (proj2)

Lemma proj2 : forall P Q : Prop,
  P /\ Q -> Q.
Proof.
  (* FILL IN HERE *) Admitted.

Lemma proj2

Lemma proj2 : forall P Q : Prop,
  P /\ Q -> Q.
Proof.
  intros P Q HPQ.
  destruct HPQ as [_ HQ].
  apply HQ.  
Qed.

最后，我们有时需要重新安排连接的顺序和/或多路连接的分组。下面的交换性和结合性定理在这种情况下很方便。

Theorem and_commut

Theorem and_commut : forall P Q : Prop,
  P /\ Q -> Q /\ P.
Proof.
  intros P Q [HP HQ].
  split.
    - (* left *) apply HQ.
    - (* right *) apply HP.  Qed.

Exercise: 2 stars, standard (and_assoc)

（在下面的关联性证明中，请注意嵌套的intros模式如何将假设H:分解为HP:P、HQ:Q和HR:R。从那里完成证明。）

Theorem and_assoc : forall P Q R : Prop,
  P /\ (Q /\ R) -> (P /\ Q) /\ R.
Proof.
  intros P Q R [HP [HQ HR]].
  (* FILL IN HERE *) Admitted.

Theorem and_assoc

Theorem and_assoc : forall P Q R : Prop,
  P /\ (Q /\ R) -> (P /\ Q) /\ R.
Proof.
  intros P Q R [HP [HQ HR]].
  split. 
  split.
  - apply HP.
  - apply HQ.
  - apply HR.
Qed.

顺便说一下，中缀符号∧ 实际上只是A和B的语法糖。也就是说，是一个Coq算子，它把两个命题作为参数，并产生一个命题。

Check and : Prop → Prop → Prop.

Disjunction

另一个重要的连接词是两个命题的析取或逻辑or：A∨B当A或B为真时为真。（此中缀符号表示 or A B，其中或：Prop→ Prop→ Prop。）

为了在证明中使用析取假设，我们进行案例分析（与其他数据类型（如nat）一样，可以使用析构函数显式地完成，也可以使用导入模式隐式地完成）：

Lemma factor_is_O

Lemma factor_is_O:
  forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
Proof.
  (* This pattern implicitly does case analysis on
     [n = 0 \/ m = 0] *)
  intros n m [Hn | Hm].
  - (* Here, [n = 0] *)
    rewrite Hn. reflexivity.
  - (* Here, [m = 0] *)
    rewrite Hm. rewrite <- mult_n_O.
    reflexivity.
Qed.

相反，为了证明析取成立，只需证明析取的一条边成立即可。这是通过左右两种策略实现的。正如他们的名字所暗示的，第一个要求证明析取的左侧，而第二个要求证明析取的右侧。这里有一个小用途。。。

Lemma or_intro_l

Lemma or_intro_l : forall A B : Prop, A -> A \/ B.
Proof.
  intros A B HA.
  left.
  apply HA.
Qed.

... 这里有一个稍微有趣的例子，需要左和右：

Lemma zero_or_succ :
  forall n : nat, n = 0 \/ n = S (pred n).
Proof.
  (* WORKED IN CLASS *)
  intros [|n'].
  - left. reflexivity.
  - right. reflexivity.
Qed.

Exercise: 1 star, standard (mult_is_O)

Lemma mult_is_O :
  forall n m, n * m = 0 -> n = 0 \/ m = 0.
Proof.
  (* FILL IN HERE *) Admitted.

Lemma mult_is_O

Lemma mult_is_O :
  forall n m, n * m = 0 -> n = 0 \/ m = 0.
Proof.
  intros.
  destruct n as [| n'].
  - left. reflexivity.
  - destruct m as [| m'].
    + right. reflexivity.
    + inversion H.
Qed.

Exercise: 1 star, standard (or_commut)

Theorem or_commut : forall P Q : Prop,
  P \/ Q  -> Q \/ P.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem or_commut

Theorem or_commut : forall P Q : Prop,
  P \/ Q  -> Q \/ P.
Proof.
  intros.
  destruct H as [Hl | Hr].
  - right. 
    apply Hl.
  - left.
    apply Hr.
Qed.

Falsehood and Negation

到目前为止，我们主要关注的是证明某些事情是真的——加法是交换的，附加列表是关联的，等等。当然，我们也可能对否定结果感兴趣，证明某些给定命题是不真的。这样的语句用逻辑否定运算符表示。

要想了解否定是如何工作的，回想一下战术一章中的爆炸原理，它断言，如果我们假设一个矛盾，那么任何其他命题都可以推导出来。根据这一直觉，我们可以将P（“非P”）定义为∀ Q、 P→ Q

Coq实际上做出了一个稍微不同（但相当）的选择，将P定义为P→ False，其中False是标准库中定义的特定矛盾命题。

Module MyNot.

Definition not (P:Prop)

Definition not (P:Prop) := P -> False.

Notation "~ x"

Notation "~ x" := (not x) : type_scope.

Check not : Prop -> Prop.

End MyNot.

由于虚假是一个矛盾的命题，爆炸原理也适用于它。如果我们在证明上下文中得到False，我们可以对其使用析构函数来完成任何目标：

Theorem ex_falso_quodlibet

Theorem ex_falso_quodlibet : forall (P:Prop),
  False -> P.
Proof.
  (* WORKED IN CLASS *)
  intros P contra.
  destruct contra.  Qed.

拉丁文ex-falso quodlibet的字面意思是，“从谎言中，你喜欢什么就跟什么”；这是爆炸原理的另一个常见名称。

Exercise: 2 stars, standard, optional (not_implies_our_not)

Fact not_implies_our_not : forall (P:Prop),
  ~ P -> (forall (Q:Prop), P -> Q).
Proof.
  (* FILL IN HERE *) Admitted.

Fact not_implies_our_not

Fact not_implies_our_not : forall (P:Prop),
  ~ P -> (forall (Q:Prop), P -> Q).
Proof.
intros.
destruct H.
apply H0.
Qed.

不等式是否定语句的一个非常常见的例子，它有一个特殊的符号x≠ y:

Notation "x <> y"

Notation "x <> y" := (~(x = y)).

我们可以使用not来声明0和1是nat的不同元素：

Theorem zero_not_one

Theorem zero_not_one : 0 <> 1.
Proof.
  (** The proposition [0 <> 1] is exactly the same as
      [~(0 = 1)], that is [not (0 = 1)], which unfolds to
      [(0 = 1) -> False]. (We use [unfold not] explicitly here
      to illustrate that point, but generally it can be omitted.) *)
  unfold not.
  (** To prove an inequality, we may assume the opposite
      equality... *)
  intros contra.
  (** ... and deduce a contradiction from it. Here, the
      equality [O = S O] contradicts the disjointness of
      constructors [O] and [S], so [discriminate] takes care
      of it. *)
  discriminate contra.
Qed.

在Coq中使用否定需要一些练习。尽管你能很好地理解为什么一个包含否定的陈述是正确的，但要让Coq理解它，一开始可能有点棘手！以下是一些让你热身的熟悉事实的证据。

Theorem not_False

Theorem not_False :
  ~ False.
Proof.
  unfold not.
  intros H.
  destruct H. 
Qed.

Theorem contradiction_implies_anything

Theorem contradiction_implies_anything : forall P Q : Prop,
  (P /\ ~P) -> Q.
Proof.
  (* WORKED IN CLASS *)
  intros P Q [HP HNA]. 
  unfold not in HNA.
  apply HNA in HP. 
  destruct HP.  
Qed.

Theorem double_neg

Theorem double_neg : forall P : Prop,
  P -> ~~P.
Proof.
  (* WORKED IN CLASS *)
  intros P H.
  unfold not.
  intros G. 
  apply G. 
  apply H.  
Qed.

Exercise: 2 stars, advanced (double_neg_inf)

写一份双负的非正式证明：

定理：P意味着~~~P，对于任何命题P。

(* FILL IN HERE *)
(* Do not modify the following line: *)
Definition manual_grade_for_double_neg_inf : option (nat×string) := None.

Exercise: 2 stars, standard, especially useful (contrapositive)

Theorem contrapositive : forall (P Q : Prop),
  (P -> Q) -> (~Q -> ~P).
Proof.
  (* FILL IN HERE *) Admitted.

Theorem contrapositive

Theorem contrapositive : forall (P Q : Prop),
  (P -> Q) -> (~Q -> ~P).
Proof.
  intros.
  unfold not.
  intros.
  destruct H0.
  apply H.
  apply H1.
Qed.

Exercise: 1 star, standard (not_both_true_and_false)

Theorem not_both_true_and_false : forall P : Prop,
  ~ (P /\ ~P).
Proof.
  (* FILL IN HERE *) Admitted.

Theorem not_both_true_and_false

Theorem not_both_true_and_false : forall P : Prop,
  ~ (P /\ ~P).
Proof.
  intros.
  unfold not.
  intros.
  inversion H.
  apply H1.
  apply H0.
Qed.

Exercise: 1 star, advanced (informal_not_PNP)

用英语写一个命题的非正式证明∀ P:Prop，~（P∧ （P）。

(* FILL IN HERE *)

(* Do not modify the following line: *)
Definition manual_grade_for_informal_not_PNP : option (nat*string) := None.

由于不平等性涉及否定，因此也需要一些练习才能流利地处理它。这里有一个有用的技巧。如果您试图证明一个无意义的目标（例如，目标状态为false=true），请应用ex_falso_quodlibet将目标更改为false。这使得在上下文中可以更容易地使用表格P的假设——特别是形式x≠y的假设。

Theorem not_true_is_false

Theorem not_true_is_false : forall b : bool,
  b <> true -> b = false.
Proof.
  intros b H.
  destruct b eqn:HE.
  - (* b = true *)
    unfold not in H.
    apply ex_falso_quodlibet.
    apply H. reflexivity.
  - (* b = false *)
    reflexivity.
Qed.

由于使用ex_falso_quodlibet进行推理非常常见，Coq提供了一个内置的策略exfalso来应用它。

Theorem not_true_is_false' : forall b : bool,
  b <> true -> b = false.
Proof.
  intros [] H.          (* note implicit [destruct b] here *)
  - (* b = true *)
    unfold not in H.
    exfalso.                (* <=== *)
    apply H. reflexivity.
  - (* b = false *) reflexivity.
Qed.

Truth

除了False，Coq的标准库还定义了True，这是一个非常正确的命题。为了证明这一点，我们使用预定义的常数I:True：

Lemma True_is_true

Lemma True_is_true : True.
Proof. apply I. Qed.

与广泛使用的False不同，True的使用相对较少，因为作为一个目标进行证明并不重要（因此也不有趣），相反，它没有提供任何有用的信息作为假设。但是，当使用条件或作为高阶Props的参数来定义复杂的Props时，它可能非常有用。稍后我们将看到示例。

例如，我们可以演示如何在不使用歧视策略的情况下实现与歧视策略类似的效果。

模式匹配允许我们为不同的构造函数做不同的事情。如果应用两个不同构造函数的结果假设相等，那么我们可以使用match将不可证明语句（如False）转换为可证明语句（如True）。

Definition disc_fn (n: nat) : Prop

Definition disc_fn (n: nat) : Prop :=
  match n with
  | O => True
  | S _ => False
  end.

Theorem disc

Theorem disc : forall n, ~ (O = S n).
Proof.
  intros n H1.
  assert (H2 : disc_fn O). { simpl. apply I. }
  rewrite H1 in H2. simpl in H2. apply H2.
Qed.

为了将其推广到其他构造函数，我们只需提供disc_fn的适当推广。为了把它推广到其他结论，我们可以用exfalso来代替它们。但内在的歧视为我们解决了所有这些问题。

Logical Equivalence

方便的“当且仅当”连接词断言两个命题具有相同的真值，它只是两个含义的结合。

Module MyIff.

Definition iff (P Q : Prop)

Definition iff (P Q : Prop) := (P -> Q) /\ (Q -> P).

Notation "P <-> Q"

Notation "P <-> Q" := (iff P Q)
                      (at level 95, no associativity)
                      : type_scope.

End MyIff.

Theorem iff_sym

Theorem iff_sym : forall P Q : Prop,
  (P <-> Q) -> (Q <-> P).
Proof.
  (* WORKED IN CLASS *)
  intros P Q [HAB HBA].
  split.
  - (* -> *) apply HBA.
  - (* <- *) apply HAB.  Qed.

Lemma not_true_iff_false

Lemma not_true_iff_false : forall b,
  b <> true <-> b = false.
Proof.
  (* WORKED IN CLASS *)
  intros b. split.
  - (* -> *) apply not_true_is_false.
  - (* <- *)
    intros H. rewrite H. intros H'. discriminate H'.
Qed.

Exercise: 1 star, standard, optional (iff_properties)

以上面关于[<->]是对称的（[iff_-sym]）的证明为指导，证明它也是自反的和传递的。

Theorem iff_refl : forall P : Prop,
  P <-> P.
Proof.
  (* FILL IN HERE *) Admitted.

Theorem iff_trans : forall P Q R : Prop,
  (P <-> Q) -> (Q <-> R) -> (P <-> R).
Proof.
  (* FILL IN HERE *) Admitted.
(** [] *)

Theorem iff_refl

Theorem iff_refl : forall P : Prop,
  P <-> P.
Proof.
  intros.
  split;
  intros;
  apply H.
Qed.

Theorem iff_trans

Theorem iff_trans : forall P Q R : Prop,
  (P <-> Q) -> (Q <-> R) -> (P <-> R).
Proof.
intros.
split.
- intros. apply H0. apply H. apply H1.
- intros. apply H. apply H0. apply H1.
Qed.

Exercise: 3 stars, standard (or_distributes_over_and)

Theorem or_distributes_over_and : forall P Q R : Prop,
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
  (* FILL IN HERE *) Admitted.

Theorem or_distributes_over_and

Theorem or_distributes_over_and : forall P Q R : Prop,
  P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R).
Proof.
intros.
split.
- intros. inversion H. split; left; apply H0.
-- inversion H0. split.
--- right. apply H1.
--- right. apply H2.
- intros. inversion H. inversion H0. apply or_commut in H0. apply or_commut in H1.
inversion H0. inversion H1.
-- left. apply H2.
-- left. apply H2.
-- left. apply H2.
-- inversion H1.
---  left. apply H3.
--- right. split.
---- apply H2.
---- apply H3. 
Qed.

Setoids and Logical Equivalence

Coq的一些策略专门处理iff语句，避免了一些低级证明状态操作的需要。特别是，重写和自反性可以用于iff语句，而不仅仅是等式。要启用此行为，我们必须导入支持它的Coq库：

From Coq Require Import Setoids.Setoid.

“setoid”是具有等价关系的集合，即自反、对称和传递的关系。当一个集合中的两个元素根据关系相等时，可以使用“重写”将一个元素替换为另一个元素。我们已经看到了等式关系=在Coq中：当x=y时，我们可以使用rewrite将x替换为y，反之亦然。

同样，逻辑等价关系↔ 是自反的，对称的，传递的，所以我们可以用它来替换命题的一部分：如果P↔ Q、 然后我们可以使用重写将P替换为Q，反之亦然。

下面是一个简单的例子，演示了这些战术如何与敌我识别一起工作。首先，让我们证明几个基本的iff等价。

Lemma mul_eq_0

Lemma mul_eq_0 : forall n m, n * m = 0 <-> n = 0 \/ m = 0.
Proof.
  split.
  - apply mult_is_O.
  - apply factor_is_O.
Qed.

Theorem or_assoc

Theorem or_assoc :
  forall P Q R : Prop, P \/ (Q \/ R) <-> (P \/ Q) \/ R.
Proof.
  intros P Q R. split.
  - intros [H | [H | H]].
    + left. left. apply H.
    + left. right. apply H.
    + right. apply H.
  - intros [[H | H] | H].
    + left. apply H.
    + right. left. apply H.
    + right. right. apply H.
Qed.

我们现在可以使用这些事实，通过重写和自反性，对涉及等价性的陈述给出平滑的证明。例如，以下是先前mult_0结果的三元版本：

Lemma mul_eq_0_ternary

Lemma mul_eq_0_ternary :
  forall n m p, n * m * p = 0 <-> n = 0 \/ m = 0 \/ p = 0.
Proof.
  intros n m p.
  rewrite mul_eq_0. rewrite mul_eq_0. rewrite or_assoc.
  reflexivity.
Qed.

应用策略也可以用于↔. 当给定一个等价物作为其参数时，apply尝试猜测等价物的哪个方向是有用的。

Lemma apply_iff_example

Lemma apply_iff_example :
  forall n m : nat, n * m = 0 -> n = 0 \/ m = 0.
Proof.
  intros n m H. apply mul_eq_0. apply H.
Qed.

Existential Quantification

另一个重要的逻辑连接词是存在量化。要说存在一些类型为T的x，使得某些属性P保持x，我们写∃ x:T，P.和∀, 如果Coq能够从上下文推断x的类型，那么类型注释：T可以省略。

证明表格的陈述∃ x、 P，我们必须证明P对于x的某些特定值选择是成立的，被称为存在论的见证。这是通过两个步骤完成的：首先，我们通过调用策略明确地告诉Coq我们想到的证人t∃ t、 然后我们证明了当x的所有出现被t替换后，P成立。

Definition Even x

Definition Even x := exists n : nat, x = double n.

Lemma four_is_even

Lemma four_is_even : Even 4.
Proof.
  unfold Even. exists 2. reflexivity.
Qed.

相反，如果我们有一个存在的假设∃ x、 在上下文中，我们可以对它进行分解，得到一个证人x和一个假设，表明P持有x。

Theorem exists_example_2

Theorem exists_example_2 : forall n,
  (exists m, n = 4 + m) ->
  (exists o, n = 2 + o).
Proof.
  (* WORKED IN CLASS *)
  intros n [m Hm]. (* note implicit [destruct] here *)
  exists (2 + m).
  apply Hm.  Qed.

Exercise: 1 star, standard, especially useful (dist_not_exists)

证明“P对所有x都成立”意味着“没有P不成立的x”（提示：当[Xe]在存在假设下工作时，析构函数H！）

Theorem dist_not_exists : forall (X:Type) (P : X -> Prop),
  (forall x, P x) -> ~ (exists x, ~ P x).
Proof.
  (* FILL IN HERE *) Admitted.

Theorem dist_not_exists

Theorem dist_not_exists : forall (X:Type) (P : X -> Prop),
  (forall x, P x) -> ~ (exists x, ~ P x).
Proof.
intros. unfold not. intros. destruct H0. apply H0. apply H. 
Qed.

Exercise: 2 stars, standard (dist_exists_or)

证明存在量化分布在析取上。

Theorem dist_exists_or : forall (X:Type) (P Q : X -> Prop),
  (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof.
   (* FILL IN HERE *) Admitted.

Theorem dist_exists_or

Theorem dist_exists_or : forall (X:Type) (P Q : X -> Prop),
  (exists x, P x \/ Q x) <-> (exists x, P x) \/ (exists x, Q x).
Proof.
  intros.
  split.
  - intros.
    destruct H as [x Hx].
    destruct Hx.
    + left. exists x. apply H.
    + right. exists x. apply H.
  - intros.
    destruct H.
    + destruct H as [x Hx].
      exists x.
      left.
      apply Hx.
    + destruct H as [x Hx].
      exists x.
      right.
      apply Hx.
Qed.