diff options
author | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-10 15:45:49 +0200 |
---|---|---|
committer | Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-10 16:25:08 +0200 |
commit | 6e66d8c551b5edcb33a9f3fbf744b2f82d944c50 (patch) | |
tree | d23b63653b8b2d58f20661fd5691ccac42e687fb /theories/Init/Specif.v | |
parent | f705a0b0ae587e323199c43e9669b4f96adf4d77 (diff) |
No more Coersion in Init.
Diffstat (limited to 'theories/Init/Specif.v')
-rw-r--r-- | theories/Init/Specif.v | 34 |
1 files changed, 13 insertions, 21 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index d1c567bec..f58c21f48 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -85,7 +85,7 @@ End Subset_projections. (** [sig2] of a predicate can be projected to a [sig]. - This allows [proj1_sig] and [proj2_sig] to work with [sig2]. + This allows [proj1_sig] and [proj2_sig] to be usable 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, @@ -96,14 +96,13 @@ Definition sig_of_sig2 (A : Type) (P Q : A -> Prop) (X : sig2 P Q) : sig 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 + and a proof [h'] that [a] satisfies [Q]. Then + [(proj1_sig (sig_of_sig2 y))] is the witness [a], + [(proj2_sig (sig_of_sig2 y))] is the proof of [(P a)], and [(proj3_sig y)] is the proof of [(Q a)]. *) Section Subset_projections2. @@ -112,7 +111,7 @@ Section Subset_projections2. Variables P Q : A -> Prop. Definition proj3_sig (e : sig2 P Q) := - let (a, b, c) return Q (proj1_sig e) := e in c. + let (a, b, c) return Q (proj1_sig (sig_of_sig2 e)) := e in c. End Subset_projections2. @@ -141,7 +140,7 @@ End Projections. (** [sigT2] of a predicate can be projected to a [sigT]. - This allows [projT1] and [projT2] to work with [sigT2]. + This allows [projT1] and [projT2] to be usable 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, @@ -152,15 +151,14 @@ Definition sigT_of_sigT2 (A : Type) (P Q : A -> Type) (X : sigT2 P Q) : sigT 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]. *) + of type [Q a]. Then, [(projT1 (sigT_of_sigT2 x))] is the first + projection, [(projT2 (sigT_of_sigT2 x))] is the second projection, + and [(projT3 x)] is the third projection, the types of which + depends on the [projT1]. *) Section Projections2. @@ -168,7 +166,7 @@ Section Projections2. Variables P Q : A -> Type. Definition projT3 (e : sigT2 P Q) := - let (a, b, c) return Q (projT1 e) := e in c. + let (a, b, c) return Q (projT1 (sigT_of_sigT2 e)) := e in c. End Projections2. @@ -180,19 +178,13 @@ Definition sig_of_sigT (A : Type) (P : A -> Prop) (X : sigT P) : sig P Definition sigT_of_sig (A : Type) (P : A -> Prop) (X : sig P) : sigT P := existT P (proj1_sig X) (proj2_sig X). -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). + := exist2 P Q (projT1 (sigT_of_sigT2 X)) (projT2 (sigT_of_sigT2 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. + := existT2 P Q (proj1_sig (sig_of_sig2 X)) (proj2_sig (sig_of_sig2 X)) (proj3_sig X). (** [sumbool] is a boolean type equipped with the justification of their value *) |