The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Is it true in Coq that any index on an inductive type could *always* be 
replaced by a type parameter with an extra equality-typed field added to 
each constructor tying the type parameter to that constructor's value 
for it?

Except of course for the type eq itself, which needs a type index 
(because of course one can't define eq using an eq-typed field to 
replace the index).

For example, fin:

Inductive fin : nat -> Set :=
| Fin1(n : nat) : fin (S n)
| FinS(n : nat) : fin n -> fin (S n).

could be redefined as:

Inductive fin(m : nat) : Set :=
| Fin1(n : nat)(_: m = S n)
| FinS(n : nat)(_: fin n)(_: m = S n).

I keep revisiting this because of various difficulties that type indexes 
create - such as the need for the inversion tactic, and the 
corresponding convoy patterns in Gallina match expressions.  Also, some 
tactics, such as case_eq, tend to misbehave when the type has indexes.  
But, is the claim really true?  If not, what is an example where a type 
index cannot be adequately replaced by a parameter/equality combo?

Defining an inductive type with indexes that vary among the constructors 
causes case analysis (elimination, destruction, induction) of instances 
of that type to induce some change to the environment in which the case 
analysis occurs.  If that inductive type is defined with type parameters 
and equality fields instead, then case analysis does not by itself 
induce any environment change - that's left for the equality fields - 
which can then be used only as needed.  Hence, there is a better 
separation of concerns.

There is the extra tedium of always having to fill in the constructors' 
new equality fields with arguments - but writing "eq_refl" a few times 
takes no brain power (and could perhaps be automated).  Similarly, the 
equality fields might accumulate in proof mode.  But tactics like subst 
and congruence make that manageable.

-- Jonathan