diff options
Diffstat (limited to 'theories/Init/Specif.v')
| -rw-r--r-- | theories/Init/Specif.v | 36 |
1 files changed, 20 insertions, 16 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 5a951d14..637994b2 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-2010 *) (* \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. @@ -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,18 +208,18 @@ 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. |