aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-03-05 20:48:52 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-03-22 17:19:51 +0100
commita4a76c253474ac4ce523b70d0150ea5dcf546385 (patch)
treeebde19ff337a88fd8029ac5dc9eca03df1202367 /theories
parentddbc3839923731686a89a401d0f9dd44f3ad339b (diff)
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.
Diffstat (limited to 'theories')
-rw-r--r--theories/Reals/ArithProp.v4
-rw-r--r--theories/Reals/RIneq.v67
-rw-r--r--theories/Reals/R_Ifp.v4
-rw-r--r--theories/Reals/Ratan.v6
-rw-r--r--theories/Reals/Raxioms.v22
-rw-r--r--theories/Reals/Rbasic_fun.v9
-rw-r--r--theories/Reals/Rlogic.v2
-rw-r--r--theories/Reals/Rtrigo1.v8
8 files changed, 77 insertions, 45 deletions
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;