Как доказать (forall x, P x/\ Q x) -> (forall x, P x) [In Coq]

Question

Как доказать (forall x, P x/\ Q x) -> (forall x , P x) в Coq? Старался часами и не мог понять, как сломать антецедента на то, что Coq может переварить. (Я Newb, очевидно :)

Answer 1

Вы можете сделать это быстрее, просто применив H, но этот сценарий должен быть более понятным.

Lemma foo : forall (A:Type) (P Q: A-> Prop), (forall x, P x /\ Q x) -> (forall x, P x). 
intros. 
destruct (H x). 
exact H0. 
Qed. 

Answer 2

Попробуйте

elim (H x). 

Answer 3

На самом деле, я полагал, что это один из, когда я нашел это:

Mathematics for Computer Scientists 2

В уроке 5 он решает точный та же проблема и использует «cut (P x/\ Q x)», который переписывает цель с «P x» на «P x/\ Q x -> P x». Оттуда вы можете сделать некоторые манипуляции, и когда цель будет просто «P x/\ Q x», вы можете применить «forall x: P x/\ Q x», а остальная - просто.

Answer 4

Assume ForAll x: P(x) /\ Q(x) 
    var x; 
     P(x) //because you assumed it earlier 
    ForAll x: P(x) 
(ForAll x: P(x) /\ Q(x)) => (ForAll x: P(x)) 

Intuitivly, если для всех х, Р (х) и Q (х), то для всех х, Р (х) имеет место.