Q2R -> IQR

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14155 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 66 insertions, 270 deletions

diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index eb4847486..2be99da1e 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -19,6 +19,7 @@ Require Import Raxioms RIneq Rpow_def DiscrR.
 Require Import QArith.
 Require Import Qfield.
 
+
 Require Setoid.
 (*Declare ML Module "micromega_plugin".*)
 
@@ -63,7 +64,7 @@ Proof.
   apply (Rmult_lt_compat_r) ; auto.
 Qed.
 
-Definition Q2R := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R.
+Definition IQR := fun x : Q => (IZR (Qnum x) * / IZR (' Qden x))%R.
 
 
 Lemma Rinv_elim : forall x y z, 
@@ -123,9 +124,9 @@ Qed.
 
 Lemma Qeq_true : forall x y,  
   Qeq_bool x y = true -> 
-   Q2R x = Q2R y.
+   IQR x = IQR y.
 Proof.
-  unfold Q2R.
+  unfold IQR.
   simpl.
   intros.
   apply Qeq_bool_eq in H.
@@ -143,12 +144,12 @@ Proof.
   split ; apply Rlt_neq ; auto.
 Qed.
 
-Lemma Qeq_false : forall x y, Qeq_bool x y = false -> Q2R x <> Q2R y.
+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,Q2R in *.
+  unfold Qeq,IQR in *.
   simpl in *.
   revert H0.
   repeat Rinv_elim.
@@ -166,12 +167,12 @@ Qed.
 
   
 
-Lemma Qle_true : forall x y : Q, Qle_bool x y = true -> Q2R x <= Q2R y.
+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 Q2R.
+  unfold IQR.
   simpl in *.
   apply IZR_le in H.
   repeat rewrite mult_IZR in H.
@@ -191,20 +192,20 @@ Qed.
 
 
 
-Lemma Q2R_0 : Q2R 0 = 0.
+Lemma IQR_0 : IQR 0 = 0.
 Proof.
   compute. apply Rinv_1.
 Qed.
 
-Lemma Q2R_1 : Q2R 1 = 1.
+Lemma IQR_1 : IQR 1 = 1.
 Proof.
   compute. apply Rinv_1.
 Qed.
 
-Lemma Q2R_plus : forall x y, Q2R (x + y) = Q2R x + Q2R y.
+Lemma IQR_plus : forall x y, IQR (x + y) = IQR x + IQR y.
 Proof.
   intros.
-  unfold Q2R.
+  unfold IQR.
   simpl in *.
   rewrite plus_IZR in *.
   rewrite mult_IZR in *.
@@ -218,28 +219,28 @@ Proof.
   split ; apply Rlt_neq ; auto.
 Qed.
 
-Lemma Q2R_opp : forall x, Q2R (- x) = - Q2R x.
+Lemma IQR_opp : forall x, IQR (- x) = - IQR x.
 Proof.
   intros.
-  unfold Q2R.
+  unfold IQR.
   simpl.
   rewrite opp_IZR.
   ring.  
 Qed.
 
-Lemma Q2R_minus : forall x y, Q2R (x - y) = Q2R x - Q2R y.
+Lemma IQR_minus : forall x y, IQR (x - y) = IQR x - IQR y.
 Proof.
   intros.
   unfold Qminus.
-  rewrite Q2R_plus.
-  rewrite Q2R_opp.
+  rewrite IQR_plus.
+  rewrite IQR_opp.
   ring.
 Qed.
 
 
-Lemma Q2R_mult : forall x y, Q2R (x * y) = Q2R x * Q2R y.
+Lemma IQR_mult : forall x y, IQR (x * y) = IQR x * IQR y.
 Proof.
-  unfold Q2R ; intros.
+  unfold IQR ; intros.
   simpl.
   repeat rewrite mult_IZR.
   simpl.  
@@ -249,10 +250,10 @@ Proof.
   intros. field ; split ; apply Rlt_neq ; auto.
 Qed.
 
-Lemma Q2R_inv_lt : forall x, (0 < x)%Q -> 
-  Q2R (/ x) =  / Q2R x.
+Lemma IQR_inv_lt : forall x, (0 < x)%Q -> 
+  IQR (/ x) =  / IQR x.
 Proof.
-  unfold Q2R ; simpl.
+  unfold IQR ; simpl.
   intros.
   unfold Qlt in H.
   revert H.
@@ -301,10 +302,10 @@ Proof.
   apply Ropp_eq_0_compat ; auto.
 Qed.
 
-Lemma Q2R_x_0 : forall x, Q2R x = 0 -> x == 0%Q.
+Lemma IQR_x_0 : forall x, IQR x = 0 -> x == 0%Q.
 Proof.
   destruct x ; simpl.
-  unfold Q2R.
+  unfold IQR.
   simpl.
   INR_nat_of_P.
   intros.
@@ -320,20 +321,20 @@ Proof.
 Qed.
   
 
-Lemma Q2R_inv_gt : forall x, (0 > x)%Q -> 
-  Q2R (/ x) =  / Q2R x.
+Lemma IQR_inv_gt : forall x, (0 > x)%Q -> 
+  IQR (/ x) =  / IQR x.
 Proof.
   intros.
   rewrite <- (Qopp_involutive_strong x).
   rewrite <- Qinv_opp.
-  rewrite Q2R_opp.
-  rewrite Q2R_inv_lt.
-  repeat rewrite Q2R_opp.
+  rewrite IQR_opp.
+  rewrite IQR_inv_lt.
+  repeat rewrite IQR_opp.
   rewrite Ropp_inv_permute.
   auto.
   intro.
   apply Ropp_0 in H0.
-  apply Q2R_x_0 in H0.
+  apply IQR_x_0 in H0.
   rewrite H0 in H.
   compute in H. discriminate.
   unfold Qlt in *.
@@ -341,8 +342,8 @@ Proof.
   auto with zarith.
 Qed.
 
-Lemma Q2R_inv : forall x, ~ x ==  0 -> 
-  Q2R (/ x) =  / Q2R x.
+Lemma IQR_inv : forall x, ~ x ==  0 -> 
+  IQR (/ x) =  / IQR x.
 Proof.
   intros.
   assert ( 0 > x \/ 0 < x)%Q.
@@ -352,12 +353,12 @@ Proof.
    right. reflexivity.
    left ; reflexivity.
   destruct H0.
-  apply Q2R_inv_gt ; auto.
-  apply Q2R_inv_lt ; auto.
+  apply IQR_inv_gt ; auto.
+  apply IQR_inv_lt ; auto.
 Qed.
 
-Lemma Q2R_inv_ext : forall x, 
-  Q2R (/ x) = (if Qeq_bool x 0 then 0 else / Q2R x).
+Lemma IQR_inv_ext : forall x, 
+  IQR (/ x) = (if Qeq_bool x 0 then 0 else / IQR x).
 Proof.
   intros.
   case_eq (Qeq_bool x 0).
@@ -371,7 +372,7 @@ Proof.
   reflexivity.
   rewrite <- H. ring.
   intros.
-  apply Q2R_inv.
+  apply IQR_inv.
   intro.
   rewrite <- Qeq_bool_iff in H0.
   congruence.
@@ -385,16 +386,16 @@ Lemma QSORaddon :
   R0 R1 Rplus Rmult Rminus Ropp  (@eq R)  Rle (* ring elements *)
   Q 0%Q 1%Q Qplus Qmult Qminus Qopp (* coefficients *)
   Qeq_bool Qle_bool
-  Q2R nat to_nat pow.
+  IQR nat to_nat pow.
 Proof.
   constructor.
   constructor ; intros ; try reflexivity.
-  apply Q2R_0.
-  apply Q2R_1.
-  apply Q2R_plus.
-  apply Q2R_minus.
-  apply Q2R_mult.
-  apply Q2R_opp.
+  apply IQR_0.
+  apply IQR_1.
+  apply IQR_plus.
+  apply IQR_minus.
+  apply IQR_mult.
+  apply IQR_opp.
   apply Qeq_true ; auto.
   apply R_power_theory.
   apply Qeq_false.
@@ -435,7 +436,7 @@ Fixpoint R_of_Rcst (r : Rcst) : R :=
     | C0 => R0
     | C1 => R1
     | CZ z => IZR z
-    | CQ q => Q2R q
+    | CQ q => IQR q
     | CPlus r1 r2  => (R_of_Rcst r1) + (R_of_Rcst r2)
     | CMinus r1 r2 => (R_of_Rcst r1) - (R_of_Rcst r2)
     | CMult r1 r2  => (R_of_Rcst r1) * (R_of_Rcst r2)
@@ -446,20 +447,20 @@ Fixpoint R_of_Rcst (r : Rcst) : R :=
       | COpp r       => - (R_of_Rcst r)
   end.
 
-Lemma Q_of_RcstR : forall c, Q2R (Q_of_Rcst c) = R_of_Rcst c.
+Lemma Q_of_RcstR : forall c, IQR (Q_of_Rcst c) = R_of_Rcst c.
 Proof.
     induction c ; simpl ; try (rewrite <- IHc1 ; rewrite <- IHc2).
-    apply Q2R_0. 
-    apply Q2R_1. 
+    apply IQR_0. 
+    apply IQR_1. 
     reflexivity.
-    unfold Q2R. simpl. rewrite Rinv_1. reflexivity.
-    apply Q2R_plus.
-    apply Q2R_minus.
-    apply Q2R_mult.
+    unfold IQR. simpl. rewrite Rinv_1. reflexivity.
+    apply IQR_plus.
+    apply IQR_minus.
+    apply IQR_mult.
     rewrite <- IHc.
-    apply Q2R_inv_ext.
+    apply IQR_inv_ext.
     rewrite <- IHc.
-    apply Q2R_opp.
+    apply IQR_opp.
   Qed.
 
 Require Import EnvRing.
@@ -492,7 +493,7 @@ Definition Reval_formula' :=
   eval_sformula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt nat_of_N pow R_of_Rcst.
 
 Definition QReval_formula := 
-  eval_formula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R nat_of_N pow .
+  eval_formula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IQR nat_of_N pow .
 
 Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f.
 Proof.
@@ -507,12 +508,12 @@ Proof.
 Qed.
 
 Definition Qeval_nformula :=
-  eval_nformula 0 Rplus Rmult  (@eq R) Rle Rlt Q2R.
+  eval_nformula 0 Rplus Rmult  (@eq R) Rle Rlt IQR.
 
 
 Lemma Reval_nformula_dec : forall env d, (Qeval_nformula env d) \/ ~ (Qeval_nformula env d).
 Proof.
-  exact (fun env d =>eval_nformula_dec Rsor Q2R env d).
+  exact (fun env d =>eval_nformula_dec Rsor IQR env d).
 Qed.
 
 Definition RWitness := Psatz Q.
diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 6c248e839..f41252b78 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -45,217 +45,6 @@ Section MakeVarMap.
                       end
     end.
 
-  (* FK: scheduled for deletion *)
-  (* an off_map (a map with offset) offers the same functionalites  as /plugins/setoid_ring/BinList.v - it is used in EnvRing.v *)
-  (*
-  Definition off_map  :=  (option positive *t )%type.
-
-
-
-  Definition jump  (j:positive) (l:off_map ) :=
-    let (o,m) := l in
-      match o with
-        | None => (Some j,m)
-        | Some j0 => (Some (j+j0)%positive,m)
-      end.
-
-  Definition nth  (n:positive) (l: off_map ) :=
-    let (o,m) := l in
-      let idx  := match o with
-                    | None => n
-                    | Some i => i + n
-                  end%positive in
-      find  idx m.
-
-
-  Definition hd  (l:off_map) := nth  xH l.
-
-
-  Definition tail (l:off_map ) := jump xH l.
-
-
-  Lemma psucc : forall p,  (match p with
-                              | xI y' => xO (Psucc y')
-                              | xO y' => xI y'
-                              | 1%positive => 2%positive
-                            end) = (p+1)%positive.
-  Proof.
-    destruct p.
-    auto with zarith.
-    rewrite xI_succ_xO.
-    auto with zarith.
-    reflexivity.
-  Qed.
-
-  Lemma jump_Pplus : forall i j l,
-    (jump (i + j) l) = (jump i (jump j l)).
-  Proof.
-    unfold jump.
-    destruct l.
-    destruct o.
-    rewrite Pplus_assoc.
-    reflexivity.
-    reflexivity.
-  Qed.
-
-  Lemma jump_simpl : forall p l,
-    jump p l =
-    match p with
-      | xH => tail l
-      | xO p => jump p (jump p l)
-      | xI p  => jump p (jump p (tail l))
-    end.
-  Proof.
-    destruct p ; unfold tail ; intros ;  repeat rewrite <- jump_Pplus.
-    (* xI p = p + p + 1 *)
-    rewrite xI_succ_xO.
-    rewrite Pplus_diag.
-    rewrite <- Pplus_one_succ_r.
-    reflexivity.
-    (* xO p = p + p *)
-    rewrite Pplus_diag.
-    reflexivity.
-    reflexivity.
-  Qed.
-
-  Ltac jump_s :=
-    repeat
-      match goal with
-        | |- context [jump xH ?e] => rewrite (jump_simpl xH)
-        | |- context [jump (xO ?p) ?e] => rewrite (jump_simpl (xO p))
-        | |- context [jump (xI ?p) ?e] => rewrite (jump_simpl (xI p))
-      end.
-
-  Lemma jump_tl : forall j l, tail (jump j l) = jump j (tail l).
-  Proof.
-    unfold tail.
-    intros.
-    repeat rewrite <- jump_Pplus.
-    rewrite Pplus_comm.
-    reflexivity.
-  Qed.
-
-  Lemma jump_Psucc : forall j l,
-    (jump (Psucc j) l) = (jump 1 (jump j l)).
-  Proof.
-    intros.
-    rewrite <- jump_Pplus.
-    rewrite Pplus_one_succ_r.
-    rewrite Pplus_comm.
-    reflexivity.
-  Qed.
-
-  Lemma jump_Pdouble_minus_one : forall i l,
-    (jump (Pdouble_minus_one i) (tail l)) = (jump i (jump i l)).
-  Proof.
-    unfold tail.
-    intros.
-    repeat rewrite <- jump_Pplus.
-    rewrite <- Pplus_one_succ_r.
-    rewrite Psucc_o_double_minus_one_eq_xO.
-    rewrite Pplus_diag.
-    reflexivity.
-  Qed.
-
-  Lemma jump_x0_tail : forall p l, jump (xO p) (tail l) = jump (xI p) l.
-  Proof.
-    intros.
-    jump_s.
-    repeat rewrite <- jump_Pplus.
-    reflexivity.
-  Qed.
-
-
-  Lemma nth_spec : forall p l,
-    nth p l =
-    match p with
-      | xH => hd  l
-      | xO p => nth p (jump p l)
-      | xI p => nth p (jump p (tail l))
-    end.
-  Proof.
-    unfold nth.
-    destruct l.
-    destruct o.
-    simpl.
-    rewrite psucc.
-    destruct p.
-    replace (p0 + xI p)%positive with ((p + (p0 + 1) + p))%positive.
-    reflexivity.
-    rewrite xI_succ_xO.
-    rewrite Pplus_one_succ_r.
-    rewrite <- Pplus_diag.
-    rewrite Pplus_comm.
-    symmetry.
-    rewrite (Pplus_comm p0).
-    rewrite <- Pplus_assoc.
-    rewrite (Pplus_comm 1)%positive.
-    rewrite <- Pplus_assoc.
-    reflexivity.
-  (**)
-    replace ((p0 + xO p))%positive with (p + p0 + p)%positive.
-    reflexivity.
-    rewrite <- Pplus_diag.
-    rewrite <- Pplus_assoc.
-    rewrite Pplus_comm.
-    rewrite Pplus_assoc.
-    reflexivity.
-    reflexivity.
-    simpl.
-    destruct p.
-    rewrite xI_succ_xO.
-    rewrite Pplus_one_succ_r.
-    rewrite <- Pplus_diag.
-    symmetry.
-    rewrite Pplus_comm.
-    rewrite Pplus_assoc.
-    reflexivity.
-    rewrite Pplus_diag.
-    reflexivity.
-    reflexivity.
-  Qed.
-
-
-  Lemma nth_jump : forall p l, nth p (tail l) = hd (jump p l).
-  Proof.
-    destruct l.
-    unfold tail.
-    unfold hd.
-    unfold jump.
-    unfold nth.
-    destruct o.
-    symmetry.
-    rewrite Pplus_comm.
-    rewrite <- Pplus_assoc.
-    rewrite (Pplus_comm p0).
-    reflexivity.
-    rewrite Pplus_comm.
-    reflexivity.
-  Qed.
-
-  Lemma nth_Pdouble_minus_one :
-    forall p l, nth (Pdouble_minus_one p) (tail l) = nth p (jump p l).
-  Proof.
-    destruct l.
-    unfold tail.
-    unfold nth, jump.
-    destruct o.
-    rewrite ((Pplus_comm p)).
-    rewrite <- (Pplus_assoc p0).
-    rewrite Pplus_diag.
-    rewrite <- Psucc_o_double_minus_one_eq_xO.
-    rewrite Pplus_one_succ_r.
-    rewrite (Pplus_comm (Pdouble_minus_one p)).
-    rewrite Pplus_assoc.
-    rewrite (Pplus_comm p0).
-    reflexivity.
-    rewrite <- Pplus_one_succ_l.
-    rewrite Psucc_o_double_minus_one_eq_xO.
-    rewrite Pplus_diag.
-    reflexivity.
-  Qed.
-
-*)
 
 End MakeVarMap.
 
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 5efe9f426..540d1b9c1 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -1182,6 +1182,7 @@ let reduce_var_change psys =
 
 
   let lia sys = 
+    LinPoly.MonT.clear ();
     let sys = List.map (develop_constraint z_spec) sys in
     let (sys:cstr_compat list) = List.map cstr_compat_of_poly sys in
     let sys = mapi (fun c i -> (c,Hyp i)) sys in
@@ -1189,6 +1190,7 @@ let reduce_var_change psys =
 
 
   let nlia sys = 
+    LinPoly.MonT.clear ();
     let sys = List.map (develop_constraint z_spec) sys in
     let sys = mapi (fun c i -> (c,Hyp i)) sys in
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 42d451a2d..50b01d751 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -407,7 +407,7 @@ struct
   let coq_Rdiv = lazy (r_constant "Rdiv")
   let coq_Rinv = lazy (r_constant "Rinv")
   let coq_Rpower = lazy (r_constant "pow")
-  let coq_Q2R    = lazy (constant "Q2R")
+  let coq_IQR    = lazy (constant "IQR")
   let coq_IZR    = lazy (constant "IZR")
 
   let coq_PEX = lazy (constant "PEX" )
@@ -997,7 +997,7 @@ struct
 	      ParseError -> 
 		match op with
 		  | op when op = Lazy.force coq_Rinv -> Mc.CInv(rconstant args.(0))
-		  | op when op = Lazy.force coq_Q2R  -> Mc.CQ (parse_q args.(0))
+		  | op when op = Lazy.force coq_IQR  -> Mc.CQ (parse_q args.(0))
 (*		  | op when op = Lazy.force coq_IZR  -> Mc.CZ (parse_z args.(0))*)
 		  | _ ->  raise ParseError
 	end
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index d203f0e87..14d312a5c 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -590,9 +590,13 @@ struct
     (** A hash table might be preferable but requires a hash function. *)
     let (index_of_monomial : int MonoMap.t ref) = ref (MonoMap.empty)
     let (monomial_of_index : Monomial.t IntMap.t ref) = ref (IntMap.empty)
+    let fresh = ref 0
 
+    let clear () = 
+      index_of_monomial := MonoMap.empty;
+      monomial_of_index := IntMap.empty ; 
+      fresh := 0
 
-    let fresh = ref 0
 
     let register m = 
       try