The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2016-03-21 20:03 GMT+01:00 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 think it is always the case. One cannot prove it directly in Coq as we would have to use "meta"functions taking a type as argument, and inspect its ​construction to build an other one which would be isomorphic.

 

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?

​If such an example exist (and I doubt of it, although I have no strong proof of it), I guess it must be so uncommon, that your approach should apply in all ​practical cases.

 

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

​Now I tend to avoid that kind of annoyance with an other approach:

Inductive finS(X:Set) : Set :=

| Fin1

| FinS : X -> finS X.

Fixpoint fin(m:nat) : Set :=

  match m with​

​  | O => emptySet​

  | S n => finS (fin m)

  end.

I find this kind of type quite convenient to use. "inversion f." becomes "destruct n; destruct f." with no weirdness to deal with.

Induction is done on the parameter rather than the type, and all basic operation have their counterparts in a not too artificial way.

I find it nice to have the ability to "reduce" the type to only those which are possible in a given context.

I am conscious on the fact that such a transcription of type is not always trivially existent, but in many cases, there is a strong relation between the constructor of the type and the constructors of the index, leading to a natural way to make it.

Cases which do not apply still, are those where the index is not a constructed type (and I don’t pretend this to be the only case).
Example: Inductive is_identity {A:Type} : (A->A)->Prop := Id : is_identity (fun x => x).