The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 3 Aug 2011 15:10:56 +0200,
Marco Servetto 
<marco.servetto AT gmail.com>
 a écrit :

> Well... may be you are overstimating me :)
> actuallly
> > You've already done the hard work of figuring out which type family
> > is matched with each of the different notations.
> I does not even understand what this sentence can mean.... i'm trying
> to understand
> http://www.lix.polytechnique.fr/coq/stdlib/Coq.Init.Specif.html
> 
> Following you advice I was able to write
> Definition ex1:= ((exist (@NoDup nat) (@nil nat) (NoDup_nil
> nat)):{x:list nat | NoDup x}).
> That again does not type since it is something of tipe ( sig NoDup ),
> that for what I was able to understand should be the same of {x:list
> nat | NoDup x}, but it seams not...

In fact {x:list nat | NoDup x} is a notation for:
sig (fun l : list nat => NoDup l).
(which equal to "sig NoDup" modulo eta expansion);
so it should typecheck if you do:

Definition ex1:=
 ((exist (fun l : list nat => @NoDup nat l)
 (@nil nat)
 (NoDup_nil nat)):{x:list nat | NoDup x}).

(Here, you don't need eta expansion anymore)

> 
> Moreover, i have noticed some Type insted of Prop in the declaration
> of sigT, but while i can imagine lots of uses for sig
> (list long at list n, and so on...), I cant figure usages for sigT :-(

Examples for sigT:

Assume "nat_arrays n" is the type of arrays of length n.
Then if you want to consider any array of any length,
you may whish to encapsulate the length of the array,
leading to something like:

{ n: nat & array n }

Now an element of this type is a pair of a natural number 'n' and an
array of length 'n'.
Note that as you remarked yourself, 'array n' can be defined using sig;
so my type could be written:

{n: nat & {l: list nat | length l = n}}
The l content is something you want to be able to inspect as well as n;
but there is nothing to inspect inside a proof such as "length l = n",
so you whish it to be in Prop; whereas you don't want l and n to be in
Prop.
That seems quite artificial as it is simply a redefinition of all lists,
but in this case, there is no computation to get the length of the
list, since it is directly a field.

Polymorphic lists:
If you want to define polymorphic list in coq you can do:

Inductive poly_list : Type :=
| poly_nil: poly_list
| poly_cons: forall A : Type, A -> poly_list -> poly_list.

But you will lack the List library, so you may want to define:
Definition poly_list := list (@sigT Type (fun A: Type => A)).