只是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.

谢谢！