The Coq mailing list

[richard dapoigny <richard.dapoigny AT univ-savoie.fr>]

Le 27/04/2015 16:51, Pierre Courtieu a écrit :
> If I understand well you want to prove:
>
> x : A
> Hi : P x
> ======
> forall y, P y
>
> which is false.
>
> Maybe you should try to prove something else :)
Ok, I do. Thanks.
> Best regards,
> P.
>
>
>
>
> 2015-04-27 16:17 GMT+02:00 richard dapoigny 
> <richard.dapoigny AT univ-savoie.fr>:
> > Le 27/04/2015 15:57, Pierre Courtieu a écrit :
> > > Hi,
> > >
> > > This is no true and therefore not provable.
> > >
> > > But if you add parenthesis over the first quantified part then it is a
> > > different property (and probably the on one you meant?) that is
> > > provable by "intro h; assumption."
> > >
> > > (forall x, (* some complex function depending on x*)) -> forall y, (*
> > > the same complex function depending on y*)
> > >
> > > For examepl:
> > >
> > > Variable A:Type.
> > > Variable P: Type -> Prop.
> > >
> > > Goal (forall x, (P x)) -> (forall y, P y).
> > > Proof.
> > >     intro h.
> > >     assumption.
> > >
> > > Best regards,
> > > Pierre
> > Thanks for the prompt answer!
> > Yes I would like to have the goal you suggest but the problem is that the
> > left part is generated by applying generalize x Hi (wher Hi is another
> > hypothesis) and therefore I cannot obtain the whole expression due to a lack
> > of parentheses
> >
> > > 2015-04-27 15:42 GMT+02:00 richard dapoigny
> > > <richard.dapoigny AT univ-savoie.fr>:
> > > > Hi all,
> > > > I try to demonstrate a goal having the form:
> > > > forall x, (* some complex function depending on x*) -> forall y, (* the
> > > > same
> > > > complex function depending on y*)
> > > > Is there a simple way to do it?
> > > > Thanks in advance,
> > > > Richard