Merge PR#415: Use a compact representation for real literals

6 files changed, 139 insertions, 382 deletions

diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index 1d7ee93ea3..a962547131 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -13,6 +13,6 @@ Require Export DiscrR.
 Require Export Fourier_util.
 Declare ML Module "fourier_plugin".
 
-Ltac fourier := abstract (fourierz; field; discrR).
+Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR).
 
 Ltac fourier_eq := apply Rge_antisym; fourier.
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 2352d78d63..30e475b710 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -18,7 +18,7 @@ Require Import Refl.
 Require Import Raxioms RIneq Rpow_def DiscrR.
 Require Import QArith.
 Require Import Qfield.
-
+Require Import Qreals.
 
 Require Setoid.
 (*Declare ML Module "micromega_plugin".*)
@@ -38,15 +38,8 @@ Proof.
   exact Rplus_opp_r.
 Qed.
 
-Add Ring Rring : Rsrt.
 Open Scope R_scope.
 
-Lemma Rmult_neutral : forall x:R , 0 * x = 0.
-Proof.
-  intro ; ring.
-Qed.
-
-
 Lemma Rsor : SOR R0 R1 Rplus Rmult Rminus Ropp (@eq R)  Rle Rlt.
 Proof.
   constructor; intros ; subst ; try (intuition (subst; try ring ; auto with real)).
@@ -59,142 +52,41 @@ Proof.
   apply (Rlt_irrefl m) ; auto.
   apply Rnot_le_lt. auto with real.
   destruct (total_order_T n m) as [ [H1 | H1] | H1] ; auto.
-  intros.
-  rewrite <- (Rmult_neutral m).
-  apply (Rmult_lt_compat_r) ; auto.
-Qed.
-
-Definition IQR := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R.
-
-
-Lemma Rinv_elim : forall x y z, 
-  y <> 0 -> (z * y = x <->   x * / y = z).
-Proof.
-  intros.
-  split ; intros.
-  subst.
-  rewrite Rmult_assoc.
-  rewrite Rinv_r; auto.
-  ring.
-  subst.
-  rewrite Rmult_assoc.
-  rewrite (Rmult_comm (/ y)).
-  rewrite Rinv_r ; auto.
-  ring.
-Qed.  
-
-Ltac INR_nat_of_P :=
-  match goal with
-    | H : context[INR (Pos.to_nat ?X)] |- _ =>
-      revert H ; 
-      let HH := fresh in
-        assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X))
-    | |- context[INR (Pos.to_nat ?X)] =>
-      let HH := fresh in
-        assert (HH := pos_INR_nat_of_P X) ; revert HH ; generalize (INR (Pos.to_nat X))
-  end.
-
-Ltac add_eq expr val := set (temp := expr) ; 
-  generalize (eq_refl temp) ;
-    unfold temp at 1 ; generalize temp ; intro val ; clear temp.
-
-Ltac Rinv_elim :=
-  match goal with
-    | |- context[?x * / ?y] => 
-      let z := fresh "v" in 
-      add_eq (x * / y) z  ;
-      let H := fresh in intro H ; rewrite <- Rinv_elim in H
-  end.
-
-Lemma Rlt_neq : forall r , 0 < r -> r <> 0.
-Proof.
-  red. intros.
-  subst.
-  apply (Rlt_irrefl 0 H).  
+  now apply Rmult_lt_0_compat.
 Qed.
 
+Notation IQR := Q2R (only parsing).
 
 Lemma Rinv_1 : forall x, x * / 1 = x.
 Proof.
   intro.
-  Rinv_elim.
-  subst ; ring.
-  apply R1_neq_R0.
+  rewrite Rinv_1.
+  apply Rmult_1_r.
 Qed.
 
-Lemma Qeq_true : forall x y,  
-  Qeq_bool x y = true -> 
-   IQR x = IQR y.
+Lemma Qeq_true : forall x y, Qeq_bool x y = true -> IQR x = IQR y.
 Proof.
-  unfold IQR.
-  simpl.
-  intros.
-  apply Qeq_bool_eq in H.
-  unfold Qeq in H.
-  assert (IZR (Qnum x * ' Qden y) = IZR (Qnum y * ' Qden x))%Z.
-     rewrite H. reflexivity.
-  repeat rewrite mult_IZR in H0.
-  simpl in H0.
-  revert H0.
-  repeat INR_nat_of_P.
   intros.
-  apply Rinv_elim in H2 ; [| apply Rlt_neq ; auto].
-  rewrite <- H2.
-  field.
-  split ; apply Rlt_neq ; auto.
+  now apply Qeq_eqR, Qeq_bool_eq.
 Qed.
 
 Lemma Qeq_false : forall x y, Qeq_bool x y = false -> IQR x <> IQR y.
 Proof.
   intros.
-  apply Qeq_bool_neq  in H.
-  intro. apply H.   clear H.
-  unfold Qeq,IQR in *.
-  simpl in *.
-  revert H0.
-  repeat Rinv_elim.
-  intros.
-  subst.
-  assert (IZR (Qnum x * ' Qden y)%Z = IZR (Qnum y * ' Qden x)%Z).
-  repeat rewrite mult_IZR.  
-  simpl.
-  rewrite <- H0. rewrite <- H.
-  ring.
-  apply eq_IZR ; auto.
-  INR_nat_of_P; intros; apply Rlt_neq ; auto. 
-  INR_nat_of_P; intros ; apply Rlt_neq ; auto. 
+  apply Qeq_bool_neq in H.
+  contradict H.
+  now apply eqR_Qeq.
 Qed.
 
-  
-
 Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> IQR x <= IQR y.
 Proof.
   intros.
-  apply Qle_bool_imp_le in H.
-  unfold Qle in H.
-  unfold IQR.
-  simpl in *.
-  apply IZR_le in H.
-  repeat rewrite mult_IZR in H.
-  simpl in H.
-  repeat INR_nat_of_P; intros.
-  assert (Hr := Rlt_neq r H).
-  assert (Hr0 := Rlt_neq r0 H0).
-  replace (IZR (Qnum x) * / r) with ((IZR (Qnum x) * r0) * (/r * /r0)).
-  replace (IZR (Qnum y) * / r0) with ((IZR (Qnum y) * r) * (/r * /r0)).
-  apply Rmult_le_compat_r ; auto.
-  apply Rmult_le_pos.
-  unfold Rle. left. apply Rinv_0_lt_compat ; auto.
-  unfold Rle. left. apply Rinv_0_lt_compat ; auto.
-  field ; intuition.
-  field ; intuition.
+  now apply Qle_Rle, Qle_bool_imp_le.
 Qed.
 
-
-
 Lemma IQR_0 : IQR 0 = 0.
 Proof.
-  compute. apply Rinv_1.
+  apply Rmult_0_l.
 Qed.
 
 Lemma IQR_1 : IQR 1 = 1.
@@ -202,160 +94,6 @@ Proof.
   compute. apply Rinv_1.
 Qed.
 
-Lemma IQR_plus : forall x y, IQR (x + y) = IQR x + IQR y.
-Proof.
-  intros.
-  unfold IQR.
-  simpl in *.
-  rewrite plus_IZR in *.
-  rewrite mult_IZR in *.
-  simpl.  
-  rewrite Pos2Nat.inj_mul.
-  rewrite mult_INR.
-  rewrite mult_IZR.
-  simpl.
-  repeat INR_nat_of_P.
-  intros. field. 
-  split ; apply Rlt_neq ; auto.
-Qed.
-
-Lemma IQR_opp : forall x, IQR (- x) = - IQR x.
-Proof.
-  intros.
-  unfold IQR.
-  simpl.
-  rewrite opp_IZR.
-  ring.  
-Qed.
-
-Lemma IQR_minus : forall x y, IQR (x - y) = IQR x - IQR y.
-Proof.
-  intros.
-  unfold Qminus.
-  rewrite IQR_plus.
-  rewrite IQR_opp.
-  ring.
-Qed.
-
-
-Lemma IQR_mult : forall x y, IQR (x * y) = IQR x * IQR y.
-Proof.
-  unfold IQR ; intros.
-  simpl.
-  repeat rewrite mult_IZR.
-  rewrite Pos2Nat.inj_mul.
-  rewrite mult_INR.
-  repeat INR_nat_of_P.
-  intros. field ; split ; apply Rlt_neq ; auto.
-Qed.
-
-Lemma IQR_inv_lt : forall x, (0 < x)%Q -> 
-  IQR (/ x) =  / IQR x.
-Proof.
-  unfold IQR ; simpl.
-  intros.
-  unfold Qlt in H.
-  revert H.
-  simpl.
-  intros.
-  unfold Qinv.
-  destruct x.
-  destruct Qnum ; simpl in *.
-  exfalso. auto with zarith.
-  clear H.
-  repeat INR_nat_of_P.
-  intros.
-  assert (HH := Rlt_neq _ H).
-  assert (HH0 := Rlt_neq _ H0).
-  rewrite Rinv_mult_distr ; auto.
-  rewrite Rinv_involutive ; auto.
-  ring.
-  apply Rinv_0_lt_compat in H0.
-  apply Rlt_neq ; auto.
-  simpl in H.
-  exfalso.
-  rewrite Pos.mul_comm  in H.
-  compute in H.
-  discriminate.
-Qed.
-
-Lemma Qinv_opp : forall x, (- (/ x) = / ( -x))%Q.
-Proof.
-  destruct x ; destruct Qnum ; reflexivity.
-Qed.
-
-Lemma Qopp_involutive_strong : forall x, (- - x = x)%Q.
-Proof.
-  intros.
-  destruct x.
-  unfold Qopp.
-  simpl.
-  rewrite Z.opp_involutive.
-  reflexivity.
-Qed.
-
-Lemma Ropp_0 : forall r , - r = 0 -> r = 0.
-Proof.
-  intros.
-  rewrite <- (Ropp_involutive r).
-  apply Ropp_eq_0_compat ; auto.
-Qed.
-
-Lemma IQR_x_0 : forall x, IQR x = 0 -> x == 0%Q.
-Proof.
-  destruct x ; simpl.
-  unfold IQR.
-  simpl.
-  INR_nat_of_P.
-  intros.
-  apply Rmult_integral in H0.  
-  destruct H0.
-  apply eq_IZR_R0 in H0.
-  subst.
-  reflexivity.
-  exfalso.
-  apply Rinv_0_lt_compat in H.
-  rewrite <- H0 in H.
-  apply Rlt_irrefl in H. auto.
-Qed.
-  
-
-Lemma IQR_inv_gt : forall x, (0 > x)%Q -> 
-  IQR (/ x) =  / IQR x.
-Proof.
-  intros.
-  rewrite <- (Qopp_involutive_strong x).
-  rewrite <- Qinv_opp.
-  rewrite IQR_opp.
-  rewrite IQR_inv_lt.
-  repeat rewrite IQR_opp.
-  rewrite Ropp_inv_permute.
-  auto.
-  intro.
-  apply Ropp_0 in H0.
-  apply IQR_x_0 in H0.
-  rewrite H0 in H.
-  compute in H. discriminate.
-  unfold Qlt in *.
-  destruct x ; simpl in *.
-  auto with zarith.
-Qed.
-
-Lemma IQR_inv : forall x, ~ x ==  0 -> 
-  IQR (/ x) =  / IQR x.
-Proof.
-  intros.
-  assert ( 0 > x \/ 0 < x)%Q.
-   destruct x ; unfold Qlt, Qeq in * ; simpl in *.
-   rewrite Z.mul_1_r in *.
-   destruct Qnum ; simpl in * ; intuition auto.
-   right. reflexivity.
-   left ; reflexivity.
-  destruct H0.
-  apply IQR_inv_gt ; auto.
-  apply IQR_inv_lt ; auto.
-Qed.
-
 Lemma IQR_inv_ext : forall x, 
   IQR (/ x) = (if Qeq_bool x 0 then 0 else / IQR x).
 Proof.
@@ -366,18 +104,13 @@ Proof.
   destruct x ; simpl.
   unfold Qeq in H.
   simpl in H.
-  replace Qnum with 0%Z.
-  compute. rewrite Rinv_1.
-  reflexivity.
-  rewrite <- H. ring.
+  rewrite Zmult_1_r in H.
+  rewrite H.
+  apply Rmult_0_l.
   intros.
-  apply IQR_inv.
-  intro.
-  rewrite <- Qeq_bool_iff in H0.
-  congruence.
+  now apply Q2R_inv, Qeq_bool_neq.
 Qed.
 
-
 Notation to_nat := N.to_nat.
 
 Lemma QSORaddon :
@@ -391,10 +124,10 @@ Proof.
   constructor ; intros ; try reflexivity.
   apply IQR_0.
   apply IQR_1.
-  apply IQR_plus.
-  apply IQR_minus.
-  apply IQR_mult.
-  apply IQR_opp.
+  apply Q2R_plus.
+  apply Q2R_minus.
+  apply Q2R_mult.
+  apply Q2R_opp.
   apply Qeq_true ; auto.
   apply R_power_theory.
   apply Qeq_false.
@@ -453,13 +186,13 @@ Proof.
     apply IQR_1. 
     reflexivity.
     unfold IQR. simpl. rewrite Rinv_1. reflexivity.
-    apply IQR_plus.
-    apply IQR_minus.
-    apply IQR_mult.
+    apply Q2R_plus.
+    apply Q2R_minus.
+    apply Q2R_mult.
     rewrite <- IHc.
     apply IQR_inv_ext.
     rewrite <- IHc.
-    apply IQR_opp.
+    apply Q2R_opp.
   Qed.
 
 Require Import EnvRing.
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 97f29df823..6051cb3d3c 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -364,6 +364,7 @@ struct
     [["Coq";"Reals" ; "Rdefinitions"];
      ["Coq";"Reals" ; "Rpow_def"] ;
      ["Coq";"Reals" ; "Raxioms"] ;
+     ["Coq";"QArith"; "Qreals"] ;
     ]
 
   let z_modules = [["Coq";"ZArith";"BinInt"]]
@@ -479,7 +480,7 @@ struct
   let coq_Rinv = lazy (r_constant "Rinv")
   let coq_Rpower = lazy (r_constant "pow")
   let coq_IZR    = lazy (r_constant "IZR")
-  let coq_IQR    = lazy (constant "IQR")
+  let coq_IQR    = lazy (r_constant "Q2R")
 
 
   let coq_PEX = lazy (constant "PEX" )
diff --git a/plugins/setoid_ring/RealField.v b/plugins/setoid_ring/RealField.v
index 293722125b..facd2e0625 100644
--- a/plugins/setoid_ring/RealField.v
+++ b/plugins/setoid_ring/RealField.v
@@ -59,11 +59,12 @@ Notation Rset := (Eqsth R).
 Notation Rext := (Eq_ext Rplus Rmult Ropp).
 
 Lemma Rlt_0_2 : 0 < 2.
+Proof.
 apply Rlt_trans with (0 + 1).
  apply Rlt_n_Sn.
  rewrite Rplus_comm.
    apply Rplus_lt_compat_l.
-    replace 1 with (0 + 1).
+    replace R1 with (0 + 1).
   apply Rlt_n_Sn.
   apply Rplus_0_l.
 Qed.
@@ -126,9 +127,17 @@ Ltac Rpow_tac t :=
   | _ => constr:(N.of_nat t)
   end.
 
-Add Field RField : Rfield
-   (completeness Zeq_bool_complete, power_tac R_power_theory [Rpow_tac]).
-
-
-
+Ltac IZR_tac t :=
+  match t with
+  | R0 => constr:(0%Z)
+  | R1 => constr:(1%Z)
+  | IZR ?u =>
+    match isZcst u with
+    | true => u
+    | _ => constr:(InitialRing.NotConstant)
+    end
+  | _ => constr:(InitialRing.NotConstant)
+  end.
 
+Add Field RField : Rfield
+   (completeness Zeq_bool_complete, constants [IZR_tac], power_tac R_power_theory [Rpow_tac]).
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index eb35d3f806..87ee666605 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -323,14 +323,16 @@ let _ = add_map "ring"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
     coq_nil, (function -1->Eval|_ -> Prot);
+    my_reference "IDphi", (function _->Eval);
+    my_reference "gen_phiZ", (function _->Eval);
     (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
     pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
     pol_cst "Pphi_pow",
-          (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
+          (function -1|8|9|10|13|15|17->Eval|11|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)])
+    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot)])
 
 (****************************************************************************)
 (* Ring database *)
@@ -756,12 +758,14 @@ let _ = add_map "field"
   (map_with_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
     coq_nil, (function -1->Eval|_ -> Prot);
+    my_reference "IDphi", (function _->Eval);
+    my_reference "gen_phiZ", (function _->Eval);
     (* display_linear: evaluate polynomials and coef operations, protect
        field operations and make recursive call on the var map *)
     my_reference "display_linear",
       (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot);
     my_reference "display_pow_linear",
-     (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot);
+     (function -1|9|10|11|14|16|18|19->Eval|12|17->Rec|_->Prot);
    (* Pphi_dev: evaluate polynomial and coef operations, protect
        ring operations and make recursive call on the var map *)
     pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot);
@@ -769,19 +773,20 @@ let _ = add_map "field"
           (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot);
     (* PEeval: evaluate morphism and polynomial, protect ring
        operations and make recursive call on the var map *)
-    pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot);
+    pol_cst "PEeval", (function -1|8|10|13->Eval|12->Rec|_->Prot);
     (* FEeval: evaluate morphism, protect field
        operations and make recursive call on the var map *)
-    my_reference "FEeval", (function -1|8|9|10|11|14->Eval|13->Rec|_->Prot)]);;
+    my_reference "FEeval", (function -1|10|12|15->Eval|14->Rec|_->Prot)]);;
 
 let _ = add_map "field_cond"
   (map_without_eq
     [coq_cons,(function -1->Eval|2->Rec|_->Prot);
      coq_nil, (function -1->Eval|_ -> Prot);
-    (* PCond: evaluate morphism and denum list, protect ring
+     my_reference "IDphi", (function _->Eval);
+     my_reference "gen_phiZ", (function _->Eval);
+    (* PCond: evaluate denum list, protect ring
        operations and make recursive call on the var map *)
-     my_reference "PCond", (function -1|9|11|14->Eval|13->Rec|_->Prot)]);;
-(*                       (function -1|9|11->Eval|10->Rec|_->Prot)]);;*)
+     my_reference "PCond", (function -1|11|14->Eval|9|13->Rec|_->Prot)]);;
 
 
 let _ = Redexpr.declare_reduction "simpl_field_expr"
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 3ae2d45f32..8f065f5282 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -9,6 +9,8 @@
 open Util
 open Names
 open Globnames
+open Glob_term
+open Bigint
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "r_syntax_plugin"
@@ -17,95 +19,105 @@ let () = Mltop.add_known_module __coq_plugin_name
 exception Non_closed_number
 
 (**********************************************************************)
-(* Parsing R via scopes                                               *)
+(* Parsing positive via scopes                                        *)
 (**********************************************************************)
 
-open Glob_term
-open Bigint
+let binnums = ["Coq";"Numbers";"BinNums"]
 
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
-let make_path dir id = Libnames.make_path dir (Id.of_string id)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
+
+let positive_path = make_path binnums "positive"
+
+(* TODO: temporary hack *)
+let make_kn dir id = Globnames.encode_mind dir id
+
+let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
+let glob_positive = IndRef (positive_kn,0)
+let path_of_xI = ((positive_kn,0),1)
+let path_of_xO = ((positive_kn,0),2)
+let path_of_xH = ((positive_kn,0),3)
+let glob_xI = ConstructRef path_of_xI
+let glob_xO = ConstructRef path_of_xO
+let glob_xH = ConstructRef path_of_xH
+
+let pos_of_bignat dloc x =
+  let ref_xI = GRef (dloc, glob_xI, None) in
+  let ref_xH = GRef (dloc, glob_xH, None) in
+  let ref_xO = GRef (dloc, glob_xO, None) in
+  let rec pos_of x =
+    match div2_with_rest x with
+      | (q,false) -> GApp (dloc, ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q])
+      | (q,true) -> ref_xH
+  in
+  pos_of x
+
+(**********************************************************************)
+(* Printing positive via scopes                                       *)
+(**********************************************************************)
+
+let rec bignat_of_pos = function
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | GRef (_, a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
+  | _ -> raise Non_closed_number
+
+(**********************************************************************)
+(* Parsing Z via scopes                                               *)
+(**********************************************************************)
 
+let z_path = make_path binnums "Z"
+let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
+let glob_z = IndRef (z_kn,0)
+let path_of_ZERO = ((z_kn,0),1)
+let path_of_POS = ((z_kn,0),2)
+let path_of_NEG = ((z_kn,0),3)
+let glob_ZERO = ConstructRef path_of_ZERO
+let glob_POS = ConstructRef path_of_POS
+let glob_NEG = ConstructRef path_of_NEG
+
+let z_of_int dloc n =
+  if not (Bigint.equal n zero) then
+    let sgn, n =
+      if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
+    GApp(dloc, GRef (dloc,sgn,None), [pos_of_bignat dloc n])
+  else
+    GRef (dloc, glob_ZERO, None)
+
+(**********************************************************************)
+(* Printing Z via scopes                                              *)
+(**********************************************************************)
+
+let bigint_of_z = function
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | GApp (_, GRef (_,b,_),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (_, a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+  | _ -> raise Non_closed_number
+
+(**********************************************************************)
+(* Parsing R via scopes                                               *)
+(**********************************************************************)
+
+let rdefinitions = ["Coq";"Reals";"Rdefinitions"]
 let r_path = make_path rdefinitions "R"
 
 (* TODO: temporary hack *)
 let make_path dir id = Globnames.encode_con dir (Id.of_string id)
 
-let r_kn = make_path rdefinitions "R"
-let glob_R = ConstRef r_kn
-let glob_R1 = ConstRef (make_path rdefinitions "R1")
-let glob_R0 = ConstRef (make_path rdefinitions "R0")
-let glob_Ropp = ConstRef (make_path rdefinitions "Ropp")
-let glob_Rplus = ConstRef (make_path rdefinitions "Rplus")
-let glob_Rmult = ConstRef (make_path rdefinitions "Rmult")
-
-let two = mult_2 one
-let three = add_1 two
-let four = mult_2 two
-
-(* Unary representation of strictly positive numbers *)
-let rec small_r dloc n =
-  if equal one n then GRef (dloc, glob_R1, None)
-  else GApp(dloc,GRef (dloc,glob_Rplus, None),
-            [GRef (dloc, glob_R1, None);small_r dloc (sub_1 n)])
-
-let r_of_posint dloc n =
-  let r1 = GRef (dloc, glob_R1, None) in
-  let r2 = small_r dloc two in
-  let rec r_of_pos n =
-    if less_than n four then small_r dloc n
-    else
-      let (q,r) = div2_with_rest n in
-      let b = GApp(dloc,GRef(dloc,glob_Rmult,None),[r2;r_of_pos q]) in
-      if r then GApp(dloc,GRef(dloc,glob_Rplus,None),[r1;b]) else b in
-  if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0,None)
+let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR")
 
 let r_of_int dloc z =
-  if is_strictly_neg z then
-    GApp (dloc, GRef(dloc,glob_Ropp,None), [r_of_posint dloc (neg z)])
-  else
-    r_of_posint dloc z
+  GApp (dloc, GRef(dloc,glob_IZR,None), [z_of_int dloc z])
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
-let bignat_of_r =
-(* for numbers > 1 *)
-let rec bignat_of_pos = function
-  (* 1+1 *)
-  | GApp (_,GRef (_,p,_), [GRef (_,o1,_); GRef (_,o2,_)])
-      when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two
-  (* 1+(1+1) *)
-  | GApp (_,GRef (_,p1,_), [GRef (_,o1,_);
-      GApp(_,GRef (_,p2,_),[GRef(_,o2,_);GRef(_,o3,_)])])
-      when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus &&
-           Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three
-  (* (1+1)*b *)
-  | GApp (_,GRef (_,p,_), [a; b]) when Globnames.eq_gr p glob_Rmult ->
-      if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
-      mult_2 (bignat_of_pos b)
-  (* 1+(1+1)*b *)
-  | GApp (_,GRef (_,p1,_), [GRef (_,o,_); GApp (_,GRef (_,p2,_),[a;b])])
-      when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1  ->
-      if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
-        add_1 (mult_2 (bignat_of_pos b))
-  | _ -> raise Non_closed_number
-in
-let bignat_of_r = function
-  | GRef (_,a,_) when Globnames.eq_gr a glob_R0 -> zero
-  | GRef (_,a,_) when Globnames.eq_gr a glob_R1 -> one
-  | r -> bignat_of_pos r
-in
-bignat_of_r
-
 let bigint_of_r = function
-  | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_Ropp ->
-      let n = bignat_of_r a in
-      if Bigint.equal n zero then raise Non_closed_number;
-      neg n
-  | a -> bignat_of_r a
+  | GApp (_,GRef (_,o,_), [a]) when Globnames.eq_gr o glob_IZR ->
+      bigint_of_z a
+  | _ -> raise Non_closed_number
 
 let uninterp_r p =
   try
@@ -113,12 +125,9 @@ let uninterp_r p =
   with Non_closed_number ->
     None
 
-let mkGRef gr = GRef (Loc.ghost,gr,None)
-
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  (List.map mkGRef 
-    [glob_Ropp;glob_R0;glob_Rplus;glob_Rmult;glob_R1],
+  ([GRef (Loc.ghost,glob_IZR,None)],
     uninterp_r,
     false)