diff options
Diffstat (limited to 'theories/Init/Specif.v')
| -rw-r--r-- | theories/Init/Specif.v | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index dd2f7697..c0f5c42a 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Specif.v 8866 2006-05-28 16:21:04Z herbelin $ i*) +(*i $Id: Specif.v 10923 2008-05-12 18:25:06Z herbelin $ i*) (** Basic specifications : sets that may contain logical information *) @@ -46,12 +46,12 @@ Arguments Scope sigT [type_scope type_scope]. Arguments Scope sigT2 [type_scope type_scope type_scope]. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. -Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. +Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. Notation "{ x : A | P }" := (sig (fun x:A => P)) : type_scope. -Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) : type_scope. -Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. -Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. +Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) : type_scope. Add Printing Let sig. @@ -107,6 +107,16 @@ Section Projections. End Projections. +(** [sigT] of a predicate is equivalent to [sig] *) + +Lemma sig_of_sigT : forall (A:Type) (P:A->Prop), sigT P -> sig P. +Proof. destruct 1 as (x,H); exists x; trivial. Defined. + +Lemma sigT_of_sig : forall (A:Type) (P:A->Prop), sig P -> sigT P. +Proof. destruct 1 as (x,H); exists x; trivial. Defined. + +Coercion sigT_of_sig : sig >-> sigT. +Coercion sig_of_sigT : sigT >-> sig. (** [sumbool] is a boolean type equipped with the justification of their value *) @@ -201,6 +211,7 @@ Proof. Qed. Hint Resolve left right inleft inright: core v62. +Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) |