How can I read the definition of Coq 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. 

What i read as

"A sig P is a type, where P is a function that takes A and returns Prop. The type is defined such that an element x of type A is of type sig P if P x."

proj1_sig defined as

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

I'm not sure what to do with this. Can someone give a more intuitive understanding?

Answer 1

Independent pairs vs sig

The type is determined so that an element x type A is of type sig P if P x is satisfied.

This is not entirely correct: we cannot say x : sig AP . The resident e type sig AP is essentially a pair of an element x : A and proof that P x holds (this is called a dependent pair). x and P x combined using the exist data constructor.

To verify this, first consider the type of independent pair prod , which is defined as follows:

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

prod Residents are pairs, such as pair 1 true (or, using the notation, (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 removed in

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

The above definition may perhaps help to see that the sig AP elements are (dependent) pairs.

What can we learn from the implementation and type proj1_sig

From the implementation, we see that proj1_sig e unpacks the pair and returns the first component, namely: x , discarding the proof of P x .

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

(sig AP) or more impressive {x:A | P x} {x:A | P x} denotes a subset of elements of type A that satisfy the predicate P

If we look at proj1_sig type

 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 to restore an element of a subset A from its subset {x : A | P x} {x : A | P x} .

Analogue between fst and proj1_sig

In addition, we can say that in a sense, proj1_sig similar to the function fst , which returns the first component of the pair:

 Check @fst. fst : forall AB : Type, A * B -> A 

There is a trivial fst property:

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

We can formulate a similar operator for proj1_sig :

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