Library Coq.Init.Specif

Basic specifications : sets that may contain logical information

Set Implicit Arguments.

Require Import Notations.
Require Import Datatypes.
Local Open Scope identity_scope.
Require Import Logic.
Local Unset Elimination Schemes.

(sig A P), or more suggestively {x:A & (P x)} is a Sigma-type. Similarly for (sig2 A P Q), also written {x:A & (P x) & (Q x)}.

Record sig {A} (P : A Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }.

Scheme sig_rect := Induction for sig Sort Type.

We make the parameters maximally inserted so that we can pass around pr1 as a function and have it actually mean "first projection" in, e.g., ap.

Arguments exist {A}%type P%type _ _.
Arguments proj1_sig {A P} _ / .
Arguments proj2_sig {A P} _ / .

Inductive sig2 (A:Type) (P Q:A Type) : Type :=
    exist2 : x:A, P x Q x sig2 P Q.

Scheme sig2_rect := Induction for sig2 Sort Type.

Arguments sig (A P)%type.
Arguments sig2 (A P Q)%type.


In standard Coq, sig and sig2 are defined as "subset types" which sum over predicates P:AProp, while sigT and sigT2 are the Type variants. Because we don't use Prop, we combine the two versions, and make sigT a notation for sig. Note that some parts of Coq (like Program Definition) expect sig to be present.

Notation sigT := sig (only parsing).
Notation existT := exist (only parsing).
Notation sigT_rect := sig_rect (only parsing).
Notation sigT_rec := sig_rect (only parsing).
Notation sigT_ind := sig_rect (only parsing).
Notation sigT2 := sig2 (only parsing).
Notation existT2 := exist2 (only parsing).
Notation sigT2_rect := sig2_rect (only parsing).
Notation sigT2_rec := sig2_rect (only parsing).
Notation sigT2_ind := sig2_rect (only parsing).

Notation ex_intro := existT (only parsing).

Notation "{ x | P }" := (sigT (fun xP)) : type_scope.
Notation "{ x | P & Q }" := (sigT2 (fun xP) (fun xQ)) : type_scope.
Notation "{ x : A | P }" := (sigT (A := A) (fun xP)) : type_scope.
Notation "{ x : A | P & Q }" := (sigT2 (A := A) (fun xP) (fun xQ)) :

Notation "'exists' x .. y , p" := (sigT (fun x ⇒ .. (sigT (fun yp)) ..))
  (at level 200, x binder, right associativity,
   format "'[' 'exists' '/ ' x .. y , '/ ' p ']'")
  : type_scope.

Notation "'exists2' x , p & q" := (sigT2 (fun xp) (fun xq))
  (at level 200, x ident, p at level 200, right associativity) : type_scope.
Notation "'exists2' x : t , p & q" := (sigT2 (fun x:tp) (fun x:tq))
  (at level 200, x ident, t at level 200, p at level 200, right associativity,
    format "'[' 'exists2' '/ ' x : t , '/ ' '[' p & '/' q ']' ']'")
  : type_scope.

Notation "{ x : A & P }" := (sigT (fun x:AP)) : type_scope.
Notation "{ x : A & P & Q }" := (sigT2 (fun x:AP) (fun x:AQ)) :

Add Printing Let sig.
Add Printing Let sig2.

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, (proj1 x) is the first projection and (proj2 x) is the second projection, the type of which depends on the proj1.

Notation projT1 := proj1_sig (only parsing).
Notation projT2 := proj2_sig (only parsing).

Various forms of the axiom of choice for specifications

Section Choice_lemmas.

  Variables S S' : Type.
  Variable R : S S' Type.
  Variable R' : S S' Type.
  Variables R1 R2 : S Type.

  Lemma Choice :
   ( x:S, {y:S' & R' x y}) {f:S S' & z:S, R' z (f z)}.
    intro H.
     (fun zprojT1 (H z)).
    intro z; destruct (H z); assumption.

End Choice_lemmas.

Section Dependent_choice_lemmas.

  Variables X : Type.
  Variable R : X X Type.

  Lemma dependent_choice :
    ( x:X, {y : _ & R x y})
     x0, {f : nat X & (f O = x0) × ( n, R (f n) (f (S n)))}.
    intros H x0.
    set (f:=fix f n := match n with Ox0 | S n'projT1 (H (f n')) end).
    split. reflexivity.
    induction n; simpl; apply projT2.

End Dependent_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.

Arguments value {A} a.
Arguments error {A}.

Definition except := False_rec.
Arguments except [P] _.

Theorem absurd_set : (A:Prop) (C:Set), A not A C.
  intros A C h1 h2.
  apply False_rec.
  apply (h2 h1).

Hint Resolve existT existT2: core.