coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] cbv evaluation in Coq?

From: Randy Pollack <rpollack0 AT gmail.com>
To: Coq-Club Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] cbv evaluation in Coq?
Date: Wed, 13 Jan 2016 15:31:01 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=rpollack0 AT gmail.com; spf=Pass smtp.mailfrom=rpollack0 AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f49.google.com
Ironport-phdr: 9a23:+ylbZBP38HkgjHUvALQl6mtUPXoX/o7sNwtQ0KIMzox0KPv/rarrMEGX3/hxlliBBdydsKIazbqJ+P6xEUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35rxh7/5pcybSj4LrQT+SIs6FA+xowTVu5teqqpZAYF19CH0pGBVcf9d32JiKAHbtR/94sCt4MwrqHwI6LoJvvRNWqTifqk+UacQTHF/azh0t4XXskzoShLKzX8BWC09lgdCS1zO6wi/VZPsuAP7sPB80W+UJ5ulY6ozXGGY5qFnWVfQjyMDPjU6uDXNkst0iKtQo0qJqBl2woqSa4aQYqktNpjBdM8XEDISFv1aUDZMV8blN9MC

Regarding Gabriel's suggestion, a similar demo shows beta-reduction
(not just delta reduction) occurring under a lambda:

Definition bb1 := fun (t:True) => bool.
Definition demo1 (t:True) : (bb1 t) := match t with I => true end.
Eval cbv in demo1.

On Wed, Jan 13, 2016 at 2:49 PM, Robbert Krebbers
<mailinglists AT robbertkrebbers.nl>
wrote:
> On 01/13/2016 03:44 PM, Matthieu Sozeau wrote:
>>
>> You are right that the cbv strategy is doing normalization under
>> binders though, not weak reduction as advertised.
>
> Thanks for clarifying. But is this a bug or intended behavior?
>

[Coq-Club] cbv evaluation in Coq?, Randy Pollack, 01/13/2016
- Re: [Coq-Club] cbv evaluation in Coq?, Robbert Krebbers, 01/13/2016
  - Re: [Coq-Club] cbv evaluation in Coq?, Gabriel Scherer, 01/13/2016
    - Re: [Coq-Club] cbv evaluation in Coq?, Matthieu Sozeau, 01/13/2016
      - Re: [Coq-Club] cbv evaluation in Coq?, Robbert Krebbers, 01/13/2016
        
        Re: [Coq-Club] cbv evaluation in Coq?, Randy Pollack, 01/13/2016
        
        Re: [Coq-Club] cbv evaluation in Coq?, Hugo Herbelin, 01/14/2016