1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
27 (******************** OTHER USEFUL TACTICS **********************)
29 let rewrite_tac ~term:equality ~status:(proof,goal) =
31 let module U = UriManager in
32 let curi,metasenv,pbo,pty = proof in
33 let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
35 prerr_endline("rewrite chiamata con "^CicPp.ppterm gty^"\n");
36 let eq_ind_r,ty,t1,t2 =
37 match CicTypeChecker.type_of_aux' metasenv context equality with
38 C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
39 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") ->
42 (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
45 | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
46 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
49 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0)
54 (ProofEngineTypes.Fail
55 "Rewrite: the argument is not a proof of an equality")
58 let gty' = CicSubstitution.lift 1 gty in
59 let t1' = CicSubstitution.lift 1 t1 in
61 ProofEngineReduction.replace_lifting
63 (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
64 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
66 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
68 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
69 let fresh_meta = ProofEngineHelpers.new_meta proof in
71 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
72 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
75 PrimitiveTactics.exact_tac
77 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
78 ~status:((curi,metasenv',pbo,pty),goal)
80 assert (List.length goals = 0) ;
84 (* ti ho beccato !!!!!!!!!! qui' salta fuori un or. perche'?*)
88 let simpl_tac ~status:(proof,goal) =
89 let curi,metasenv,pbo,pty = proof in
90 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
92 prerr_endline("simpl_tac su "^CicPp.ppterm ty);
94 let new_ty = ProofEngineReduction.simpl context ty in
96 prerr_endline("ritorna "^CicPp.ppterm new_ty);
101 (n,_,_) when n = metano -> (metano,context,new_ty)
105 (curi,new_metasenv,pbo,pty), [metano]
109 let rewrite_simpl_tac ~term ~status =
111 Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status
115 (******************** THE FOURIER TACTIC ***********************)
117 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
118 des inéquations et équations sont entiers. En attendant la tactique Field.
124 let debug x = print_string ("____ "^x) ; flush stdout;;
126 let debug_pcontext x =
128 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
129 a ^ " " | _ ->()) x ;
130 debug ("contesto : "^ (!str) ^ "\n")
133 (******************************************************************************
134 Operations on linear combinations.
136 Opérations sur les combinaisons linéaires affines.
137 La partie homogène d'une combinaison linéaire est en fait une table de hash
138 qui donne le coefficient d'un terme du calcul des constructions,
139 qui est zéro si le terme n'y est pas.
145 The type for linear combinations
147 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
151 @return an empty flin
153 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
159 @return the rational associated with x (coefficient)
163 (Hashtbl.find f.fhom x)
169 Adds c to the coefficient of x
176 let cx = flin_coef f x in
177 Hashtbl.remove f.fhom x;
178 Hashtbl.add f.fhom x (rplus cx c);
187 let flin_add_cste f c =
189 fcste=rplus f.fcste c}
193 @return a empty flin with r1 in fcste
195 let flin_one () = flin_add_cste (flin_zero()) r1;;
200 let flin_plus f1 f2 =
201 let f3 = flin_zero() in
202 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
203 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
204 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
210 let flin_minus f1 f2 =
211 let f3 = flin_zero() in
212 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
213 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
214 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
221 let f2 = flin_zero() in
222 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
223 flin_add_cste f2 (rmult a f.fcste);
227 (*****************************************************************************)
232 @return proiection on string of t
234 let rec string_of_term t =
236 Cic.Cast (t1,t2) -> string_of_term t1
237 |Cic.Const (u,boh) -> UriManager.string_of_uri u
238 |Cic.Var (u) -> UriManager.string_of_uri u
239 | _ -> "not_of_constant"
243 let string_of_constr = string_of_term
249 @raise Failure if conversion is impossible
250 @return rational proiection of t
252 let rec rational_of_term t =
253 (* fun to apply f to the first and second rational-term of l *)
254 let rat_of_binop f l =
255 let a = List.hd l and
256 b = List.hd(List.tl l) in
257 f (rational_of_term a) (rational_of_term b)
259 (* as before, but f is unary *)
260 let rat_of_unop f l =
261 f (rational_of_term (List.hd l))
264 | Cic.Cast (t1,t2) -> (rational_of_term t1)
265 | Cic.Appl (t1::next) ->
268 (match (UriManager.string_of_uri u) with
269 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
271 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
272 rat_of_unop rinv next
273 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
274 rat_of_binop rmult next
275 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
276 rat_of_binop rdiv next
277 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
278 rat_of_binop rplus next
279 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
280 rat_of_binop rminus next
281 | _ -> failwith "not a rational")
282 | _ -> failwith "not a rational")
283 | Cic.Const (u,boh) ->
284 (match (UriManager.string_of_uri u) with
285 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
286 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
287 | _ -> failwith "not a rational")
288 | _ -> failwith "not a rational"
292 let rational_of_const = rational_of_term;;
296 let rec flin_of_term t =
297 let fl_of_binop f l =
298 let a = List.hd l and
299 b = List.hd(List.tl l) in
300 f (flin_of_term a) (flin_of_term b)
304 | Cic.Cast (t1,t2) -> (flin_of_term t1)
305 | Cic.Appl (t1::next) ->
310 match (UriManager.string_of_uri u) with
311 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
312 flin_emult (rop r1) (flin_of_term (List.hd next))
313 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
314 fl_of_binop flin_plus next
315 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
316 fl_of_binop flin_minus next
317 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
319 let arg1 = (List.hd next) and
320 arg2 = (List.hd(List.tl next))
324 let a = rational_of_term arg1 in
327 let b = (rational_of_term arg2) in
328 (flin_add_cste (flin_zero()) (rmult a b))
331 _ -> (flin_add (flin_zero()) arg2 a)
334 _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
336 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
337 let a=(rational_of_term (List.hd next)) in
338 flin_add_cste (flin_zero()) (rinv a)
339 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
341 let b=(rational_of_term (List.hd(List.tl next))) in
344 let a = (rational_of_term (List.hd next)) in
345 (flin_add_cste (flin_zero()) (rdiv a b))
348 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
354 | Cic.Const (u,boh) ->
356 match (UriManager.string_of_uri u) with
357 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
358 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
362 with _ -> flin_add (flin_zero()) t r1
366 let flin_of_constr = flin_of_term;;
370 Translates a flin to (c,x) list
372 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
374 let flin_to_alist f =
376 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
380 (* Représentation des hypothèses qui sont des inéquations ou des équations.
384 The structure for ineq
386 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
387 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
394 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
397 let ineq1_of_term (h,t) =
398 debug("Trasformo in ineq "^CicPp.ppterm t^"\n");
399 match t with (* match t *)
400 Cic.Appl (t1::next) ->
401 let arg1= List.hd next in
402 let arg2= List.hd(List.tl next) in
403 (match t1 with (* match t1 *)
405 (match UriManager.string_of_uri u with (* match u *)
406 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
411 hflin= flin_minus (flin_of_term arg1)
414 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
419 hflin= flin_minus (flin_of_term arg2)
422 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
427 hflin= flin_minus (flin_of_term arg1)
430 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
435 hflin= flin_minus (flin_of_term arg2)
438 |_->assert false)(* match u *)
439 | Cic.MutInd (u,i,o) ->
440 (match UriManager.string_of_uri u with
441 "cic:/Coq/Init/Logic_Type/eqT.ind" ->
442 debug("Ho trovato una ==\n");
445 let arg2= List.hd(List.tl (List.tl next)) in
448 (match UriManager.string_of_uri u with
449 "cic:/Coq/Reals/Rdefinitions/R.con"->
455 hflin= flin_minus (flin_of_term arg1)
462 hflin= flin_minus (flin_of_term arg2)
465 |_-> debug("eqT deve essere applicato a const R\n");assert false)
466 |_-> debug("eqT deve essere appl a const\n");assert false)
467 |_-> debug("Il trmine e' un appl mutind ma non eqT\n");assert false)
468 |_-> debug("Il termine non e' una app di const o app di mutind\n");assert false)(* match t1 *)
469 |_-> debug("Il termine non e' una applicazione\n");assert false (* match t *)
472 let ineq1_of_constr = ineq1_of_term;;
475 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
481 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
484 let rec print_sys l =
487 | (a,b)::next -> (print_rl a;
488 print_string (if b=true then "strict\n"else"\n");
493 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
496 let fourier_lineq lineq1 =
498 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
500 Hashtbl.iter (fun x c ->
501 try (Hashtbl.find hvar x;())
502 with _-> nvar:=(!nvar)+1;
503 Hashtbl.add hvar x (!nvar))
507 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
508 let sys= List.map (fun h->
509 let v=Array.create ((!nvar)+1) r0 in
510 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
512 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
514 debug ("chiamo unsolvable sul sistema di "^
515 string_of_int (List.length sys) ^"\n");
520 (*****************************************************************************
521 Construction de la preuve en cas de succès de la méthode de Fourier,
522 i.e. on obtient une contradiction.
526 let _eqT = Cic.MutInd(UriManager.uri_of_string
527 "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
528 let _False = Cic.MutInd (UriManager.uri_of_string
529 "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
530 let _not = Cic.Const (UriManager.uri_of_string
531 "cic:/Coq/Init/Logic/not.con") 0;;
532 let _R0 = Cic.Const (UriManager.uri_of_string
533 "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
534 let _R1 = Cic.Const (UriManager.uri_of_string
535 "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
536 let _R = Cic.Const (UriManager.uri_of_string
537 "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
538 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
539 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
540 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
541 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
542 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
543 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
544 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
545 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
546 let _Rfourier_le=Cic.Const (UriManager.uri_of_string
547 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
548 let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
549 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
550 let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
551 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
552 let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
553 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
554 let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
555 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
556 let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
557 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
558 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
559 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
560 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
561 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
562 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
563 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
564 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
565 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
566 let _Rinv = Cic.Const (UriManager.uri_of_string
567 "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
568 let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
569 "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
570 let _Rle = Cic.Const (UriManager.uri_of_string
571 "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
572 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
573 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
574 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
575 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
576 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
577 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
578 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
579 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
580 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
581 "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
582 let _Rlt = Cic.Const (UriManager.uri_of_string
583 "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
584 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
585 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
586 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
587 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
588 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
589 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
590 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
591 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
592 let _Rminus = Cic.Const (UriManager.uri_of_string
593 "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
594 let _Rmult = Cic.Const (UriManager.uri_of_string
595 "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
596 let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
597 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
598 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
599 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
600 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
601 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
602 let _Ropp = Cic.Const (UriManager.uri_of_string
603 "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
604 let _Rplus = Cic.Const (UriManager.uri_of_string
605 "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
606 let _sym_eqT = Cic.Const(UriManager.uri_of_string
607 "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
609 (******************************************************************************)
611 let is_int x = (x.den)=1
614 (* fraction = couple (num,den) *)
615 let rec rational_to_fraction x= (x.num,x.den)
618 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
621 let rec int_to_real_aux n =
623 0 -> _R0 (* o forse R0 + R0 ????? *)
625 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
630 let x = int_to_real_aux (abs n) in
632 Cic.Appl [ _Ropp ; x ]
638 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
641 let rational_to_real x =
642 let (n,d)=rational_to_fraction x in
643 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
646 (* preuve que 0<n*1/d
649 let tac_zero_inf_pos (n,d) ~status =
650 (*let cste = pf_parse_constr gl in*)
651 let pall str ~status:(proof,goal) t =
652 debug ("tac "^str^" :\n" );
653 let curi,metasenv,pbo,pty = proof in
654 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
655 debug ("th = "^ CicPp.ppterm t ^"\n");
656 debug ("ty = "^ CicPp.ppterm ty^"\n");
659 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
660 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
662 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
663 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
667 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
668 ~status _Rlt_zero_pos_plus1;
669 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
670 ~continuation:!tacn);
673 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
674 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
675 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
680 debug("TAC ZERO INF POS\n");
682 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
691 (* preuve que 0<=n*1/d
694 let tac_zero_infeq_pos gl (n,d) ~status =
695 (*let cste = pf_parse_constr gl in*)
696 debug("inizio tac_zero_infeq_pos\n");
699 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
701 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
704 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
706 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
707 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
710 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
711 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
714 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
715 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
716 debug("fine tac_zero_infeq_pos\n");
722 (* preuve que 0<(-n)*(1/d) => False
725 let tac_zero_inf_false gl (n,d) ~status=
726 debug("inizio tac_zero_inf_false\n");
728 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
732 (debug "2\n";let r = (Tacticals.then_ ~start:(
733 fun ~status:(proof,goal as status) ->
734 let curi,metasenv,pbo,pty = proof in
735 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
736 debug("!!!!!!!!1:unify "^CicPp.ppterm _Rle_not_lt^" with "
737 ^ CicPp.ppterm ty ^" fails\n");
738 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
739 debug("!!!!!!!!!2\n");
742 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
748 (* preuve que 0<=(-n)*(1/d) => False
751 let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
752 debug("stat tac_zero_infeq_false\n");
755 let curi,metasenv,pbo,pty = proof in
756 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
758 debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
759 Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
760 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
761 debug("end tac_zero_infeq_false\n");
767 (* *********** ********** ******** ??????????????? *********** **************)
769 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
770 let curi,metasenv,pbo,pty = proof in
771 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
772 let fresh_meta = ProofEngineHelpers.new_meta proof in
774 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
775 let metasenv' = (fresh_meta,context,t)::metasenv in
776 let proof' = curi,metasenv',pbo,pty in
778 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta
779 (fresh_meta,irl),t))::al)) ~status:(proof',goal)
781 proof'',fresh_meta::goals
788 let my_cut ~term:c ~status:(proof,goal)=
789 let curi,metasenv,pbo,pty = proof in
790 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
792 let fresh_meta = ProofEngineHelpers.new_meta proof in
794 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
795 let metasenv' = (fresh_meta,context,c)::metasenv in
796 let proof' = curi,metasenv',pbo,pty in
798 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
799 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
800 ~status:(proof',goal)
802 (* We permute the generated goals to be consistent with Coq *)
805 | he::tl -> proof'',he::fresh_meta::tl
809 let exact = PrimitiveTactics.exact_tac;;
811 let tac_use h ~status:(proof,goal as status) =
812 debug("Inizio TC_USE\n");
813 let curi,metasenv,pbo,pty = proof in
814 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
815 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
816 debug ("ty = "^ CicPp.ppterm ty^"\n");
820 "Rlt" -> exact ~term:h.hname ~status
821 |"Rle" -> exact ~term:h.hname ~status
822 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
823 ~term:_Rfourier_gt_to_lt)
824 ~continuation:(exact ~term:h.hname)) ~status
825 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
826 ~term:_Rfourier_ge_to_le)
827 ~continuation:(exact ~term:h.hname)) ~status
828 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
829 ~term:_Rfourier_eqLR_to_le)
830 ~continuation:(exact ~term:h.hname)) ~status
831 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
832 ~term:_Rfourier_eqRL_to_le)
833 ~continuation:(exact ~term:h.hname)) ~status
836 debug("Fine TAC_USE\n");
844 Cic.Appl ( Cic.Const(u,boh)::next) ->
845 (match (UriManager.string_of_uri u) with
846 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
847 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
848 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
849 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
850 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
851 (match (List.hd next) with
852 Cic.Const (uri,_) when
853 UriManager.string_of_uri uri =
854 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
860 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
863 Cic.Appl(Array.to_list a)
866 (* Résolution d'inéquations linéaires dans R *)
867 let rec strip_outer_cast c = match c with
868 | Cic.Cast (c,_) -> strip_outer_cast c
872 let find_in_context id context =
873 let rec find_in_context_aux c n =
875 [] -> failwith (id^" not found in context")
876 | a::next -> (match a with
877 Some (Cic.Name(name),_) when name = id -> n
878 (*? magari al posto di _ qualcosaltro?*)
879 | _ -> find_in_context_aux next (n+1))
881 find_in_context_aux context 1
884 (* mi sembra quadratico *)
885 let rec filter_real_hyp context cont =
888 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
889 let n = find_in_context h cont in
890 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
891 | a::next -> debug(" no\n"); filter_real_hyp next cont
894 (* lifts everithing at the conclusion level *)
895 let rec superlift c n=
898 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
899 CicSubstitution.lift n a))] @ superlift next (n+1)
900 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
901 CicSubstitution.lift n a))] @ superlift next (n+1)
902 | _::next -> superlift next (n+1) (*?? ??*)
906 let equality_replace a b ~status =
907 debug("inizio EQ\n");
908 let module C = Cic in
909 let proof,goal = status in
910 let curi,metasenv,pbo,pty = proof in
911 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
912 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
913 let fresh_meta = ProofEngineHelpers.new_meta proof in
915 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
916 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
917 debug("chamo rewrite tac su "^CicPp.ppterm (C.Meta (fresh_meta,irl))^" e ty "^CicPp.ppterm ty ^"\n");
919 rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
920 ~status:((curi,metasenv',pbo,pty),goal)
922 let new_goals = fresh_meta::goals in
923 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
924 ^string_of_int( List.length goals)^"+ meta\n");
928 let tcl_fail a ~status:(proof,goal) =
930 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
935 let assumption_tac ~status:(proof,goal)=
936 let curi,metasenv,pbo,pty = proof in
937 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
939 let tac_list = List.map
940 ( fun x -> num := !num + 1;
942 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
943 | _ -> ("fake",tcl_fail 1)
947 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
950 (* !!!!! fix !!!!!!!!!! *)
951 let contradiction_tac ~status:(proof,goal)=
953 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
954 ~continuation:(Tacticals.then_
955 ~start:(Ring.elim_type_tac ~term:_False)
956 ~continuation:(assumption_tac))
960 (* ********************* TATTICA ******************************** *)
962 let rec fourier ~status:(s_proof,s_goal)=
963 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
964 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
967 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
968 debug_pcontext s_context;
970 let fhyp = String.copy "new_hyp_for_fourier" in
972 (* here we need to negate the thesis, but to do this we need to apply the right
973 theoreme,so let's parse our thesis *)
975 let th_to_appl = ref _Rfourier_not_le_gt in
977 Cic.Appl ( Cic.Const(u,boh)::args) ->
978 (match UriManager.string_of_uri u with
979 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
981 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
983 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
985 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
987 |_-> failwith "fourier can't be applyed")
988 |_-> failwith "fourier can't be applyed");
989 (* fix maybe strip_outer_cast goes here?? *)
991 (* now let's change our thesis applying the th and put it with hp *)
993 let proof,gl = Tacticals.then_
994 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
995 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
996 ~status:(s_proof,s_goal) in
997 let goal = if List.length gl = 1 then List.hd gl
998 else failwith "a new goal" in
1000 debug ("port la tesi sopra e la nego. contesto :\n");
1001 debug_pcontext s_context;
1003 (* now we have all the right environment *)
1005 let curi,metasenv,pbo,pty = proof in
1006 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1009 (* now we want to convert hp to inequations, but first we must lift
1010 everyting to thesis level, so that a variable has the save Rel(n)
1011 in each hp ( needed by ineq1_of_term ) *)
1013 (* ? fix if None ?????*)
1014 (* fix change superlift with a real name *)
1016 let l_context = superlift context 1 in
1017 let hyps = filter_real_hyp l_context l_context in
1019 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
1021 let lineq =ref [] in
1023 (* transform hyps into inequations *)
1025 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1026 with _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");)
1030 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1033 let res=fourier_lineq (!lineq) in
1034 let tac=ref Ring.id_tac in
1036 (print_string "Tactic Fourier fails.\n";flush stdout;
1037 failwith "fourier can't proove it")
1040 match res with (*match res*)
1043 (* in lc we have the coefficient to "reduce" the system *)
1045 print_string "Fourier's method can prove the goal...\n";flush stdout;
1047 debug "I coeff di moltiplicazione rit sono: ";
1051 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1052 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1054 (List.combine (!lineq) lc);
1056 print_string (" quindi lutil e' lunga "^
1057 string_of_int (List.length (!lutil))^"\n");
1059 (* on construit la combinaison linéaire des inéquation *)
1061 (match (!lutil) with (*match (!lutil) *)
1063 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1065 let s=ref (h1.hstrict) in
1068 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1069 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1071 List.iter (fun (h,c) ->
1072 s:=(!s)||(h.hstrict);
1073 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1074 [_Rmult;rational_to_real c;h.hleft ] ]);
1075 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1076 [_Rmult;rational_to_real c;h.hright] ]))
1079 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1080 let tc=rational_to_real cres in
1083 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1085 debug "inizio a costruire tac1\n";
1086 Fourier.print_rational(c1);
1088 let tac1=ref ( fun ~status ->
1093 debug ("inizio t1 strict\n");
1094 let curi,metasenv,pbo,pty = proof in
1095 let metano,context,ty = List.find
1096 (function (m,_,_) -> m=goal) metasenv in
1097 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1098 debug ("ty = "^ CicPp.ppterm ty^"\n");
1099 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1100 ~continuations:[tac_use h1;tac_zero_inf_pos
1101 (rational_to_fraction c1)]
1106 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1107 ~continuations:[tac_use h1;tac_zero_inf_pos
1108 (rational_to_fraction c1)] ~status
1114 List.iter (fun (h,c) ->
1118 tac1:=(Tacticals.thens
1119 ~start:(PrimitiveTactics.apply_tac
1120 ~term:_Rfourier_lt_lt)
1121 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1122 (rational_to_fraction c)])
1126 Fourier.print_rational(c1);
1127 tac1:=(Tacticals.thens
1130 debug("INIZIO TAC 1 2\n");
1131 let curi,metasenv,pbo,pty = proof in
1132 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1134 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1135 debug ("ty = "^ CicPp.ppterm ty^"\n");
1136 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1137 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1138 (rational_to_fraction c)])
1144 tac1:=(Tacticals.thens
1145 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1146 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1147 (rational_to_fraction c)])
1151 tac1:=(Tacticals.thens
1152 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1153 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1154 (rational_to_fraction c)])
1158 s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1162 tac_zero_inf_false goal (rational_to_fraction cres)
1164 tac_zero_infeq_false goal (rational_to_fraction cres)
1166 tac:=(Tacticals.thens
1167 ~start:(my_cut ~term:ineq)
1168 ~continuations:[Tacticals.then_
1169 ~start:(fun ~status:(proof,goal as status) ->
1170 let curi,metasenv,pbo,pty = proof in
1171 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1174 debug("Change_tac "^CicPp.ppterm ty^" with "^CicPp.ppterm (Cic.Appl [ _not; ineq]) ^"\n");
1176 PrimitiveTactics.change_tac ~what:ty
1177 ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1178 ~continuation:(Tacticals.then_
1179 ~start:(PrimitiveTactics.apply_tac ~term:
1180 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1181 ~continuation:(Tacticals.thens
1184 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1187 (match r with (p,gl) ->
1188 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1190 ~continuations:[(Tacticals.thens
1192 fun ~status:(proof,goals as status) ->
1194 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1195 (match r with (p,gl) ->
1196 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1199 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1200 (* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
1201 di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
1202 parametri della equality_replace vengono passati al contrario? Oppure la
1203 tattica usa i parametri al contrario?
1204 ~continuations:[Tacticals.then_
1206 fun ~status:(proof,goal as status) ->
1208 let curi,metasenv,pbo,pty = proof in
1209 let metano,context,ty = List.find (function (m,_,_) -> m=
1211 debug("ty = "^CicPp.ppterm ty^"\n");
1212 let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
1214 debug("fine ECCOCI\n");
1216 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1218 ;Tacticals.try_tactics
1219 ~tactics:[ "ring", (fun ~status ->
1220 debug("begin RING\n");
1221 let r = Ring.ring_tac ~status in
1222 debug ("end RING\n");
1224 ; "id", Ring.id_tac]
1229 fun ~status:(proof,goal as status) ->
1230 let curi,metasenv,pbo,pty = proof in
1231 let metano,context,ty = List.find (function (m,_,_) -> m=
1233 (* check if ty is of type *)
1235 debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1237 (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*)
1238 Cic.Prod (Cic.Anonimous,a,b) -> (Cic.Appl [_not;a])
1241 let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1242 debug("fine MY_CHNGE\n");
1245 ~continuation:Ring.id_tac(*tac2*)]))
1246 ;Ring.id_tac(*!tac1*)]);(*end tac:=*)
1247 tac:=(Tacticals.thens
1248 ~start:(PrimitiveTactics.cut_tac ~term:_False)
1249 ~continuations:[Tacticals.then_
1250 ~start:(PrimitiveTactics.intros_tac ~name:"??")
1251 ~continuation:contradiction_tac
1255 |_-> assert false)(*match (!lutil) *)
1256 |_-> assert false); (*match res*)
1257 debug ("finalmente applico tac\n");
1258 (!tac ~status:(proof,goal))
1261 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;