The Coq mailing list

[Luke Palmer <lrpalmer AT gmail.com>]

On Sat, Apr 11, 2009 at 4:53 PM, emily_p <emilypurfield AT gmail.com> wrote:

Hello,

I am fairly new to Coq and I am not sure if this is the right place to ask
but I am hoping someone can help me. I am having trouble with what I think
should be a simple proof. I am trying to solve the following

forall x, P x^Q x |- (forall x Px) ^(forall x Qx)

I have managed to solve the reverse of this but for this question I can't
seem to complete the proof. I can get to the stage where I have two subgoals
Px0 and Qx0 with the hypothesis forall x : S, Px^Qx but I am not sure how to
combine the goals to get a conjunction. I have used the following to get
this far but I may have gone down the wrong route completely.

intros. split. intro x0. 2: intro x0.

Thanks to anyone who can shed some light on this.

Remember that forall propositions are functions.

intros P Q H.
split ; intro x ; destruct (H x) ; assumption.

The key was destruct (H x); you can eliminate things which are not immediately your hypotheses.  You can take it more granularly and "pose (H x)", which will give you a hypothesis "e : P x /\ Q x".

Luke