universal - 只是 coq 证明中普遍量化的假设

Question

另一个艰难的目标（当然对我来说）如下：

Goal ~(forall P Q: nat -> Prop,
  (exists x, P x) /\ (exists x, Q x) ->
  (exists x, P x /\ Q x)).
Proof.

我完全不知道我能做什么。如果我引入一些东西，我会在假设中得到一个全称量词，然后我不能用它做任何事情。

我想它存在管理这种情况的标准方法，但我无法找到它。

Answer 1

要在该证明中取得进展，您将必须展示一个实例P和一个实例，Q以便您的假设产生矛盾。

一个简单的方法是使用：

P : fun x => x = 0
Q : fun x => x = 1

为了处理引入的假设，您可能需要使用以下策略specialize：

Goal ~(forall P Q : nat -> Prop,
  (exists x, P x) /\ (exists x, Q x) ->
  (exists x, P x /\ Q x)).
Proof.
  intro H.
  specialize (H (fun x => x = 0) (fun x => x = 1)).

它允许您在某些输入上应用您的假设之​​一（当假设是一个函数时）。从现在开始，你应该能够很容易地推导出一个矛盾。

或者specialize，您还可以执行以下操作：

  pose proof (H (fun x => x = 0) (fun x => x = 1)) as Happlied.

这将保留 H 并Happlied为应用程序提供另一个术语（您选择名称）。

Answer 2

Ptival 的回答成功了。以下是完整证明的代码：

Goal ~(forall P Q: nat -> Prop,
  (exists x, P x) /\ (exists x, Q x) ->
  (exists x, P x /\ Q x)).
Proof.
  unfold not. intros.
  destruct (H (fun x => x = 0) (fun x => x = 1)).
    split.
      exists 0. reflexivity.
      exists 1. reflexivity.
    destruct H0. rewrite H0 in H1. inversion H1.
Qed.

谢谢！