The Coq mailing list

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

Le Wed, 03 Aug 2011 07:56:10 -0400,
Adam Chlipala 
<adam AT chlipala.net>
 a écrit :

> Marco Servetto wrote:
> > Hi, I'm tring to understand sig, sigT, their differences and how to
> > use they.
> >
> > For example, i tried to define elements
> >
> > Definition ex1:= (( [ ], (NoDup_nil nat)) :{x:list nat | NoDup x}).
> > Definition ex2:= (( [ ], (NoDup_nil nat)) :{x:list nat&  NoDup x}).
> >
> > but with no success.
> > How to define elements of type {x:list nat | NoDup x} or {x:list
> > nat& NoDup x} ? and what is the difference between this two types?
> >    
> 
> You've already done the hard work of figuring out which type family
> is matched with each of the different notations.  If you need to do
> that in the future, you might like to use the [Locate] command,
> illustrated like: Locate "{ _ : _ | _ }".
> 
> This command finds [sig].  Then you can run:
>      Print sig.
> ...which will show you the type definition, including the single 
> constructor and its type.  As far as I know, the standard library 
> contains no shorthand syntax for applying this constructor, so you
> just call it directly (or define your own notation, as I often do).
> 

On this page you can find an example for such a notation:
http://coq.inria.fr/cocorico/AUGER_ExtractionTuto

I copy paste the interesting part (and remove some comments, you may
not be interested in)
====================================================================
Record spec (T: Type) (Spe: T → Prop): Type :=
Cast { spec_val: T;
       π: Spe spec_val
}.
(** This definition is isomorphic to the one of sig,
    so you may replace Cast by exist, and spec with sig;
    I defined a Record not to have to define projections,
    but you can of course do:

Definition spec_val {A: Type} {P: A -> Prop} (s: sigT P) :=
 let (x,_) := s in x.

and

Definition π {A: Type} {P: A -> Prop} (s: sigT P) :=
 let (_,x) := s in x.

to have them
 *)

Notation "{ x : T 'st' Π }" :=
 (spec (fun (x: T) =>  Π))
 (x at level 99, format "'[' {  x  :  T  '/' 'st'  Π  } ']'").
Notation "{ x 'st' Π }" := {x:_ st Π}
 (x at level 99, format "'[' {  x  '/' 'st'  Π  } ']'").
Notation "{ x '&' Π }" :=
 (spec (fun (_: x) => Π))
 (x at level 99, format "'[' {  x  '/' '&'  Π  } ']'").

Notation "{: x :}" := {|spec_val:=x|}.
(** This syntax will mark places where a proof is expected
    inside of refine terms (since the [π] term is not provided).

    So in practice, we will find [{: x (*label to a proof*) :}].
    Thus we can refer us to it inside of our term definitions. *)

 Definition dummy: {unit & True}.
 refine ( {: tt (*tt is such that err... True *) :} ).
 Proof.
  (*tt is such that err... True *)
  trivial.
 Defined.
==================================================================
So that in your case, you can do:

Notation "{: x :}" := (exist _ x _).
Notation "{: x, y :}" := (existT _ x y).

Definition ex1: {x: list nat | NoDup x}.
refine (
  {· [ ] (* [] has no duplication *) ·}
).
Proof. (* [] has no duplication *)
 apply NoDup_nil.
Defined.

Definition ex1': {x: list nat | NoDup x} := exist _ _ (NoDup_nil nat).

Definition ex2: {x:list nat &  NoDup x} := {: [ ], NoDup_nil nat :}.
Definition ex2': {x:list nat &  NoDup x}
 := existT _ [ ] (NoDup_nil nat).

I didn't test it, so it may contain some error(s), but the wiki page
has been tested on coq 8.3

> If this advice is insufficient, please feel free to write again!
> 
> (The same advice should also make it possible to see the difference 
> between [sig] and [sigT].)