From 6e66d8c551b5edcb33a9f3fbf744b2f82d944c50 Mon Sep 17 00:00:00 2001 From: Pierre Boutillier Date: Thu, 10 Apr 2014 15:45:49 +0200 Subject: No more Coersion in Init. --- theories/Init/Specif.v | 34 +++++++++++++--------------------- theories/Reals/Rseries.v | 2 +- theories/Reals/SeqProp.v | 2 +- 3 files changed, 15 insertions(+), 23 deletions(-) (limited to 'theories') 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 *) diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index a5e4f8f7e..328ba27e6 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -261,7 +261,7 @@ Section sequence. Lemma Un_cv_crit : Un_growing -> bound EUn -> exists l : R, Un_cv l. Proof. intros Hug Heub. - exists (projT1 (completeness EUn Heub EUn_noempty)). + exists (proj1_sig (completeness EUn Heub EUn_noempty)). destruct (completeness EUn Heub EUn_noempty) as (l, H). now apply Un_cv_crit_lub. Qed. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 5254ff2cc..52657b401 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -27,7 +27,7 @@ Lemma growing_cv : forall Un:nat -> R, Un_growing Un -> has_ub Un -> { l:R | Un_cv Un l }. Proof. intros Un Hug Heub. - exists (projT1 (completeness (EUn Un) Heub (EUn_noempty Un))). + exists (proj1_sig (completeness (EUn Un) Heub (EUn_noempty Un))). destruct (completeness _ Heub (EUn_noempty Un)) as (l, H). now apply Un_cv_crit_lub. Qed. -- cgit v1.2.3