(* 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/. *) (******************** 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 open ProofEngineTypes 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 = match x with Cic.Rel(n) ->( let cx = flin_coef f x in Hashtbl.remove f.fhom x; Hashtbl.add f.fhom x (rplus cx c); f) |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n"); 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 a times f *) 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 @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) -> if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then rat_of_unop rop next else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then rat_of_unop rinv next else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then rat_of_binop rmult next else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then rat_of_binop rdiv next else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then rat_of_binop rplus next else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then rat_of_binop rminus next else failwith "not a rational" | _ -> failwith "not a rational") | Cic.Const (u,boh) -> if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then r1 else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then r0 else failwith "not a rational" | _ -> failwith "not a rational" ;; (* coq wrapper let rational_of_const = rational_of_term;; *) let fails f a = try let tmp = (f a) in false with _-> true ;; 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 if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then flin_emult (rop r1) (flin_of_term (List.hd next)) else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then fl_of_binop flin_plus next else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then fl_of_binop flin_minus next else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then begin let arg1 = (List.hd next) and arg2 = (List.hd(List.tl next)) in if fails rational_of_term arg1 then if fails rational_of_term arg2 then ( (* prodotto tra 2 incognite ????? impossibile*) failwith "Sistemi lineari!!!!\n" ) else ( match arg1 with Cic.Rel(n) -> (*trasformo al volo*) (flin_add (flin_zero()) arg1 (rational_of_term arg2)) |_-> (* test this *) let tmp = flin_of_term arg1 in flin_emult (rational_of_term arg2) (tmp) ) else if fails rational_of_term arg2 then ( match arg2 with Cic.Rel(n) -> (*trasformo al volo*) (flin_add (flin_zero()) arg2 (rational_of_term arg1)) |_-> (* test this *) let tmp = flin_of_term arg2 in flin_emult (rational_of_term arg1) (tmp) ) else ( (*prodotto tra razionali*) (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2))) ) (*try begin (*let a = rational_of_term arg1 in debug("ho fatto rational of term di "^CicPp.ppterm arg1^ " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*) let a = flin_of_term arg1 try begin let b = (rational_of_term arg2) in debug("ho fatto rational of term di "^CicPp.ppterm arg2^ " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n"); (flin_add_cste (flin_zero()) (rmult a b)) end with _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n"); (flin_add (flin_zero()) arg2 a) end with _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n"); (flin_add(flin_zero()) arg1 (rational_of_term arg2)) *) end else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then let a=(rational_of_term (List.hd next)) in flin_add_cste (flin_zero()) (rinv a) else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then 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 else assert false end |_ -> assert false end | Cic.Const (u,boh) -> begin if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then flin_one () else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then flin_zero () else assert false end |_-> assert false) with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");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) = 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) -> if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then [{hname=h; htype="Rlt"; hleft=arg1; hright=arg2; hflin= flin_minus (flin_of_term arg1) (flin_of_term arg2); hstrict=true}] else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then [{hname=h; htype="Rgt"; hleft=arg2; hright=arg1; hflin= flin_minus (flin_of_term arg2) (flin_of_term arg1); hstrict=true}] else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then [{hname=h; htype="Rle"; hleft=arg1; hright=arg2; hflin= flin_minus (flin_of_term arg1) (flin_of_term arg2); hstrict=false}] else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then [{hname=h; htype="Rge"; hleft=arg2; hright=arg1; hflin= flin_minus (flin_of_term arg2) (flin_of_term arg1); hstrict=false}] else assert false | Cic.MutInd (u,i,o) -> if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then 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) -> if UriManager.eq u HelmLibraryObjects.Reals.r_URI then [{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}] else assert false |_-> assert false) else assert false |_-> assert false)(* match t1 *) |_-> 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); debug("aggiungo una var "^ string_of_int !nvar^" per "^ CicPp.ppterm x^"\n")) 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(HelmLibraryObjects.Logic.eq_URI, 0, []) ;; let _False = Cic.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []) ;; let _not = Cic.Const (HelmLibraryObjects.Logic.not_URI,[]);; let _R0 = Cic.Const (HelmLibraryObjects.Reals.r0_URI,[]);; let _R1 = Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);; let _R = Cic.Const (HelmLibraryObjects.Reals.r_URI,[]);; let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;; let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;; let _Rfourier_ge_to_le =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;; let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;; let _Rfourier_le=Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;; let _Rfourier_le_le =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con"), []) ;; let _Rfourier_le_lt =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con"), []) ;; let _Rfourier_lt=Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con"), []) ;; let _Rfourier_lt_le =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con"), []) ;; let _Rfourier_lt_lt =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con"), []) ;; let _Rfourier_not_ge_lt = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con"), []) ;; let _Rfourier_not_gt_le = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con"), []) ;; let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;; let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;; let _Rinv = Cic.Const (HelmLibraryObjects.Reals.rinv_URI, []);; let _Rinv_R1 = Cic.Const(HelmLibraryObjects.Reals.rinv_r1_URI, []);; let _Rle = Cic.Const (HelmLibraryObjects.Reals.rle_URI, []);; let _Rle_mult_inv_pos = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;; let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con"), []) ;; let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;; let _Rle_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;; let _Rlt = Cic.Const (HelmLibraryObjects.Reals.rlt_URI, []);; let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;; let _Rlt_not_le = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con"), []) ;; let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;; let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;; let _Rminus = Cic.Const (HelmLibraryObjects.Reals.rminus_URI, []);; let _Rmult = Cic.Const (HelmLibraryObjects.Reals.rmult_URI, []);; let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;; let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;; let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;; let _Ropp = Cic.Const (HelmLibraryObjects.Reals.ropp_URI, []);; let _Rplus = Cic.Const (HelmLibraryObjects.Reals.rplus_URI, []);; (******************************************************************************) 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 pall "n0" status _Rlt_zero_1 ; apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in let tacd=ref (mk_tactic (fun status -> pall "d0" status _Rlt_zero_1 ; apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in for i=1 to n-1 do tacn:=(Tacticals.then_ ~start:(mk_tactic (fun status -> pall ("n"^string_of_int i) status _Rlt_zero_pos_plus1; apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) status)) ~continuation:!tacn); done; for i=1 to d-1 do tacd:=(Tacticals.then_ ~start:(mk_tactic (fun status -> pall "d" status _Rlt_zero_pos_plus1 ; apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) status)) ~continuation:!tacd); done; debug("TAC ZERO INF POS\n"); apply_tactic (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn ;!tacd ] ) status in mk_tactic (tac_zero_inf_pos (n,d)) ;; (* preuve que 0<=n*1/d *) let tac_zero_infeq_pos gl (n,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; apply_tactic (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) status in mk_tactic (tac_zero_infeq_pos gl (n,d)) ;; (* preuve que 0<(-n)*(1/d) => False *) let tac_zero_inf_false gl (n,d) = let tac_zero_inf_false gl (n,d) status = if n=0 then apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status else apply_tactic (Tacticals.then_ ~start:( mk_tactic (fun status -> let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status)) ~continuation:(tac_zero_infeq_pos gl (-n,d))) status in mk_tactic (tac_zero_inf_false gl (n,d)) ;; (* preuve que 0<=n*(1/d) => False ; n est negatif *) let tac_zero_infeq_false gl (n,d) = let tac_zero_infeq_false gl (n,d) status = let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug("faccio fold di " ^ CicPp.ppterm (Cic.Appl [_Rle ; _R0 ; Cic.Appl [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]] ] ) ^ "\n") ; debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n"); (*CSC: Patch to undo the over-simplification of RewriteSimpl *) apply_tactic (Tacticals.then_ ~start: (ReductionTactics.fold_tac ~reduction:CicReduction.whd ~pattern:(ProofEngineTypes.conclusion_pattern None) ~term: (Cic.Appl [_Rle ; _R0 ; Cic.Appl [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])) ~continuation: (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le) ~continuation:(tac_zero_inf_pos (-n,d)))) status in mk_tactic (tac_zero_infeq_false gl (n,d)) ;; (* *********** ********** ******** ??????????????? *********** **************) let apply_type_tac ~cast:t ~applist:al = let apply_type_tac ~cast:t ~applist:al (proof,goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.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 = apply_tactic (PrimitiveTactics.apply_tac (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) *) ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al))) (* ??? *) (proof',goal) in proof'',fresh_meta::goals in mk_tactic (apply_type_tac ~cast:t ~applist:al) ;; let my_cut ~term:c = let my_cut ~term:c (proof,goal) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.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_tactic (apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]) (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 in mk_tactic (my_cut ~term:c) ;; let exact = PrimitiveTactics.exact_tac;; let tac_use h = let tac_use h status = let (proof, goal) = status in debug("Inizio TC_USE\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("hname = "^ CicPp.ppterm h.hname ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); apply_tactic (match h.htype with "Rlt" -> exact ~term:h.hname | "Rle" -> exact ~term:h.hname | "Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt) ~continuation:(exact ~term:h.hname)) | "Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le) ~continuation:(exact ~term:h.hname)) | "eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le) ~continuation:(exact ~term:h.hname)) | "eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le) ~continuation:(exact ~term:h.hname)) | _->assert false) status in mk_tactic (tac_use h) ;; let is_ineq (h,t) = match t with Cic.Appl ( Cic.Const(u,boh)::next) -> (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI or UriManager.eq u HelmLibraryObjects.Reals.rgt_URI or UriManager.eq u HelmLibraryObjects.Reals.rle_URI or UriManager.eq u HelmLibraryObjects.Reals.rge_URI then true else if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then (match (List.hd next) with Cic.Const (uri,_) when UriManager.eq uri HelmLibraryObjects.Reals.r_URI -> true | _ -> false) else 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 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n"); [(Cic.Rel(n),t)] @ filter_real_hyp next cont) | a::next -> debug(" no\n"); filter_real_hyp next cont ;;*) let filter_real_hyp context _ = let rec filter_aux context num = match context with [] -> [] | Some(Cic.Name(h),Cic.Decl(t))::next -> [(Cic.Rel(num),t)] @ filter_aux next (num+1) | a::next -> filter_aux next (num+1) in filter_aux context 1 ;; (* 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,None))::next -> [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1) | Some(name,Cic.Def(a,Some ty))::next -> [Some(name, Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty))) ] @ superlift next (n+1) | _::next -> superlift next (n+1) (*?? ??*) ;; let equality_replace a b = 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 = CicUtil.lookup_meta goal metasenv in let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in let irl = CicMkImplicit.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))); let (proof,goals) = apply_tactic (EqualityTactics.rewrite_simpl_tac ~direction:`LeftToRight ~pattern:(ProofEngineTypes.conclusion_pattern None) (C.Meta (fresh_meta,irl))) ((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) in mk_tactic (equality_replace a b) ;; let tcl_fail a (proof,goal) = match a with 1 -> raise (ProofEngineTypes.Fail "fail-tactical") | _ -> (proof,[goal]) ;; (* Galla: moved in variousTactics.ml let assumption_tac (proof,goal)= let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta 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.first ~tactics:tac_list (proof,goal) ;; *) (* Galla: moved in negationTactics.ml (* !!!!! fix !!!!!!!!!! *) let contradiction_tac (proof,goal)= Tacticals.then_ (*inutile sia questo che quello prima della chiamata*) ~start:PrimitiveTactics.intros_tac ~continuation:(Tacticals.then_ ~start:(VariousTactics.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) (proof,goal) ;; *) (* ********************* TATTICA ******************************** *) let rec fourier (s_proof,s_goal)= let s_curi,s_metasenv,s_pbo,s_pty = s_proof in let s_metano,s_context,s_ty = CicUtil.lookup_meta 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) -> th_to_appl := (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then _Rfourier_not_ge_lt else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then _Rfourier_not_gt_le else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then _Rfourier_not_le_gt else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then _Rfourier_not_lt_ge else 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 = apply_tactic (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl) ~continuation:(PrimitiveTactics.intros_tac ())) (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 = CicUtil.lookup_meta 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 _-> ()) hyps; debug ("applico fourier a "^ string_of_int (List.length !lineq)^ " disequazioni\n"); let res=fourier_lineq (!lineq) in let tac=ref Tacticals.id_tac in if res=[] then (print_string "Tactic Fourier fails.\n";flush stdout; failwith "fourier_tac fails") 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 ( mk_tactic (fun status -> apply_tactic (if h1.hstrict then (Tacticals.thens ~start:(mk_tactic (fun status -> debug ("inizio t1 strict\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); apply_tactic (PrimitiveTactics.apply_tac ~term:_Rfourier_lt) status)) ~continuations:[tac_use h1; tac_zero_inf_pos (rational_to_fraction c1)]) 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:(mk_tactic (fun status -> debug("INIZIO TAC 1 2\n"); let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n"); debug ("ty = "^ CicPp.ppterm ty^"\n"); apply_tactic (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)) (* end fun -> *) 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:( mk_tactic (fun status -> let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in apply_tactic (ReductionTactics.change_tac ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty)) (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:(mk_tactic (fun status -> debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^ CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n"); let r = apply_tactic (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:(mk_tactic (fun status -> let r = apply_tactic (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; Tacticals.first ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] ]) ;(*Tacticals.id_tac*) Tacticals.then_ ~start:(mk_tactic (fun status -> let (proof, goal) = status in let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta 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 Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a]) |_ -> assert false) in let r = apply_tactic (ReductionTactics.change_tac ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty)) w1) status in debug("fine MY_CHNGE\n"); r)) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*) debug ("finalmente applico tac\n"); ( let r = apply_tactic !tac (proof,goal) in debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r ) ;; let fourier_tac = mk_tactic fourier