diff options
Diffstat (limited to 'theories7/Init/Specif.v')
| -rwxr-xr-x | theories7/Init/Specif.v | 204 |
1 files changed, 0 insertions, 204 deletions
diff --git a/theories7/Init/Specif.v b/theories7/Init/Specif.v deleted file mode 100755 index c39e5ed8..00000000 --- a/theories7/Init/Specif.v +++ /dev/null @@ -1,204 +0,0 @@ -(************************************************************************) -(* 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 ?). -]. - |