How can I read Coq's definition of proj1_sig?

Link:

https://stackoverflow.com/q/41461247

Question

In Coq, sig is defined as

Inductive sig (A : Type) (P : A -> Prop) : Type :=
    exist : forall x : A, P x -> {x : A | P x}

Arguments sig [A]%type_scope _%type_scope
Arguments exist [A]%type_scope _%function_scope _ _

Which I read as

A sig P is a type, where P is a function taking an A and returning a Prop. The type is defined such that an element x of type A is of type sig P if P x holds.

proj1_sig is defined as

proj1_sig = 
fun (A : Type) (P : A -> Prop) (e : {x : A | P x}) =>
let (a, _) := e in a
     : forall (A : Type) (P : A -> Prop),
       {x : A | P x} -> A

Arguments proj1_sig [A]%type_scope [P]%function_scope
  _

I'm not sure what to make of that. Could somebody provide a more intuitive understanding?

A: This question is somewhat related. And this one and this. Also, this question on equality of sigma types can be of some interest too. I've added these links because the automatic ones were not too close.

Answer

Non-dependent pairs vs. sig

The type is defined such that an element x of type A is of type sig P if P x holds.

That is not entirely correct: we can't say x : sig A P. An inhabitant e of type sig A P is essentially a pair of an element x : A and a proof that P x holds (this is called a dependent pair). x and P x are "wrapped" together using the data constructor exist.

To see this let us first consider the non-dependent pair type prod, which is defined as follows:

Inductive prod (A B : Type) : Type :=
    pair : A -> B -> A * B

Arguments prod (_ _)%type_scope
Arguments pair {A B}%type_scope _ _

prod's inhabitants are pairs, like pair 1 true (or, using notations, (1, true)), where the types of both components are independent of each other.

Since A -> B in Coq is just syntactic sugar for forall _ : A, B (defined here), the definition of prod can be desugared into

Inductive prod (A B : Type) : Type :=  pair : forall _ : A, B -> prod A B.

The above definition, perhaps, can help to see that elements of sig A P are (dependent) pairs.

What we can derive from implementation and type of proj1_sig

From the implementation we can see that proj1_sig e unpacks the pair and returns the first component, viz. x, throwing away the proof of P x.

The Coq.Init.Specif module contains the following comment:

(sig A P), or more suggestively {x:A | P x}, denotes the subset of elements of the type A which satisfy the predicate P.

If we look at the type of proj1_sig

proj1_sig
     : forall (A : Type) (P : A -> Prop),
       {x : A | P x} -> A

we will see that proj1_sig gives us a way of recovering an element of a superset A from its subset {x : A | P x}.

Analogue between fst and proj1_sig

Also, we can say that in some sense proj1_sig is analogous to the fst function, which returns the first component of a pair:

@fst
     : forall A B : Type, A * B -> A

There is a trivial property of fst:

forall (A B : Type) (a : A) (b : B), fst (a, b) = a


forall (A B : Type) (a : A) (b : B), fst (a, b) = a
 reflexivity. Qed.

We can formulate a similar statement for proj1_sig:

forall (A : Type) (P : A -> Prop) (x : A) (prf : P x),
proj1_sig (exist P x prf) = x


forall (A : Type) (P : A -> Prop) (x : A) (prf : P x),
proj1_sig (exist P x prf) = x
 reflexivity. Qed.

Q: Okay, so suppose I have an element x of sig P. Is proj1_sig x just x?

A: No, it's not. x is a "pair". You probably meant something like this proj1_sig (exist P x prf) = x, which is an analogue of fst (a, b) = a.