Wie um zu beweisen (forall x, P x / \ Q x) -> (forall x, P x) [In Coq]

Question

Wie kann man beweisen (forall x, P x / \ Q x) -> (forall x, P x) in Coq? Versucht, stundenlang und kann nicht herausfinden, wie man die Vorgeschichte zu etwas brechen, die Coq verdauen können. (Ich bin ein newb, offensichtlich:)

Answer 1

Sie können es schneller von nur H Anwendung, aber das Skript sollte mehr klar.

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

Versuchen

elim (H x).

Answer 3

Eigentlich dachte ich, dies heraus, wenn ich das gefunden:

Mathematik für Informatiker 2

In Lektion 5 er genau die gleiche Problem löst und verwendet "schneiden (P x / \ Q x)", die neu schreibt das Ziel von "P x" auf "P x / \ Q x -> P x". Von dort aus können Sie einige Manipulationen tun und wenn das Ziel nur "P x / \ Q x" können Sie sich bewerben "forall x: P x / \ Q x". Und der Rest ist einfach

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, wenn für alle x, P (x) und Q (x) halten, dann für alle x, P (x) gilt.