coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: James McKinna <james.mckinna AT ed.ac.uk>
- To: "michael.soegtrop AT intel.com" <michael.soegtrop AT intel.com>
- Cc: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] proving a lemma in a proof
- Date: Wed, 23 Jan 2019 08:54:38 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=james.mckinna AT ed.ac.uk; spf=Pass smtp.mailfrom=james.mckinna AT ed.ac.uk; spf=None smtp.helo=postmaster AT loire.is.ed.ac.uk
- Ironport-phdr: 9a23:6lKndhMytQMYRzE3ES4l6mtUPXoX/o7sNwtQ0KIMzox0Ivz/rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgbODE37WHZhMtyg6xVrxyvpBJ/zZDPbYGJLfp+e7/RfdMGSWdDWMtaSixPApm7b4sKF+cPOfxXr4zjqFsVsBCwAhWjCubuyj9OgH/5x7Ax3uMjEQ7c2QwvAckOvG7RrNrpN6cSUOa1zK/SwjjYcfxZxC3x55LUfRw7vPGMXqt9fMzMwkchEAPFi0+fqY3jPz6N1+QNtXSb4PRkVe61lmEotQd8qSWsyMc0koTFm5wZx1Te+Sln3Yo4Jce0RFN6bNK+DZdcqzmWO5ZyT84iWW1kpjg2x7IctZKmYCQHx44rywPcZvCadYWD/wjtW/yLIThigXJoYLK/iAi28Uin0uD8Us600FdQriVbiNXMt2sN2wbN5ceaUPdy5Fuu1SyS1wDQ8u1EIEY0mrTHK5M537I8iJ4evV7dEiPrmEj6lrKae0Q+9uS19+jrerDmqYWdN49whAH+KKMumsmnDOQ6KAcOWnaU+f+m2L3m4UL5Q7RKjvswkqbDq53VO9kUqrSjDABJyIoj9hW/Ay+80NsEhXkHME5FeBWfgof1PFHOOen0Auu7g1Sxizhm3OvGP73kApXVNHfPirbhfbBn605d0gU/195f54gHQo0Gdbj2W0TxvdHcSAQ+PgOo2eH/INR7yo4aH2mIB+XRZKbTul+B6+ZpOO6Ba5MPvy7VKv456vqohng8zwwzZ66siLkebX2jVtFtAESfZ3Ok1tUIFGoR+A81T+3sjlSqXDIVbn30QqFqtWJzM56vEYqWHtPlu7eGxiruRsQHNFADMUiFFDLTT6vBXv4NbCyIJco4ym4JWf6oQMk81kP37VOo+/9cNuPRvxYgm9f7ztEsv7/emVc7/nppDJbFijzffyRPhmoNAgQO8uV/rEh6kwbR1a95mfEeFMcV6v8PWwx8KJ2Ol+E=
Dear Michael,
To rephrase Gäetan's point in a slightly more piquant way, if I understand
your proposal correctly:
What would it be like to have to write haskell programs in which each use of
a 'where' clause would have to be explicitly lambda-lifted by the programmer
before the type-checker would accept it?
I wonder if the (sub-)conscious influences of ML on Coq/Gallina, and haskell
on Agda, lead us into unexpected affordances, or lack thereof, in the
interaction surface to our (preferred) systems.
Best,
dr. James McKinna
LFCS, School of Informatics
University of Edinburgh
10 Crichton Street
Edinburgh EH8 9AB
> On 23 Jan 2019, at 07:53, "Soegtrop, Michael"
> <michael.soegtrop AT intel.com>
> wrote:
>
> Dear Maxime,
>
> if I remember right, we had a discussion on the topic during the Coq
> Implementers Workshop in Nice last year. I think you said that the main
> difficulty with nested proofs is that they may depend on the local context
> (the context of the outer proof). I also use nested proofs frequently, but
> I don't use nested proofs which depend on the local context, that is which
> could not be moved in front of the outer lemma. Since Andrew said he
> usually moves the proofs outside eventually, I guess he also doesn't use
> nested lemmas which depend on the local context. Maybe Adam and other
> friends of this feature can comment on their usage.
>
> In cases others agree to this, would it be an option to remove support for
> nested lemmas which depend on the current context? I don't see how this
> would be in any way more complicated than parallel proofs - essentially it
> should be the same. Also I think removing the feature that a nested lemma
> can depend on the outer proof's context would be even an advantage, because
> I would think most people who use this feature use it accidentally and not
> willingly.
>
> Best regards,
>
> Michael
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
- Re: [Coq-Club] proving a lemma in a proof, (continued)
- Re: [Coq-Club] proving a lemma in a proof, Enrico Tassi, 01/25/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/24/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
- Re: [Coq-Club] proving a lemma in a proof, Enrico Tassi, 01/25/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/25/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/25/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/26/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/28/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/28/2019
- Re: [Coq-Club] proving a lemma in a proof, Christian Doczkal, 01/23/2019
- RE: [Coq-Club] proving a lemma in a proof, Soegtrop, Michael, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Jan Bessai, 01/22/2019
- Re: [Coq-Club] proving a lemma in a proof, Pierre Courtieu, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Maxime Dénès, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Théo Zimmermann, 01/23/2019
- Re: [Coq-Club] proving a lemma in a proof, Adam Chlipala, 01/23/2019
Archive powered by MHonArc 2.6.18.