The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/18/2015 12:00 PM, Matej Kosik wrote:
> Hello there,
>
> What is "sig", and how to construct values of "sig" seems clear.
>
> I am trying to wrap my head around "sigT".
> https://coq.inria.fr/library/Coq.Init.Specif.html#sigT
>
> This seems to be simple enough example term:
>
>         {n : nat & {m : nat | n < m}}
>
> Coq says that it has type Set.
>
> I am trying to figure out:
>
>    1. what that set represents

It is the Set of triples (actually a pair nested in a pair) of the nat 
n, the nat m, and a proof that n < m.  It is a Set instead of a Prop 
because it is informative about n and m - each instance can be 
informatively deconstructed to get at n and m, unlike sigs (sigs can 
only be deconstructed to produce other uninformative Props).

>    2. how can I construct elements of that Set.

You would use the existT and exist constructors.  An example instance is:

(existT (fun n : nat => {m : nat & n < m}) 1 (exist (fun m : nat => 1 < 
m) 2 (le_n 2)))

which Coq can infer from this much easier to read version:

(existT _ 1 (exist _ 2 (le_n 2)))


-- Jonathan