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.

1 files changed, 19 insertions, 3 deletions

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                                  *)