The Coq mailing list

[richard Dapoigny <richard.dapoigny AT univ-smb.fr>]

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. ******