Просто квантор всеобщности hypotesis в 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. 

Спасибо!