diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /theories/Init/Specif.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
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 *) |