The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

> yes but since the forall X, PX comes from a "generalize X Y H4." where
> H4 is an hypothesis, how to introduce parenthesis?

It doesn't sound possible from what you've said, perhaps your proof went 
wrong somewhere earlier.

Gaëtan Gilbert

On 01/10/2019 10:09, richard Dapoigny wrote:
> Thanks for your answer,
>
> Le 01/10/2019 à 00:16, Gaëtan Gilbert a écrit :
> > What do you mean "variables are dummy"?
> they are not related
> > Your statement seems similar to "forall X, P X -> forall Y, P Y" which 
> > is true iff "forall x, P x"
> > maybe you meant to parenthesize as "(forall X, P X) -> forall Y, P Y"?
> yes but since the forall X, PX comes from a "generalize X Y H4." where 
> H4 is an hypothesis, how to introduce parenthesis?
> > Gaëtan Gilbert
> >
> > On 01/10/2019 00:14, richard Dapoigny wrote:
> > > Dear Coq users,
> > >
> > > Assuming classical logic, i have the following goal:
> > >
> > > ∀ X0 Y0 : N,
> > >    (eta X0 Balls ∧ eta Y0 Balls ∧ eta B (el X0) ∧ eta X0 (ext A) ∧ 
> > > eta B (el Y0) ∧ eta Y0 (ext A)  → eta X0 (el Y0) ∨ eta Y0 (el X0))
> > >    → ∀ X'0 Y'0 : N,
> > >        eta X'0 Balls ∧ eta Y'0 Balls ∧ eta B (el X'0) ∧ eta X'0 (ext 
> > > A) ∧ eta B (el Y'0) ∧ eta Y'0 (ext A)  → eta X'0 (el Y'0) ∨ eta Y'0 
> > > (el X'0)
> > >
> > > since variables are dummy, I expect to solve it with classical 
> > > tactics such as eauto, tauto, etc. However none of these seems to 
> > > work. Is anybody has some hints?
> > >
> > > Thanks for your help,
> > >
> > > Richard
> > >
> > > --
> > > *Richard Dapoigny*
> > > /Associate Professor/ - LISTIC Laboratory
> > > University Savoie Mont-Blanc
> > > 5, chemin de Bellevue
> > > Po. Box 80439
> > > Annecy-le-Vieux 74940
> > > FRANCE
> > > https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/ 
> > >
> > >
> > > /****** People who don't know history are condemned to repeat it. 
> > > ******/
> --
> *Richard Dapoigny*
> /Associate Professor/ - LISTIC Laboratory
> University Savoie Mont-Blanc
> 5, chemin de Bellevue
> Po. Box 80439
> Annecy-le-Vieux 74940
> FRANCE
> https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/ 
>
>
> /****** People who don't know history are condemned to repeat it. ******/