就在COQ证明

Question

另一个硬目标（对我来说，当然）普遍量化hypotesis如下：

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. 

谢谢！