The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

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