The Coq mailing list

[Jasper Hugunin <jasperh AT cs.washington.edu>]

Hello,

I ran into the following function:

(fix shift n := match n with O => a | S m => shift m end) : nat -> A

which clearly on any concrete n reduces to a.

It would be very convenient if this was judgmentally equal to (fun _ => a).

Of course, this is not implemented in Coq, but I haven't been able find any references discussing such a reduction. Does anyone know what the cost of adding such a reduction would be?

(does it break decidable type-checking, or introduce unreasonable computational overhead?)

Where this comes from, is that I actually have a family of types A : nat -> Type, along with

forall n, A n = A (S n), and a0 : A 0. My function then looks like (fun n => nat_rect A a0 (coerce) n),

but for some specific instances A is actually independent of n, and the equalities are eq_refl.

In the general case, I don't see how to do a useful reduction, but when given such nice data I would

have liked to return just a, independent of n.

- Jasper Hugunin