Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] simpl should reduce on constructor?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] simpl should reduce on constructor?


Chronological Thread 
  • From: Maxime Dénès <mail AT maximedenes.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] simpl should reduce on constructor?
  • Date: Sat, 29 Oct 2016 20:46:04 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 6.mo2.mail-out.ovh.net
  • Ironport-phdr: 9a23:hXhK5h/WcRi+fP9uRHKM819IXTAuvvDOBiVQ1KB+1OscTK2v8tzYMVDF4r011RmSDN+dtK8P0rCI++C4ACpbvsbH6ChDOLV3FDY7yuwu1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9dazJHdvZiN3y3OSv8bXSZR9JjXyze+BcNhKz+CDYpsgTjMNOq6Cx0VOdp3JJf8xTzHNpIF+fkhDx/YG+5sgwoGxrp/s9+psYAu3BdKMiQOkAAQ==

Sorry, my previous message was incomplete. As a workaround, you can do:

Arguments baz {_ _} !pf _ /.

Note the "/".

This bug is known and being fixed in 8.6.

Hope it helps.

Maxime.

On 10/29/16 20:44, Maxime Dénès wrote:
> Hi Greg,
>
> As a workaround, you can do:
>
> Arguments baz {_ _} !pf _.
>
>
>
> On 10/29/16 19:46, Gregory Malecha wrote:
>> Hello --
>>
>> I have three functions that look roughly like this:
>>
>> Definition foo {a b : Type} (F : Type -> Type) (pf : a = b) : F a -> F b :=
>> match pf with
>> | eq_refl => fun x => x
>> end.
>>
>> Definition bar {a b : Type} (pf : a = b) : a -> b :=
>> @foo a b (fun x => x) pf.
>>
>> Definition baz {a b : Type} (pf : a = b) : b -> a :=
>> @bar b a (eq_sym pf).
>>
>> I am writing the following annotations for simpl.
>>
>> Arguments foo {_ _} _ !pf _.
>> Arguments bar {_ _} !pf _.
>> Arguments baz {_ _} !pf _.
>>
>> And I get the following behavior:
>>
>> Eval simpl in @foo nat nat (fun x => x) eq_refl 1. (* = 1 *)
>> Eval simpl in @bar nat nat eq_refl 1. (* = 1 *)
>> Eval simpl in @baz nat nat eq_refl 1. (* = baz eq_refl 1 *)
>>
>> The first two of these are exactly what I expect, but the third seems
>> wrong. If I understand correctly, the documentation says that baz should
>> be reduced if the proof argument is a constructor (which it is:
>> eq_refl). Once that unfolds, eq_sym should reduce since it is applied to
>> a constructor (just to be sure I added an: Arguments eq_sym {_ _ _}
>> !_.), and then bar should reduce and finally foo should reduce.
>>
>> Is there any work-around that does not involve inlining the definition
>> of `foo` inside `baz`?
>>
>> Thanks.
>> --
>>
>> - gregory malecha
>> gmalecha.github.io <http://gmalecha.github.io>
>>



Archive powered by MHonArc 2.6.18.

Top of Page