Como provar (forall x, P x / \ Q x) -> (forall x, P x) [Em Coq]

Question

Como se provar (forall x, P x / \ Q x) -> (forall x, P x) em Coq? Tentado por horas e não pode descobrir como quebrar o antecedente a algo que Coq pode digerir. (Eu sou um newb, obviamente:)

Answer 1

Você pode fazê-lo mais rapidamente, apenas aplicando H, mas este script deve ser mais clara.

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

Tente

elim (H x).

Answer 3

Na verdade, eu descobri um presente para fora quando eu encontrei isto:

Matemática para cientistas da computação 2

Na lição 5 ele resolve exatamente o mesmo problema e usos "cut (P x / \ Q X)", que re-escreve o objetivo de "P x" para "P x / \ Q x -> P x". De lá você pode fazer algumas manipulações e quando o objetivo é apenas "P x / \ Q x" você pode aplicar. "Forall x: P x / \ Q x" eo resto é simples

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, se para todo x, P (x) e Q (x) espera, em seguida, para todo x, P (x) vale.