From: Claudio Sacerdoti Coen Date: Wed, 25 Jun 2003 12:26:38 +0000 (+0000) Subject: Removed (it should have already been in ocaml/tactics) X-Git-Tag: camera_ready~53 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=4b0a298d79b4033ebdf0ca6713c6cda34d00fd32 Removed (it should have already been in ocaml/tactics) --- diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml deleted file mode 100644 index a4630ab7a..000000000 --- a/helm/gTopLevel/fourierR.ml +++ /dev/null @@ -1,1263 +0,0 @@ -(* 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/. - *) - - -(******************** 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 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. - -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. -*) - - - -(** - The type for linear combinations -*) -type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational} -;; - -(** - @return an empty flin -*) -let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0} -;; - -(** - @param f a flin - @param x a Cic.term - @return the rational associated with x (coefficient) -*) -let flin_coef f x = - try - (Hashtbl.find f.fhom x) - with - _ -> r0 -;; - -(** - Adds c to the coefficient of x - @param f a flin - @param x a Cic.term - @param c a rational - @return the new flin -*) -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 -;; -(** - Adds c to f.fcste - @param f a flin - @param c a rational - @return the new flin -*) -let flin_add_cste f c = - {fhom=f.fhom; - fcste=rplus f.fcste c} -;; - -(** - @return a empty flin with r1 in fcste -*) -let flin_one () = flin_add_cste (flin_zero()) r1;; - -(** - Adds two flin -*) -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; -;; - -(** - Substracts two flin -*) -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); -;; - -(** - @return f times a -*) -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); -;; - - -(*****************************************************************************) - - -(** - @param t a term - @return proiection on string of t -*) -let rec string_of_term t = - match t with - Cic.Cast (t1,t2) -> string_of_term t1 - |Cic.Const (u,boh) -> UriManager.string_of_uri u - |Cic.Var (u) -> UriManager.string_of_uri u - | _ -> "not_of_constant" -;; - -(* coq wrapper -let string_of_constr = string_of_term -;; -*) - -(** - @param t a term - @raise Failure if conversion is impossible - @return rational proiection of t -*) -let rec rational_of_term t = - (* fun to apply f to the first and second rational-term of l *) - let rat_of_binop f l = - let a = List.hd l and - b = List.hd(List.tl l) in - f (rational_of_term a) (rational_of_term b) - in - (* as before, but f is unary *) - let rat_of_unop f l = - f (rational_of_term (List.hd l)) - in - match t with - | Cic.Cast (t1,t2) -> (rational_of_term t1) - | Cic.Appl (t1::next) -> - (match t1 with - Cic.Const (u,boh) -> - (match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> - rat_of_unop rop next - |"cic:/Coq/Reals/Rdefinitions/Rinv.con" -> - rat_of_unop rinv next - |"cic:/Coq/Reals/Rdefinitions/Rmult.con" -> - rat_of_binop rmult next - |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" -> - rat_of_binop rdiv next - |"cic:/Coq/Reals/Rdefinitions/Rplus.con" -> - rat_of_binop rplus next - |"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.con" -> r1 - |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0 - | _ -> failwith "not a rational") - | _ -> failwith "not a rational" -;; - -(* coq wrapper -let rational_of_const = rational_of_term;; -*) - - -let rec flin_of_term t = - let fl_of_binop f l = - let a = List.hd l and - b = List.hd(List.tl l) in - f (flin_of_term a) (flin_of_term b) - in - try( - match t with - | Cic.Cast (t1,t2) -> (flin_of_term t1) - | Cic.Appl (t1::next) -> - begin - match t1 with - Cic.Const (u,boh) -> - begin - match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/Ropp.con" -> - flin_emult (rop r1) (flin_of_term (List.hd next)) - |"cic:/Coq/Reals/Rdefinitions/Rplus.con"-> - fl_of_binop flin_plus next - |"cic:/Coq/Reals/Rdefinitions/Rminus.con"-> - fl_of_binop flin_minus next - |"cic:/Coq/Reals/Rdefinitions/Rmult.con"-> - begin - let arg1 = (List.hd next) and - arg2 = (List.hd(List.tl next)) - in - try - begin - let a = rational_of_term arg1 in - try - begin - let b = (rational_of_term arg2) in - (flin_add_cste (flin_zero()) (rmult a b)) - end - with - _ -> (flin_add (flin_zero()) arg2 a) - end - with - _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2)) - end - |"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.con"-> - begin - let b=(rational_of_term (List.hd(List.tl next))) in - try - begin - let a = (rational_of_term (List.hd next)) in - (flin_add_cste (flin_zero()) (rdiv a b)) - end - with - _-> (flin_add (flin_zero()) (List.hd next) (rinv b)) - end - |_->assert false - end - |_ -> assert false - end - | Cic.Const (u,boh) -> - begin - match (UriManager.string_of_uri u) with - "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one () - |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero () - |_-> assert false - end - |_-> assert false) - with _ -> flin_add (flin_zero()) t r1 -;; - -(* coq wrapper -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. -*) - -(** - 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: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_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=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) - (flin_of_term arg2); - hstrict=true}] - |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> - [{hname=h; - htype="Rgt"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) - (flin_of_term arg1); - hstrict=true}] - |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> - [{hname=h; - htype="Rle"; - hleft=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) - (flin_of_term arg2); - hstrict=false}] - |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> - [{hname=h; - htype="Rge"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) - (flin_of_term arg1); - hstrict=false}] - |_->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=arg1; - hright=arg2; - hflin= flin_minus (flin_of_term arg1) - (flin_of_term arg2); - hstrict=false}; - {hname=h; - htype="eqTRL"; - hleft=arg2; - hright=arg1; - hflin= flin_minus (flin_of_term arg2) - (flin_of_term arg1); - hstrict=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 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 -> - Hashtbl.iter (fun x c -> - try (Hashtbl.find hvar x;()) - with _-> nvar:=(!nvar)+1; - 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 _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) -;; - -(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1))) -*) - -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 - 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) ~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) ~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 - (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) ~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 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 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 -;; - -let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; - -let mkAppL a = - 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 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 -;; - -(* 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) (*?? ??*) - -;; - -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) -;; - -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:=(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=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);; - -