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
34 let eq_ind_r,ty,t1,t2 =
35 match CicTypeChecker.type_of_aux' metasenv context equality with
36 C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
37 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
40 (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
43 | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
44 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
47 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
52 (ProofEngineTypes.Fail
53 "Rewrite: the argument is not a proof of an equality")
56 let gty' = CicSubstitution.lift 1 gty in
57 let t1' = CicSubstitution.lift 1 t1 in
59 ProofEngineReduction.replace_lifting
60 ~equality:ProofEngineReduction.alpha_equivalence
61 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
63 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
65 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
66 let fresh_meta = ProofEngineHelpers.new_meta proof in
68 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
69 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
72 PrimitiveTactics.exact_tac
74 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
75 ~status:((curi,metasenv',pbo,pty),goal)
77 assert (List.length goals = 0) ;
82 let rewrite_simpl_tac ~term ~status =
83 Tacticals.then_ ~start:(rewrite_tac ~term)
85 (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
89 (******************** THE FOURIER TACTIC ***********************)
91 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
92 des inéquations et équations sont entiers. En attendant la tactique Field.
98 let debug x = print_string ("____ "^x) ; flush stdout;;
100 let debug_pcontext x =
102 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
103 a ^ " " | _ ->()) x ;
104 debug ("contesto : "^ (!str) ^ "\n")
107 (******************************************************************************
108 Operations on linear combinations.
110 Opérations sur les combinaisons linéaires affines.
111 La partie homogène d'une combinaison linéaire est en fait une table de hash
112 qui donne le coefficient d'un terme du calcul des constructions,
113 qui est zéro si le terme n'y est pas.
119 The type for linear combinations
121 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
125 @return an empty flin
127 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
133 @return the rational associated with x (coefficient)
137 (Hashtbl.find f.fhom x)
143 Adds c to the coefficient of x
152 let cx = flin_coef f x in
153 Hashtbl.remove f.fhom x;
154 Hashtbl.add f.fhom x (rplus cx c);
156 |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n");
157 let cx = flin_coef f x in
158 Hashtbl.remove f.fhom x;
159 Hashtbl.add f.fhom x (rplus cx c);
168 let flin_add_cste f c =
170 fcste=rplus f.fcste c}
174 @return a empty flin with r1 in fcste
176 let flin_one () = flin_add_cste (flin_zero()) r1;;
181 let flin_plus f1 f2 =
182 let f3 = flin_zero() in
183 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
184 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
185 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
191 let flin_minus f1 f2 =
192 let f3 = flin_zero() in
193 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
194 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
195 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
202 let f2 = flin_zero() in
203 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
204 flin_add_cste f2 (rmult a f.fcste);
208 (*****************************************************************************)
213 @raise Failure if conversion is impossible
214 @return rational proiection of t
216 let rec rational_of_term t =
217 (* fun to apply f to the first and second rational-term of l *)
218 let rat_of_binop f l =
219 let a = List.hd l and
220 b = List.hd(List.tl l) in
221 f (rational_of_term a) (rational_of_term b)
223 (* as before, but f is unary *)
224 let rat_of_unop f l =
225 f (rational_of_term (List.hd l))
228 | Cic.Cast (t1,t2) -> (rational_of_term t1)
229 | Cic.Appl (t1::next) ->
232 (match (UriManager.string_of_uri u) with
233 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
235 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
236 rat_of_unop rinv next
237 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
238 rat_of_binop rmult next
239 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
240 rat_of_binop rdiv next
241 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
242 rat_of_binop rplus next
243 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
244 rat_of_binop rminus next
245 | _ -> failwith "not a rational")
246 | _ -> failwith "not a rational")
247 | Cic.Const (u,boh) ->
248 (match (UriManager.string_of_uri u) with
249 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
250 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
251 | _ -> failwith "not a rational")
252 | _ -> failwith "not a rational"
256 let rational_of_const = rational_of_term;;
266 let rec flin_of_term t =
267 let fl_of_binop f l =
268 let a = List.hd l and
269 b = List.hd(List.tl l) in
270 f (flin_of_term a) (flin_of_term b)
274 | Cic.Cast (t1,t2) -> (flin_of_term t1)
275 | Cic.Appl (t1::next) ->
280 match (UriManager.string_of_uri u) with
281 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
282 flin_emult (rop r1) (flin_of_term (List.hd next))
283 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
284 fl_of_binop flin_plus next
285 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
286 fl_of_binop flin_minus next
287 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
289 let arg1 = (List.hd next) and
290 arg2 = (List.hd(List.tl next))
292 if fails rational_of_term arg1
294 if fails rational_of_term arg2
296 ( (* prodotto tra 2 incognite ????? impossibile*)
297 failwith "Sistemi lineari!!!!\n"
302 Cic.Rel(n) -> (*trasformo al volo*)
303 (flin_add (flin_zero()) arg1 (rational_of_term arg2))
305 let tmp = flin_of_term arg1 in
306 flin_emult (rational_of_term arg2) (tmp)
309 if fails rational_of_term arg2
313 Cic.Rel(n) -> (*trasformo al volo*)
314 (flin_add (flin_zero()) arg2 (rational_of_term arg1))
316 let tmp = flin_of_term arg2 in
317 flin_emult (rational_of_term arg1) (tmp)
321 ( (*prodotto tra razionali*)
322 (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
326 (*let a = rational_of_term arg1 in
327 debug("ho fatto rational of term di "^CicPp.ppterm arg1^
328 " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
329 let a = flin_of_term arg1
332 let b = (rational_of_term arg2) in
333 debug("ho fatto rational of term di "^CicPp.ppterm arg2^
334 " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
335 (flin_add_cste (flin_zero()) (rmult a b))
338 _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
339 (flin_add (flin_zero()) arg2 a)
342 _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
343 (flin_add(flin_zero()) arg1 (rational_of_term arg2))
346 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
347 let a=(rational_of_term (List.hd next)) in
348 flin_add_cste (flin_zero()) (rinv a)
349 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
351 let b=(rational_of_term (List.hd(List.tl next))) in
354 let a = (rational_of_term (List.hd next)) in
355 (flin_add_cste (flin_zero()) (rdiv a b))
358 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
364 | Cic.Const (u,boh) ->
366 match (UriManager.string_of_uri u) with
367 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
368 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
372 with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
376 let flin_of_constr = flin_of_term;;
380 Translates a flin to (c,x) list
382 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
384 let flin_to_alist f =
386 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
390 (* Représentation des hypothèses qui sont des inéquations ou des équations.
394 The structure for ineq
396 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
397 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
404 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
407 let ineq1_of_term (h,t) =
408 match t with (* match t *)
409 Cic.Appl (t1::next) ->
410 let arg1= List.hd next in
411 let arg2= List.hd(List.tl next) in
412 (match t1 with (* match t1 *)
414 (match UriManager.string_of_uri u with (* match u *)
415 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
420 hflin= flin_minus (flin_of_term arg1)
423 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
428 hflin= flin_minus (flin_of_term arg2)
431 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
436 hflin= flin_minus (flin_of_term arg1)
439 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
444 hflin= flin_minus (flin_of_term arg2)
447 |_->assert false)(* match u *)
448 | Cic.MutInd (u,i,o) ->
449 (match UriManager.string_of_uri u with
450 "cic:/Coq/Init/Logic_Type/eqT.ind" ->
453 let arg2= List.hd(List.tl (List.tl next)) in
456 (match UriManager.string_of_uri u with
457 "cic:/Coq/Reals/Rdefinitions/R.con"->
462 hflin= flin_minus (flin_of_term arg1)
469 hflin= flin_minus (flin_of_term arg2)
475 |_-> assert false)(* match t1 *)
476 |_-> assert false (* match t *)
479 let ineq1_of_constr = ineq1_of_term;;
482 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
488 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
491 let rec print_sys l =
494 | (a,b)::next -> (print_rl a;
495 print_string (if b=true then "strict\n"else"\n");
500 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
503 let fourier_lineq lineq1 =
505 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
507 Hashtbl.iter (fun x c ->
508 try (Hashtbl.find hvar x;())
509 with _-> nvar:=(!nvar)+1;
510 Hashtbl.add hvar x (!nvar);
511 debug("aggiungo una var "^
512 string_of_int !nvar^" per "^
513 CicPp.ppterm x^"\n"))
517 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
518 let sys= List.map (fun h->
519 let v=Array.create ((!nvar)+1) r0 in
520 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c)
522 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
524 debug ("chiamo unsolvable sul sistema di "^
525 string_of_int (List.length sys) ^"\n");
530 (*****************************************************************************
531 Construction de la preuve en cas de succès de la méthode de Fourier,
532 i.e. on obtient une contradiction.
536 let _eqT = Cic.MutInd(UriManager.uri_of_string
537 "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [] ;;
538 let _False = Cic.MutInd (UriManager.uri_of_string
539 "cic:/Coq/Init/Logic/False.ind") 0 [] ;;
540 let _not = Cic.Const (UriManager.uri_of_string
541 "cic:/Coq/Init/Logic/not.con") [];;
542 let _R0 = Cic.Const (UriManager.uri_of_string
543 "cic:/Coq/Reals/Rdefinitions/R0.con") [] ;;
544 let _R1 = Cic.Const (UriManager.uri_of_string
545 "cic:/Coq/Reals/Rdefinitions/R1.con") [] ;;
546 let _R = Cic.Const (UriManager.uri_of_string
547 "cic:/Coq/Reals/Rdefinitions/R.con") [] ;;
548 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
549 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [] ;;
550 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
551 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [] ;;
552 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
553 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [] ;;
554 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
555 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [] ;;
556 let _Rfourier_le=Cic.Const (UriManager.uri_of_string
557 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") [] ;;
558 let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
559 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") [] ;;
560 let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
561 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") [] ;;
562 let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
563 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") [] ;;
564 let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
565 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") [] ;;
566 let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
567 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") [] ;;
568 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
569 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [] ;;
570 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
571 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [] ;;
572 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
573 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [] ;;
574 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
575 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [] ;;
576 let _Rinv = Cic.Const (UriManager.uri_of_string
577 "cic:/Coq/Reals/Rdefinitions/Rinv.con") [] ;;
578 let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
579 "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [] ;;
580 let _Rle = Cic.Const (UriManager.uri_of_string
581 "cic:/Coq/Reals/Rdefinitions/Rle.con") [] ;;
582 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
583 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [] ;;
584 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
585 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [] ;;
586 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
587 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [] ;;
588 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
589 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [] ;;
590 (*let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
591 "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;*)
592 let _Rlt = Cic.Const (UriManager.uri_of_string
593 "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;;
594 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
595 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [] ;;
596 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
597 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [] ;;
598 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
599 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [] ;;
600 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
601 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [] ;;
602 let _Rminus = Cic.Const (UriManager.uri_of_string
603 "cic:/Coq/Reals/Rdefinitions/Rminus.con") [] ;;
604 let _Rmult = Cic.Const (UriManager.uri_of_string
605 "cic:/Coq/Reals/Rdefinitions/Rmult.con") [] ;;
606 let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
607 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [] ;;
608 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
609 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [] ;;
610 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
611 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [] ;;
612 let _Ropp = Cic.Const (UriManager.uri_of_string
613 "cic:/Coq/Reals/Rdefinitions/Ropp.con") [] ;;
614 let _Rplus = Cic.Const (UriManager.uri_of_string
615 "cic:/Coq/Reals/Rdefinitions/Rplus.con") [] ;;
617 (******************************************************************************)
619 let is_int x = (x.den)=1
622 (* fraction = couple (num,den) *)
623 let rec rational_to_fraction x= (x.num,x.den)
626 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
629 let rec int_to_real_aux n =
631 0 -> _R0 (* o forse R0 + R0 ????? *)
633 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
638 let x = int_to_real_aux (abs n) in
640 Cic.Appl [ _Ropp ; x ]
646 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
649 let rational_to_real x =
650 let (n,d)=rational_to_fraction x in
651 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
654 (* preuve que 0<n*1/d
657 let tac_zero_inf_pos (n,d) ~status =
658 (*let cste = pf_parse_constr gl in*)
659 let pall str ~status:(proof,goal) t =
660 debug ("tac "^str^" :\n" );
661 let curi,metasenv,pbo,pty = proof in
662 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
663 debug ("th = "^ CicPp.ppterm t ^"\n");
664 debug ("ty = "^ CicPp.ppterm ty^"\n");
667 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
668 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
670 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
671 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
675 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
676 ~status _Rlt_zero_pos_plus1;
677 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
678 ~continuation:!tacn);
681 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
682 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
683 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
688 debug("TAC ZERO INF POS\n");
690 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
699 (* preuve que 0<=n*1/d
702 let tac_zero_infeq_pos gl (n,d) ~status =
703 (*let cste = pf_parse_constr gl in*)
704 debug("inizio tac_zero_infeq_pos\n");
707 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
709 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
712 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
714 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
715 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
718 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
719 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
722 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
723 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
724 debug("fine tac_zero_infeq_pos\n");
730 (* preuve que 0<(-n)*(1/d) => False
733 let tac_zero_inf_false gl (n,d) ~status=
734 debug("inizio tac_zero_inf_false\n");
736 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
740 (debug "2\n";let r = (Tacticals.then_ ~start:(
741 fun ~status:(proof,goal as status) ->
742 let curi,metasenv,pbo,pty = proof in
743 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
744 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
745 ^ CicPp.ppterm ty ^"\n");
746 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
747 debug("!!!!!!!!!2\n");
750 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
756 (* preuve que 0<=n*(1/d) => False ; n est negatif
759 let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
760 debug("stat tac_zero_infeq_false\n");
762 let curi,metasenv,pbo,pty = proof in
763 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
765 debug("faccio fold di " ^ CicPp.ppterm
769 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
772 debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
773 (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
776 (ReductionTactics.fold_tac ~also_in_hypotheses:false
781 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
786 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
787 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
788 debug("end tac_zero_infeq_false\n");
791 Tacticals.id_tac ~status
796 (* *********** ********** ******** ??????????????? *********** **************)
798 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
799 let curi,metasenv,pbo,pty = proof in
800 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
801 let fresh_meta = ProofEngineHelpers.new_meta proof in
803 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
804 let metasenv' = (fresh_meta,context,t)::metasenv in
805 let proof' = curi,metasenv',pbo,pty in
807 PrimitiveTactics.apply_tac
808 (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
809 ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
810 ~status:(proof',goal)
812 proof'',fresh_meta::goals
819 let my_cut ~term:c ~status:(proof,goal)=
820 let curi,metasenv,pbo,pty = proof in
821 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
823 debug("my_cut di "^CicPp.ppterm c^"\n");
826 let fresh_meta = ProofEngineHelpers.new_meta proof in
828 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
829 let metasenv' = (fresh_meta,context,c)::metasenv in
830 let proof' = curi,metasenv',pbo,pty in
832 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
833 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
834 ~status:(proof',goal)
836 (* We permute the generated goals to be consistent with Coq *)
839 | he::tl -> proof'',he::fresh_meta::tl
843 let exact = PrimitiveTactics.exact_tac;;
845 let tac_use h ~status:(proof,goal as status) =
846 debug("Inizio TC_USE\n");
847 let curi,metasenv,pbo,pty = proof in
848 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
849 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
850 debug ("ty = "^ CicPp.ppterm ty^"\n");
854 "Rlt" -> exact ~term:h.hname ~status
855 |"Rle" -> exact ~term:h.hname ~status
856 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
857 ~term:_Rfourier_gt_to_lt)
858 ~continuation:(exact ~term:h.hname)) ~status
859 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
860 ~term:_Rfourier_ge_to_le)
861 ~continuation:(exact ~term:h.hname)) ~status
862 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
863 ~term:_Rfourier_eqLR_to_le)
864 ~continuation:(exact ~term:h.hname)) ~status
865 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
866 ~term:_Rfourier_eqRL_to_le)
867 ~continuation:(exact ~term:h.hname)) ~status
870 debug("Fine TAC_USE\n");
878 Cic.Appl ( Cic.Const(u,boh)::next) ->
879 (match (UriManager.string_of_uri u) with
880 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
881 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
882 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
883 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
884 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
885 (match (List.hd next) with
886 Cic.Const (uri,_) when
887 UriManager.string_of_uri uri =
888 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
894 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
897 Cic.Appl(Array.to_list a)
900 (* Résolution d'inéquations linéaires dans R *)
901 let rec strip_outer_cast c = match c with
902 | Cic.Cast (c,_) -> strip_outer_cast c
906 (*let find_in_context id context =
907 let rec find_in_context_aux c n =
909 [] -> failwith (id^" not found in context")
910 | a::next -> (match a with
911 Some (Cic.Name(name),_) when name = id -> n
912 (*? magari al posto di _ qualcosaltro?*)
913 | _ -> find_in_context_aux next (n+1))
915 find_in_context_aux context 1
918 (* mi sembra quadratico *)
919 let rec filter_real_hyp context cont =
922 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
923 let n = find_in_context h cont in
924 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
925 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
926 | a::next -> debug(" no\n"); filter_real_hyp next cont
928 let filter_real_hyp context _ =
929 let rec filter_aux context num =
932 | Some(Cic.Name(h),Cic.Decl(t))::next ->
934 (*let n = find_in_context h cont in*)
935 debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
936 [(Cic.Rel(num),t)] @ filter_aux next (num+1)
938 | a::next -> filter_aux next (num+1)
944 (* lifts everithing at the conclusion level *)
945 let rec superlift c n=
948 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
949 CicSubstitution.lift n a))] @ superlift next (n+1)
950 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
951 CicSubstitution.lift n a))] @ superlift next (n+1)
952 | _::next -> superlift next (n+1) (*?? ??*)
956 let equality_replace a b ~status =
957 debug("inizio EQ\n");
958 let module C = Cic in
959 let proof,goal = status in
960 let curi,metasenv,pbo,pty = proof in
961 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
962 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
963 let fresh_meta = ProofEngineHelpers.new_meta proof in
965 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
966 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
967 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
969 rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
970 ~status:((curi,metasenv',pbo,pty),goal)
972 let new_goals = fresh_meta::goals in
973 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
974 ^string_of_int( List.length goals)^"+ meta\n");
978 let tcl_fail a ~status:(proof,goal) =
980 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
985 let assumption_tac ~status:(proof,goal)=
986 let curi,metasenv,pbo,pty = proof in
987 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
989 let tac_list = List.map
990 ( fun x -> num := !num + 1;
992 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
993 | _ -> ("fake",tcl_fail 1)
997 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
1000 (* !!!!! fix !!!!!!!!!! *)
1001 let contradiction_tac ~status:(proof,goal)=
1003 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
1004 ~continuation:(Tacticals.then_
1005 ~start:(Ring.elim_type_tac ~term:_False)
1006 ~continuation:(assumption_tac))
1007 ~status:(proof,goal)
1010 (* ********************* TATTICA ******************************** *)
1012 let rec fourier ~status:(s_proof,s_goal)=
1013 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
1014 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
1017 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
1018 debug_pcontext s_context;
1020 let fhyp = String.copy "new_hyp_for_fourier" in
1022 (* here we need to negate the thesis, but to do this we need to apply the right
1023 theoreme,so let's parse our thesis *)
1025 let th_to_appl = ref _Rfourier_not_le_gt in
1027 Cic.Appl ( Cic.Const(u,boh)::args) ->
1028 (match UriManager.string_of_uri u with
1029 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
1031 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
1033 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
1035 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
1037 |_-> failwith "fourier can't be applyed")
1038 |_-> failwith "fourier can't be applyed");
1039 (* fix maybe strip_outer_cast goes here?? *)
1041 (* now let's change our thesis applying the th and put it with hp *)
1043 let proof,gl = Tacticals.then_
1044 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
1045 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
1046 ~status:(s_proof,s_goal) in
1047 let goal = if List.length gl = 1 then List.hd gl
1048 else failwith "a new goal" in
1050 debug ("port la tesi sopra e la nego. contesto :\n");
1051 debug_pcontext s_context;
1053 (* now we have all the right environment *)
1055 let curi,metasenv,pbo,pty = proof in
1056 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1059 (* now we want to convert hp to inequations, but first we must lift
1060 everyting to thesis level, so that a variable has the save Rel(n)
1061 in each hp ( needed by ineq1_of_term ) *)
1063 (* ? fix if None ?????*)
1064 (* fix change superlift with a real name *)
1066 let l_context = superlift context 1 in
1067 let hyps = filter_real_hyp l_context l_context in
1069 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
1071 let lineq =ref [] in
1073 (* transform hyps into inequations *)
1075 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1080 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1083 let res=fourier_lineq (!lineq) in
1084 let tac=ref Tacticals.id_tac in
1086 (print_string "Tactic Fourier fails.\n";flush stdout;
1087 failwith "fourier_tac fails")
1090 match res with (*match res*)
1093 (* in lc we have the coefficient to "reduce" the system *)
1095 print_string "Fourier's method can prove the goal...\n";flush stdout;
1097 debug "I coeff di moltiplicazione rit sono: ";
1101 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1102 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1104 (List.combine (!lineq) lc);
1106 print_string (" quindi lutil e' lunga "^
1107 string_of_int (List.length (!lutil))^"\n");
1109 (* on construit la combinaison linéaire des inéquation *)
1111 (match (!lutil) with (*match (!lutil) *)
1113 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1115 let s=ref (h1.hstrict) in
1118 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1119 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1121 List.iter (fun (h,c) ->
1122 s:=(!s)||(h.hstrict);
1123 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1124 [_Rmult;rational_to_real c;h.hleft ] ]);
1125 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1126 [_Rmult;rational_to_real c;h.hright] ]))
1129 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1130 let tc=rational_to_real cres in
1133 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1135 debug "inizio a costruire tac1\n";
1136 Fourier.print_rational(c1);
1138 let tac1=ref ( fun ~status ->
1143 debug ("inizio t1 strict\n");
1144 let curi,metasenv,pbo,pty = proof in
1145 let metano,context,ty = List.find
1146 (function (m,_,_) -> m=goal) metasenv in
1147 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1148 debug ("ty = "^ CicPp.ppterm ty^"\n");
1149 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1150 ~continuations:[tac_use h1;tac_zero_inf_pos
1151 (rational_to_fraction c1)]
1156 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1157 ~continuations:[tac_use h1;tac_zero_inf_pos
1158 (rational_to_fraction c1)] ~status
1164 List.iter (fun (h,c) ->
1168 tac1:=(Tacticals.thens
1169 ~start:(PrimitiveTactics.apply_tac
1170 ~term:_Rfourier_lt_lt)
1171 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1172 (rational_to_fraction c)])
1176 Fourier.print_rational(c1);
1177 tac1:=(Tacticals.thens
1180 debug("INIZIO TAC 1 2\n");
1181 let curi,metasenv,pbo,pty = proof in
1182 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1184 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1185 debug ("ty = "^ CicPp.ppterm ty^"\n");
1186 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1187 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1188 (rational_to_fraction c)])
1194 tac1:=(Tacticals.thens
1195 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1196 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1197 (rational_to_fraction c)])
1201 tac1:=(Tacticals.thens
1202 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1203 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1204 (rational_to_fraction c)])
1208 s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1212 tac_zero_inf_false goal (rational_to_fraction cres)
1214 tac_zero_infeq_false goal (rational_to_fraction cres)
1216 tac:=(Tacticals.thens
1217 ~start:(my_cut ~term:ineq)
1218 ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
1219 ~start:(fun ~status:(proof,goal as status) ->
1220 let curi,metasenv,pbo,pty = proof in
1221 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1223 PrimitiveTactics.change_tac ~what:ty
1224 ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1225 ~continuation:(Tacticals.then_
1226 ~start:(PrimitiveTactics.apply_tac ~term:
1227 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1228 ~continuation:(Tacticals.thens
1231 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1232 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1235 (match r with (p,gl) ->
1236 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1238 ~continuations:[(Tacticals.thens
1241 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1242 (match r with (p,gl) ->
1243 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1246 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1247 ;Tacticals.try_tactics
1248 ~tactics:[ "ring", (fun ~status ->
1249 debug("begin RING\n");
1250 let r = Ring.ring_tac ~status in
1251 debug ("end RING\n");
1253 ; "id", Tacticals.id_tac]
1255 ;(*Tacticals.id_tac*)
1259 fun ~status:(proof,goal as status) ->
1260 let curi,metasenv,pbo,pty = proof in
1261 let metano,context,ty = List.find (function (m,_,_) -> m=
1263 (* check if ty is of type *)
1265 debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1267 Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1270 let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1271 debug("fine MY_CHNGE\n");
1275 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1276 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1278 |_-> assert false)(*match (!lutil) *)
1279 |_-> assert false); (*match res*)
1280 debug ("finalmente applico tac\n");
1282 let r = !tac ~status:(proof,goal) in
1283 debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1288 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;