The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/22/2016 02:37 PM, Cedric Auger wrote:
> 2016-03-21 20:03 GMT+01:00 Jonathan Leivent 
> <jonikelee AT gmail.com
> <mailto: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?
>
> ...
>
>
> ​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.

Thanks.  I did not expect it to be provable in Coq.  I was just 
wondering if, by avoiding type indexes, I'd eventually find a good 
reason to have kept them.

> ...
>
>
> ​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).

This construction is interesting, but not useful in most of my cases.  
The issue is that I want the type parameters and indexes to vanish via 
Extraction along with all trace of their trails through the code, and 
incorporating one as a match discriminee will likely prevent that.

-- Jonathan