The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

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