diff options
Diffstat (limited to 'theories/Numbers/Rational/BigQ/QMake.v')
| -rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 485 |
1 files changed, 242 insertions, 243 deletions
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 995fbb9e..a13bb511 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -19,14 +19,14 @@ Require Import NSig ZSig QSig. denominators. But first we will need some glue between [NType] and [ZType]. *) -Module Type NType_ZType (N:NType)(Z:ZType). - Parameter Z_of_N : N.t -> Z.t. - Parameter spec_Z_of_N : forall n, Z.to_Z (Z_of_N n) = N.to_Z n. - Parameter Zabs_N : Z.t -> N.t. - Parameter spec_Zabs_N : forall z, N.to_Z (Zabs_N z) = Zabs (Z.to_Z z). +Module Type NType_ZType (NN:NType)(ZZ:ZType). + Parameter Z_of_N : NN.t -> ZZ.t. + Parameter spec_Z_of_N : forall n, ZZ.to_Z (Z_of_N n) = NN.to_Z n. + Parameter Zabs_N : ZZ.t -> NN.t. + Parameter spec_Zabs_N : forall z, NN.to_Z (Zabs_N z) = Z.abs (ZZ.to_Z z). End NType_ZType. -Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. +Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. (** The notation of a rational number is either an integer x, interpreted as itself or a pair (x,y) of an integer x and a natural @@ -34,8 +34,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. interpreted as 0. *) Inductive t_ := - | Qz : Z.t -> t_ - | Qq : Z.t -> N.t -> t_. + | Qz : ZZ.t -> t_ + | Qq : ZZ.t -> NN.t -> t_. Definition t := t_. @@ -45,41 +45,41 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Local Open Scope Q_scope. - Definition of_Z x: t := Qz (Z.of_Z x). + Definition of_Z x: t := Qz (ZZ.of_Z x). Definition of_Q (q:Q) : t := let (x,y) := q in match y with - | 1%positive => Qz (Z.of_Z x) - | _ => Qq (Z.of_Z x) (N.of_N (Npos y)) + | 1%positive => Qz (ZZ.of_Z x) + | _ => Qq (ZZ.of_Z x) (NN.of_N (Npos y)) end. Definition to_Q (q: t) := match q with - | Qz x => Z.to_Z x # 1 - | Qq x y => if N.eqb y N.zero then 0 - else Z.to_Z x # Z2P (N.to_Z y) + | Qz x => ZZ.to_Z x # 1 + | Qq x y => if NN.eqb y NN.zero then 0 + else ZZ.to_Z x # Z.to_pos (NN.to_Z y) end. Notation "[ x ]" := (to_Q x). Lemma N_to_Z_pos : - forall x, (N.to_Z x <> N.to_Z N.zero)%Z -> (0 < N.to_Z x)%Z. + forall x, (NN.to_Z x <> NN.to_Z NN.zero)%Z -> (0 < NN.to_Z x)%Z. Proof. - intros x; rewrite N.spec_0; generalize (N.spec_pos x). romega. + intros x; rewrite NN.spec_0; generalize (NN.spec_pos x). romega. Qed. Ltac destr_zcompare := case Z.compare_spec; intros ?H. Ltac destr_eqb := match goal with - | |- context [Z.eqb ?x ?y] => - rewrite (Z.spec_eqb x y); - case (Z.eqb_spec (Z.to_Z x) (Z.to_Z y)); + | |- context [ZZ.eqb ?x ?y] => + rewrite (ZZ.spec_eqb x y); + case (Z.eqb_spec (ZZ.to_Z x) (ZZ.to_Z y)); destr_eqb - | |- context [N.eqb ?x ?y] => - rewrite (N.spec_eqb x y); - case (Z.eqb_spec (N.to_Z x) (N.to_Z y)); + | |- context [NN.eqb ?x ?y] => + rewrite (NN.spec_eqb x y); + case (Z.eqb_spec (NN.to_Z x) (NN.to_Z y)); [ | let H:=fresh "H" in try (intro H;generalize (N_to_Z_pos _ H); clear H)]; destr_eqb @@ -87,11 +87,11 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. end. Hint Rewrite - Zplus_0_r Zplus_0_l Zmult_0_r Zmult_0_l Zmult_1_r Zmult_1_l - Z.spec_0 N.spec_0 Z.spec_1 N.spec_1 Z.spec_m1 Z.spec_opp - Z.spec_compare N.spec_compare - Z.spec_add N.spec_add Z.spec_mul N.spec_mul Z.spec_div N.spec_div - Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1 + Z.add_0_r Z.add_0_l Z.mul_0_r Z.mul_0_l Z.mul_1_r Z.mul_1_l + ZZ.spec_0 NN.spec_0 ZZ.spec_1 NN.spec_1 ZZ.spec_m1 ZZ.spec_opp + ZZ.spec_compare NN.spec_compare + ZZ.spec_add NN.spec_add ZZ.spec_mul NN.spec_mul ZZ.spec_div NN.spec_div + ZZ.spec_gcd NN.spec_gcd Z.gcd_abs_l Z.gcd_1_r spec_Z_of_N spec_Zabs_N : nz. @@ -99,13 +99,13 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Ltac qsimpl := try red; unfold to_Q; simpl; intros; destr_eqb; simpl; nzsimpl; intros; - rewrite ?Z2P_correct by auto; + rewrite ?Z2Pos.id by auto; auto. Theorem strong_spec_of_Q: forall q: Q, [of_Q q] = q. Proof. - intros(x,y); destruct y; simpl; rewrite ?Z.spec_of_Z; auto; - destr_eqb; now rewrite ?N.spec_0, ?N.spec_of_N. + intros(x,y); destruct y; simpl; rewrite ?ZZ.spec_of_Z; auto; + destr_eqb; now rewrite ?NN.spec_0, ?NN.spec_of_N. Qed. Theorem spec_of_Q: forall q: Q, [of_Q q] == q. @@ -115,9 +115,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Definition eq x y := [x] == [y]. - Definition zero: t := Qz Z.zero. - Definition one: t := Qz Z.one. - Definition minus_one: t := Qz Z.minus_one. + Definition zero: t := Qz ZZ.zero. + Definition one: t := Qz ZZ.one. + Definition minus_one: t := Qz ZZ.minus_one. Lemma spec_0: [zero] == 0. Proof. @@ -136,20 +136,20 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Definition compare (x y: t) := match x, y with - | Qz zx, Qz zy => Z.compare zx zy + | Qz zx, Qz zy => ZZ.compare zx zy | Qz zx, Qq ny dy => - if N.eqb dy N.zero then Z.compare zx Z.zero - else Z.compare (Z.mul zx (Z_of_N dy)) ny + if NN.eqb dy NN.zero then ZZ.compare zx ZZ.zero + else ZZ.compare (ZZ.mul zx (Z_of_N dy)) ny | Qq nx dx, Qz zy => - if N.eqb dx N.zero then Z.compare Z.zero zy - else Z.compare nx (Z.mul zy (Z_of_N dx)) + if NN.eqb dx NN.zero then ZZ.compare ZZ.zero zy + else ZZ.compare nx (ZZ.mul zy (Z_of_N dx)) | Qq nx dx, Qq ny dy => - match N.eqb dx N.zero, N.eqb dy N.zero with + match NN.eqb dx NN.zero, NN.eqb dy NN.zero with | true, true => Eq - | true, false => Z.compare Z.zero ny - | false, true => Z.compare nx Z.zero - | false, false => Z.compare (Z.mul nx (Z_of_N dy)) - (Z.mul ny (Z_of_N dx)) + | true, false => ZZ.compare ZZ.zero ny + | false, true => ZZ.compare nx ZZ.zero + | false, false => ZZ.compare (ZZ.mul nx (Z_of_N dy)) + (ZZ.mul ny (Z_of_N dx)) end end. @@ -188,7 +188,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *) Definition check_int n d := - match N.compare N.one d with + match NN.compare NN.one d with | Lt => Qq n d | Eq => Qz n | Gt => zero (* n/0 encodes 0 *) @@ -207,9 +207,9 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (** Normalisation function *) Definition norm n d : t := - let gcd := N.gcd (Zabs_N n) d in - match N.compare N.one gcd with - | Lt => check_int (Z.div n (Z_of_N gcd)) (N.div d gcd) + let gcd := NN.gcd (Zabs_N n) d in + match NN.compare NN.one gcd with + | Lt => check_int (ZZ.div n (Z_of_N gcd)) (NN.div d gcd) | Eq => check_int n d | Gt => zero (* gcd = 0 => both numbers are 0 *) end. @@ -217,8 +217,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_norm: forall n q, [norm n q] == [Qq n q]. Proof. intros p q; unfold norm. - assert (Hp := N.spec_pos (Zabs_N p)). - assert (Hq := N.spec_pos q). + assert (Hp := NN.spec_pos (Zabs_N p)). + assert (Hq := NN.spec_pos q). nzsimpl. destr_zcompare. (* Eq *) @@ -226,15 +226,15 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (* Lt *) rewrite strong_spec_check_int. qsimpl. - generalize (Zgcd_div_pos (Z.to_Z p) (N.to_Z q)). romega. - replace (N.to_Z q) with 0%Z in * by assumption. + generalize (Zgcd_div_pos (ZZ.to_Z p) (NN.to_Z q)). romega. + replace (NN.to_Z q) with 0%Z in * by assumption. rewrite Zdiv_0_l in *; auto with zarith. apply Zgcd_div_swap0; romega. (* Gt *) qsimpl. - assert (H' : Zgcd (Z.to_Z p) (N.to_Z q) = 0%Z). - generalize (Zgcd_is_pos (Z.to_Z p) (N.to_Z q)); romega. - symmetry; apply (Zgcd_inv_0_l _ _ H'); auto. + assert (H' : Z.gcd (ZZ.to_Z p) (NN.to_Z q) = 0%Z). + generalize (Z.gcd_nonneg (ZZ.to_Z p) (NN.to_Z q)); romega. + symmetry; apply (Z.gcd_eq_0_l _ _ H'); auto. Qed. Theorem strong_spec_norm : forall p q, [norm p q] = Qred [Qq p q]. @@ -244,8 +244,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (apply Qred_complete; apply spec_norm). symmetry; apply Qred_identity. unfold norm. - assert (Hp := N.spec_pos (Zabs_N p)). - assert (Hq := N.spec_pos q). + assert (Hp := NN.spec_pos (Zabs_N p)). + assert (Hq := NN.spec_pos q). nzsimpl. destr_zcompare; rewrite ?strong_spec_check_int. (* Eq *) @@ -253,10 +253,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (* Lt *) qsimpl. rewrite Zgcd_1_rel_prime. - destruct (Z_lt_le_dec 0 (N.to_Z q)). + destruct (Z_lt_le_dec 0 (NN.to_Z q)). apply Zis_gcd_rel_prime; auto with zarith. apply Zgcd_is_gcd. - replace (N.to_Z q) with 0%Z in * by romega. + replace (NN.to_Z q) with 0%Z in * by romega. rewrite Zdiv_0_l in *; romega. (* Gt *) simpl; auto with zarith. @@ -292,20 +292,20 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. match x with | Qz zx => match y with - | Qz zy => Qz (Z.add zx zy) + | Qz zy => Qz (ZZ.add zx zy) | Qq ny dy => - if N.eqb dy N.zero then x - else Qq (Z.add (Z.mul zx (Z_of_N dy)) ny) dy + if NN.eqb dy NN.zero then x + else Qq (ZZ.add (ZZ.mul zx (Z_of_N dy)) ny) dy end | Qq nx dx => - if N.eqb dx N.zero then y + if NN.eqb dx NN.zero then y else match y with - | Qz zy => Qq (Z.add nx (Z.mul zy (Z_of_N dx))) dx + | Qz zy => Qq (ZZ.add nx (ZZ.mul zy (Z_of_N dx))) dx | Qq ny dy => - if N.eqb dy N.zero then x + if NN.eqb dy NN.zero then x else - let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in - let d := N.mul dx dy in + let n := ZZ.add (ZZ.mul nx (Z_of_N dy)) (ZZ.mul ny (Z_of_N dx)) in + let d := NN.mul dx dy in Qq n d end end. @@ -314,30 +314,30 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Proof. intros [x | nx dx] [y | ny dy]; unfold Qplus; qsimpl; auto with zarith. - rewrite Pmult_1_r, Z2P_correct; auto. - rewrite Pmult_1_r, Z2P_correct; auto. - destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition. - rewrite Zpos_mult_morphism, 2 Z2P_correct; auto. + rewrite Pos.mul_1_r, Z2Pos.id; auto. + rewrite Pos.mul_1_r, Z2Pos.id; auto. + rewrite Z.mul_eq_0 in *; intuition. + rewrite Pos2Z.inj_mul, 2 Z2Pos.id; auto. Qed. Definition add_norm (x y: t): t := match x with | Qz zx => match y with - | Qz zy => Qz (Z.add zx zy) + | Qz zy => Qz (ZZ.add zx zy) | Qq ny dy => - if N.eqb dy N.zero then x - else norm (Z.add (Z.mul zx (Z_of_N dy)) ny) dy + if NN.eqb dy NN.zero then x + else norm (ZZ.add (ZZ.mul zx (Z_of_N dy)) ny) dy end | Qq nx dx => - if N.eqb dx N.zero then y + if NN.eqb dx NN.zero then y else match y with - | Qz zy => norm (Z.add nx (Z.mul zy (Z_of_N dx))) dx + | Qz zy => norm (ZZ.add nx (ZZ.mul zy (Z_of_N dx))) dx | Qq ny dy => - if N.eqb dy N.zero then x + if NN.eqb dy NN.zero then x else - let n := Z.add (Z.mul nx (Z_of_N dy)) (Z.mul ny (Z_of_N dx)) in - let d := N.mul dx dy in + let n := ZZ.add (ZZ.mul nx (Z_of_N dy)) (ZZ.mul ny (Z_of_N dx)) in + let d := NN.mul dx dy in norm n d end end. @@ -363,18 +363,18 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Definition opp (x: t): t := match x with - | Qz zx => Qz (Z.opp zx) - | Qq nx dx => Qq (Z.opp nx) dx + | Qz zx => Qz (ZZ.opp zx) + | Qq nx dx => Qq (ZZ.opp nx) dx end. Theorem strong_spec_opp: forall q, [opp q] = -[q]. Proof. intros [z | x y]; simpl. - rewrite Z.spec_opp; auto. - match goal with |- context[N.eqb ?X ?Y] => - generalize (N.spec_eqb X Y); case N.eqb - end; auto; rewrite N.spec_0. - rewrite Z.spec_opp; auto. + rewrite ZZ.spec_opp; auto. + match goal with |- context[NN.eqb ?X ?Y] => + generalize (NN.spec_eqb X Y); case NN.eqb + end; auto; rewrite NN.spec_0. + rewrite ZZ.spec_opp; auto. Qed. Theorem spec_opp : forall q, [opp q] == -[q]. @@ -416,28 +416,28 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Definition mul (x y: t): t := match x, y with - | Qz zx, Qz zy => Qz (Z.mul zx zy) - | Qz zx, Qq ny dy => Qq (Z.mul zx ny) dy - | Qq nx dx, Qz zy => Qq (Z.mul nx zy) dx - | Qq nx dx, Qq ny dy => Qq (Z.mul nx ny) (N.mul dx dy) + | Qz zx, Qz zy => Qz (ZZ.mul zx zy) + | Qz zx, Qq ny dy => Qq (ZZ.mul zx ny) dy + | Qq nx dx, Qz zy => Qq (ZZ.mul nx zy) dx + | Qq nx dx, Qq ny dy => Qq (ZZ.mul nx ny) (NN.mul dx dy) end. Ltac nsubst := - match goal with E : N.to_Z _ = _ |- _ => rewrite E in * end. + match goal with E : NN.to_Z _ = _ |- _ => rewrite E in * end. Theorem spec_mul : forall x y, [mul x y] == [x] * [y]. Proof. intros [x | nx dx] [y | ny dy]; unfold Qmult; simpl; qsimpl. - rewrite Pmult_1_r, Z2P_correct; auto. - destruct (Zmult_integral (N.to_Z dx) (N.to_Z dy)); intuition. + rewrite Pos.mul_1_r, Z2Pos.id; auto. + rewrite Z.mul_eq_0 in *; intuition. nsubst; auto with zarith. nsubst; auto with zarith. nsubst; nzsimpl; auto with zarith. - rewrite Zpos_mult_morphism, 2 Z2P_correct; auto. + rewrite Pos2Z.inj_mul, 2 Z2Pos.id; auto. Qed. Definition norm_denum n d := - if N.eqb d N.one then Qz n else Qq n d. + if NN.eqb d NN.one then Qz n else Qq n d. Lemma spec_norm_denum : forall n d, [norm_denum n d] == [Qq n d]. @@ -448,40 +448,40 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Qed. Definition irred n d := - let gcd := N.gcd (Zabs_N n) d in - match N.compare gcd N.one with - | Gt => (Z.div n (Z_of_N gcd), N.div d gcd) + let gcd := NN.gcd (Zabs_N n) d in + match NN.compare gcd NN.one with + | Gt => (ZZ.div n (Z_of_N gcd), NN.div d gcd) | _ => (n, d) end. Lemma spec_irred : forall n d, exists g, let (n',d') := irred n d in - (Z.to_Z n' * g = Z.to_Z n)%Z /\ (N.to_Z d' * g = N.to_Z d)%Z. + (ZZ.to_Z n' * g = ZZ.to_Z n)%Z /\ (NN.to_Z d' * g = NN.to_Z d)%Z. Proof. intros. unfold irred; nzsimpl; simpl. destr_zcompare. exists 1%Z; nzsimpl; auto. exists 0%Z; nzsimpl. - assert (Zgcd (Z.to_Z n) (N.to_Z d) = 0%Z). - generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega. + assert (Z.gcd (ZZ.to_Z n) (NN.to_Z d) = 0%Z). + generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); romega. clear H. split. - symmetry; apply (Zgcd_inv_0_l _ _ H0). - symmetry; apply (Zgcd_inv_0_r _ _ H0). - exists (Zgcd (Z.to_Z n) (N.to_Z d)). + symmetry; apply (Z.gcd_eq_0_l _ _ H0). + symmetry; apply (Z.gcd_eq_0_r _ _ H0). + exists (Z.gcd (ZZ.to_Z n) (NN.to_Z d)). simpl. split. nzsimpl. - destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)). - rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith. + destruct (Zgcd_is_gcd (ZZ.to_Z n) (NN.to_Z d)). + rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith. nzsimpl. - destruct (Zgcd_is_gcd (Z.to_Z n) (N.to_Z d)). - rewrite Zmult_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith. + destruct (Zgcd_is_gcd (ZZ.to_Z n) (NN.to_Z d)). + rewrite Z.mul_comm; symmetry; apply Zdivide_Zdiv_eq; auto with zarith. Qed. Lemma spec_irred_zero : forall n d, - (N.to_Z d = 0)%Z <-> (N.to_Z (snd (irred n d)) = 0)%Z. + (NN.to_Z d = 0)%Z <-> (NN.to_Z (snd (irred n d)) = 0)%Z. Proof. intros. unfold irred. @@ -494,8 +494,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. nzsimpl; destr_zcompare; simpl; auto. nzsimpl. intros. - generalize (N.spec_pos d); intros. - destruct (N.to_Z d); auto. + generalize (NN.spec_pos d); intros. + destruct (NN.to_Z d); auto. assert (0 < 0)%Z. rewrite <- H0 at 2. apply Zgcd_div_pos; auto with zarith. @@ -505,49 +505,49 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Qed. Lemma strong_spec_irred : forall n d, - (N.to_Z d <> 0%Z) -> - let (n',d') := irred n d in Zgcd (Z.to_Z n') (N.to_Z d') = 1%Z. + (NN.to_Z d <> 0%Z) -> + let (n',d') := irred n d in Z.gcd (ZZ.to_Z n') (NN.to_Z d') = 1%Z. Proof. unfold irred; intros. nzsimpl. destr_zcompare; simpl; auto. elim H. - apply (Zgcd_inv_0_r (Z.to_Z n)). - generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega. + apply (Z.gcd_eq_0_r (ZZ.to_Z n)). + generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); romega. nzsimpl. rewrite Zgcd_1_rel_prime. apply Zis_gcd_rel_prime. - generalize (N.spec_pos d); romega. - generalize (Zgcd_is_pos (Z.to_Z n) (N.to_Z d)); romega. + generalize (NN.spec_pos d); romega. + generalize (Z.gcd_nonneg (ZZ.to_Z n) (NN.to_Z d)); romega. apply Zgcd_is_gcd; auto. Qed. Definition mul_norm_Qz_Qq z n d := - if Z.eqb z Z.zero then zero + if ZZ.eqb z ZZ.zero then zero else - let gcd := N.gcd (Zabs_N z) d in - match N.compare gcd N.one with + let gcd := NN.gcd (Zabs_N z) d in + match NN.compare gcd NN.one with | Gt => - let z := Z.div z (Z_of_N gcd) in - let d := N.div d gcd in - norm_denum (Z.mul z n) d - | _ => Qq (Z.mul z n) d + let z := ZZ.div z (Z_of_N gcd) in + let d := NN.div d gcd in + norm_denum (ZZ.mul z n) d + | _ => Qq (ZZ.mul z n) d end. Definition mul_norm (x y: t): t := match x, y with - | Qz zx, Qz zy => Qz (Z.mul zx zy) + | Qz zx, Qz zy => Qz (ZZ.mul zx zy) | Qz zx, Qq ny dy => mul_norm_Qz_Qq zx ny dy | Qq nx dx, Qz zy => mul_norm_Qz_Qq zy nx dx | Qq nx dx, Qq ny dy => let (nx, dy) := irred nx dy in let (ny, dx) := irred ny dx in - norm_denum (Z.mul ny nx) (N.mul dx dy) + norm_denum (ZZ.mul ny nx) (NN.mul dx dy) end. Lemma spec_mul_norm_Qz_Qq : forall z n d, - [mul_norm_Qz_Qq z n d] == [Qq (Z.mul z n) d]. + [mul_norm_Qz_Qq z n d] == [Qq (ZZ.mul z n) d]. Proof. intros z n d; unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. destr_eqb; nzsimpl; intros Hz. @@ -558,7 +558,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. qsimpl. rewrite Zdiv_gcd_zero in GT; auto with zarith. nsubst. rewrite Zdiv_0_l in *; discriminate. - rewrite <- Zmult_assoc, (Zmult_comm (Z.to_Z n)), Zmult_assoc. + rewrite <- Z.mul_assoc, (Z.mul_comm (ZZ.to_Z n)), Z.mul_assoc. rewrite Zgcd_div_swap0; try romega. ring. Qed. @@ -582,34 +582,34 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destr_eqb; simpl; nzsimpl; auto. nzsimpl; rewrite Hd, Zdiv_0_l; auto with zarith. - rewrite Z2P_correct in H; auto. + rewrite Z2Pos.id in H; auto. unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto. destruct Z_le_gt_dec as [H'|H']. simpl; nzsimpl. destr_eqb; simpl; nzsimpl; auto. intros. - rewrite Z2P_correct; auto. + rewrite Z2Pos.id; auto. apply Zgcd_mult_rel_prime; auto. - generalize (Zgcd_inv_0_l (Z.to_Z z) (N.to_Z d)) - (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega. + generalize (Z.gcd_eq_0_l (ZZ.to_Z z) (NN.to_Z d)) + (Z.gcd_nonneg (ZZ.to_Z z) (NN.to_Z d)); romega. destr_eqb; simpl; nzsimpl; auto. unfold norm_denum. destr_eqb; nzsimpl; simpl; destr_eqb; simpl; auto. intros; nzsimpl. - rewrite Z2P_correct; auto. + rewrite Z2Pos.id; auto. apply Zgcd_mult_rel_prime. rewrite Zgcd_1_rel_prime. apply Zis_gcd_rel_prime. - generalize (N.spec_pos d); romega. - generalize (Zgcd_is_pos (Z.to_Z z) (N.to_Z d)); romega. + generalize (NN.spec_pos d); romega. + generalize (Z.gcd_nonneg (ZZ.to_Z z) (NN.to_Z d)); romega. apply Zgcd_is_gcd. - destruct (Zgcd_is_gcd (Z.to_Z z) (N.to_Z d)) as [ (z0,Hz0) (d0,Hd0) Hzd]. - replace (N.to_Z d / Zgcd (Z.to_Z z) (N.to_Z d))%Z with d0. + destruct (Zgcd_is_gcd (ZZ.to_Z z) (NN.to_Z d)) as [ (z0,Hz0) (d0,Hd0) Hzd]. + replace (NN.to_Z d / Z.gcd (ZZ.to_Z z) (NN.to_Z d))%Z with d0. rewrite Zgcd_1_rel_prime in *. apply bezout_rel_prime. destruct (rel_prime_bezout _ _ H) as [u v Huv]. - apply Bezout_intro with u (v*(Zgcd (Z.to_Z z) (N.to_Z d)))%Z. + apply Bezout_intro with u (v*(Z.gcd (ZZ.to_Z z) (NN.to_Z d)))%Z. rewrite <- Huv; rewrite Hd0 at 2; ring. rewrite Hd0 at 1. symmetry; apply Z_div_mult_full; auto with zarith. @@ -634,14 +634,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. qsimpl. match goal with E : (_ * _ = 0)%Z |- _ => - destruct (Zmult_integral _ _ E) as [Eq|Eq] end. + rewrite Z.mul_eq_0 in E; destruct E as [Eq|Eq] end. rewrite Eq in *; simpl in *. rewrite <- Hg2' in *; auto with zarith. rewrite Eq in *; simpl in *. rewrite <- Hg2 in *; auto with zarith. match goal with E : (_ * _ = 0)%Z |- _ => - destruct (Zmult_integral _ _ E) as [Eq|Eq] end. + rewrite Z.mul_eq_0 in E; destruct E as [Eq|Eq] end. rewrite Hz' in Eq; rewrite Eq in *; auto with zarith. rewrite Hz in Eq; rewrite Eq in *; auto with zarith. @@ -671,31 +671,31 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. unfold norm_denum; qsimpl. - assert (NEQ : N.to_Z dy <> 0%Z) by + assert (NEQ : NN.to_Z dy <> 0%Z) by (rewrite Hz; intros EQ; rewrite EQ in *; romega). specialize (Hgc NEQ). - assert (NEQ' : N.to_Z dx <> 0%Z) by + assert (NEQ' : NN.to_Z dx <> 0%Z) by (rewrite Hz'; intro EQ; rewrite EQ in *; romega). specialize (Hgc' NEQ'). revert H H0. rewrite 2 strong_spec_red, 2 Qred_iff; simpl. destr_eqb; simpl; nzsimpl; try romega; intros. - rewrite Z2P_correct in *; auto. + rewrite Z2Pos.id in *; auto. - apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; - apply Zgcd_mult_rel_prime; rewrite Zgcd_comm; auto. + apply Zgcd_mult_rel_prime; rewrite Z.gcd_comm; + apply Zgcd_mult_rel_prime; rewrite Z.gcd_comm; auto. rewrite Zgcd_1_rel_prime in *. apply bezout_rel_prime. - destruct (rel_prime_bezout (Z.to_Z ny) (N.to_Z dy)) as [u v Huv]; trivial. + destruct (rel_prime_bezout (ZZ.to_Z ny) (NN.to_Z dy)) as [u v Huv]; trivial. apply Bezout_intro with (u*g')%Z (v*g)%Z. rewrite <- Huv, <- Hg1', <- Hg2. ring. rewrite Zgcd_1_rel_prime in *. apply bezout_rel_prime. - destruct (rel_prime_bezout (Z.to_Z nx) (N.to_Z dx)) as [u v Huv]; trivial. + destruct (rel_prime_bezout (ZZ.to_Z nx) (NN.to_Z dx)) as [u v Huv]; trivial. apply Bezout_intro with (u*g)%Z (v*g')%Z. rewrite <- Huv, <- Hg2', <- Hg1. ring. Qed. @@ -703,16 +703,16 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Definition inv (x: t): t := match x with | Qz z => - match Z.compare Z.zero z with + match ZZ.compare ZZ.zero z with | Eq => zero - | Lt => Qq Z.one (Zabs_N z) - | Gt => Qq Z.minus_one (Zabs_N z) + | Lt => Qq ZZ.one (Zabs_N z) + | Gt => Qq ZZ.minus_one (Zabs_N z) end | Qq n d => - match Z.compare Z.zero n with + match ZZ.compare ZZ.zero n with | Eq => zero | Lt => Qq (Z_of_N d) (Zabs_N n) - | Gt => Qq (Z.opp (Z_of_N d)) (Zabs_N n) + | Gt => Qq (ZZ.opp (Z_of_N d)) (Zabs_N n) end end. @@ -721,29 +721,29 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destruct x as [ z | n d ]. (* Qz z *) simpl. - rewrite Z.spec_compare; destr_zcompare. + rewrite ZZ.spec_compare; destr_zcompare. (* 0 = z *) rewrite <- H. simpl; nzsimpl; compute; auto. (* 0 < z *) simpl. - destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ]. - set (z':=Z.to_Z z) in *; clearbody z'. + destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; romega | intros _ ]. + set (z':=ZZ.to_Z z) in *; clearbody z'. red; simpl. - rewrite Zabs_eq by romega. - rewrite Z2P_correct by auto. + rewrite Z.abs_eq by romega. + rewrite Z2Pos.id by auto. unfold Qinv; simpl; destruct z'; simpl; auto; discriminate. (* 0 > z *) simpl. - destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ]. - set (z':=Z.to_Z z) in *; clearbody z'. + destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; romega | intros _ ]. + set (z':=ZZ.to_Z z) in *; clearbody z'. red; simpl. - rewrite Zabs_non_eq by romega. - rewrite Z2P_correct by romega. + rewrite Z.abs_neq by romega. + rewrite Z2Pos.id by romega. unfold Qinv; simpl; destruct z'; simpl; auto; discriminate. (* Qq n d *) simpl. - rewrite Z.spec_compare; destr_zcompare. + rewrite ZZ.spec_compare; destr_zcompare. (* 0 = n *) rewrite <- H. simpl; nzsimpl. @@ -751,51 +751,51 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (* 0 < n *) simpl. destr_eqb; nzsimpl; intros. - intros; rewrite Zabs_eq in *; romega. - intros; rewrite Zabs_eq in *; romega. + intros; rewrite Z.abs_eq in *; romega. + intros; rewrite Z.abs_eq in *; romega. nsubst; compute; auto. - set (n':=Z.to_Z n) in *; clearbody n'. - rewrite Zabs_eq by romega. + set (n':=ZZ.to_Z n) in *; clearbody n'. + rewrite Z.abs_eq by romega. red; simpl. - rewrite Z2P_correct by auto. + rewrite Z2Pos.id by auto. unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate. - rewrite Zpos_mult_morphism, Z2P_correct; auto. + rewrite Pos2Z.inj_mul, Z2Pos.id; auto. (* 0 > n *) simpl. destr_eqb; nzsimpl; intros. - intros; rewrite Zabs_non_eq in *; romega. - intros; rewrite Zabs_non_eq in *; romega. + intros; rewrite Z.abs_neq in *; romega. + intros; rewrite Z.abs_neq in *; romega. nsubst; compute; auto. - set (n':=Z.to_Z n) in *; clearbody n'. + set (n':=ZZ.to_Z n) in *; clearbody n'. red; simpl; nzsimpl. - rewrite Zabs_non_eq by romega. - rewrite Z2P_correct by romega. + rewrite Z.abs_neq by romega. + rewrite Z2Pos.id by romega. unfold Qinv; simpl; destruct n'; simpl; auto; try discriminate. - assert (T : forall x, Zneg x = Zopp (Zpos x)) by auto. - rewrite T, Zpos_mult_morphism, Z2P_correct; auto; ring. + assert (T : forall x, Zneg x = Z.opp (Zpos x)) by auto. + rewrite T, Pos2Z.inj_mul, Z2Pos.id; auto; ring. Qed. Definition inv_norm (x: t): t := match x with | Qz z => - match Z.compare Z.zero z with + match ZZ.compare ZZ.zero z with | Eq => zero - | Lt => Qq Z.one (Zabs_N z) - | Gt => Qq Z.minus_one (Zabs_N z) + | Lt => Qq ZZ.one (Zabs_N z) + | Gt => Qq ZZ.minus_one (Zabs_N z) end | Qq n d => - if N.eqb d N.zero then zero else - match Z.compare Z.zero n with + if NN.eqb d NN.zero then zero else + match ZZ.compare ZZ.zero n with | Eq => zero | Lt => - match Z.compare n Z.one with + match ZZ.compare n ZZ.one with | Gt => Qq (Z_of_N d) (Zabs_N n) | _ => Qz (Z_of_N d) end | Gt => - match Z.compare n Z.minus_one with - | Lt => Qq (Z.opp (Z_of_N d)) (Zabs_N n) - | _ => Qz (Z.opp (Z_of_N d)) + match ZZ.compare n ZZ.minus_one with + | Lt => Qq (ZZ.opp (Z_of_N d)) (Zabs_N n) + | _ => Qz (ZZ.opp (Z_of_N d)) end end end. @@ -807,7 +807,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. destruct x as [ z | n d ]. (* Qz z *) simpl. - rewrite Z.spec_compare; destr_zcompare; auto with qarith. + rewrite ZZ.spec_compare; destr_zcompare; auto with qarith. (* Qq n d *) simpl; nzsimpl; destr_eqb. destr_zcompare; simpl; auto with qarith. @@ -818,12 +818,12 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (* 0 < n *) destr_zcompare; auto with qarith. destr_zcompare; nzsimpl; simpl; auto with qarith; intros. - destr_eqb; nzsimpl; [ intros; rewrite Zabs_eq in *; romega | intros _ ]. + destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; romega | intros _ ]. rewrite H0; auto with qarith. romega. (* 0 > n *) destr_zcompare; nzsimpl; simpl; auto with qarith. - destr_eqb; nzsimpl; [ intros; rewrite Zabs_non_eq in *; romega | intros _ ]. + destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; romega | intros _ ]. rewrite H0; auto with qarith. romega. Qed. @@ -847,36 +847,36 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. (* 0 < n *) destr_zcompare; simpl; nzsimpl; auto. destr_eqb; nzsimpl; simpl; auto. - rewrite Zabs_eq; romega. + rewrite Z.abs_eq; romega. intros _. rewrite strong_spec_norm; simpl; nzsimpl. destr_eqb; nzsimpl. - rewrite Zabs_eq; romega. + rewrite Z.abs_eq; romega. intros _. rewrite Qred_iff. simpl. - rewrite Zabs_eq; auto with zarith. - rewrite Z2P_correct in *; auto. - rewrite Zgcd_comm; auto. + rewrite Z.abs_eq; auto with zarith. + rewrite Z2Pos.id in *; auto. + rewrite Z.gcd_comm; auto. (* 0 > n *) destr_eqb; nzsimpl; simpl; auto; intros. destr_zcompare; simpl; nzsimpl; auto. destr_eqb; nzsimpl. - rewrite Zabs_non_eq; romega. + rewrite Z.abs_neq; romega. intros _. rewrite strong_spec_norm; simpl; nzsimpl. destr_eqb; nzsimpl. - rewrite Zabs_non_eq; romega. + rewrite Z.abs_neq; romega. intros _. rewrite Qred_iff. simpl. - rewrite Z2P_correct in *; auto. + rewrite Z2Pos.id in *; auto. intros. - rewrite Zgcd_comm, Zgcd_Zabs, Zgcd_comm. + rewrite Z.gcd_comm, Z.gcd_abs_l, Z.gcd_comm. apply Zis_gcd_gcd; auto with zarith. apply Zis_gcd_minus. - rewrite Zopp_involutive, <- H1; apply Zgcd_is_gcd. - rewrite Zabs_non_eq; romega. + rewrite Z.opp_involutive, <- H1; apply Zgcd_is_gcd. + rewrite Z.abs_neq; romega. Qed. Definition div x y := mul x (inv y). @@ -909,31 +909,30 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Definition square (x: t): t := match x with - | Qz zx => Qz (Z.square zx) - | Qq nx dx => Qq (Z.square nx) (N.square dx) + | Qz zx => Qz (ZZ.square zx) + | Qq nx dx => Qq (ZZ.square nx) (NN.square dx) end. Theorem spec_square : forall x, [square x] == [x] ^ 2. Proof. destruct x as [ z | n d ]. - simpl; rewrite Z.spec_square; red; auto. + simpl; rewrite ZZ.spec_square; red; auto. simpl. destr_eqb; nzsimpl; intros. apply Qeq_refl. - rewrite N.spec_square in *; nzsimpl. - match goal with E : (_ * _ = 0)%Z |- _ => - elim (Zmult_integral _ _ E); romega end. - rewrite N.spec_square in *; nzsimpl; nsubst; romega. - rewrite Z.spec_square, N.spec_square. + rewrite NN.spec_square in *; nzsimpl. + rewrite Z.mul_eq_0 in *; romega. + rewrite NN.spec_square in *; nzsimpl; nsubst; romega. + rewrite ZZ.spec_square, NN.spec_square. red; simpl. - rewrite Zpos_mult_morphism; rewrite !Z2P_correct; auto. - apply Zmult_lt_0_compat; auto. + rewrite Pos2Z.inj_mul; rewrite !Z2Pos.id; auto. + apply Z.mul_pos_pos; auto. Qed. Definition power_pos (x : t) p : t := match x with - | Qz zx => Qz (Z.pow_pos zx p) - | Qq nx dx => Qq (Z.pow_pos nx p) (N.pow_pos dx p) + | Qz zx => Qz (ZZ.pow_pos zx p) + | Qq nx dx => Qq (ZZ.pow_pos nx p) (NN.pow_pos dx p) end. Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p. @@ -941,26 +940,26 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. intros [ z | n d ] p; unfold power_pos. (* Qz *) simpl. - rewrite Z.spec_pow_pos. - rewrite Qpower_decomp. + rewrite ZZ.spec_pow_pos, Qpower_decomp. red; simpl; f_equal. - rewrite Zpower_pos_1_l; auto. + now rewrite Pos2Z.inj_pow, Z.pow_1_l. (* Qq *) simpl. - rewrite Z.spec_pow_pos. + rewrite ZZ.spec_pow_pos. destr_eqb; nzsimpl; intros. - apply Qeq_sym; apply Qpower_positive_0. - rewrite N.spec_pow_pos in *. - assert (0 < N.to_Z d ^ ' p)%Z by - (apply Zpower_gt_0; auto with zarith). - romega. - exfalso. - rewrite N.spec_pow_pos in *. nsubst. - rewrite Zpower_0_l in *; [romega|discriminate]. - rewrite Qpower_decomp. - red; simpl; do 3 f_equal. - rewrite Z2P_correct by (generalize (N.spec_pos d); romega). - rewrite N.spec_pow_pos. auto. + - apply Qeq_sym; apply Qpower_positive_0. + - rewrite NN.spec_pow_pos in *. + assert (0 < NN.to_Z d ^ ' p)%Z by + (apply Z.pow_pos_nonneg; auto with zarith). + romega. + - exfalso. + rewrite NN.spec_pow_pos in *. nsubst. + rewrite Z.pow_0_l' in *; [romega|discriminate]. + - rewrite Qpower_decomp. + red; simpl; do 3 f_equal. + apply Pos2Z.inj. rewrite Pos2Z.inj_pow. + rewrite 2 Z2Pos.id by (generalize (NN.spec_pos d); romega). + now rewrite NN.spec_pow_pos. Qed. Instance strong_spec_power_pos x p `(Reduced x) : Reduced (power_pos x p). @@ -976,10 +975,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl. destr_eqb; nzsimpl; simpl; intros. exfalso. - rewrite N.spec_pow_pos in *. nsubst. - rewrite Zpower_0_l in *; [romega|discriminate]. - rewrite Z2P_correct in *; auto. - rewrite N.spec_pow_pos, Z.spec_pow_pos; auto. + rewrite NN.spec_pow_pos in *. nsubst. + rewrite Z.pow_0_l' in *; [romega|discriminate]. + rewrite Z2Pos.id in *; auto. + rewrite NN.spec_pow_pos, ZZ.spec_pow_pos; auto. rewrite Zgcd_1_rel_prime in *. apply rel_prime_Zpower; auto with zarith. Qed. @@ -1086,7 +1085,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. [[add x y]] = [[x]] + [[y]]. Proof. unfold to_Qc. - apply trans_equal with (!! ([x] + [y])). + transitivity (!! ([x] + [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete; apply spec_add; auto. @@ -1100,7 +1099,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. [[add_norm x y]] = [[x]] + [[y]]. Proof. unfold to_Qc. - apply trans_equal with (!! ([x] + [y])). + transitivity (!! ([x] + [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete; apply spec_add_norm; auto. @@ -1148,7 +1147,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. [[mul x y]] = [[x]] * [[y]]. Proof. unfold to_Qc. - apply trans_equal with (!! ([x] * [y])). + transitivity (!! ([x] * [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete; apply spec_mul; auto. @@ -1162,7 +1161,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. [[mul_norm x y]] = [[x]] * [[y]]. Proof. unfold to_Qc. - apply trans_equal with (!! ([x] * [y])). + transitivity (!! ([x] * [y])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete; apply spec_mul_norm; auto. @@ -1186,7 +1185,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. [[inv x]] = /[[x]]. Proof. unfold to_Qc. - apply trans_equal with (!! (/[x])). + transitivity (!! (/[x])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete; apply spec_inv; auto. @@ -1200,7 +1199,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. [[inv_norm x]] = /[[x]]. Proof. unfold to_Qc. - apply trans_equal with (!! (/[x])). + transitivity (!! (/[x])). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete; apply spec_inv_norm; auto. @@ -1248,7 +1247,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Theorem spec_squarec x: [[square x]] = [[x]]^2. Proof. unfold to_Qc. - apply trans_equal with (!! ([x]^2)). + transitivity (!! ([x]^2)). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete; apply spec_square; auto. @@ -1262,24 +1261,24 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Qed. Theorem spec_power_posc x p: - [[power_pos x p]] = [[x]] ^ nat_of_P p. + [[power_pos x p]] = [[x]] ^ Pos.to_nat p. Proof. unfold to_Qc. - apply trans_equal with (!! ([x]^Zpos p)). + transitivity (!! ([x]^Zpos p)). unfold Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete; apply spec_power_pos; auto. - induction p using Pind. + induction p using Pos.peano_ind. simpl; ring. - rewrite Psucc_S; simpl Qcpower. + rewrite Pos2Nat.inj_succ; simpl Qcpower. rewrite <- IHp; clear IHp. unfold Qcmult, Q2Qc. apply Qc_decomp; intros _ _; unfold this. apply Qred_complete. - setoid_replace ([x] ^ ' Psucc p)%Q with ([x] * [x] ^ ' p)%Q. + setoid_replace ([x] ^ ' Pos.succ p)%Q with ([x] * [x] ^ ' p)%Q. apply Qmult_comp; apply Qeq_sym; apply Qred_correct. simpl. - rewrite Pplus_one_succ_l. + rewrite <- Pos.add_1_l. rewrite Qpower_plus_positive; simpl; apply Qeq_refl. Qed. |