diff options
Diffstat (limited to 'theories7/Init/Specif.v')
| -rwxr-xr-x | theories7/Init/Specif.v | 204 |
1 files changed, 204 insertions, 0 deletions
diff --git a/theories7/Init/Specif.v b/theories7/Init/Specif.v new file mode 100755 index 00000000..c39e5ed8 --- /dev/null +++ b/theories7/Init/Specif.v @@ -0,0 +1,204 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Specif.v,v 1.2.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) + +Set Implicit Arguments. +V7only [Unset Implicit Arguments.]. + +(** Basic specifications : Sets containing logical information *) + +Require Notations. +Require Datatypes. +Require Logic. + +(** Subsets *) + +(** [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset + of elements of the Set [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 Set [A] which satisfy both [P] and [Q]. *) + +Inductive sig [A:Set;P:A->Prop] : Set + := exist : (x:A)(P x) -> (sig A P). + +Inductive sig2 [A:Set;P,Q:A->Prop] : Set + := exist2 : (x:A)(P x) -> (Q x) -> (sig2 A P Q). + +(** [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant + of subset where [P] is now of type [Set]. + Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *) + +Inductive sigS [A:Set;P:A->Set] : Set + := existS : (x:A)(P x) -> (sigS A P). + +Inductive sigS2 [A:Set;P,Q:A->Set] : Set + := existS2 : (x:A)(P x) -> (Q x) -> (sigS2 A P Q). + +Arguments Scope sig [type_scope type_scope]. +Arguments Scope sig2 [type_scope type_scope type_scope]. +Arguments Scope sigS [type_scope type_scope]. +Arguments Scope sigS2 [type_scope type_scope type_scope]. + +Notation "{ x : A | P }" := (sig A [x:A]P) : type_scope. +Notation "{ x : A | P & Q }" := (sig2 A [x:A]P [x:A]Q) : type_scope. +Notation "{ x : A & P }" := (sigS A [x:A]P) : type_scope. +Notation "{ x : A & P & Q }" := (sigS2 A [x:A]P [x:A]Q) : type_scope. + +Add Printing Let sig. +Add Printing Let sig2. +Add Printing Let sigS. +Add Printing Let sigS2. + + +(** Projections of sig *) + +Section Subset_projections. + + Variable A:Set. + Variable P:A->Prop. + + Definition proj1_sig := + [e:(sig A P)]Cases e of (exist a b) => a end. + + Definition proj2_sig := + [e:(sig A P)] + <[e:(sig A P)](P (proj1_sig e))>Cases e of (exist a b) => b end. + +End Subset_projections. + + +(** Projections of sigS *) + +Section Projections. + + Variable A:Set. + Variable P:A->Set. + + (** 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 [(projS1 y)] is the witness [a] + and [(projS2 y)] is the proof of [(P a)] *) + + Definition projS1 : (sigS A P) -> A + := [x:(sigS A P)]Cases x of (existS a _) => a end. + Definition projS2 : (x:(sigS A P))(P (projS1 x)) + := [x:(sigS A P)]<[x:(sigS A P)](P (projS1 x))> + Cases x of (existS _ h) => h end. + +End Projections. + + +(** Extended_booleans *) + +Inductive sumbool [A,B:Prop] : Set + := left : A -> {A}+{B} + | right : B -> {A}+{B} + +where "{ A } + { B }" := (sumbool A B) : type_scope. + +Inductive sumor [A:Set;B:Prop] : Set + := inleft : A -> A+{B} + | inright : B -> A+{B} + +where "A + { B }" := (sumor A B) : type_scope. + +(** Choice *) + +Section Choice_lemmas. + + (** The following lemmas state various forms of the axiom of choice *) + + Variables S,S':Set. + Variable R:S->S'->Prop. + Variable R':S->S'->Set. + Variables R1,R2 :S->Prop. + + Lemma Choice : ((x:S)(sig ? [y:S'](R x y))) -> + (sig ? [f:S->S'](z:S)(R z (f z))). + Proof. + Intro H. + Exists [z:S]Cases (H z) of (exist y _) => y end. + Intro z; NewDestruct (H z); Trivial. + Qed. + + Lemma Choice2 : ((x:S)(sigS ? [y:S'](R' x y))) -> + (sigS ? [f:S->S'](z:S)(R' z (f z))). + Proof. + Intro H. + Exists [z:S]Cases (H z) of (existS y _) => y end. + Intro z; NewDestruct (H z); Trivial. + Qed. + + Lemma bool_choice : + ((x:S)(sumbool (R1 x) (R2 x))) -> + (sig ? [f:S->bool] (x:S)( ((f x)=true /\ (R1 x)) + \/ ((f x)=false /\ (R2 x)))). + Proof. + Intro H. + Exists [z:S]Cases (H z) of (left _) => true | (right _) => false end. + Intro z; NewDestruct (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:Set] : Set := value : A->(Exc A) | error : (Exc A)] + it is implemented using the option type. *) + +Definition Exc := option. +Definition value := Some. +Definition error := !None. + +Implicits error [1]. + +Definition except := False_rec. (* for compatibility with previous versions *) + +Implicits except [1]. + +V7only [ +Notation Except := (!except ?) (only parsing). +Notation Error := (!error ?) (only parsing). +V7only [Implicits error [].]. +V7only [Implicits except [].]. +]. +Theorem absurd_set : (A:Prop)(C:Set)A->(~A)->C. +Proof. + Intros A C h1 h2. + Apply False_rec. + Apply (h2 h1). +Qed. + +Hints Resolve left right inleft inright : core v62. + +(** Sigma Type at Type level [sigT] *) + +Inductive sigT [A:Type;P:A->Type] : Type + := existT : (x:A)(P x) -> (sigT A P). + +Section projections_sigT. + + Variable A:Type. + Variable P:A->Type. + + Definition projT1 : (sigT A P) -> A + := [H:(sigT A P)]Cases H of (existT x _) => x end. + + Definition projT2 : (x:(sigT A P))(P (projT1 x)) + := [H:(sigT A P)]<[H:(sigT A P)](P (projT1 H))> + Cases H of (existT x h) => h end. + +End projections_sigT. + +V7only [ +Notation ProjS1 := (projS1 ? ?). +Notation ProjS2 := (projS2 ? ?). +Notation Value := (value ?). +]. + |