diff options
Diffstat (limited to 'theories/Init/Specif.v')
| -rw-r--r-- | theories/Init/Specif.v | 64 |
1 files changed, 34 insertions, 30 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 5a951d14..d1610f0a 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Specif.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Basic specifications : sets that may contain logical information *) Set Implicit Arguments. @@ -40,10 +38,10 @@ Inductive sigT2 (A:Type) (P Q:A -> Type) : Type := (* Notations *) -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]. +Arguments sig (A P)%type. +Arguments sig2 (A P Q)%type. +Arguments sigT (A P)%type. +Arguments sigT2 (A P Q)%type. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. @@ -62,7 +60,7 @@ Add Printing Let sigT2. (** Projections of [sig] - An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] + 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)] *) @@ -128,6 +126,9 @@ Inductive sumbool (A B:Prop) : Set := Add Printing If sumbool. +Arguments left {A B} _, [A] B _. +Arguments right {A B} _ , A [B] _. + (** [sumor] is an option type equipped with the justification of why it may not be a regular value *) @@ -138,6 +139,9 @@ Inductive sumor (A:Type) (B:Prop) : Type := Add Printing If sumor. +Arguments inleft {A B} _ , [A] B _. +Arguments inright {A B} _ , A [B] _. + (** Various forms of the axiom of choice for specifications *) Section Choice_lemmas. @@ -152,16 +156,16 @@ Section Choice_lemmas. Proof. intro H. exists (fun z => proj1_sig (H z)). - intro z; destruct (H z); trivial. - Qed. + intro z; destruct (H z); assumption. + Defined. Lemma Choice2 : (forall x:S, {y:S' & R' x y}) -> {f:S -> S' & forall z:S, R' z (f z)}. Proof. intro H. exists (fun z => projT1 (H z)). - intro z; destruct (H z); trivial. - Qed. + intro z; destruct (H z); assumption. + Defined. Lemma bool_choice : (forall x:S, {R1 x} + {R2 x}) -> @@ -170,7 +174,7 @@ Section Choice_lemmas. intro H. exists (fun z:S => if H z then true else false). intro z; destruct (H z); auto. - Qed. + Defined. End Choice_lemmas. @@ -188,7 +192,7 @@ Section Dependent_choice_lemmas. exists f. split. reflexivity. induction n; simpl; apply proj2_sig. - Qed. + Defined. End Dependent_choice_lemmas. @@ -204,34 +208,34 @@ Definition Exc := option. Definition value := Some. Definition error := @None. -Implicit Arguments error [A]. +Arguments error [A]. Definition except := False_rec. (* for compatibility with previous versions *) -Implicit Arguments except [P]. +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. +Defined. Hint Resolve left right inleft inright: core v62. Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) -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). +Notation sigS := sigT (compat "8.2"). +Notation existS := existT (compat "8.2"). +Notation sigS_rect := sigT_rect (compat "8.2"). +Notation sigS_rec := sigT_rec (compat "8.2"). +Notation sigS_ind := sigT_ind (compat "8.2"). +Notation projS1 := projT1 (compat "8.2"). +Notation projS2 := projT2 (compat "8.2"). + +Notation sigS2 := sigT2 (compat "8.2"). +Notation existS2 := existT2 (compat "8.2"). +Notation sigS2_rect := sigT2_rect (compat "8.2"). +Notation sigS2_rec := sigT2_rec (compat "8.2"). +Notation sigS2_ind := sigT2_ind (compat "8.2"). |