# Library Coq.Init.Specif

``` ```
Basic specifications : sets that may contain logical information
``` Set Implicit Arguments. Require Import Notations. Require Import Datatypes. Require Import Logic. ```
Subsets and Sigma-types
``` ```
`(sig A P)`, or more suggestively `{x:A | P x}`, denotes the subset of elements of the type `A` which satisfy the predicate `P`. Similarly `(sig2 A P Q)`, or `{x:A | P x & Q x}`, denotes the subset of elements of the type `A` which satisfy both `P` and `Q`.
``` Inductive sig (A:Type) (P:A -> Prop) : Type :=     exist : forall x:A, P x -> sig P. Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=     exist2 : forall x:A, P x -> Q x -> sig2 P Q. ```
`(sigT A P)`, or more suggestively `{x:A & (P x)}` is a Sigma-type. Similarly for `(sigT2 A P Q)`, also written `{x:A & (P x) & (Q x)}`.
``` Inductive sigT (A:Type) (P:A -> Type) : Type :=     existT : forall x:A, P x -> sigT P. Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=     existT2 : forall x:A, P x -> Q x -> sigT2 P Q. Arguments Scope sig [type_scope type_scope]. Arguments Scope sig2 [type_scope type_scope type_scope]. Arguments Scope sigT [type_scope type_scope]. Arguments Scope sigT2 [type_scope type_scope type_scope]. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A | P }" := (sig (fun x:A => P)) : type_scope. Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :   type_scope. Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) :   type_scope. Add Printing Let sig. Add Printing Let sig2. Add Printing Let sigT. Add Printing Let sigT2. ```
Projections of `sig`

An element `y` of a subset `{x:A & (P x)}` is the pair of an `a` of type `A` and of a proof `h` that `a` satisfies `P`. Then `(proj1_sig y)` is the witness `a` and `(proj2_sig y)` is the proof of `(P a)`
``` Section Subset_projections.   Variable A : Type.   Variable P : A -> Prop.   Definition proj1_sig (e:sig P) := match e with                                     | exist a b => a                                     end.   Definition proj2_sig (e:sig P) :=     match e return P (proj1_sig e) with     | exist a b => b     end. End Subset_projections. ```
Projections of `sigT`

An element `x` of a sigma-type `{y:A & P y}` is a dependent pair made of an `a` of type `A` and an `h` of type `P a`. Then, `(projT1 x)` is the first projection and `(projT2 x)` is the second projection, the type of which depends on the `projT1`.
``` Section Projections.   Variable A : Type.   Variable P : A -> Type.   Definition projT1 (x:sigT P) : A := match x with                                       | existT a _ => a                                       end.   Definition projT2 (x:sigT P) : P (projT1 x) :=     match x return P (projT1 x) with     | existT _ h => h     end. End Projections. ```
`sumbool` is a boolean type equipped with the justification of their value
``` Inductive sumbool (A B:Prop) : Set :=   | left : A -> {A} + {B}   | right : B -> {A} + {B}  where "{ A } + { B }" := (sumbool A B) : type_scope. Add Printing If sumbool. ```
`sumor` is an option type equipped with the justification of why it may not be a regular value
``` Inductive sumor (A:Type) (B:Prop) : Type :=   | inleft : A -> A + {B}   | inright : B -> A + {B}  where "A + { B }" := (sumor A B) : type_scope. Add Printing If sumor. ```
Various forms of the axiom of choice for specifications
``` Section Choice_lemmas.   Variables S S' : Set.   Variable R : S -> S' -> Prop.   Variable R' : S -> S' -> Set.   Variables R1 R2 : S -> Prop.   Lemma Choice :    (forall x:S, sig (fun y:S' => R x y)) ->    sig (fun f:S -> S' => forall z:S, R z (f z)).   Proof.    intro H.    exists (fun z:S => match H z with                       | exist y _ => y                       end).    intro z; destruct (H z); trivial.   Qed.   Lemma Choice2 :    (forall x:S, sigT (fun y:S' => R' x y)) ->    sigT (fun f:S -> S' => forall z:S, R' z (f z)).   Proof.     intro H.     exists (fun z:S => match H z with                        | existT y _ => y                        end).     intro z; destruct (H z); trivial.   Qed.   Lemma bool_choice :    (forall x:S, {R1 x} + {R2 x}) ->    sig      (fun f:S -> bool =>         forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x).   Proof.     intro H.     exists      (fun z:S => match H z with                  | left _ => true                  | right _ => false                  end).     intro z; destruct (H z); auto.   Qed. End Choice_lemmas. ```
A result of type `(Exc A)` is either a normal value of type `A` or an `error` :

`Inductive Exc [A:Type] : Type := value : A->(Exc A) | error : (Exc A)`.

It is implemented using the option type.
``` Definition Exc := option. Definition value := Some. Definition error := @None. Implicit Arguments error [A]. Definition except := False_rec. Implicit Arguments except [P]. Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C. Proof.   intros A C h1 h2.   apply False_rec.   apply (h2 h1). Qed. Hint Resolve left right inleft inright: core v62. Notation sigS := sigT (only parsing). Notation existS := existT (only parsing). Notation sigS_rect := sigT_rect (only parsing). Notation sigS_rec := sigT_rec (only parsing). Notation sigS_ind := sigT_ind (only parsing). Notation projS1 := projT1 (only parsing). Notation projS2 := projT2 (only parsing). Notation sigS2 := sigT2 (only parsing). Notation existS2 := existT2 (only parsing). Notation sigS2_rect := sigT2_rect (only parsing). Notation sigS2_rec := sigT2_rec (only parsing). Notation sigS2_ind := sigT2_ind (only parsing). ```