micromega: better handling of exponentiation + correction of test-suite termination bug

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

7 files changed, 92 insertions, 46 deletions

diff --git a/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 7b2c0231f..1d7fbd569 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -20,6 +20,7 @@ Require Import RMicromega.
 Require Import VarMap.
 Require Import RingMicromega.
 Require Import NArith.
+Require Import QArith.
 
 Extract Inductive prod => "( * )" [ "(,)" ].
 Extract Inductive List.list => list [ "[]" "(::)" ].
@@ -39,7 +40,7 @@ Extract Inlined Constant andb => "(&&)".
 
 Extraction "micromega.ml"
   List.map simpl_cone (*map_cone  indexes*)
-  denorm
+  denorm Qpower
   n_of_Z Nnat.N_of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
 
 (* Local Variables: *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index d10ae00c8..0e960146c 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -408,9 +408,9 @@ let dump_q q =
 	   [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|])
 
 let parse_q term =
- match Term.kind_of_term term with
-  | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
-	{Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
+    match Term.kind_of_term term with
+      | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
+	    {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
       else raise ParseError
   |  _ -> raise ParseError
 
@@ -690,8 +690,8 @@ let parse_q term =
 		  begin
 		    try
 		      let (expr,env) = parse_expr env args.(0) in
-		      let exp = (parse_exp args.(1)) in
-			(Mc.PEpow(expr, exp)  , env)
+		      let power = (parse_exp expr args.(1)) in 
+			(power  , env) 
 		    with _ ->   (* if the exponent is a variable *)
 		      let (env,n) = Env.compute_rank_add env term in (Mc.PEX n, env)
 		  end
@@ -753,16 +753,40 @@ let rconstant term =
   |  _ -> raise ParseError
 
 
-let parse_zexpr =
- parse_expr zconstant (fun x -> Mc.n_of_Z (parse_z x))  zop_spec
-let parse_qexpr  =
- parse_expr qconstant (fun x -> Mc.n_of_Z (parse_z x)) qop_spec
-let parse_rexpr =
- parse_expr rconstant  (fun x -> Mc.n_of_nat (parse_nat x)) rop_spec
-
-
- let  parse_arith parse_op parse_expr env cstr =
-  if debug
+let parse_zexpr =  parse_expr 
+   zconstant 
+   (fun expr x -> 
+     let exp = (parse_z x) in
+       match exp with
+	 | Mc.Zneg _ -> Mc.PEc Mc.Z0
+	 |   _     ->  Mc.PEpow(expr, Mc.n_of_Z exp))
+   zop_spec 
+
+let parse_qexpr  =  parse_expr 
+  qconstant 
+   (fun expr x -> 
+     let exp = parse_z x in
+       match exp with
+	 | Mc.Zneg _ -> 
+	     begin
+	       match expr with
+	       | Mc.PEc q -> Mc.PEc (Mc.qpower q exp)
+	       |     _    -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError
+	     end
+	 | _     ->  let exp = Mc.n_of_Z  exp in
+		       Mc.PEpow(expr,exp))
+  qop_spec 
+
+let parse_rexpr =  parse_expr 
+  rconstant  
+  (fun expr x -> 
+     let exp = Mc.n_of_nat (parse_nat x) in
+       Mc.PEpow(expr,exp))  
+  rop_spec
+
+
+ let  parse_arith parse_op parse_expr env cstr = 
+  if debug 
   then (Pp.pp_flush ();
 	Pp.pp (Pp.str "parse_arith: ");
 	Pp.pp (Printer.prterm  cstr);
@@ -923,9 +947,6 @@ let same_proof sg cl1 cl2 =
       && (xsame_proof sg ) in
   xsame_proof sg
 
-
-
-
 let tags_of_clause tgs wit clause =
  let rec xtags tgs = function
   | Mc.PsatzIn n -> Names.Idset.union tgs
@@ -1115,8 +1136,6 @@ let abstract_formula hyps f =
   in  xabs f
 
 
-
-
 let micromega_order_change spec cert cert_typ env  ff gl =
  let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[|  spec.coeff|])) in
 
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 5c45c8f5f..c350ed0f6 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -220,6 +220,13 @@ type n =
   | N0
   | Npos of positive
 
+(** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)
+
+let rec pow_pos rmul x = function
+  | XI i0 -> let p = pow_pos rmul x i0 in rmul x (rmul p p)
+  | XO i0 -> let p = pow_pos rmul x i0 in rmul p p
+  | XH -> x
+
 type z =
   | Z0
   | Zpos of positive
@@ -341,12 +348,12 @@ let zabs = function
   | Zpos p -> Zpos p
   | Zneg p -> Zpos p
 
-(** val z_gt_dec : z -> z -> bool **)
+(** val zmax : z -> z -> z **)
 
-let z_gt_dec x y =
-  match zcompare x y with
-    | Gt -> true
-    | _ -> false
+let zmax m n0 =
+  match zcompare m n0 with
+    | Lt -> n0
+    | _ -> m
 
 (** val zle_bool : z -> z -> bool **)
 
@@ -1349,6 +1356,26 @@ let qopp x =
 let qminus x y =
   qplus x (qopp y)
 
+(** val qinv : q -> q **)
+
+let qinv x =
+  match x.qnum with
+    | Z0 -> { qnum = Z0; qden = XH }
+    | Zpos p -> { qnum = (Zpos x.qden); qden = p }
+    | Zneg p -> { qnum = (Zneg x.qden); qden = p }
+
+(** val qpower_positive : q -> positive -> q **)
+
+let qpower_positive q0 p =
+  pow_pos qmult q0 p
+
+(** val qpower : q -> z -> q **)
+
+let qpower q0 = function
+  | Z0 -> { qnum = (Zpos XH); qden = XH }
+  | Zpos p -> qpower_positive q0 p
+  | Zneg p -> qinv (qpower_positive q0 p)
+
 (** val pgcdn : nat -> positive -> positive -> positive **)
 
 let rec pgcdn n0 a b =
@@ -1486,11 +1513,10 @@ type zArithProof =
   | CutProof of zWitness * zArithProof
   | EnumProof of zWitness * zWitness * zArithProof list
 
-(** val isZ0 : z -> bool **)
+(** val zgcdM : z -> z -> z **)
 
-let isZ0 = function
-  | Z0 -> true
-  | _ -> false
+let zgcdM x y =
+  zmax (zgcd x y) (Zpos XH)
 
 (** val zgcd_pol : z polC -> z  *  z **)
 
@@ -1499,12 +1525,7 @@ let rec zgcd_pol = function
   | Pinj (p2, p3) -> zgcd_pol p3
   | PX (p2, p3, q0) ->
       let g1 , c1 = zgcd_pol p2 in
-      let g2 , c2 = zgcd_pol q0 in
-      if isZ0 g1
-      then Z0 , c2
-      else if isZ0 (zgcd g1 c1)
-           then Z0 , c2
-           else if isZ0 g2 then Z0 , c2 else (zgcd (zgcd g1 c1) g2) , c2
+      let g2 , c2 = zgcd_pol q0 in (zgcdM (zgcdM g1 c1) g2) , c2
 
 (** val zdiv_pol : z polC -> z -> z polC **)
 
@@ -1604,10 +1625,7 @@ let rec zChecker l = function
 
                                                   match pfs with
                                                     |
-                                                  [] ->
-                                                  if z_gt_dec lb ub
-                                                  then true
-                                                  else false
+                                                  [] -> zgt_bool lb ub
                                                     |
                                                   pf1 :: rsr ->
                                                   (&&)
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 34f61904a..3e3ae2c31 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -61,6 +61,8 @@ type n =
   | N0
   | Npos of positive
 
+val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1
+
 type z =
   | Z0
   | Zpos of positive
@@ -86,7 +88,7 @@ val zcompare : z -> z -> comparison
 
 val zabs : z -> z
 
-val z_gt_dec : z -> z -> bool
+val zmax : z -> z -> z
 
 val zle_bool : z -> z -> bool
 
@@ -349,6 +351,12 @@ val qopp : q -> q
 
 val qminus : q -> q -> q
 
+val qinv : q -> q
+
+val qpower_positive : q -> positive -> q
+
+val qpower : q -> z -> q
+
 val pgcdn : nat -> positive -> positive -> positive
 
 val pgcd : positive -> positive -> positive
@@ -388,7 +396,7 @@ type zArithProof =
   | CutProof of zWitness * zArithProof
   | EnumProof of zWitness * zWitness * zArithProof list
 
-val isZ0 : z -> bool
+val zgcdM : z -> z -> z
 
 val zgcd_pol : z polC -> z  *  z
 
diff --git a/test-suite/micromega/csdp.cache b/test-suite/micromega/csdp.cache
index 961d159bf..114f714f3 100644
--- a/test-suite/micromega/csdp.cache
+++ b/test-suite/micromega/csdp.cache
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index c9c779f90..76dc52e6c 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -67,12 +67,12 @@ Qed.
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
   intros.
-  psatz Q 2.
+  psatz Q 3.
 Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 # 1) *x^2*y^2) >= 0.
 Proof.
-  intros ; psatz Q.
+  intros ; psatz Q 3.
 Qed.
 
 
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index c957add69..9bb9daccb 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -64,12 +64,12 @@ Qed.
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
   intros.
-  psatz R 2.
+  psatz R 3.
 Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 ) *x^2*y^2) >= 0.
 Proof.
-  intros ; psatz R.
+  intros ; psatz R 2.
 Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).