coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Variable closure

From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Variable closure
Date: Sun, 12 May 2019 11:21:18 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=arthur.aa AT gmail.com; spf=Pass smtp.mailfrom=arthur.aa AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f170.google.com
Ironport-phdr: 9a23:oSxAFBb8vSFqfGLzCuHfVxn/LSx+4OfEezUN459isYplN5qZr8+7bnLW6fgltlLVR4KTs6sC17OP9fG6EjxQqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5vIBmsqQjdqMYajIhhJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlTwKPCAl/m7JlsNwjbpboBO/qBx5347Ue5yeOP5ncq/AYd8WWW9NU8BMXCJDH4y8dZMCAOUPPelar4fzqVgAowagCwawH+7g0CNEi2Xs0KEmz+gsEwfL1xEgEdIUt3TUqc34ObsIUeCpzKnI0C/DZO5K1Db89ofIbA4uruyLXbltbMXe11QkGh/AjlWXs4zlPjaV3fkKvmeB9epgSeKvi3M9qw1ruDeg3NwhiobMho0Py1DE8T91z5oyJd29UUN2Z8OvHpVXtyGfLYR2Q8UiTnl1uCY8y70Gp4e3fDMPyJs83RLfZeaHfo6V6RzgTOacOSl0iG5hdb6lhBu/8VKsxvD9W8S2ylpGsyhInsXKu3sQzRLc8NKHReF4/kq52TaAyQTT6uZcLEAxj6XbKpohzqc3lpoSrEjPByH2lFj0gaOKbEkk9e+o6+PoYrXiuJCQLZN7igb7Mqg2m8y/B/o3MhQWUmSF5eix0Kfv8E75TblQk/E7k6vUvIrHKckZuqK1GwpV3Zwi6xa7ATemytMYnXwfIV1fYhKHk4jpO0zUIPziF/iwmU+hkDhux//cP73hBo/BIWTEkLfkZbp98VJTyBIvzdBD4JJZEq0OIPXqWkPoqNPYCgI5PBevzub8CNR905seVniVDq+YNqPSq16I6fg1L+mCfo9G8Ar6ftMi/rbFiWIz0QsWerDs1p8KYli5GO5nKgOXeyy/rM0GFDIjpBY+UfaioU+PTzNfYD6+UuoV4zYhCYfuWY7ZWoCwmvqI1Q+0G5RXYiZNDVXaQiSgTJmNR/pZMHHaGcRmiDFREOH5E9Z8hyHrjxfzzv9cFsSR+iAcssi9ht185umWkhBrsDItUJzb3GaKQGV52GgPQm1uhfwtkQlG0l6GlJNArblAD9UKvqFGVw47MdjXyOkoU4mjCDKERc+ATROdevvjBDgwStwrxNpXOhRyHtyjilbI2C/4WrI=

I don't think this holds. For instance,

forall n, (forall m, m=0) -> n=0

is true, but

forall n m, m=0 -> n=0

is not.

On Sun, May 12, 2019, 11:16 richard Dapoigny <richard.dapoigny AT univ-smb.fr> wrote:

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/

[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