The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

Hi Jasper!

    This rule is sometimes called "eta for inductives" or "commutative conversions". In some versions it may break confluence, and in general is quite difficult to implement in Coq.

See also this discussion:  https://github.com/coq/coq/issues/3119

If you post your complete example, someone may have a workaround which does not require such a powerful conversion rule!

Best,

Cody

On Tue, Jan 2, 2018 at 2:20 AM, Jasper Hugunin <jasperh AT cs.washington.edu> wrote:

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