From 5a8a7dd777c55a9907699a709760b0616b571919 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 4 Sep 2002 15:34:28 +0000 Subject: [PATCH] Fourier tactic --- helm/gTopLevel/.depend | 3 + helm/gTopLevel/Makefile | 4 +- helm/gTopLevel/fourier.ml | 205 +++++++++++ helm/gTopLevel/fourierR.ml | 605 +++++++++++++++++++++++++++++++++ helm/gTopLevel/fourierR.mli | 2 + helm/gTopLevel/gTopLevel.ml | 10 +- helm/gTopLevel/proofEngine.ml | 1 + helm/gTopLevel/proofEngine.mli | 1 + 8 files changed, 827 insertions(+), 4 deletions(-) create mode 100644 helm/gTopLevel/fourier.ml create mode 100644 helm/gTopLevel/fourierR.ml create mode 100644 helm/gTopLevel/fourierR.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index dea92351a..2a707ead1 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -19,6 +19,9 @@ ring.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ proofEngineTypes.cmx ring.cmi ring.cmi: proofEngineTypes.cmo +fourierR.cmo: fourier.cmo fourierR.cmi +fourierR.cmx: fourier.cmx fourierR.cmi +fourierR.cmi: proofEngineTypes.cmo proofEngine.cmo: primitiveTactics.cmi proofEngineHelpers.cmi \ proofEngineReduction.cmi proofEngineStructuralRules.cmi \ proofEngineTypes.cmo ring.cmi proofEngine.cmi diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 584fc3659..0b3fd06b1 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -17,7 +17,7 @@ opt: gTopLevel.opt DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ proofEngineReduction.ml proofEngineReduction.mli \ proofEngineStructuralRules.ml proofEngineStructuralRules.mli \ - primitiveTactics.ml primitiveTactics.mli ring.ml ring.mli \ + primitiveTactics.ml primitiveTactics.mli ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\ proofEngine.ml proofEngine.mli \ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \ @@ -26,7 +26,7 @@ DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ proofEngineReduction.cmo proofEngineStructuralRules.cmo \ - primitiveTactics.cmo ring.cmo proofEngine.cmo \ + primitiveTactics.cmo ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \ doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \ gTopLevel.cmo diff --git a/helm/gTopLevel/fourier.ml b/helm/gTopLevel/fourier.ml new file mode 100644 index 000000000..bb8b4ea13 --- /dev/null +++ b/helm/gTopLevel/fourier.ml @@ -0,0 +1,205 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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. +*) +let unsolvable lie = + let lr = deduce lie in + let res = ref [] in + (try (List.iter (fun e -> + match e with + {coef=[c];hist=lc;strict=s} -> + if (rinf c r0 && (not s)) || (rinfeq c r0 && s) + then (res := [c,s,lc]; + raise (Failure "contradiction found")) + |_->assert false) + lr) + with _ -> ()); + !res +;; + +(* 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;; + +*) \ No newline at end of file diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml new file mode 100644 index 000000000..7f37602be --- /dev/null +++ b/helm/gTopLevel/fourierR.ml @@ -0,0 +1,605 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + + + +(* 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 Term +open Tactics +open Clenv +open Names +open Tacmach*) +open Fourier + +(****************************************************************************** +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. +*) + +(*type flin = {fhom:(constr , rational)Hashtbl.t; + fcste:rational};; + +let flin_zero () = {fhom=Hashtbl.create 50;fcste=r0};; + +let flin_coef f x = try (Hashtbl.find f.fhom x) with _-> r0;; + +let flin_add f x c = + let cx = flin_coef f x in + Hashtbl.remove f.fhom x; + Hashtbl.add 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 + Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; + Hashtbl.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 + Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom; + Hashtbl.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 + Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom; + flin_add_cste f2 (rmult a f.fcste); +;;*) + +(*****************************************************************************) +(*let parse_ast = Pcoq.parse_string Pcoq.Constr.constr;; +let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);; +let pf_parse_constr gl s = + Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);; + +let rec string_of_constr c = + match kind_of_term c with + Cast (c,t) -> string_of_constr c + |Const c -> string_of_path c + |Var(c) -> string_of_id c + | _ -> "not_of_constant" +;; + +let rec rational_of_constr c = + match kind_of_term c with + | Cast (c,t) -> (rational_of_constr c) + | App (c,args) -> + (match kind_of_term c with + Const c -> + (match (string_of_path c) with + "Coq.Reals.Rdefinitions.Ropp" -> + rop (rational_of_constr args.(0)) + |"Coq.Reals.Rdefinitions.Rinv" -> + rinv (rational_of_constr args.(0)) + |"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)) + |"Coq.Reals.Rdefinitions.Rminus" -> + rminus (rational_of_constr args.(0)) + (rational_of_constr args.(1)) + | _ -> failwith "not a rational") + | _ -> failwith "not a rational") + | Const c -> + (match (string_of_path c) with + "Coq.Reals.Rdefinitions.R1" -> r1 + |"Coq.Reals.Rdefinitions.R0" -> r0 + | _ -> failwith "not a rational") + | _ -> failwith "not a rational" +;; + +let rec flin_of_constr c = + try( + match kind_of_term c with + | Cast (c,t) -> (flin_of_constr c) + | App (c,args) -> + (match kind_of_term c with + Const c -> + (match (string_of_path c) with + "Coq.Reals.Rdefinitions.Ropp" -> + flin_emult (rop r1) (flin_of_constr args.(0)) + |"Coq.Reals.Rdefinitions.Rplus"-> + flin_plus (flin_of_constr args.(0)) + (flin_of_constr args.(1)) + |"Coq.Reals.Rdefinitions.Rminus"-> + flin_minus (flin_of_constr args.(0)) + (flin_of_constr args.(1)) + |"Coq.Reals.Rdefinitions.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 _-> (flin_add (flin_zero()) + args.(1) + a)) + 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) + | Const c -> + (match (string_of_path c) with + "Coq.Reals.Rdefinitions.R1" -> flin_one () + |"Coq.Reals.Rdefinitions.R0" -> flin_zero () + |_-> assert false) + |_-> assert false) + with _ -> flin_add (flin_zero()) + c + r1 +;; + +let flin_to_alist f = + let res=ref [] in + Hashtbl.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 +*) +(*let ineq1_of_constr (h,t) = + match (kind_of_term t) with + App (f,args) -> + let t1= args.(0) in + let t2= args.(1) in + (match kind_of_term f with + Const c -> + (match (string_of_path c) with + "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h; + htype="Rlt"; + hleft=t1; + hright=t2; + hflin= flin_minus (flin_of_constr t1) + (flin_of_constr t2); + hstrict=true}] + |"Coq.Reals.Rdefinitions.Rgt" -> [{hname=h; + htype="Rgt"; + hleft=t2; + hright=t1; + hflin= flin_minus (flin_of_constr t2) + (flin_of_constr t1); + hstrict=true}] + |"Coq.Reals.Rdefinitions.Rle" -> [{hname=h; + htype="Rle"; + hleft=t1; + hright=t2; + hflin= flin_minus (flin_of_constr t1) + (flin_of_constr t2); + hstrict=false}] + |"Coq.Reals.Rdefinitions.Rge" -> [{hname=h; + htype="Rge"; + hleft=t2; + hright=t1; + hflin= flin_minus (flin_of_constr t2) + (flin_of_constr t1); + hstrict=false}] + |_->assert false) + | Ind (sp,i) -> + (match (string_of_path sp) with + "Coq.Init.Logic_Type.eqT" -> let t0= args.(0) in + let t1= args.(1) in + let t2= args.(2) in + (match (kind_of_term t0) with + Const c -> + (match (string_of_path c) with + "Coq.Reals.Rdefinitions.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}] + |_-> assert false) + |_-> assert false) + |_-> assert false) + |_-> assert false) + |_-> assert false +;;*) + +(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) +*) + +(*let fourier_lineq lineq1 = + let nvar=ref (-1) in + let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *) + List.iter (fun f -> + Hashtbl.iter (fun x c -> + try (Hashtbl.find hvar x;()) + with _-> nvar:=(!nvar)+1; + Hashtbl.add hvar x (!nvar)) + f.hflin.fhom) + lineq1; + let sys= List.map (fun h-> + let v=Array.create ((!nvar)+1) r0 in + Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c) + h.hflin.fhom; + ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict)) + lineq1 in + unsolvable sys +;;*) + +(****************************************************************************** +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 rec 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 + let s=ref "" in + if nn=0 + then s:="R0" + else (s:="R1"; + for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;); + if n<0 then s:="(Ropp "^(!s)^")"; + !s +;;*) +(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1))) +*) +(*let rational_to_real x = + let (n,d)=rational_to_fraction x in + ("(Rmult "^(int_to_real n)^" (Rinv "^(int_to_real d)^"))") +;;*) + +(* preuve que 0 False +*) +(*let tac_zero_inf_false gl (n,d) = + let cste = pf_parse_constr gl in + if n=0 then (apply (cste "Rnot_lt0")) + else + (tclTHEN (apply (cste "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 cste = pf_parse_constr gl in + (tclTHEN (apply (cste "Rlt_not_le")) + (tac_zero_inf_pos gl (-n,d))) +;; + +let create_meta () = mkMeta(new_meta());; + +let my_cut c gl= + let concl = pf_concl gl in + apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl +;; +let exact = exact_check;; + +let tac_use h = match h.htype with + "Rlt" -> exact h.hname + |"Rle" -> exact h.hname + |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt")) + (exact h.hname)) + |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le")) + (exact h.hname)) + |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le")) + (exact h.hname)) + |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le")) + (exact h.hname)) + |_->assert false +;; + +let is_ineq (h,t) = + match (kind_of_term t) with + App (f,args) -> + (match (string_of_constr f) with + "Coq.Reals.Rdefinitions.Rlt" -> true + |"Coq.Reals.Rdefinitions.Rgt" -> true + |"Coq.Reals.Rdefinitions.Rle" -> true + |"Coq.Reals.Rdefinitions.Rge" -> true + |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with + "Coq.Reals.Rdefinitions.R"->true + |_->false) + |_->false) + |_->false +;; + +let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; + +let mkAppL a = + let l = Array.to_list a in + mkApp(List.hd l, Array.of_list (List.tl l)) +;;*) + +(* Résolution d'inéquations linéaires dans R *) + +(* +let rec fourier gl= + let parse = pf_parse_constr gl in + let goal = strip_outer_cast (pf_concl gl) 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 (let tac = + match (kind_of_term goal) with + App (f,args) -> + (match (string_of_constr f) with + "Coq.Reals.Rdefinitions.Rlt" -> + (tclTHEN + (tclTHEN (apply (parse "Rfourier_not_ge_lt")) + (intro_using fhyp)) + fourier) + |"Coq.Reals.Rdefinitions.Rle" -> + (tclTHEN + (tclTHEN (apply (parse "Rfourier_not_gt_le")) + (intro_using fhyp)) + fourier) + |"Coq.Reals.Rdefinitions.Rgt" -> + (tclTHEN + (tclTHEN (apply (parse "Rfourier_not_le_gt")) + (intro_using fhyp)) + fourier) + |"Coq.Reals.Rdefinitions.Rge" -> + (tclTHEN + (tclTHEN (apply (parse "Rfourier_not_lt_ge")) + (intro_using fhyp)) + fourier) + |_->assert false) + |_->assert false + in tac gl) + with _ -> +*) + (* les hypothèses *) + +(* + let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t))) + (list_of_sign (pf_hyps gl)) in + let lineq =ref [] in + List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq)) + with _-> ()) + hyps; +*) + + (* lineq = les inéquations découlant des hypothèses *) + + +(* + let res=fourier_lineq (!lineq) in + let tac=ref tclIDTAC in + if res=[] + then (print_string "Tactic Fourier fails.\n"; + flush stdout) + +*) + (* 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 + 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 [|parse "Rmult"; + parse (rational_to_real c1); + h1.hleft|]) in + let t2=ref (mkAppL [|parse "Rmult"; + parse (rational_to_real c1); + h1.hright|]) in + List.iter (fun (h,c) -> + s:=(!s)||(h.hstrict); + t1:=(mkAppL [|parse "Rplus"; + !t1; + mkAppL [|parse "Rmult"; + parse (rational_to_real c); + h.hleft|] |]); + t2:=(mkAppL [|parse "Rplus"; + !t2; + mkAppL [|parse "Rmult"; + parse (rational_to_real c); + h.hright|] |])) + lutil; + let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle"); + !t1; + !t2 |] in + let tc=parse (rational_to_real cres) in +*) + (* puis sa preuve *) +(* + let tac1=ref (if h1.hstrict + then (tclTHENS (apply (parse "Rfourier_lt")) + [tac_use h1; + tac_zero_inf_pos gl + (rational_to_fraction c1)]) + else (tclTHENS (apply (parse "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:=(tclTHENS (apply (parse "Rfourier_lt_lt")) + [!tac1;tac_use h; + tac_zero_inf_pos gl + (rational_to_fraction c)]) + else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le")) + [!tac1;tac_use h; + tac_zero_inf_pos gl + (rational_to_fraction c)])) + else (if h.hstrict + then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt")) + [!tac1;tac_use h; + tac_zero_inf_pos gl + (rational_to_fraction c)]) + else tac1:=(tclTHENS (apply (parse "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:=(tclTHENS (my_cut ineq) + [tclTHEN (change_in_concl + (mkAppL [| parse "not"; ineq|] + )) + (tclTHEN (apply (if sres then parse "Rnot_lt_lt" + else parse "Rnot_le_le")) + (tclTHENS (Equality.replace + (mkAppL [|parse "Rminus";!t2;!t1|] + ) + tc) + [tac2; + (tclTHENS (Equality.replace (parse "(Rinv R1)") + (parse "R1")) +*) +(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *) +(* + [tclORELSE + (Ring.polynom []) + tclIDTAC; + (tclTHEN (apply (parse "sym_eqT")) + (apply (parse "Rinv_R1")))] + + ) + ])); + !tac1]); + tac:=(tclTHENS (cut (parse "False")) + [tclTHEN intro contradiction; + !tac]) + |_-> assert false) |_-> assert false + ); + ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl) + (!tac gl) + ((tclABSTRACT None !tac) gl) + +;; + +let fourier_tac x gl = + fourier gl +;; + +let v_fourier = add_tactic "Fourier" fourier_tac +*) + +(*open CicReduction*) +(*open PrimitiveTactics*) +(*open ProofEngineTypes*) +let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;; + diff --git a/helm/gTopLevel/fourierR.mli b/helm/gTopLevel/fourierR.mli new file mode 100644 index 000000000..68bc34288 --- /dev/null +++ b/helm/gTopLevel/fourierR.mli @@ -0,0 +1,2 @@ +val fourier_tac: ProofEngineTypes.tactic + diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index bf2918593..1a4e6ce65 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -47,9 +47,9 @@ let htmlfooter = "" ;; -let prooffile = "/home/galata/miohelm/currentproof";; +let prooffile = "/home/tassi/miohelm/currentproof";; (*CSC: the getter should handle the innertypes, not the FS *) -let innertypesfile = "/home/galata/miohelm/innertypes";; +let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; (* GLOBAL REFERENCES (USED BY CALLBACKS) *) @@ -682,6 +682,8 @@ let clear rendering_window = call_tactic_with_hypothesis_input ProofEngine.clear rendering_window ;; +let fourier rendering_window = call_tactic ProofEngine.fourier rendering_window;; + let whd_in_scratch scratch_window = call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch @@ -1428,6 +1430,9 @@ class rendering_window output proofw (label : GMisc.label) = let clearb = GButton.button ~label:"Clear" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let fourierb = + GButton.button ~label:"Fourier" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -1481,6 +1486,7 @@ object(self) ignore(ringb#connect#clicked (ring self)) ; ignore(clearbodyb#connect#clicked (clearbody self)) ; ignore(clearb#connect#clicked (clear self)) ; + ignore(fourierb#connect#clicked (fourier self)) ; ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 47af12f4e..69e8062ee 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -317,4 +317,5 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) let elim_type term = apply_tactic (Ring.elim_type_tac ~term) let ring () = apply_tactic Ring.ring_tac +let fourier () = apply_tactic FourierR.fourier_tac diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index 66bb4620e..f9233ea05 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -59,3 +59,4 @@ val clear : Cic.hypothesis -> unit (* other tactics *) val elim_type : Cic.term -> unit val ring : unit -> unit +val fourier : unit -> unit -- 2.39.2