coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Variable closure

From: Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Variable closure
Date: Sun, 12 May 2019 15:46:18 +0000
Accept-language: en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Thorsten.Altenkirch AT nottingham.ac.uk; spf=Pass smtp.mailfrom=Thorsten.Altenkirch AT nottingham.ac.uk; spf=None smtp.helo=postmaster AT uidappmx02.nottingham.ac.uk
Ironport-phdr: 9a23:5PotKxwd6EftjCvXCy+O+j09IxM/srCxBDY+r6Qd2uwVIJqq85mqBkHD//Il1AaPAdyCraMewLuN+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhViDanZb5+Mhq6oAHfu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qFmQwLqhigaLT406GHZhNJtgqJHrhyvpBJ/zIzab4GUKPVxcbjQcskGSWpERMtdSzZMD4G6YoASD+QBJ+FYr4zlqlUQrRu+AhOsBPjzyjBWgH/9wLE30+A9EQ7Y2gwgHNMOsG7Io9X1KawfVv67zKnPzTXZdPNWxSny6I7Sfh09pfGMQax/cczSyUkuDQPKklWQpJfjPzOSyuQNr2mb7+xvVeKvkWEnrht9rSKzycs2l4nJhZsYx1bZ/it3x4Y1IMe3SE99YdO8DZtQsSCaN5VvTsM5RmFnozw2yrMcuZO9YSMEy4wnygbCZ/CZcIWE+AzvWemfLDtii39odqiziwus/UWg0uHxVci53ExUoidGiNXAqG4B2h3J5sSaSfZx4F+t2TiR2A3Q9u1JJEU5mKrGJ5MjxrM9k4EcvVjAEy/4nUj7jKubeVkr9+Wt9ejofLrrqYGaOoRpkA/xKL4ulda6AekgMggBQWyb+eOk2b3+/E32Xa9FjuUukqncv5HWOdoXqrS/Aw9SzoYj9xe/DzGp0NQYh3YHKUhJdwibgITzJlHOI+j0Dfa5g1uyjDdm3+3KMqPiD5nXMHTOn7nscaxy5kNS0gY/0M5T6pJMBrEEOv3zW0vxtNLCDh8+Ngy52/jpCNV61oMEQmKPHrGWMKXIvVKU4uIvP/eDZIkWuDb8Mfgq+/7ugGQ/mV8aYampwZoXaHa3HvRmOUqZZGDgjc0dHmsQowo+T/TmiEeeXj5Le3ayQ6U86yknB4KhFIfPX5yigLic3CigBZBWfWBHClWUEXjybYmEWvEMaDiTIsB7iDAEW6KhGMcd0kTkvwjjjrFjM+D8+ysCtJul2sI/r7nYkgh3/jhpBeyc1XuMRid6hDVbaSUx2fVDoUtn0UuO1+BRh+BVE99S/fhJGlMGNZnG1PB3DZbbXh7MeNSIUl2matOhHS0wSN0xytpIak07Btb03UOL5DajH7JAz+/DP5cz6K+JhyGsdfY48G7P0ewat3djQsZLMjf31LN++wHLH4vZyx/fkaG2aaUa0y7E8SGKxiyTvxMACV8iYeD+RXkaI3Dug5H870LGQaWpDO13YA1G1dKDLKRKY9ivhF4AWfSxYY2CMVL0oH+5AFOz/p3JdJDjIjVP2iLBFEkCnAAa+DCPPk4jBXX5rg==

If you replace “forall y,F” by “exists y, F” it even holds intuitionistically. In the present form it is false, even classically.

From: <coq-club-request AT inria.fr> on behalf of richard Dapoigny <richard.dapoigny AT univ-smb.fr>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Sunday, 12 May 2019 at 16:15
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Variable closure

Dear all,

using classical logic in Coq, is there a way to prove that the following equivalence holds?

forall x, ((forall y, F) -> G) <-> forall x y, (F -> G)

in which F depends on x an y while G only depends on x

Thanks for your answer,

Rich

--
Richard Dapoigny
Associate Professor - LISTIC Laboratory
University Savoie Mont-Blanc
5, chemin Bellevue
Po. Box 80439
Annecy-le-Vieux 74940
FRANCE
https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/


This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.

[Coq-Club] Variable closure, richard Dapoigny, 05/12/2019
- Re: [Coq-Club] Variable closure, Arthur Azevedo de Amorim, 05/12/2019
- Re: [Coq-Club] Variable closure, Jeremy Dawson, 05/12/2019
  - Re: [Coq-Club] Variable closure, richard Dapoigny, 05/12/2019
    - Re: [Coq-Club] Variable closure, Tadeusz Litak, 05/12/2019
      - Re: [Coq-Club] Variable closure, Kenji Maillard, 05/12/2019
- Re: [Coq-Club] Variable closure, Thorsten Altenkirch, 05/12/2019
- Re: [Coq-Club] Variable closure, Michel Levy, 05/12/2019