The Coq mailing list

[James McKinna <james.mckinna AT ed.ac.uk>]

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.