From fa40ac396cc5de7cbda65e1d15c406b4baa36040 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 28 Feb 2017 14:59:34 +0100 Subject: [PATCH] Adapt to new definition of IZR. --- src/Core/Fcore_Raux.v | 166 ++++-------------------------------------- 1 file changed, 14 insertions(+), 152 deletions(-) diff --git a/src/Core/Fcore_Raux.v b/src/Core/Fcore_Raux.v index ebaf1db..932bac1 100644 --- a/src/Core/Fcore_Raux.v +++ b/src/Core/Fcore_Raux.v @@ -387,132 +387,20 @@ Qed. End Rmissing. -Section Z2R. - -(** Z2R function (Z -> R) *) -Fixpoint P2R (p : positive) := - match p with - | xH => 1%R - | xO xH => 2%R - | xO t => (2 * P2R t)%R - | xI xH => 3%R - | xI t => (1 + 2 * P2R t)%R - end. - -Definition Z2R n := - match n with - | Zpos p => P2R p - | Zneg p => Ropp (P2R p) - | Z0 => R0 - end. - -Theorem P2R_INR : - forall n, P2R n = INR (nat_of_P n). -Proof. -induction n ; simpl ; try ( - rewrite IHn ; - rewrite <- (mult_INR 2) ; - rewrite <- (nat_of_P_mult_morphism 2) ; - change (2 * n)%positive with (xO n)). -(* xI *) -rewrite (Rplus_comm 1). -change (nat_of_P (xO n)) with (Pmult_nat n 2). -case n ; intros ; simpl ; try apply refl_equal. -case (Pmult_nat p 4) ; intros ; try apply refl_equal. -rewrite Rplus_0_l. -apply refl_equal. -apply Rplus_comm. -(* xO *) -case n ; intros ; apply refl_equal. -(* xH *) -apply refl_equal. -Qed. - -Theorem Z2R_IZR : - forall n, Z2R n = IZR n. -Proof. -intro. -case n ; intros ; simpl. -apply refl_equal. -apply P2R_INR. -apply Ropp_eq_compat. -apply P2R_INR. -Qed. - -Theorem Z2R_opp : - forall n, Z2R (-n) = (- Z2R n)%R. -Proof. -intros. -repeat rewrite Z2R_IZR. -apply Ropp_Ropp_IZR. -Qed. - -Theorem Z2R_plus : - forall m n, (Z2R (m + n) = Z2R m + Z2R n)%R. -Proof. -intros. -repeat rewrite Z2R_IZR. -apply plus_IZR. -Qed. - -Theorem minus_IZR : - forall n m : Z, - IZR (n - m) = (IZR n - IZR m)%R. -Proof. -intros. -unfold Zminus. -rewrite plus_IZR. -rewrite Ropp_Ropp_IZR. -apply refl_equal. -Qed. - -Theorem Z2R_minus : - forall m n, (Z2R (m - n) = Z2R m - Z2R n)%R. -Proof. -intros. -repeat rewrite Z2R_IZR. -apply minus_IZR. -Qed. - -Theorem Z2R_mult : - forall m n, (Z2R (m * n) = Z2R m * Z2R n)%R. -Proof. -intros. -repeat rewrite Z2R_IZR. -apply mult_IZR. -Qed. - -Theorem le_Z2R : - forall m n, (Z2R m <= Z2R n)%R -> (m <= n)%Z. -Proof. -intros m n. -repeat rewrite Z2R_IZR. -apply le_IZR. -Qed. - -Theorem Z2R_le : - forall m n, (m <= n)%Z -> (Z2R m <= Z2R n)%R. -Proof. -intros m n. -repeat rewrite Z2R_IZR. -apply IZR_le. -Qed. - -Theorem lt_Z2R : - forall m n, (Z2R m < Z2R n)%R -> (m < n)%Z. -Proof. -intros m n. -repeat rewrite Z2R_IZR. -apply lt_IZR. -Qed. +Notation Z2R := IZR. +Notation Z2R_opp := opp_IZR. +Notation Z2R_plus := plus_IZR. +Notation Z2R_minus := minus_IZR. +Notation Z2R_mult := mult_IZR. +Notation le_Z2R := le_IZR. +Notation Z2R_le := IZR_le. +Notation lt_Z2R := lt_IZR. +Notation Z2R_lt := IZR_lt. +Notation eq_Z2R := eq_IZR. +Notation Z2R_neq := IZR_neq. +Notation Z2R_abs := abs_IZR. -Theorem Z2R_lt : - forall m n, (m < n)%Z -> (Z2R m < Z2R n)%R. -Proof. -intros m n. -repeat rewrite Z2R_IZR. -apply IZR_lt. -Qed. +Section Z2R. Theorem Z2R_le_lt : forall m n p, (m <= n < p)%Z -> (Z2R m <= Z2R n < Z2R p)%R. @@ -532,14 +420,6 @@ now apply le_Z2R. now apply lt_Z2R. Qed. -Theorem eq_Z2R : - forall m n, (Z2R m = Z2R n)%R -> (m = n)%Z. -Proof. -intros m n H. -apply eq_IZR. -now rewrite <- 2!Z2R_IZR. -Qed. - Theorem neq_Z2R : forall m n, (Z2R m <> Z2R n)%R -> (m <> n)%Z. Proof. @@ -548,22 +428,6 @@ apply H. now apply f_equal. Qed. -Theorem Z2R_neq : - forall m n, (m <> n)%Z -> (Z2R m <> Z2R n)%R. -Proof. -intros m n. -repeat rewrite Z2R_IZR. -apply IZR_neq. -Qed. - -Theorem Z2R_abs : - forall z, Z2R (Zabs z) = Rabs (Z2R z). -Proof. -intros. -repeat rewrite Z2R_IZR. -now rewrite Rabs_Zabs. -Qed. - End Z2R. (** Decidable comparison on reals *) @@ -1000,7 +864,6 @@ intros x. unfold Zfloor. rewrite Z2R_minus. simpl. -rewrite Z2R_IZR. apply Rplus_le_reg_r with (1 - x)%R. ring_simplify. exact (proj2 (archimed x)). @@ -1016,7 +879,6 @@ rewrite Z2R_minus. unfold Rminus. rewrite Rplus_assoc. rewrite Rplus_opp_l, Rplus_0_r. -rewrite Z2R_IZR. exact (proj1 (archimed x)). Qed. @@ -1643,7 +1505,7 @@ intros e. unfold bpow. rewrite Zpower_pos_nat. unfold Z2R at 2. -rewrite P2R_INR. +rewrite <- INR_IPR. induction (nat_of_P e). rewrite Rmult_0_l. now rewrite exp_0. -- 2.22.0