diff options
author | 2001-05-07 15:33:06 +0000 | |
---|---|---|
committer | 2001-05-07 15:33:06 +0000 | |
commit | d4815f9ccc6b59565f36cc5a4c66d9916728d202 (patch) | |
tree | 2de622392a1de9f277b72d6c31db04bbeb7ed91b | |
parent | aec4317b506e4f47b292cfc5ca79a3b025cf854d (diff) |
integration de field a fourier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1734 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/fourier/Fourier.v | 8 | ||||
-rw-r--r-- | contrib/fourier/fourier.ml | 3 | ||||
-rw-r--r-- | contrib/fourier/fourierR.ml | 22 |
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) *) ;; |