coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Variable closure

From: richard Dapoigny <richard.dapoigny AT univ-smb.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Variable closure
Date: Sun, 12 May 2019 17:17:05 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=richard.dapoigny AT univ-smb.fr; spf=Pass smtp.mailfrom=richard.dapoigny AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout20.partage.renater.fr

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