Come provare (forall x, P x / \ Q x) - > (forall x, P x) [In Coq]

Question

Come si dimostra (forall x, P x / \ Q x) - > (forall x, P x) in Coq? Ho provato per ore e non riesco a capire come abbattere l'antecedente a qualcosa che Coq può digerire. (Sono un novizio, ovviamente :)

Answer 1

Puoi farlo più rapidamente semplicemente applicando H, ma questo script dovrebbe essere più chiaro.

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

Prova

elim (H x).

Answer 3

In realtà, l'ho capito quando l'ho trovato:

Mathematics for Computer Scientists 2

Nella lezione 5 risolve esattamente lo stesso problema e usa " cut (P x / \ Q x) " che riscrive l'obiettivo da " P x " a " P x / \ Q x - > P x " ;. Da lì puoi fare alcune manipolazioni e quando l'obiettivo è solo " P x / \ Q x " puoi applicare " forall x: P x / \ Q x " e il resto è semplice.

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))

Intuitivamente, se per tutte le x, P (x) E Q (x) tieni, quindi per tutte le x, P (x).