X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FfourierR.ml;h=a4630ab7aca1e47db84676838ceaead5d6ffb742;hb=caab26f85122e0040555139c48a9111a0b2b9fff;hp=c11947a0e8f595c33cb0e5f30f9c575009225418;hpb=1357d4a7e43e986c2f2f9fe4a569f11230c6771e;p=helm.git diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index c11947a0e..a4630ab7a 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -24,18 +24,112 @@ *) +(******************** OTHER USEFUL TACTICS **********************) + +let rewrite_tac ~term:equality ~status:(proof,goal) = + let module C = Cic in + let module U = UriManager in + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + + prerr_endline("rewrite chiamata con "^CicPp.ppterm gty^"\n"); + let eq_ind_r,ty,t1,t2 = + match CicTypeChecker.type_of_aux' metasenv context equality with + C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") -> + let eq_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0) + in + eq_ind_r,ty,t1,t2 + | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2] + when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") -> + let eqT_ind_r = + C.Const + (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0) + in + eqT_ind_r,ty,t1,t2 + | _ -> + raise + (ProofEngineTypes.Fail + "Rewrite: the argument is not a proof of an equality") + in + let pred = + let gty' = CicSubstitution.lift 1 gty in + let t1' = CicSubstitution.lift 1 t1 in + let gty'' = + ProofEngineReduction.replace_lifting + ~equality: + (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true) + ~what:t1' ~with_what:(C.Rel 1) ~where:gty' + in + C.Lambda (C.Name "dummy_for_rewrite", ty, gty'') + in +prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in + + let (proof',goals) = + PrimitiveTactics.exact_tac + ~term:(C.Appl + [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]) + ~status:((curi,metasenv',pbo,pty),goal) + in + assert (List.length goals = 0) ; + (proof',[fresh_meta]) +;; + +(* ti ho beccato !!!!!!!!!! qui' salta fuori un or. perche'?*) + + + +let simpl_tac ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + +prerr_endline("simpl_tac su "^CicPp.ppterm ty); + + let new_ty = ProofEngineReduction.simpl context ty in + +prerr_endline("ritorna "^CicPp.ppterm new_ty); + + let new_metasenv = + List.map + (function + (n,_,_) when n = metano -> (metano,context,new_ty) + | _ as t -> t + ) metasenv + in + (curi,new_metasenv,pbo,pty), [metano] + +;; + +let rewrite_simpl_tac ~term ~status = + + Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status + +;; + +(******************** THE FOURIER TACTIC ***********************) (* 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 // in coq/kernel -open Tactics -open Clenv -open Names -open Tacmach*) open Fourier + +let debug x = print_string ("____ "^x) ; flush stdout;; + +let debug_pcontext x = + let str = ref "" in + List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^ + a ^ " " | _ ->()) x ; + debug ("contesto : "^ (!str) ^ "\n") +;; + (****************************************************************************** Operations on linear combinations. @@ -132,16 +226,6 @@ let flin_emult a f = (*****************************************************************************) -(* - - no idea about helm parser ?????????????????????????????? - -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);; -*) - (** @param t a term @@ -182,24 +266,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 +308,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)) @@ -247,12 +331,12 @@ let rec flin_of_term t = _ -> (flin_add (flin_zero()) arg2 a) end with - _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 )) + _-> (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 +354,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 +366,134 @@ 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) = + debug("Trasformo in ineq "^CicPp.ppterm t^"\n"); + match t with (* match t *) + Cic.Appl (t1::next) -> + let arg1= List.hd next in + let arg2= List.hd(List.tl next) in + (match t1 with (* match t1 *) + Cic.Const (u,boh) -> + (match UriManager.string_of_uri u with (* match u *) + "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"-> + |_->assert false)(* match u *) + | Cic.MutInd (u,i,o) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Init/Logic_Type/eqT.ind" -> + debug("Ho trovato una ==\n"); + 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 -;;*) + |_-> debug("eqT deve essere applicato a const R\n");assert false) + |_-> debug("eqT deve essere appl a const\n");assert false) + |_-> debug("Il trmine e' un appl mutind ma non eqT\n");assert false) + |_-> debug("Il termine non e' una app di const o app di mutind\n");assert false)(* match t1 *) + |_-> debug("Il termine non e' una applicazione\n");assert false (* match t *) +;; +(* 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 rec print_rl l = + match l with + []-> () + | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next +;; + +let rec print_sys l = + match l with + [] -> () + | (a,b)::next -> (print_rl a; + print_string (if b=true then "strict\n"else"\n"); + print_sys next) + ;; + +(*let print_hash h = + Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h +;;*) + +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 -> @@ -382,125 +503,356 @@ type hineq={hname:constr; (* le nom de l'hypoth Hashtbl.add hvar x (!nvar)) f.hflin.fhom) lineq1; + (*print_hash hvar;*) + debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n"); 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 + debug ("chiamo unsolvable sul sistema di "^ + string_of_int (List.length sys) ^"\n"); + print_sys sys; 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 _eqT = Cic.MutInd(UriManager.uri_of_string + "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;; +let _False = Cic.MutInd (UriManager.uri_of_string + "cic:/Coq/Init/Logic/False.ind") 0 0 ;; +let _not = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Init/Logic/not.con") 0;; +let _R0 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;; +let _R1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;; +let _R = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;; +let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;; +let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;; +let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;; +let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;; +let _Rfourier_le=Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;; +let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;; +let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;; +let _Rfourier_lt=Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;; +let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;; +let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;; +let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;; +let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;; +let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;; +let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;; +let _Rinv = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;; +let _Rinv_R1 = Cic.Const(UriManager.uri_of_string + "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;; +let _Rle = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;; +let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;; +let _Rle_not_lt = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;; +let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;; +let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;; +let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;; +let _Rlt = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;; +let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;; +let _Rlt_not_le = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;; +let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;; +let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;; +let _Rminus = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;; +let _Rmult = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;; +let _Rnot_le_le =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;; +let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;; +let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;; +let _Ropp = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;; +let _Rplus = Cic.Const (UriManager.uri_of_string + "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;; +let _sym_eqT = Cic.Const(UriManager.uri_of_string + "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;; + +(******************************************************************************) + +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 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 -;;*) + +let rec int_to_real_aux n = + match n with + 0 -> _R0 (* o forse R0 + R0 ????? *) + | 1 -> _R1 + | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ] +;; + + +let int_to_real n = + let x = int_to_real_aux (abs n) in + if n < 0 then + Cic.Appl [ _Ropp ; x ] + else + x +;; + + (* -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)^"))") -;;*) + +let rational_to_real x = + let (n,d)=rational_to_fraction x in + Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ] +;; (* preuve que 0 m=goal) metasenv in + debug ("th = "^ CicPp.ppterm t ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + in + let tacn=ref + (fun ~status -> pall "n0" ~status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + let tacd=ref + (fun ~status -> pall "d0" ~status _Rlt_zero_1 ; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in + + + for i=1 to n-1 do + tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) + ~status _Rlt_zero_pos_plus1; + PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) + ~continuation:!tacn); + done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" + ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); + done; + + + +debug("TAC ZERO INF POS\n"); + +(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) + ~continuations:[ + !tacn ; + !tacd ] + ~status) +;; + + (* preuve que 0<=n*1/d *) -(*let tac_zero_infeq_pos gl (n,d)= - let cste = pf_parse_constr gl in - let tacn=ref (if n=0 - then (apply (cste "Rle_zero_zero")) - else (apply (cste "Rle_zero_1"))) in - let tacd=ref (apply (cste "Rlt_zero_1")) in - for i=1 to n-1 do - tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done; - for i=1 to d-1 do - tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done; - (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd]) -;;*) - + +let tac_zero_infeq_pos gl (n,d) ~status = + (*let cste = pf_parse_constr gl in*) + debug("inizio tac_zero_infeq_pos\n"); + let tacn = ref + (if n=0 then + (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) + else + (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ) + ) + in + let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in + for i=1 to n-1 do + tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); + done; + for i=1 to d-1 do + tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); + done; + let r = + (Tacticals.thens ~start:(PrimitiveTactics.apply_tac + ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in + debug("fine tac_zero_infeq_pos\n"); + r +;; + + + (* preuve que 0<(-n)*(1/d) => False *) -(*let tac_zero_inf_false gl (n,d) = - let cste = pf_parse_constr gl in - if n=0 then (apply (cste "Rnot_lt0")) + +let tac_zero_inf_false gl (n,d) ~status= + debug("inizio tac_zero_inf_false\n"); + if n=0 then + (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in + debug("fine\n"); + r) else - (tclTHEN (apply (cste "Rle_not_lt")) - (tac_zero_infeq_pos gl (-n,d))) -;;*) + (debug "2\n";let r = (Tacticals.then_ ~start:( + fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + debug("!!!!!!!!1:unify "^CicPp.ppterm _Rle_not_lt^" with " + ^ CicPp.ppterm ty ^" fails\n"); + let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in + debug("!!!!!!!!!2\n"); + r + ) + ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in + debug("fine\n"); + r + ) +;; (* 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 tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)= +debug("stat tac_zero_infeq_false\n"); +(*let r = + ( + let curi,metasenv,pbo,pty = proof in + let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in + + debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); + Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) + ~continuation:(tac_zero_inf_pos (-n,d))) ~status in + debug("end tac_zero_infeq_false\n"); + r*) + Ring.id_tac ~status +;; + + +(* *********** ********** ******** ??????????????? *********** **************) + +let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,t)::metasenv in + let proof' = curi,metasenv',pbo,pty in + let proof'',goals = + PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta + (fresh_meta,irl),t))::al)) ~status:(proof',goal) + in + proof'',fresh_meta::goals ;; -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 my_cut ~term:c ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,c)::metasenv in + let proof' = curi,metasenv',pbo,pty in + let proof'',goals = + apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c, + CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] + ~status:(proof',goal) + in + (* We permute the generated goals to be consistent with Coq *) + match goals with + [] -> assert false + | he::tl -> proof'',he::fresh_meta::tl ;; + +let exact = PrimitiveTactics.exact_tac;; + +let tac_use h ~status:(proof,goal as status) = +debug("Inizio TC_USE\n"); +let curi,metasenv,pbo,pty = proof in +let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in +debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); +debug ("ty = "^ CicPp.ppterm ty^"\n"); + +let res = +match h.htype with + "Rlt" -> exact ~term:h.hname ~status + |"Rle" -> exact ~term:h.hname ~status + |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_gt_to_lt) + ~continuation:(exact ~term:h.hname)) ~status + |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_ge_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_eqLR_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_eqRL_to_le) + ~continuation:(exact ~term:h.hname)) ~status + |_->assert false +in +debug("Fine TAC_USE\n"); +res +;; + + + 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) + match t with + Cic.Appl ( Cic.Const(u,boh)::next) -> + (match (UriManager.string_of_uri u) with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true + |"cic:/Coq/Init/Logic_Type/eqT.con" -> + (match (List.hd next) with + Cic.Const (uri,_) when + UriManager.string_of_uri uri = + "cic:/Coq/Reals/Rdefinitions/R.con" -> true + | _ -> false) |_->false) |_->false ;; @@ -508,204 +860,404 @@ let is_ineq (h,t) = 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)) -;;*) + Cic.Appl(Array.to_list a) +;; (* Résolution d'inéquations linéaires dans R *) +let rec strip_outer_cast c = match c with + | Cic.Cast (c,_) -> strip_outer_cast c + | _ -> c +;; -(* -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 find_in_context id context = + let rec find_in_context_aux c n = + match c with + [] -> failwith (id^" not found in context") + | a::next -> (match a with + Some (Cic.Name(name),_) when name = id -> n + (*? magari al posto di _ qualcosaltro?*) + | _ -> find_in_context_aux next (n+1)) + in + find_in_context_aux context 1 +;; +(* mi sembra quadratico *) +let rec filter_real_hyp context cont = + match context with + [] -> [] + | Some(Cic.Name(h),Cic.Decl(t))::next -> ( + let n = find_in_context h cont in + [(Cic.Rel(n),t)] @ filter_real_hyp next cont) + | a::next -> debug(" no\n"); filter_real_hyp next cont +;; -(* - let res=fourier_lineq (!lineq) in - let tac=ref tclIDTAC in - if res=[] - then (print_string "Tactic Fourier fails.\n"; - flush stdout) +(* lifts everithing at the conclusion level *) +let rec superlift c n= + match c with + [] -> [] + | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl( + CicSubstitution.lift n a))] @ superlift next (n+1) + | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def( + CicSubstitution.lift n a))] @ superlift next (n+1) + | _::next -> superlift next (n+1) (*?? ??*) + +;; -*) - (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) +let equality_replace a b ~status = +debug("inizio EQ\n"); + let module C = Cic in + let proof,goal = status in + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in + let fresh_meta = ProofEngineHelpers.new_meta proof in + let irl = + ProofEngineHelpers.identity_relocation_list_for_metavariable context in + let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in +debug("chamo rewrite tac su "^CicPp.ppterm (C.Meta (fresh_meta,irl))^" e ty "^CicPp.ppterm ty ^"\n"); + let (proof,goals) = + rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) + ~status:((curi,metasenv',pbo,pty),goal) + in + let new_goals = fresh_meta::goals in +debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = " + ^string_of_int( List.length goals)^"+ meta\n"); + (proof,new_goals) +;; -(* - 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) -> +let tcl_fail a ~status:(proof,goal) = + match a with + 1 -> raise (ProofEngineTypes.Fail "fail-tactical") + |_-> (proof,[goal]) +;; + + +let assumption_tac ~status:(proof,goal)= + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let num = ref 0 in + let tac_list = List.map + ( fun x -> num := !num + 1; + match x with + Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num))) + | _ -> ("fake",tcl_fail 1) + ) + context + in + Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal) +;; + +(* !!!!! fix !!!!!!!!!! *) +let contradiction_tac ~status:(proof,goal)= + Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) + ~continuation:(Tacticals.then_ + ~start:(Ring.elim_type_tac ~term:_False) + ~continuation:(assumption_tac)) + ~status:(proof,goal) +;; + +(* ********************* TATTICA ******************************** *) + +let rec fourier ~status:(s_proof,s_goal)= + let s_curi,s_metasenv,s_pbo,s_pty = s_proof in + let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) + s_metasenv in + + debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n"); + debug_pcontext s_context; + + let fhyp = String.copy "new_hyp_for_fourier" in + +(* here we need to negate the thesis, but to do this we need to apply the right +theoreme,so let's parse our thesis *) + + let th_to_appl = ref _Rfourier_not_le_gt in + (match s_ty with + Cic.Appl ( Cic.Const(u,boh)::args) -> + (match UriManager.string_of_uri u with + "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := + _Rfourier_not_ge_lt + |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := + _Rfourier_not_gt_le + |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := + _Rfourier_not_le_gt + |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := + _Rfourier_not_lt_ge + |_-> failwith "fourier can't be applyed") + |_-> failwith "fourier can't be applyed"); + (* fix maybe strip_outer_cast goes here?? *) + + (* now let's change our thesis applying the th and put it with hp *) + + let proof,gl = Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) + ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp) + ~status:(s_proof,s_goal) in + let goal = if List.length gl = 1 then List.hd gl + else failwith "a new goal" in + + debug ("port la tesi sopra e la nego. contesto :\n"); + debug_pcontext s_context; + + (* now we have all the right environment *) + + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + + + (* now we want to convert hp to inequations, but first we must lift + everyting to thesis level, so that a variable has the save Rel(n) + in each hp ( needed by ineq1_of_term ) *) + + (* ? fix if None ?????*) + (* fix change superlift with a real name *) + + let l_context = superlift context 1 in + let hyps = filter_real_hyp l_context l_context in + + debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n"); + + let lineq =ref [] in + + (* transform hyps into inequations *) + + List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq)) + with _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");) + hyps; + + + debug ("applico fourier a "^ string_of_int (List.length !lineq)^ + " disequazioni\n"); + + let res=fourier_lineq (!lineq) in + let tac=ref Ring.id_tac in + if res=[] then + (print_string "Tactic Fourier fails.\n";flush stdout; + failwith "fourier can't proove it") + else + ( + match res with (*match res*) + [(cres,sres,lc)]-> + + (* in lc we have the coefficient to "reduce" the system *) + + print_string "Fourier's method can prove the goal...\n";flush stdout; + + debug "I coeff di moltiplicazione rit sono: "; + + let lutil=ref [] in + List.iter + (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil); + (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *)) + ) + (List.combine (!lineq) lc); + + print_string (" quindi lutil e' lunga "^ + string_of_int (List.length (!lutil))^"\n"); + + (* on construit la combinaison linéaire des inéquation *) + + (match (!lutil) with (*match (!lutil) *) + (h1,c1)::lutil -> + debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n"; + + let s=ref (h1.hstrict) in + + + let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in + let t2 = ref (Cic.Appl [_Rmult;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|] |])) + t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl + [_Rmult;rational_to_real c;h.hleft ] ]); + t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl + [_Rmult;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 + + let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in + let tc=rational_to_real cres in + + +(* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *) + + debug "inizio a costruire tac1\n"; + Fourier.print_rational(c1); + + let tac1=ref ( fun ~status -> + if h1.hstrict then + (Tacticals.thens + ~start:( + fun ~status -> + debug ("inizio t1 strict\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find + (function (m,_,_) -> m=goal) metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status) + ~continuations:[tac_use h1;tac_zero_inf_pos + (rational_to_fraction c1)] + ~status + ) + else + (Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le) + ~continuations:[tac_use h1;tac_zero_inf_pos + (rational_to_fraction c1)] ~status + ) + ) + + in + s:=h1.hstrict; + List.iter (fun (h,c) -> + (if (!s) then + (if h.hstrict then + (debug("tac1 1\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac + ~term:_Rfourier_lt_lt) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + else + (debug("tac1 2\n"); + Fourier.print_rational(c1); + tac1:=(Tacticals.thens + ~start:( + fun ~status -> + debug("INIZIO TAC 1 2\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) + metasenv in + debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); + debug ("ty = "^ CicPp.ppterm ty^"\n"); + PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + ) + else + (if h.hstrict then + (debug("tac1 3\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + else + (debug("tac1 4\n"); + tac1:=(Tacticals.thens + ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le) + ~continuations:[!tac1;tac_use h;tac_zero_inf_pos + (rational_to_fraction c)]) + ) + ) + ); + s:=(!s)||(h.hstrict)) lutil;(*end List.iter*) + + let tac2 = + if sres then + tac_zero_inf_false goal (rational_to_fraction cres) + else + tac_zero_infeq_false goal (rational_to_fraction cres) + in + tac:=(Tacticals.thens + ~start:(my_cut ~term:ineq) + ~continuations:[Tacticals.then_ + ~start:(fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) + metasenv in + + debug("Change_tac "^CicPp.ppterm ty^" with "^CicPp.ppterm (Cic.Appl [ _not; ineq]) ^"\n"); + + PrimitiveTactics.change_tac ~what:ty + ~with_what:(Cic.Appl [ _not; ineq]) ~status) + ~continuation:(Tacticals.then_ + ~start:(PrimitiveTactics.apply_tac ~term: + (if sres then _Rnot_lt_lt else _Rnot_le_le)) + ~continuation:(Tacticals.thens + ~start:( + fun ~status -> + let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc + ~status + in + (match r with (p,gl) -> + debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations:[(Tacticals.thens + ~start:( + fun ~status:(proof,goals as status) -> + + let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in + (match r with (p,gl) -> + debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" )); + r) + ~continuations: + [PrimitiveTactics.apply_tac ~term:_Rinv_R1 +(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno + di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i + parametri della equality_replace vengono passati al contrario? Oppure la + tattica usa i parametri al contrario? + ~continuations:[Tacticals.then_ + ~start:( + fun ~status:(proof,goal as status) -> + debug("ECCOCI\n"); + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m= + goal) metasenv in + debug("ty = "^CicPp.ppterm ty^"\n"); + let r = PrimitiveTactics.apply_tac ~term:_sym_eqT + ~status in + debug("fine ECCOCI\n"); + r) + ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1) *) + ;Tacticals.try_tactics + ~tactics:[ "ring", (fun ~status -> + debug("begin RING\n"); + let r = Ring.ring_tac ~status in + debug ("end RING\n"); + r) + ; "id", Ring.id_tac] + ]) + ;Tacticals.then_ + ~start: + ( + fun ~status:(proof,goal as status) -> + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m= + goal) metasenv in + (* check if ty is of type *) + let w1 = + debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n"); + (match ty with + (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*) + Cic.Prod (Cic.Anonimous,a,b) -> (Cic.Appl [_not;a]) + |_ -> assert false) + in + let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in + debug("fine MY_CHNGE\n"); + r + ) + ~continuation:Ring.id_tac(*tac2*)])) + ;Ring.id_tac(*!tac1*)]);(*end tac:=*) + tac:=(Tacticals.thens + ~start:(PrimitiveTactics.cut_tac ~term:_False) + ~continuations:[Tacticals.then_ + ~start:(PrimitiveTactics.intros_tac ~name:"??") + ~continuation:contradiction_tac + ;!tac]) + + + |_-> assert false)(*match (!lutil) *) + |_-> assert false); (*match res*) + debug ("finalmente applico tac\n"); + (!tac ~status:(proof,goal)) +;; + +let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);; -(*open CicReduction*) -(*open PrimitiveTactics*) -(*open ProofEngineTypes*) -let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;