From a4a76c253474ac4ce523b70d0150ea5dcf546385 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sun, 5 Mar 2017 20:48:52 +0100 Subject: Make IZR use a compact representation of integers. That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means that, after reduction, real constants no longer exponentially blow up. Note that I was not able to fix the test-suite for the declarative mode, so the missing proof terms have been admitted. --- theories/Reals/ArithProp.v | 4 +-- theories/Reals/RIneq.v | 67 +++++++++++++++++++++++++++------------------ theories/Reals/R_Ifp.v | 4 +-- theories/Reals/Ratan.v | 6 ++-- theories/Reals/Raxioms.v | 22 +++++++++++++-- theories/Reals/Rbasic_fun.v | 9 +++--- theories/Reals/Rlogic.v | 2 +- theories/Reals/Rtrigo1.v | 8 +++--- 8 files changed, 77 insertions(+), 45 deletions(-) (limited to 'theories/Reals') diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 6fca9c8ad..7d9fff276 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -106,7 +106,7 @@ Proof. split. ring. unfold k0; case (Rcase_abs y) as [Hlt|Hge]. - assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl; + assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; change (IZR 1) with 1; unfold Rminus. replace (- ((1 + - IZR (up (x / - y))) * y)) with ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ]. @@ -140,7 +140,7 @@ Proof. rewrite <- Ropp_mult_distr_r_reverse; rewrite (Ropp_inv_permute _ H); elim H0; unfold Rdiv; intros H1 _; exact H1. apply Ropp_neq_0_compat; assumption. - assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl; + assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; change (IZR 1) with 1; cut (0 < y). intro; unfold Rminus; replace (- ((IZR (up (x / y)) + -1) * y)) with ((1 - IZR (up (x / y))) * y); diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 07bcd9836..686077327 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1743,24 +1743,40 @@ Proof. intros z; idtac; apply Z_of_nat_complete; assumption. Qed. +Lemma INR_IPR : forall p, INR (Pos.to_nat p) = IPR p. +Proof. + assert (H: forall p, 2 * INR (Pos.to_nat p) = IPR_2 p). + induction p as [p|p|] ; simpl IPR_2. + rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- IHp. + now rewrite (Rplus_comm (2 * _)). + now rewrite Pos2Nat.inj_xO, mult_INR, <- IHp. + apply Rmult_1_r. + intros [p|p|] ; unfold IPR. + rewrite Pos2Nat.inj_xI, S_INR, mult_INR, <- H. + apply Rplus_comm. + now rewrite Pos2Nat.inj_xO, mult_INR, <- H. + easy. +Qed. + (**********) Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z.of_nat n). Proof. - simple induction n; auto with real. - intros; simpl; rewrite SuccNat2Pos.id_succ; - auto with real. + intros [|n]. + easy. + simpl Z.of_nat. unfold IZR. + now rewrite <- INR_IPR, SuccNat2Pos.id_succ. Qed. Lemma plus_IZR_NEG_POS : forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q). Proof. intros p q; simpl. rewrite Z.pos_sub_spec. - case Pos.compare_spec; intros H; simpl. + case Pos.compare_spec; intros H; unfold IZR. subst. ring. - rewrite Pos2Nat.inj_sub by trivial. + rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial. rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt). ring. - rewrite Pos2Nat.inj_sub by trivial. + rewrite <- 3!INR_IPR, Pos2Nat.inj_sub by trivial. rewrite minus_INR by (now apply lt_le_weak, Pos2Nat.inj_lt). ring. Qed. @@ -1769,26 +1785,18 @@ Qed. Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m. Proof. intro z; destruct z; intro t; destruct t; intros; auto with real. - simpl; intros; rewrite Pos2Nat.inj_add; auto with real. + simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add. apply plus_INR. apply plus_IZR_NEG_POS. rewrite Z.add_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS. - simpl; intros; rewrite Pos2Nat.inj_add; rewrite plus_INR; - auto with real. + simpl. unfold IZR. rewrite <- 3!INR_IPR, Pos2Nat.inj_add, plus_INR. + apply Ropp_plus_distr. Qed. (**********) Lemma mult_IZR : forall n m:Z, IZR (n * m) = IZR n * IZR m. Proof. - intros z t; case z; case t; simpl; auto with real. - intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real. - intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real. - rewrite Rmult_comm. - rewrite Ropp_mult_distr_l_reverse; auto with real. - apply Ropp_eq_compat; rewrite mult_comm; auto with real. - intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real. - rewrite Ropp_mult_distr_l_reverse; auto with real. - intros t1 z1; rewrite Pos2Nat.inj_mul; auto with real. - rewrite Rmult_opp_opp; auto with real. + intros z t; case z; case t; simpl; auto with real; + unfold IZR; intros m n; rewrite <- 3!INR_IPR, Pos2Nat.inj_mul, mult_INR; ring. Qed. Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Z.pow z (Z.of_nat n)). @@ -1810,7 +1818,7 @@ Qed. (**********) Lemma opp_IZR : forall n:Z, IZR (- n) = - IZR n. Proof. - intro z; case z; simpl; auto with real. + intros [|z|z]; unfold IZR; simpl; auto with real. Qed. Definition Ropp_Ropp_IZR := opp_IZR. @@ -1833,10 +1841,12 @@ Qed. Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z. Proof. intro z; case z; simpl; intros. - absurd (0 < 0); auto with real. - unfold Z.lt; simpl; trivial. - case Rlt_not_le with (1 := H). - replace 0 with (-0); auto with real. + elim (Rlt_irrefl _ H). + easy. + elim (Rlt_not_le _ _ H). + unfold IZR. + rewrite <- INR_IPR. + auto with real. Qed. (**********) @@ -1852,9 +1862,12 @@ Qed. Lemma eq_IZR_R0 : forall n:Z, IZR n = 0 -> n = 0%Z. Proof. intro z; destruct z; simpl; intros; auto with zarith. - case (Rlt_not_eq 0 (INR (Pos.to_nat p))); auto with real. - case (Rlt_not_eq (- INR (Pos.to_nat p)) 0); auto with real. - apply Ropp_lt_gt_0_contravar. unfold Rgt; apply pos_INR_nat_of_P. + elim Rgt_not_eq with (2 := H). + unfold IZR. rewrite <- INR_IPR. + apply lt_0_INR, Pos2Nat.is_pos. + elim Rlt_not_eq with (2 := H). + unfold IZR. rewrite <- INR_IPR. + apply Ropp_lt_gt_0_contravar, lt_0_INR, Pos2Nat.is_pos. Qed. (**********) diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index b6d072837..d0f9aea28 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -92,7 +92,7 @@ Proof. auto with zarith real. (*inf a 1*) cut (r - IZR (up r) < 0). - rewrite <- Z_R_minus; simpl; intro; unfold Rminus; + rewrite <- Z_R_minus; change (IZR 1) with 1; intro; unfold Rminus; rewrite Ropp_plus_distr; rewrite <- Rplus_assoc; fold (r - IZR (up r)); rewrite Ropp_involutive; elim (Rplus_ne 1); intros a b; pattern 1 at 2; @@ -376,7 +376,7 @@ Proof. rewrite (Ropp_involutive (IZR 1)); rewrite (Ropp_involutive (IZR (Int_part r2))); rewrite (Ropp_plus_distr (IZR (Int_part r1))); - rewrite (Ropp_involutive (IZR (Int_part r2))); simpl; + rewrite (Ropp_involutive (IZR (Int_part r2))); change (IZR 1) with 1; rewrite <- (Rplus_assoc (r1 + - r2) (- IZR (Int_part r1) + IZR (Int_part r2)) 1) ; rewrite (Rplus_assoc r1 (- r2) (- IZR (Int_part r1) + IZR (Int_part r2))); diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index e13ef1f2c..d9aa6b859 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -322,8 +322,8 @@ apply Rlt_le_trans with (2 := t); clear t. unfold cos_approx; simpl; unfold cos_term. simpl mult; replace ((-1)^ 0) with 1 by ring; replace ((-1)^2) with 1 by ring; replace ((-1)^4) with 1 by ring; replace ((-1)^1) with (-1) by ring; - replace ((-1)^3) with (-1) by ring; replace 3 with (IZR 3) by (simpl; ring); - replace 2 with (IZR 2) by (simpl; ring); simpl Z.of_nat; + replace ((-1)^3) with (-1) by ring; change 3 with (IZR 3); + change 2 with (IZR 2); simpl Z.of_nat; rewrite !INR_IZR_INZ, Ropp_mult_distr_l_reverse, Rmult_1_l. match goal with |- _ < ?a => replace a with ((- IZR 3 ^ 6 * IZR (Z.of_nat (fact 0)) * IZR (Z.of_nat (fact 2)) * @@ -853,6 +853,8 @@ intros x Hx eps Heps. apply Rlt_trans with (2 := H). apply Rinv_0_lt_compat. exact Heps. + unfold N. + rewrite INR_IZR_INZ, positive_nat_Z. exact HN. apply lt_INR. omega. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 9fbda92a2..e9098104c 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -118,14 +118,30 @@ Arguments INR n%nat. (** * Injection from [Z] to [R] *) (**********************************************************) +(* compact representation for 2*p *) +Fixpoint IPR_2 (p:positive) : R := + match p with + | xH => 1 + 1 + | xO p => (1 + 1) * IPR_2 p + | xI p => (1 + 1) * (1 + IPR_2 p) + end. + +Definition IPR (p:positive) : R := + match p with + | xH => 1 + | xO p => IPR_2 p + | xI p => 1 + IPR_2 p + end. +Arguments IPR p%positive : simpl never. + (**********) Definition IZR (z:Z) : R := match z with | Z0 => 0 - | Zpos n => INR (Pos.to_nat n) - | Zneg n => - INR (Pos.to_nat n) + | Zpos n => IPR n + | Zneg n => - IPR n end. -Arguments IZR z%Z. +Arguments IZR z%Z : simpl never. (**********************************************************) (** * [R] Archimedean *) diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index c889d7347..fe5402e6e 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -613,11 +613,12 @@ Qed. Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z). Proof. - intros z; case z; simpl; auto with real. - apply Rabs_right; auto with real. - intros p0; apply Rabs_right; auto with real zarith. + intros z; case z; unfold Zabs. + apply Rabs_R0. + now intros p0; apply Rabs_pos_eq, (IZR_le 0). + unfold IZR at 1. intros p0; rewrite Rabs_Ropp. - apply Rabs_right; auto with real zarith. + now apply Rabs_pos_eq, (IZR_le 0). Qed. Lemma abs_IZR : forall z, IZR (Z.abs z) = Rabs (IZR z). diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index b9a9458c8..7bd6c916d 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -82,7 +82,7 @@ assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R). apply Rle_lt_trans with (1 := H1l). apply archimed. rewrite minus_IZR. - simpl. + change (IZR 2) with 2%R. ring. assert (Hl': (/ (INR (S N) + 1) < l)%R). rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 5f2e0d5b5..6b1754021 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -182,8 +182,8 @@ destruct (pre_cos_bound _ 0 lo up) as [_ upper]. apply Rle_lt_trans with (1 := upper). apply Rlt_le_trans with (2 := lower). unfold cos_approx, sin_approx. -simpl sum_f_R0; replace 7 with (IZR 7) by (simpl; field). -replace 8 with (IZR 8) by (simpl; field). +simpl sum_f_R0; change 7 with (IZR 7). +change 8 with (IZR 8). unfold cos_term, sin_term; simpl fact; rewrite !INR_IZR_INZ. simpl plus; simpl mult. field_simplify; @@ -1798,7 +1798,7 @@ Lemma cos_eq_0_0 (x:R) : Proof. rewrite cos_sin. intros Hx. destruct (sin_eq_0_0 (PI/2 + x) Hx) as (k,Hk). clear Hx. - exists (k-1)%Z. rewrite <- Z_R_minus; simpl. + exists (k-1)%Z. rewrite <- Z_R_minus; change (IZR 1) with 1. symmetry in Hk. field_simplify [Hk]. field. Qed. @@ -1836,7 +1836,7 @@ Proof. - right; left; auto. - left. clear Hi. subst. - replace 0 with (IZR 0 * PI) by (simpl; ring). f_equal. f_equal. + replace 0 with (IZR 0 * PI) by apply Rmult_0_l. f_equal. f_equal. apply one_IZR_lt1. split. + apply Rlt_le_trans with 0; -- cgit v1.2.3