The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Excellent. Thanks.

On Sat, Oct 29, 2016 at 2:46 PM Maxime Dénès <mail AT maximedenes.fr> wrote:

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>
>>

--

- gregory malecha
  gmalecha.github.io