Comment prouver (pour tout x, P x / \ Q x) - > (pour tout x, P x) [en Coq]

Question

Comment prouver (pour tout x, P x / \ Q x) - > (pour tout x, P x) en Coq? Cela fait des heures que nous essayons et nous ne savons pas comment éliminer l'antécédent de quelque chose que Coq peut digérer. (Je suis un newb, évidemment:)

Answer 1

Vous pouvez le faire plus rapidement en appliquant simplement H, mais ce script devrait être plus clair.

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

Essayez

elim (H x).

Answer 3

En fait, j'ai découvert celui-ci quand j'ai découvert ceci:

Mathématiques pour informaticiens 2

Dans la leçon 5, il résout exactement le même problème et utilise "cut (P x / \ Q x)". qui réécrit le but de " P x " à " P x / \ Q x - > P x ". À partir de là, vous pouvez effectuer certaines manipulations et lorsque l'objectif est simplement "P x / \ Q x". vous pouvez appliquer " forall x: P x / \ Q x " et le reste est simple.

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

Intuitivement, si pour tout x, P (x) ET Q (x) sont valides, alors pour tout x, P (x) sont valides.