The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

Hi,

I don't think that's really a fair comparison. The way I understand it is 
that nested Lemmas are used during interactive development for things that 
should be independent preceding lemmas, and the reason to use them is mostly 
that backtracking, stating the lemma, and going back to the current point may 
be time consuming in the presence of slow-running automation. 

For something that is intended to permanently stay inside the proof there is 
assert (which is invisible from the outside and may, of course, use local 
assumptions) which, as far as I understand, corresponds much more closely to 
"where" clauses. 

Best,
Christian


On 1/23/19 9:54 AM, James McKinna wrote:
> 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
>

Attachment: signature.asc
Description: OpenPGP digital signature