How can I read Coq's definition of proj1_sig?

Question

In Coq, sig is defined as

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

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

Definition proj1_sig (e:sig P) := match e with
                                    | exist _ a b => a
                                    end.

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

Answer 1

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

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

Check 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:

Check @fst.

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

There is a trivial property of fst:

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

We can formulate a similar statement for proj1_sig:

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