就在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. 

謝謝！