diff options
Diffstat (limited to 'plugins/fourier')
-rw-r--r-- | plugins/fourier/Fourier.v | 20 | ||||
-rw-r--r-- | plugins/fourier/Fourier_util.v | 222 | ||||
-rw-r--r-- | plugins/fourier/fourier.ml | 204 | ||||
-rw-r--r-- | plugins/fourier/fourierR.ml | 644 | ||||
-rw-r--r-- | plugins/fourier/fourier_plugin.mlpack | 3 | ||||
-rw-r--r-- | plugins/fourier/g_fourier.ml4 | 18 |
6 files changed, 0 insertions, 1111 deletions
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v deleted file mode 100644 index 07f32be8..00000000 --- a/plugins/fourier/Fourier.v +++ /dev/null @@ -1,20 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* "Fourier's method to solve linear inequations/equations systems.".*) - -Require Export Field. -Require Export DiscrR. -Require Export Fourier_util. -Declare ML Module "fourier_plugin". - -Ltac fourier := abstract (compute [IZR IPR IPR_2] in *; fourierz; field; discrR). - -Ltac fourier_eq := apply Rge_antisym; fourier. diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v deleted file mode 100644 index d3159698..00000000 --- a/plugins/fourier/Fourier_util.v +++ /dev/null @@ -1,222 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -Require Export Rbase. -Comments "Lemmas used by the tactic Fourier". - -Open Scope R_scope. - -Lemma Rfourier_lt : forall x1 y1 a:R, x1 < y1 -> 0 < a -> a * x1 < a * y1. -intros; apply Rmult_lt_compat_l; assumption. -Qed. - -Lemma Rfourier_le : forall x1 y1 a:R, x1 <= y1 -> 0 < a -> a * x1 <= a * y1. -red. -intros. -case H; auto with real. -Qed. - -Lemma Rfourier_lt_lt : - forall x1 y1 x2 y2 a:R, - x1 < y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -apply Rplus_lt_compat. -try exact H. -apply Rfourier_lt. -try exact H0. -try exact H1. -Qed. - -Lemma Rfourier_lt_le : - forall x1 y1 x2 y2 a:R, - x1 < y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H0; intros. -apply Rplus_lt_compat. -try exact H. -apply Rfourier_lt; auto with real. -rewrite H2. -rewrite (Rplus_comm y1 (a * y2)). -rewrite (Rplus_comm x1 (a * y2)). -apply Rplus_lt_compat_l. -try exact H. -Qed. - -Lemma Rfourier_le_lt : - forall x1 y1 x2 y2 a:R, - x1 <= y1 -> x2 < y2 -> 0 < a -> x1 + a * x2 < y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H; intros. -apply Rfourier_lt_le; auto with real. -rewrite H2. -apply Rplus_lt_compat_l. -apply Rfourier_lt; auto with real. -Qed. - -Lemma Rfourier_le_le : - forall x1 y1 x2 y2 a:R, - x1 <= y1 -> x2 <= y2 -> 0 < a -> x1 + a * x2 <= y1 + a * y2. -intros x1 y1 x2 y2 a H H0 H1; try assumption. -case H0; intros. -red. -left; try assumption. -apply Rfourier_le_lt; auto with real. -rewrite H2. -case H; intros. -red. -left; try assumption. -rewrite (Rplus_comm x1 (a * y2)). -rewrite (Rplus_comm y1 (a * y2)). -apply Rplus_lt_compat_l. -try exact H3. -rewrite H3. -red. -right; try assumption. -auto with real. -Qed. - -Lemma Rlt_zero_pos_plus1 : forall x:R, 0 < x -> 0 < 1 + x. -intros x H; try assumption. -rewrite Rplus_comm. -apply Rle_lt_0_plus_1. -red; auto with real. -Qed. - -Lemma Rlt_mult_inv_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x * / y. -intros x y H H0; try assumption. -replace 0 with (x * 0). -apply Rmult_lt_compat_l; auto with real. -ring. -Qed. - -Lemma Rlt_zero_1 : 0 < 1. -exact Rlt_0_1. -Qed. - -Lemma Rle_zero_pos_plus1 : forall x:R, 0 <= x -> 0 <= 1 + x. -intros x H; try assumption. -case H; intros. -red. -left; try assumption. -apply Rlt_zero_pos_plus1; auto with real. -rewrite <- H0. -replace (1 + 0) with 1. -red; left. -exact Rlt_zero_1. -ring. -Qed. - -Lemma Rle_mult_inv_pos : forall x y:R, 0 <= x -> 0 < y -> 0 <= x * / y. -intros x y H H0; try assumption. -case H; intros. -red; left. -apply Rlt_mult_inv_pos; auto with real. -rewrite <- H1. -red; right; ring. -Qed. - -Lemma Rle_zero_1 : 0 <= 1. -red; left. -exact Rlt_zero_1. -Qed. - -Lemma Rle_not_lt : forall n d:R, 0 <= n * / d -> ~ 0 < - n * / d. -intros n d H; red; intros H0; try exact H0. -generalize (Rgt_not_le 0 (n * / d)). -intros H1; elim H1; try assumption. -replace (n * / d) with (- - (n * / d)). -replace 0 with (- -0). -replace (- (n * / d)) with (- n * / d). -replace (-0) with 0. -red. -apply Ropp_gt_lt_contravar. -red. -exact H0. -ring. -ring. -ring. -ring. -Qed. - -Lemma Rnot_lt0 : forall x:R, ~ 0 < 0 * x. -intros x; try assumption. -replace (0 * x) with 0. -apply Rlt_irrefl. -ring. -Qed. - -Lemma Rlt_not_le_frac_opp : forall n d:R, 0 < n * / d -> ~ 0 <= - n * / d. -intros n d H; try assumption. -apply Rgt_not_le. -replace 0 with (-0). -replace (- n * / d) with (- (n * / d)). -apply Ropp_lt_gt_contravar. -try exact H. -ring. -ring. -Qed. - -Lemma Rnot_lt_lt : forall x y:R, ~ 0 < y - x -> ~ x < y. -unfold not; intros. -apply H. -apply Rplus_lt_reg_l with x. -replace (x + 0) with x. -replace (x + (y - x)) with y. -try exact H0. -ring. -ring. -Qed. - -Lemma Rnot_le_le : forall x y:R, ~ 0 <= y - x -> ~ x <= y. -unfold not; intros. -apply H. -case H0; intros. -left. -apply Rplus_lt_reg_l with x. -replace (x + 0) with x. -replace (x + (y - x)) with y. -try exact H1. -ring. -ring. -right. -rewrite H1; ring. -Qed. - -Lemma Rfourier_gt_to_lt : forall x y:R, y > x -> x < y. -unfold Rgt; intros; assumption. -Qed. - -Lemma Rfourier_ge_to_le : forall x y:R, y >= x -> x <= y. -intros x y; exact (Rge_le y x). -Qed. - -Lemma Rfourier_eqLR_to_le : forall x y:R, x = y -> x <= y. -exact Req_le. -Qed. - -Lemma Rfourier_eqRL_to_le : forall x y:R, y = x -> x <= y. -exact Req_le_sym. -Qed. - -Lemma Rfourier_not_ge_lt : forall x y:R, (x >= y -> False) -> x < y. -exact Rnot_ge_lt. -Qed. - -Lemma Rfourier_not_gt_le : forall x y:R, (x > y -> False) -> x <= y. -exact Rnot_gt_le. -Qed. - -Lemma Rfourier_not_le_gt : forall x y:R, (x <= y -> False) -> x > y. -exact Rnot_le_lt. -Qed. - -Lemma Rfourier_not_lt_ge : forall x y:R, (x < y -> False) -> x >= y. -exact Rnot_lt_ge. -Qed. diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml deleted file mode 100644 index bee2b3b5..00000000 --- a/plugins/fourier/fourier.ml +++ /dev/null @@ -1,204 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* Méthode d'élimination de Fourier *) -(* Référence: -Auteur(s) : Fourier, Jean-Baptiste-Joseph - -Titre(s) : Oeuvres de Fourier [Document électronique]. Tome second. Mémoires publiés dans divers recueils / publ. par les soins de M. Gaston Darboux,... - -Publication : Numérisation BnF de l'édition de Paris : Gauthier-Villars, 1890 - -Pages: 326-327 - -http://gallica.bnf.fr/ -*) - -(* Un peu de calcul sur les rationnels... -Les opérations rendent des rationnels normalisés, -i.e. le numérateur et le dénominateur sont premiers entre eux. -*) -type rational = {num:int; - den:int} -;; -let print_rational x = - print_int x.num; - print_string "/"; - print_int x.den -;; - -let rec pgcd x y = if y = 0 then x else pgcd y (x mod y);; - - -let r0 = {num=0;den=1};; -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};; - -let rplus x y = rnorm {num=x.num*y.den + y.num*x.den;den=x.den*y.den};; - -let rminus x y = rnorm {num=x.num*y.den - y.num*x.den;den=x.den*y.den};; - -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;; - -(* {coef;hist;strict}, où coef=[c1; ...; cn; d], représente l'inéquation -c1x1+...+cnxn < d si strict=true, <= sinon, -hist donnant les coefficients (positifs) d'une combinaison linéaire qui permet d'obtenir l'inéquation à partir de celles du départ. -*) - -type ineq = {coef:rational list; - hist:rational list; - strict:bool};; - -let pop x l = l:=x::(!l);; - -(* sépare la liste d'inéquations s selon que leur premier coefficient est -négatif, nul ou positif. *) -let partitionne s = - let lpos=ref [] in - let lneg=ref [] in - let lnul=ref [] in - List.iter (fun ie -> match ie.coef with - [] -> raise (Failure "empty ineq") - |(c::r) -> if rinf c r0 - then pop ie lneg - else if rinf r0 c then pop ie lpos - else pop ie lnul) - s; - [!lneg;!lnul;!lpos] -;; -(* initialise les histoires d'une liste d'inéquations données par leurs listes de coefficients et leurs strictitudes (!): -(add_hist [(equation 1, s1);...;(équation n, sn)]) -= -[{équation 1, [1;0;...;0], s1}; - {équation 2, [0;1;...;0], s2}; - ... - {équation n, [0;0;...;1], sn}] -*) -let add_hist le = - let n = List.length le in - let i = ref 0 in - List.map (fun (ie,s) -> - let h = ref [] in - for _k = 1 to (n - (!i) - 1) do pop r0 h; done; - pop r1 h; - for _k = 1 to !i do pop r0 h; done; - i:=!i+1; - {coef=ie;hist=(!h);strict=s}) - le -;; -(* additionne deux inéquations *) -let ie_add ie1 ie2 = {coef=List.map2 rplus ie1.coef ie2.coef; - hist=List.map2 rplus ie1.hist ie2.hist; - strict=ie1.strict || ie2.strict} -;; -(* multiplication d'une inéquation par un rationnel (positif) *) -let ie_emult a ie = {coef=List.map (fun x -> rmult a x) ie.coef; - hist=List.map (fun x -> rmult a x) ie.hist; - strict= ie.strict} -;; -(* on enlève le premier coefficient *) -let ie_tl ie = {coef=List.tl ie.coef;hist=ie.hist;strict=ie.strict} -;; -(* le premier coefficient: "tête" de l'inéquation *) -let hd_coef ie = List.hd ie.coef -;; - -(* calcule toutes les combinaisons entre inéquations de tête négative et inéquations de tête positive qui annulent le premier coefficient. -*) -let deduce_add lneg lpos = - let res=ref [] in - List.iter (fun i1 -> - List.iter (fun i2 -> - let a = rop (hd_coef i1) in - let b = hd_coef i2 in - pop (ie_tl (ie_add (ie_emult b i1) - (ie_emult a i2))) res) - lpos) - lneg; - !res -;; -(* élimination de la première variable à partir d'une liste d'inéquations: -opération qu'on itère dans l'algorithme de Fourier. -*) -let deduce1 s = - match (partitionne s) with - [lneg;lnul;lpos] -> - let lnew = deduce_add lneg lpos in - (List.map ie_tl lnul)@lnew - |_->assert false -;; -(* algorithme de Fourier: on élimine successivement toutes les variables. -*) -let deduce lie = - let n = List.length (fst (List.hd lie)) in - let lie=ref (add_hist lie) in - for _i = 1 to n - 1 do - lie:= deduce1 !lie; - done; - !lie -;; - -(* donne [] si le système a des solutions, -sinon donne [c,s,lc] -où lc est la combinaison linéaire des inéquations de départ -qui donne 0 < c si s=true - ou 0 <= c sinon -cette inéquation étant absurde. -*) - -exception Contradiction of (rational * bool * rational list) list - -let unsolvable lie = - let lr = deduce lie in - let check = function - | {coef=[c];hist=lc;strict=s} -> - if (rinf c r0 && (not s)) || (rinfeq c r0 && s) - then raise (Contradiction [c,s,lc]) - |_->assert false - in - try List.iter check lr; [] - with Contradiction l -> l - -(* Exemples: - -let test1=[[r1;r1;r0],true;[rop r1;r1;r1],false;[r0;rop r1;rop r1],false];; -deduce test1;; -unsolvable test1;; - -let test2=[ -[r1;r1;r0;r0;r0],false; -[r0;r1;r1;r0;r0],false; -[r0;r0;r1;r1;r0],false; -[r0;r0;r0;r1;r1],false; -[r1;r0;r0;r0;r1],false; -[rop r1;rop r1;r0;r0;r0],false; -[r0;rop r1;rop r1;r0;r0],false; -[r0;r0;rop r1;rop r1;r0],false; -[r0;r0;r0;rop r1;rop r1],false; -[rop r1;r0;r0;r0;rop r1],false -];; -deduce test2;; -unsolvable test2;; - -*) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml deleted file mode 100644 index b1c003de..00000000 --- a/plugins/fourier/fourierR.ml +++ /dev/null @@ -1,644 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - - - -(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients -des inéquations et équations sont entiers. En attendant la tactique Field. -*) - -open Constr -open Tactics -open Names -open Globnames -open Fourier -open Contradiction -open Proofview.Notations - -(****************************************************************************** -Opérations sur les combinaisons linéaires affines. -La partie homogène d'une combinaison linéaire est en fait une table de hash -qui donne le coefficient d'un terme du calcul des constructions, -qui est zéro si le terme n'y est pas. -*) - -module Constrhash = Hashtbl.Make(Constr) - -type flin = {fhom: rational Constrhash.t; - fcste:rational};; - -let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};; - -let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;; - -let flin_add f x c = - let cx = flin_coef f x in - Constrhash.replace f.fhom x (rplus cx c); - f -;; -let flin_add_cste f c = - {fhom=f.fhom; - fcste=rplus f.fcste c} -;; - -let flin_one () = flin_add_cste (flin_zero()) r1;; - -let flin_plus f1 f2 = - let f3 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom; - flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste; -;; - -let flin_minus f1 f2 = - let f3 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; - Constrhash.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom; - flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste); -;; -let flin_emult a f = - let f2 = flin_zero() in - Constrhash.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; - flin_add_cste f2 (rmult a f.fcste); -;; - -(*****************************************************************************) - -type ineq = Rlt | Rle | Rgt | Rge - -let string_of_R_constant kn = - match Constant.repr3 kn with - | ModPath.MPfile dir, sec_dir, id when - sec_dir = DirPath.empty && - DirPath.to_string dir = "Coq.Reals.Rdefinitions" - -> Label.to_string id - | _ -> "constant_not_of_R" - -let rec string_of_R_constr c = - match Constr.kind c with - Cast (c,_,_) -> string_of_R_constr c - |Const (c,_) -> string_of_R_constant c - | _ -> "not_of_constant" - -exception NoRational - -let rec rational_of_constr c = - match Constr.kind c with - | Cast (c,_,_) -> (rational_of_constr c) - | App (c,args) -> - (match (string_of_R_constr c) with - | "Ropp" -> - rop (rational_of_constr args.(0)) - | "Rinv" -> - rinv (rational_of_constr args.(0)) - | "Rmult" -> - rmult (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rdiv" -> - rdiv (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rplus" -> - rplus (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | "Rminus" -> - rminus (rational_of_constr args.(0)) - (rational_of_constr args.(1)) - | _ -> raise NoRational) - | Const (kn,_) -> - (match (string_of_R_constant kn) with - "R1" -> r1 - |"R0" -> r0 - | _ -> raise NoRational) - | _ -> raise NoRational -;; - -exception NoLinear - -let rec flin_of_constr c = - try( - match Constr.kind c with - | Cast (c,_,_) -> (flin_of_constr c) - | App (c,args) -> - (match (string_of_R_constr c) with - "Ropp" -> - flin_emult (rop r1) (flin_of_constr args.(0)) - | "Rplus"-> - flin_plus (flin_of_constr args.(0)) - (flin_of_constr args.(1)) - | "Rminus"-> - flin_minus (flin_of_constr args.(0)) - (flin_of_constr args.(1)) - | "Rmult"-> - (try - let a = rational_of_constr args.(0) in - try - let b = rational_of_constr args.(1) in - flin_add_cste (flin_zero()) (rmult a b) - with NoRational -> - flin_add (flin_zero()) args.(1) a - with NoRational -> - flin_add (flin_zero()) args.(0) - (rational_of_constr args.(1))) - | "Rinv"-> - let a = rational_of_constr args.(0) in - flin_add_cste (flin_zero()) (rinv a) - | "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 NoRational -> - flin_add (flin_zero()) args.(0) (rinv b)) - |_-> raise NoLinear) - | Const (c,_) -> - (match (string_of_R_constant c) with - "R1" -> flin_one () - |"R0" -> flin_zero () - |_-> raise NoLinear) - |_-> raise NoLinear) - with NoRational | NoLinear -> flin_add (flin_zero()) c r1 -;; - -let flin_to_alist f = - let res=ref [] in - Constrhash.iter (fun x c -> res:=(c,x)::(!res)) f; - !res -;; - -(* Représentation des hypothèses qui sont des inéquations ou des équations. -*) -type hineq={hname:constr; (* le nom de l'hypothèse *) - htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) - hleft:constr; - hright:constr; - hflin:flin; - hstrict:bool} -;; - -(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0 -*) - -exception NoIneq - -let ineq1_of_constr (h,t) = - let h = EConstr.Unsafe.to_constr h in - let t = EConstr.Unsafe.to_constr t in - match (Constr.kind t) with - | App (f,args) -> - (match Constr.kind f with - | Const (c,_) when Array.length args = 2 -> - let t1= args.(0) in - let t2= args.(1) in - (match (string_of_R_constant c) with - |"Rlt" -> [{hname=h; - htype="Rlt"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=true}] - |"Rgt" -> [{hname=h; - htype="Rgt"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=true}] - |"Rle" -> [{hname=h; - htype="Rle"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=false}] - |"Rge" -> [{hname=h; - htype="Rge"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=false}] - |_-> raise NoIneq) - | Ind ((kn,i),_) -> - if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq; - let t0= args.(0) in - let t1= args.(1) in - let t2= args.(2) in - (match (Constr.kind t0) with - | Const (c,_) -> - (match (string_of_R_constant c) with - | "R"-> - [{hname=h; - htype="eqTLR"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); - hstrict=false}; - {hname=h; - htype="eqTRL"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); - hstrict=false}] - |_-> raise NoIneq) - |_-> raise NoIneq) - |_-> raise NoIneq) - |_-> raise NoIneq -;; - -(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) -*) - -let fourier_lineq lineq1 = - let nvar=ref (-1) in - let hvar=Constrhash.create 50 in (* la table des variables des inéquations *) - List.iter (fun f -> - Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin - nvar:=(!nvar)+1; - Constrhash.add hvar x (!nvar) - end) - f.hflin.fhom) - lineq1; - let sys= List.map (fun h-> - let v=Array.make ((!nvar)+1) r0 in - Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c) - h.hflin.fhom; - ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) - lineq1 in - unsolvable sys -;; - -(*********************************************************************) -(* Defined constants *) - -let get = Lazy.force -let cget = get -let eget c = EConstr.of_constr (Lazy.force c) -let constant path s = Universes.constr_of_global @@ - Coqlib.coq_reference "Fourier" path s - -(* Standard library *) -open Coqlib -let coq_sym_eqT = lazy (build_coq_eq_sym ()) -let coq_False = lazy (Universes.constr_of_global @@ build_coq_False ()) -let coq_not = lazy (Universes.constr_of_global @@ build_coq_not ()) -let coq_eq = lazy (Universes.constr_of_global @@ build_coq_eq ()) - -(* Rdefinitions *) -let constant_real = constant ["Reals";"Rdefinitions"] - -let coq_Rlt = lazy (constant_real "Rlt") -let coq_Rgt = lazy (constant_real "Rgt") -let coq_Rle = lazy (constant_real "Rle") -let coq_Rge = lazy (constant_real "Rge") -let coq_R = lazy (constant_real "R") -let coq_Rminus = lazy (constant_real "Rminus") -let coq_Rmult = lazy (constant_real "Rmult") -let coq_Rplus = lazy (constant_real "Rplus") -let coq_Ropp = lazy (constant_real "Ropp") -let coq_Rinv = lazy (constant_real "Rinv") -let coq_R0 = lazy (constant_real "R0") -let coq_R1 = lazy (constant_real "R1") - -(* RIneq *) -let coq_Rinv_1 = lazy (constant ["Reals";"RIneq"] "Rinv_1") - -(* Fourier_util *) -let constant_fourier = constant ["fourier";"Fourier_util"] - -let coq_Rlt_zero_1 = lazy (constant_fourier "Rlt_zero_1") -let coq_Rlt_zero_pos_plus1 = lazy (constant_fourier "Rlt_zero_pos_plus1") -let coq_Rle_zero_pos_plus1 = lazy (constant_fourier "Rle_zero_pos_plus1") -let coq_Rlt_mult_inv_pos = lazy (constant_fourier "Rlt_mult_inv_pos") -let coq_Rle_zero_zero = lazy (constant_fourier "Rle_zero_zero") -let coq_Rle_zero_1 = lazy (constant_fourier "Rle_zero_1") -let coq_Rle_mult_inv_pos = lazy (constant_fourier "Rle_mult_inv_pos") -let coq_Rnot_lt0 = lazy (constant_fourier "Rnot_lt0") -let coq_Rle_not_lt = lazy (constant_fourier "Rle_not_lt") -let coq_Rfourier_gt_to_lt = lazy (constant_fourier "Rfourier_gt_to_lt") -let coq_Rfourier_ge_to_le = lazy (constant_fourier "Rfourier_ge_to_le") -let coq_Rfourier_eqLR_to_le = lazy (constant_fourier "Rfourier_eqLR_to_le") -let coq_Rfourier_eqRL_to_le = lazy (constant_fourier "Rfourier_eqRL_to_le") - -let coq_Rfourier_not_ge_lt = lazy (constant_fourier "Rfourier_not_ge_lt") -let coq_Rfourier_not_gt_le = lazy (constant_fourier "Rfourier_not_gt_le") -let coq_Rfourier_not_le_gt = lazy (constant_fourier "Rfourier_not_le_gt") -let coq_Rfourier_not_lt_ge = lazy (constant_fourier "Rfourier_not_lt_ge") -let coq_Rfourier_lt = lazy (constant_fourier "Rfourier_lt") -let coq_Rfourier_le = lazy (constant_fourier "Rfourier_le") -let coq_Rfourier_lt_lt = lazy (constant_fourier "Rfourier_lt_lt") -let coq_Rfourier_lt_le = lazy (constant_fourier "Rfourier_lt_le") -let coq_Rfourier_le_lt = lazy (constant_fourier "Rfourier_le_lt") -let coq_Rfourier_le_le = lazy (constant_fourier "Rfourier_le_le") -let coq_Rnot_lt_lt = lazy (constant_fourier "Rnot_lt_lt") -let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le") -let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp") - -(****************************************************************************** -Construction de la preuve en cas de succès de la méthode de Fourier, -i.e. on obtient une contradiction. -*) -let is_int x = (x.den)=1 -;; - -(* fraction = couple (num,den) *) -let rational_to_fraction x= (x.num,x.den) -;; - -(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) -*) -let int_to_real n = - let nn=abs n in - if nn=0 - then get coq_R0 - else - (let s=ref (get coq_R1) in - for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done; - if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s) -;; -(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) -*) -let rational_to_real x = - let (n,d)=rational_to_fraction x in - mkApp (get coq_Rmult, - [|int_to_real n;mkApp(get coq_Rinv,[|int_to_real d|])|]) -;; - -(* preuve que 0<n*1/d -*) -let tac_zero_inf_pos gl (n,d) = - let get = eget in - let tacn=ref (apply (get coq_Rlt_zero_1)) in - let tacd=ref (apply (get coq_Rlt_zero_1)) in - for _i = 1 to n - 1 do - tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done; - for _i = 1 to d - 1 do - tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd]) -;; - -(* preuve que 0<=n*1/d -*) -let tac_zero_infeq_pos gl (n,d)= - let get = eget in - let tacn=ref (if n=0 - then (apply (get coq_Rle_zero_zero)) - else (apply (get coq_Rle_zero_1))) in - let tacd=ref (apply (get coq_Rlt_zero_1)) in - for _i = 1 to n - 1 do - tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done; - for _i = 1 to d - 1 do - tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done; - (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd]) -;; - -(* preuve que 0<(-n)*(1/d) => False -*) -let tac_zero_inf_false gl (n,d) = - let get = eget in -if n=0 then (apply (get coq_Rnot_lt0)) - else - (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt)) - (tac_zero_infeq_pos gl (-n,d))) -;; - -(* preuve que 0<=(-n)*(1/d) => False -*) -let tac_zero_infeq_false gl (n,d) = - let get = eget in - (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp)) - (tac_zero_inf_pos gl (-n,d))) -;; - -let exact = exact_check;; - -let tac_use h = - let get = eget in - let tac = exact (EConstr.of_constr h.hname) in - match h.htype with - "Rlt" -> tac - |"Rle" -> tac - |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac) - |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac) - |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac) - |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac) - |_->assert false -;; - -(* -let is_ineq (h,t) = - match (Constr.kind t) with - App (f,args) -> - (match (string_of_R_constr f) with - "Rlt" -> true - | "Rgt" -> true - | "Rle" -> true - | "Rge" -> true -(* Wrong:not in Rdefinitions: *) | "eqT" -> - (match (string_of_R_constr args.(0)) with - "R" -> true - | _ -> false) - | _ ->false) - |_->false -;; -*) - -let list_of_sign s = - let open Context.Named.Declaration in - List.map (function LocalAssum (name, typ) -> name, typ - | LocalDef (name, _, typ) -> name, typ) - s;; - -let mkAppL a = - let l = Array.to_list a in - mkApp(List.hd l, Array.of_list (List.tl l)) -;; - -exception GoalDone - -(* Résolution d'inéquations linéaires dans R *) -let rec fourier () = - Proofview.Goal.nf_enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let sigma = Tacmach.New.project gl in - Coqlib.check_required_library ["Coq";"fourier";"Fourier"]; - let goal = Termops.strip_outer_cast sigma concl in - let goal = EConstr.Unsafe.to_constr goal in - let fhyp=Id.of_string "new_hyp_for_fourier" in - (* si le but est une inéquation, on introduit son contraire, - et le but à prouver devient False *) - try - match (Constr.kind goal) with - App (f,args) -> - let get = eget in - (match (string_of_R_constr f) with - "Rlt" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt)) - (intro_using fhyp)) - (fourier ())) - |"Rle" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le)) - (intro_using fhyp)) - (fourier ())) - |"Rgt" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt)) - (intro_using fhyp)) - (fourier ())) - |"Rge" -> - (Tacticals.New.tclTHEN - (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge)) - (intro_using fhyp)) - (fourier ())) - |_-> raise GoalDone) - |_-> raise GoalDone - with GoalDone -> - (* les hypothèses *) - let hyps = List.map (fun (h,t)-> (EConstr.mkVar h,t)) - (list_of_sign (Proofview.Goal.hyps gl)) in - let lineq =ref [] in - List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) - with NoIneq -> ()) - hyps; - (* lineq = les inéquations découlant des hypothèses *) - if !lineq=[] then CErrors.user_err Pp.(str "No inequalities"); - let res=fourier_lineq (!lineq) in - let tac=ref (Proofview.tclUNIT ()) in - if res=[] - then CErrors.user_err Pp.(str "fourier failed") - (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) - else (match res with - [(cres,sres,lc)]-> - (* lc=coefficients multiplicateurs des inéquations - qui donnent 0<cres ou 0<=cres selon sres *) - (*print_string "Fourier's method can prove the goal...";flush stdout;*) - let lutil=ref [] in - List.iter - (fun (h,c) -> - if c<>r0 - then (lutil:=(h,c)::(!lutil)(*; - print_rational(c);print_string " "*))) - (List.combine (!lineq) lc); - (* on construit la combinaison linéaire des inéquation *) - (match (!lutil) with - (h1,c1)::lutil -> - let s=ref (h1.hstrict) in - let t1=ref (mkAppL [|get coq_Rmult; - rational_to_real c1; - h1.hleft|]) in - let t2=ref (mkAppL [|get coq_Rmult; - rational_to_real c1; - h1.hright|]) in - List.iter (fun (h,c) -> - s:=(!s)||(h.hstrict); - t1:=(mkAppL [|get coq_Rplus; - !t1; - mkAppL [|get coq_Rmult; - rational_to_real c; - h.hleft|] |]); - t2:=(mkAppL [|get coq_Rplus; - !t2; - mkAppL [|get coq_Rmult; - rational_to_real c; - h.hright|] |])) - lutil; - let ineq=mkAppL [|if (!s) then get coq_Rlt else get coq_Rle; - !t1; - !t2 |] in - let tc=rational_to_real cres in - (* puis sa preuve *) - let get = eget in - let tac1=ref (if h1.hstrict - then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt)) - [tac_use h1; - tac_zero_inf_pos gl - (rational_to_fraction c1)]) - else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le)) - [tac_use h1; - tac_zero_inf_pos gl - (rational_to_fraction c1)])) in - s:=h1.hstrict; - List.iter (fun (h,c)-> - (if (!s) - then (if h.hstrict - then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]) - else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)])) - else (if h.hstrict - then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]) - else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le)) - [!tac1;tac_use h; - tac_zero_inf_pos gl - (rational_to_fraction c)]))); - s:=(!s)||(h.hstrict)) - lutil; - let tac2= if sres - then tac_zero_inf_false gl (rational_to_fraction cres) - else tac_zero_infeq_false gl (rational_to_fraction cres) - in - tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq)) - [Tacticals.New.tclTHEN (change_concl - (EConstr.of_constr (mkAppL [| cget coq_not; ineq|] - ))) - (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt - else get coq_Rnot_le_le)) - (Tacticals.New.tclTHENS (Equality.replace - (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|] - )) - (EConstr.of_constr tc)) - [tac2; - (Tacticals.New.tclTHENS - (Equality.replace - (EConstr.of_constr (mkApp (cget coq_Rinv, - [|cget coq_R1|]))) - (get coq_R1)) -(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) - - [Tacticals.New.tclORELSE - (* TODO : Ring.polynom []*) (Proofview.tclUNIT ()) - (Proofview.tclUNIT ()); - Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) >>= fun symeq -> - (Tacticals.New.tclTHEN (apply symeq) - (apply (get coq_Rinv_1)))] - - ) - ])); - !tac1]); - tac:=(Tacticals.New.tclTHENS (cut (get coq_False)) - [Tacticals.New.tclTHEN intro (contradiction None); - !tac]) - |_-> assert false) |_-> assert false - ); -(* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *) - !tac -(* ((tclABSTRACT None !tac) gl) *) - end -;; - -(* -let fourier_tac x gl = - fourier gl -;; - -let v_fourier = add_tactic "Fourier" fourier_tac -*) - diff --git a/plugins/fourier/fourier_plugin.mlpack b/plugins/fourier/fourier_plugin.mlpack deleted file mode 100644 index b6262f8a..00000000 --- a/plugins/fourier/fourier_plugin.mlpack +++ /dev/null @@ -1,3 +0,0 @@ -Fourier -FourierR -G_fourier diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 deleted file mode 100644 index 44560ac1..00000000 --- a/plugins/fourier/g_fourier.ml4 +++ /dev/null @@ -1,18 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Ltac_plugin -open FourierR - -DECLARE PLUGIN "fourier_plugin" - -TACTIC EXTEND fourier - [ "fourierz" ] -> [ fourier () ] -END |