integration de field a fourier

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

3 files changed, 29 insertions, 4 deletions

diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v
index 67d734281..32c61b6d2 100644
--- a/contrib/fourier/Fourier.v
+++ b/contrib/fourier/Fourier.v
@@ -14,14 +14,20 @@ Declare ML Module "quote".
 Declare ML Module "ring".
 Declare ML Module "fourier".
 Declare ML Module "fourierR".
+Declare ML Module "field".
 
 Require Export Fourier_util.
+Require Export Field.
+Require Export DiscrR.
 
 Grammar tactic simple_tactic:ast:=
   fourier
-  ["Fourier" constrarg_list($arg)] ->
+  ["FourierZ" constrarg_list($arg)] ->
   [(Fourier ($LIST $arg))].
 
+Tactic Definition Fourier  :=
+  Abstract (FourierZ;Field;DiscrR).
+
 Tactic Definition FourierEq  :=
   Apply Rge_ge_eq ; Fourier.
 
diff --git a/contrib/fourier/fourier.ml b/contrib/fourier/fourier.ml
index ea124ed17..bb8b4ea13 100644
--- a/contrib/fourier/fourier.ml
+++ b/contrib/fourier/fourier.ml
@@ -43,6 +43,7 @@ let r1 = {num=1;den=1};;
 let rnorm x = let x = (if x.den<0 then {num=(-x.num);den=(-x.den)} else x) in
               if x.num=0 then r0
               else (let d=pgcd x.num x.den in
+		    let d= (if d<0 then -d else d) in
                     {num=(x.num)/d;den=(x.den)/d});;
  
 let rop x = rnorm {num=(-x.num);den=x.den};;
@@ -55,6 +56,8 @@ let rmult x y = rnorm {num=x.num*y.num;den=x.den*y.den};;
 
 let rinv x = rnorm {num=x.den;den=x.num};;
 
+let rdiv x y = rnorm {num=x.num*y.den;den=x.den*y.num};;
+
 let rinf x y = x.num*y.den < y.num*x.den;;
 let rinfeq x y = x.num*y.den <= y.num*x.den;;
 
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index c85ead536..49706bbd3 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -95,6 +95,9 @@ let rec rational_of_constr c =
                 |"Coq.Reals.Rdefinitions.Rmult" -> 
                       rmult (rational_of_constr args.(0))
                             (rational_of_constr args.(1))
+                |"Coq.Reals.Rdefinitions.Rdiv" -> 
+                      rdiv (rational_of_constr args.(0))
+                            (rational_of_constr args.(1))
                 |"Coq.Reals.Rdefinitions.Rplus" -> 
                       rplus (rational_of_constr args.(0))
                             (rational_of_constr args.(1))
@@ -137,6 +140,16 @@ let rec flin_of_constr c =
 	      with _-> (flin_add (flin_zero())
 				 args.(0) 
 				 (rational_of_constr args.(1))))
+	    |"Coq.Reals.Rdefinitions.Rinv"->
+	       let a=(rational_of_constr args.(0)) in
+	       flin_add_cste (flin_zero()) (rinv a)
+	    |"Coq.Reals.Rdefinitions.Rdiv"->
+	      (let b=(rational_of_constr args.(1)) in
+	       try (let a = (rational_of_constr args.(0)) in
+		       (flin_add_cste (flin_zero()) (rdiv a b)))
+	       with _-> (flin_add (flin_zero())
+		             args.(0) 
+                             (rinv b)))
             |_->assert false)
            |_ -> assert false)
   | IsConst (c,l) ->
@@ -423,7 +436,7 @@ let rec fourier gl=
     let res=fourier_lineq (!lineq) in
     let tac=ref tclIDTAC in
     if res=[]
-    then (print_string "Tactic Fourier fails, perhaps because it cannot prove some equality on rationnal numbers with the tactic Ring.";
+    then (print_string "Tactic Fourier fails.";
 		       flush stdout)
     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
     else (match res with
@@ -517,7 +530,9 @@ let rec fourier gl=
 							   (parse "R1"))
 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)	
 
-      			        [(Ring.polynom []);
+      			        [tclORELSE
+                                   (Ring.polynom [])
+                                   tclIDTAC;
 					  (tclTHEN (apply (parse "sym_eqT"))
 						(apply (parse "Rinv_R1")))]
                                
@@ -530,7 +545,8 @@ let rec fourier gl=
       |_-> assert false) |_-> assert false
 	  );
 (*    ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
-      ((tclABSTRACT None !tac) gl)
+      (!tac gl) 
+(*      ((tclABSTRACT None !tac) gl) *)
 
 ;;