The Coq mailing list

[fdabrows AT irisa.fr]

Hi,

you can try (it applies the same tactics to both subgoals)

         split; (intro; destruct (H x); assumption).

or having coq helping you
         split; (intro; apply (H x)).

Hope this helps,
Frédéric.

>
> 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.
>
> Emily
> --
> View this message in context:
> http://www.nabble.com/Proof-Help-tp23006221p23006221.html
> Sent from the Coq mailing list archive at Nabble.com.
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>