From: Enrico Tassi Date: Mon, 9 Sep 2002 09:39:51 +0000 (+0000) Subject: Fourier tactic update X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~83 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1c055e64e5a1a37112622548e54326c658552de6;p=helm.git Fourier tactic update --- diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index c11947a0e..1942e1821 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -182,24 +182,24 @@ let rec rational_of_term t = (match t1 with Cic.Const (u,boh) -> (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Ropp" -> + "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> rat_of_unop rop next - |"cic:/Coq/Reals/Rdefinitions/Rinv" -> + |"cic:/Coq/Reals/Rdefinitions/Rinv.con" -> rat_of_unop rinv next - |"cic:/Coq/Reals/Rdefinitions/Rmult" -> + |"cic:/Coq/Reals/Rdefinitions/Rmult.con" -> rat_of_binop rmult next - |"cic:/Coq/Reals/Rdefinitions/Rdiv" -> + |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" -> rat_of_binop rdiv next - |"cic:/Coq/Reals/Rdefinitions/Rplus" -> + |"cic:/Coq/Reals/Rdefinitions/Rplus.con" -> rat_of_binop rplus next - |"cic:/Coq/Reals/Rdefinitions/Rminus" -> + |"cic:/Coq/Reals/Rdefinitions/Rminus.con" -> rat_of_binop rminus next | _ -> failwith "not a rational") | _ -> failwith "not a rational") | Cic.Const (u,boh) -> (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/R1" -> r1 - |"cic:/Coq/Reals/Rdefinitions/R0" -> r0 + "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1 + |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0 | _ -> failwith "not a rational") | _ -> failwith "not a rational" ;; @@ -224,13 +224,13 @@ let rec flin_of_term t = Cic.Const (u,boh) -> begin match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Ropp" -> + "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> flin_emult (rop r1) (flin_of_term (List.hd next)) - |"cic:/Coq/Reals/Rdefinitions/Rplus"-> + |"cic:/Coq/Reals/Rdefinitions/Rplus.con"-> fl_of_binop flin_plus next - |"cic:/Coq/Reals/Rdefinitions/Rminus"-> + |"cic:/Coq/Reals/Rdefinitions/Rminus.con"-> fl_of_binop flin_minus next - |"cic:/Coq/Reals/Rdefinitions/Rmult"-> + |"cic:/Coq/Reals/Rdefinitions/Rmult.con"-> begin let arg1 = (List.hd next) and arg2 = (List.hd(List.tl next)) @@ -249,10 +249,10 @@ let rec flin_of_term t = with _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 )) end - |"cic:/Coq/Reals/Rdefinitions/Rinv"-> + |"cic:/Coq/Reals/Rdefinitions/Rinv.con"-> let a=(rational_of_term (List.hd next)) in flin_add_cste (flin_zero()) (rinv a) - |"cic:/Coq/Reals/Rdefinitions/Rdiv"-> + |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"-> begin let b=(rational_of_term (List.hd(List.tl next))) in try @@ -270,8 +270,8 @@ let rec flin_of_term t = | Cic.Const (u,boh) -> begin match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/R1" -> flin_one () - |"cic:/Coq/Reals/Rdefinitions/R0" -> flin_zero () + "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one () + |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero () |_-> assert false end |_-> assert false) @@ -282,97 +282,109 @@ let rec flin_of_term t = let flin_of_constr = flin_of_term;; *) -(* +(** + Translates a flin to (c,x) list + @param f a flin + @return something like (c1,x1)::(c2,x2)::...::(cn,xn) +*) 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 *) + +(** + The structure for ineq +*) +type hineq={hname:Cic.term; (* le nom de l'hypothèse *) htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *) - hleft:constr; - hright:constr; + hleft:Cic.term; + hright:Cic.term; 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; + +let ineq1_of_term (h,t) = + match t with + Cic.Appl (t1::next) -> + let arg1= List.hd next in + let arg2= List.hd(List.tl next) in + (match t1 with + Cic.Const (u,boh) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h; htype="Rlt"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); hstrict=true}] - |"Coq.Reals.Rdefinitions.Rgt" -> [{hname=h; + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h; htype="Rgt"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); hstrict=true}] - |"Coq.Reals.Rdefinitions.Rle" -> [{hname=h; + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h; htype="Rle"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); hstrict=false}] - |"Coq.Reals.Rdefinitions.Rge" -> [{hname=h; + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h; htype="Rge"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); 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"-> + | Cic.MutInd (u,i,o) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Init/Logic_Type/eqT.con" -> + let t0= arg1 in + let arg1= arg2 in + let arg2= List.hd(List.tl (List.tl next)) in + (match t0 with + Cic.Const (u,boh) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Reals/Rdefinitions/R.con"-> [{hname=h; htype="eqTLR"; - hleft=t1; - hright=t2; - hflin= flin_minus (flin_of_constr t1) - (flin_of_constr t2); + hleft=arg1; + hright=arg2; + hflin= flin_minus (flin_of_term arg1) + (flin_of_term arg2); hstrict=false}; {hname=h; htype="eqTRL"; - hleft=t2; - hright=t1; - hflin= flin_minus (flin_of_constr t2) - (flin_of_constr t1); + hleft=arg2; + hright=arg1; + hflin= flin_minus (flin_of_term arg2) + (flin_of_term arg1); hstrict=false}] |_-> assert false) |_-> assert false) |_-> assert false) |_-> assert false) |_-> assert false -;;*) +;; +(* coq wrapper +let ineq1_of_constr = ineq1_of_term;; +*) (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq) *) -(*let fourier_lineq lineq1 = +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 -> @@ -389,23 +401,23 @@ type hineq={hname:constr; (* le nom de l'hypoth ((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 -;;*) +let is_int x = (x.den)=1 +;; (* fraction = couple (num,den) *) -(*let rec rational_to_fraction x= (x.num,x.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 int_to_real n = let nn=abs n in let s=ref "" in if nn=0 @@ -414,13 +426,14 @@ i.e. on obtient une contradiction. 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 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