diff options
author | Jason Gross <jgross@mit.edu> | 2013-11-21 18:42:43 -0500 |
---|---|---|
committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-10 15:05:13 +0200 |
commit | f705a0b0ae587e323199c43e9669b4f96adf4d77 (patch) | |
tree | 08af2d10889d5bbe5593a61241d9e3a70d2b150e /theories/Init/Specif.v | |
parent | ff8bac52149f8a32498f765bd579e00fcbd4f080 (diff) |
Define [projT3] and [proj3_sig]
Also allow [projT1]/[projT2] to work for [sigT2]s and
[proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions.
This closes Bug 3044.
This closes Pull Request #4.
Diffstat (limited to 'theories/Init/Specif.v')
-rw-r--r-- | theories/Init/Specif.v | 78 |
1 files changed, 78 insertions, 0 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index ee8111639..d1c567bec 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -83,6 +83,40 @@ Section Subset_projections. End Subset_projections. +(** [sig2] of a predicate can be projected to a [sig]. + + This allows [proj1_sig] and [proj2_sig] to work with [sig2]. + + The [let] statements occur in the body of the [exist] so that + [proj1_sig] of a coerced [X : sig2 P Q] will unify with [let (a, + _, _) := X in a] *) + +Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig P + := exist P + (let (a, _, _) := X in a) + (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p). + +Coercion sig_of_sig2 : sig2 >-> sig. + +(** Projections of [sig2] + + An element [y] of a subset [{x:A | (P x) & (Q x)}] is the triple + of an [a] of type [A], a of a proof [h] that [a] satisfies [P], + and a proof [h'] that [a] satisfies [Q]. Then [(proj1_sig y)] is + the witness [a], [(proj2_sig y)] is the proof of [(P a)], and + [(proj3_sig y)] is the proof of [(Q a)]. *) + +Section Subset_projections2. + + Variable A : Type. + Variables P Q : A -> Prop. + + Definition proj3_sig (e : sig2 P Q) := + let (a, b, c) return Q (proj1_sig e) := e in c. + +End Subset_projections2. + + (** Projections of [sigT] An element [x] of a sigma-type [{y:A & P y}] is a dependent pair @@ -105,6 +139,39 @@ Section Projections. End Projections. +(** [sigT2] of a predicate can be projected to a [sigT]. + + This allows [projT1] and [projT2] to work with [sigT2]. + + The [let] statements occur in the body of the [existT] so that + [projT1] of a coerced [X : sigT2 P Q] will unify with [let (a, + _, _) := X in a] *) + +Definition sigT_of_sigT2 (A : Type) (P Q : A -> Type) (X : sigT2 P Q) : sigT P + := existT P + (let (a, _, _) := X in a) + (let (x, p, _) as s return (P (let (a, _, _) := s in a)) := X in p). + +Coercion sigT_of_sigT2 : sigT2 >-> sigT. + +(** Projections of [sigT2] + + An element [x] of a sigma-type [{y:A & P y & Q y}] is a dependent + pair made of an [a] of type [A], an [h] of type [P a], and an [h'] + of type [Q a]. Then, [(projT1 x)] is the first projection, + [(projT2 x)] is the second projection, and [(projT3 x)] is the + third projection, the types of which depends on the [projT1]. *) + +Section Projections2. + + Variable A : Type. + Variables P Q : A -> Type. + + Definition projT3 (e : sigT2 P Q) := + let (a, b, c) return Q (projT1 e) := e in c. + +End Projections2. + (** [sigT] of a predicate is equivalent to [sig] *) Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P @@ -116,6 +183,17 @@ Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P Coercion sigT_of_sig : sig >-> sigT. Coercion sig_of_sigT : sigT >-> sig. +(** [sigT2] of a predicate is equivalent to [sig2] *) + +Definition sig2_of_sigT2 (A : Type) (P Q : A -> Prop) (X : sigT2 P Q) : sig2 P Q + := exist2 P Q (projT1 X) (projT2 X) (projT3 X). + +Definition sigT2_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sigT2 P Q + := existT2 P Q (proj1_sig X) (proj2_sig X) (proj3_sig X). + +Coercion sigT2_of_sig2 : sig2 >-> sigT2. +Coercion sig2_of_sigT2 : sigT2 >-> sig2. + (** [sumbool] is a boolean type equipped with the justification of their value *) |