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.

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;