只是 coq 证明中的一个普遍量化的假设答案

【问题标题】：Just a universally quantified hypotesis in coq proof只是 coq 证明中的一个普遍量化的假设
【发布时间】：2013-10-03 22:17:56
【问题描述】：

另一个艰巨的目标（当然是对我而言）如下：

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

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

我认为它存在管理此类情况的标准方法，但我无法找到它。

【问题讨论】：

标签： universal coq quantifiers

【解决方案1】：

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.

谢谢！

【讨论】：

【解决方案2】：

要在该证明中取得进展，您必须展示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（您选择名称）。

【讨论】：