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 **********************)
28 (* Galla: moved in variousTactics.ml
30 let rewrite_tac ~term:equality ~status:(proof,goal) =
32 let module U = UriManager in
33 let curi,metasenv,pbo,pty = proof in
34 let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
35 let eq_ind_r,ty,t1,t2 =
36 match CicTypeChecker.type_of_aux' metasenv context equality with
37 C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
38 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
41 (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
44 | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
45 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
48 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
53 (ProofEngineTypes.Fail
54 "Rewrite: the argument is not a proof of an equality")
57 let gty' = CicSubstitution.lift 1 gty in
58 let t1' = CicSubstitution.lift 1 t1 in
60 ProofEngineReduction.replace_lifting
61 ~equality:ProofEngineReduction.alpha_equivalence
62 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
64 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
66 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
67 let fresh_meta = ProofEngineHelpers.new_meta proof in
69 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
70 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
73 PrimitiveTactics.exact_tac
75 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
76 ~status:((curi,metasenv',pbo,pty),goal)
78 assert (List.length goals = 0) ;
83 let rewrite_simpl_tac ~term ~status =
84 Tacticals.then_ ~start:(rewrite_tac ~term)
86 (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
91 (******************** THE FOURIER TACTIC ***********************)
93 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
94 des inéquations et équations sont entiers. En attendant la tactique Field.
100 let debug x = print_string ("____ "^x) ; flush stdout;;
102 let debug_pcontext x =
104 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
105 a ^ " " | _ ->()) x ;
106 debug ("contesto : "^ (!str) ^ "\n")
109 (******************************************************************************
110 Operations on linear combinations.
112 Opérations sur les combinaisons linéaires affines.
113 La partie homogène d'une combinaison linéaire est en fait une table de hash
114 qui donne le coefficient d'un terme du calcul des constructions,
115 qui est zéro si le terme n'y est pas.
121 The type for linear combinations
123 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
127 @return an empty flin
129 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
135 @return the rational associated with x (coefficient)
139 (Hashtbl.find f.fhom x)
145 Adds c to the coefficient of x
154 let cx = flin_coef f x in
155 Hashtbl.remove f.fhom x;
156 Hashtbl.add f.fhom x (rplus cx c);
158 |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n");
159 let cx = flin_coef f x in
160 Hashtbl.remove f.fhom x;
161 Hashtbl.add f.fhom x (rplus cx c);
170 let flin_add_cste f c =
172 fcste=rplus f.fcste c}
176 @return a empty flin with r1 in fcste
178 let flin_one () = flin_add_cste (flin_zero()) r1;;
183 let flin_plus f1 f2 =
184 let f3 = flin_zero() in
185 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
186 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
187 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
193 let flin_minus f1 f2 =
194 let f3 = flin_zero() in
195 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
196 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
197 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
204 let f2 = flin_zero() in
205 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
206 flin_add_cste f2 (rmult a f.fcste);
210 (*****************************************************************************)
215 @raise Failure if conversion is impossible
216 @return rational proiection of t
218 let rec rational_of_term t =
219 (* fun to apply f to the first and second rational-term of l *)
220 let rat_of_binop f l =
221 let a = List.hd l and
222 b = List.hd(List.tl l) in
223 f (rational_of_term a) (rational_of_term b)
225 (* as before, but f is unary *)
226 let rat_of_unop f l =
227 f (rational_of_term (List.hd l))
230 | Cic.Cast (t1,t2) -> (rational_of_term t1)
231 | Cic.Appl (t1::next) ->
234 (match (UriManager.string_of_uri u) with
235 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
237 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
238 rat_of_unop rinv next
239 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
240 rat_of_binop rmult next
241 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
242 rat_of_binop rdiv next
243 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
244 rat_of_binop rplus next
245 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
246 rat_of_binop rminus next
247 | _ -> failwith "not a rational")
248 | _ -> failwith "not a rational")
249 | Cic.Const (u,boh) ->
250 (match (UriManager.string_of_uri u) with
251 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
252 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
253 | _ -> failwith "not a rational")
254 | _ -> failwith "not a rational"
258 let rational_of_const = rational_of_term;;
268 let rec flin_of_term t =
269 let fl_of_binop f l =
270 let a = List.hd l and
271 b = List.hd(List.tl l) in
272 f (flin_of_term a) (flin_of_term b)
276 | Cic.Cast (t1,t2) -> (flin_of_term t1)
277 | Cic.Appl (t1::next) ->
282 match (UriManager.string_of_uri u) with
283 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
284 flin_emult (rop r1) (flin_of_term (List.hd next))
285 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
286 fl_of_binop flin_plus next
287 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
288 fl_of_binop flin_minus next
289 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
291 let arg1 = (List.hd next) and
292 arg2 = (List.hd(List.tl next))
294 if fails rational_of_term arg1
296 if fails rational_of_term arg2
298 ( (* prodotto tra 2 incognite ????? impossibile*)
299 failwith "Sistemi lineari!!!!\n"
304 Cic.Rel(n) -> (*trasformo al volo*)
305 (flin_add (flin_zero()) arg1 (rational_of_term arg2))
307 let tmp = flin_of_term arg1 in
308 flin_emult (rational_of_term arg2) (tmp)
311 if fails rational_of_term arg2
315 Cic.Rel(n) -> (*trasformo al volo*)
316 (flin_add (flin_zero()) arg2 (rational_of_term arg1))
318 let tmp = flin_of_term arg2 in
319 flin_emult (rational_of_term arg1) (tmp)
323 ( (*prodotto tra razionali*)
324 (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
328 (*let a = rational_of_term arg1 in
329 debug("ho fatto rational of term di "^CicPp.ppterm arg1^
330 " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
331 let a = flin_of_term arg1
334 let b = (rational_of_term arg2) in
335 debug("ho fatto rational of term di "^CicPp.ppterm arg2^
336 " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
337 (flin_add_cste (flin_zero()) (rmult a b))
340 _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
341 (flin_add (flin_zero()) arg2 a)
344 _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
345 (flin_add(flin_zero()) arg1 (rational_of_term arg2))
348 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
349 let a=(rational_of_term (List.hd next)) in
350 flin_add_cste (flin_zero()) (rinv a)
351 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
353 let b=(rational_of_term (List.hd(List.tl next))) in
356 let a = (rational_of_term (List.hd next)) in
357 (flin_add_cste (flin_zero()) (rdiv a b))
360 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
366 | Cic.Const (u,boh) ->
368 match (UriManager.string_of_uri u) with
369 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
370 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
374 with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
378 let flin_of_constr = flin_of_term;;
382 Translates a flin to (c,x) list
384 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
386 let flin_to_alist f =
388 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
392 (* Représentation des hypothèses qui sont des inéquations ou des équations.
396 The structure for ineq
398 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
399 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
406 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
409 let ineq1_of_term (h,t) =
410 match t with (* match t *)
411 Cic.Appl (t1::next) ->
412 let arg1= List.hd next in
413 let arg2= List.hd(List.tl next) in
414 (match t1 with (* match t1 *)
416 (match UriManager.string_of_uri u with (* match u *)
417 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
422 hflin= flin_minus (flin_of_term arg1)
425 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
430 hflin= flin_minus (flin_of_term arg2)
433 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
438 hflin= flin_minus (flin_of_term arg1)
441 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
446 hflin= flin_minus (flin_of_term arg2)
449 |_->assert false)(* match u *)
450 | Cic.MutInd (u,i,o) ->
451 (match UriManager.string_of_uri u with
452 "cic:/Coq/Init/Logic_Type/eqT.ind" ->
455 let arg2= List.hd(List.tl (List.tl next)) in
458 (match UriManager.string_of_uri u with
459 "cic:/Coq/Reals/Rdefinitions/R.con"->
464 hflin= flin_minus (flin_of_term arg1)
471 hflin= flin_minus (flin_of_term arg2)
477 |_-> assert false)(* match t1 *)
478 |_-> assert false (* match t *)
481 let ineq1_of_constr = ineq1_of_term;;
484 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
490 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
493 let rec print_sys l =
496 | (a,b)::next -> (print_rl a;
497 print_string (if b=true then "strict\n"else"\n");
502 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
505 let fourier_lineq lineq1 =
507 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
509 Hashtbl.iter (fun x c ->
510 try (Hashtbl.find hvar x;())
511 with _-> nvar:=(!nvar)+1;
512 Hashtbl.add hvar x (!nvar);
513 debug("aggiungo una var "^
514 string_of_int !nvar^" per "^
515 CicPp.ppterm x^"\n"))
519 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
520 let sys= List.map (fun h->
521 let v=Array.create ((!nvar)+1) r0 in
522 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c)
524 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
526 debug ("chiamo unsolvable sul sistema di "^
527 string_of_int (List.length sys) ^"\n");
532 (*****************************************************************************
533 Construction de la preuve en cas de succès de la méthode de Fourier,
534 i.e. on obtient une contradiction.
538 let _eqT = Cic.MutInd((UriManager.uri_of_string
539 "cic:/Coq/Init/Logic_Type/eqT.ind"), 0, []) ;;
540 let _False = Cic.MutInd ((UriManager.uri_of_string
541 "cic:/Coq/Init/Logic/False.ind"), 0, []) ;;
542 let _not = Cic.Const ((UriManager.uri_of_string
543 "cic:/Coq/Init/Logic/not.con"), []);;
544 let _R0 = Cic.Const ((UriManager.uri_of_string
545 "cic:/Coq/Reals/Rdefinitions/R0.con"), []) ;;
546 let _R1 = Cic.Const ((UriManager.uri_of_string
547 "cic:/Coq/Reals/Rdefinitions/R1.con"), []) ;;
548 let _R = Cic.Const ((UriManager.uri_of_string
549 "cic:/Coq/Reals/Rdefinitions/R.con"), []) ;;
550 let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string
551 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;;
552 let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string
553 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;;
554 let _Rfourier_ge_to_le =Cic.Const ((UriManager.uri_of_string
555 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;;
556 let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string
557 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;;
558 let _Rfourier_le=Cic.Const ((UriManager.uri_of_string
559 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;;
560 let _Rfourier_le_le =Cic.Const ((UriManager.uri_of_string
561 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con"), []) ;;
562 let _Rfourier_le_lt =Cic.Const ((UriManager.uri_of_string
563 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con"), []) ;;
564 let _Rfourier_lt=Cic.Const ((UriManager.uri_of_string
565 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con"), []) ;;
566 let _Rfourier_lt_le =Cic.Const ((UriManager.uri_of_string
567 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con"), []) ;;
568 let _Rfourier_lt_lt =Cic.Const ((UriManager.uri_of_string
569 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con"), []) ;;
570 let _Rfourier_not_ge_lt = Cic.Const ((UriManager.uri_of_string
571 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con"), []) ;;
572 let _Rfourier_not_gt_le = Cic.Const ((UriManager.uri_of_string
573 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con"), []) ;;
574 let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string
575 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;;
576 let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string
577 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;;
578 let _Rinv = Cic.Const ((UriManager.uri_of_string
579 "cic:/Coq/Reals/Rdefinitions/Rinv.con"), []) ;;
580 let _Rinv_R1 = Cic.Const((UriManager.uri_of_string
581 "cic:/Coq/Reals/Rbase/Rinv_R1.con" ), []) ;;
582 let _Rle = Cic.Const ((UriManager.uri_of_string
583 "cic:/Coq/Reals/Rdefinitions/Rle.con"), []) ;;
584 let _Rle_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
585 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;;
586 let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string
587 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con"), []) ;;
588 let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string
589 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;;
590 let _Rle_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
591 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;;
592 (*let _Rle_zero_zero = Cic.Const ((UriManager.uri_of_string
593 "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con"), []) ;;*)
594 let _Rlt = Cic.Const ((UriManager.uri_of_string
595 "cic:/Coq/Reals/Rdefinitions/Rlt.con"), []) ;;
596 let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
597 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;;
598 let _Rlt_not_le = Cic.Const ((UriManager.uri_of_string
599 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con"), []) ;;
600 let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string
601 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;;
602 let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
603 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;;
604 let _Rminus = Cic.Const ((UriManager.uri_of_string
605 "cic:/Coq/Reals/Rdefinitions/Rminus.con"), []) ;;
606 let _Rmult = Cic.Const ((UriManager.uri_of_string
607 "cic:/Coq/Reals/Rdefinitions/Rmult.con"), []) ;;
608 let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string
609 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;;
610 let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string
611 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;;
612 let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string
613 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;;
614 let _Ropp = Cic.Const ((UriManager.uri_of_string
615 "cic:/Coq/Reals/Rdefinitions/Ropp.con"), []) ;;
616 let _Rplus = Cic.Const ((UriManager.uri_of_string
617 "cic:/Coq/Reals/Rdefinitions/Rplus.con"), []) ;;
619 (******************************************************************************)
621 let is_int x = (x.den)=1
624 (* fraction = couple (num,den) *)
625 let rec rational_to_fraction x= (x.num,x.den)
628 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
631 let rec int_to_real_aux n =
633 0 -> _R0 (* o forse R0 + R0 ????? *)
635 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
640 let x = int_to_real_aux (abs n) in
642 Cic.Appl [ _Ropp ; x ]
648 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
651 let rational_to_real x =
652 let (n,d)=rational_to_fraction x in
653 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
656 (* preuve que 0<n*1/d
659 let tac_zero_inf_pos (n,d) ~status =
660 (*let cste = pf_parse_constr gl in*)
661 let pall str ~status:(proof,goal) t =
662 debug ("tac "^str^" :\n" );
663 let curi,metasenv,pbo,pty = proof in
664 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
665 debug ("th = "^ CicPp.ppterm t ^"\n");
666 debug ("ty = "^ CicPp.ppterm ty^"\n");
669 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
670 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
672 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
673 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
677 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
678 ~status _Rlt_zero_pos_plus1;
679 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
680 ~continuation:!tacn);
683 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
684 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
685 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
690 debug("TAC ZERO INF POS\n");
692 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
701 (* preuve que 0<=n*1/d
704 let tac_zero_infeq_pos gl (n,d) ~status =
705 (*let cste = pf_parse_constr gl in*)
706 debug("inizio tac_zero_infeq_pos\n");
709 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
711 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
714 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
716 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
717 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
720 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
721 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
724 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
725 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
726 debug("fine tac_zero_infeq_pos\n");
732 (* preuve que 0<(-n)*(1/d) => False
735 let tac_zero_inf_false gl (n,d) ~status=
736 debug("inizio tac_zero_inf_false\n");
738 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
742 (debug "2\n";let r = (Tacticals.then_ ~start:(
743 fun ~status:(proof,goal as status) ->
744 let curi,metasenv,pbo,pty = proof in
745 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
746 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
747 ^ CicPp.ppterm ty ^"\n");
748 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
749 debug("!!!!!!!!!2\n");
752 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
758 (* preuve que 0<=n*(1/d) => False ; n est negatif
761 let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
762 debug("stat tac_zero_infeq_false\n");
764 let curi,metasenv,pbo,pty = proof in
765 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
767 debug("faccio fold di " ^ CicPp.ppterm
771 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
774 debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
775 (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
778 (ReductionTactics.fold_tac ~reduction:CicReduction.whd
779 ~also_in_hypotheses:false
784 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
789 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
790 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
791 debug("end tac_zero_infeq_false\n");
794 Tacticals.id_tac ~status
799 (* *********** ********** ******** ??????????????? *********** **************)
801 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
802 let curi,metasenv,pbo,pty = proof in
803 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
804 let fresh_meta = ProofEngineHelpers.new_meta proof in
806 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
807 let metasenv' = (fresh_meta,context,t)::metasenv in
808 let proof' = curi,metasenv',pbo,pty in
810 PrimitiveTactics.apply_tac
811 (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
812 ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
813 ~status:(proof',goal)
815 proof'',fresh_meta::goals
822 let my_cut ~term:c ~status:(proof,goal)=
823 let curi,metasenv,pbo,pty = proof in
824 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
826 debug("my_cut di "^CicPp.ppterm c^"\n");
829 let fresh_meta = ProofEngineHelpers.new_meta proof in
831 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
832 let metasenv' = (fresh_meta,context,c)::metasenv in
833 let proof' = curi,metasenv',pbo,pty in
835 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
836 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
837 ~status:(proof',goal)
839 (* We permute the generated goals to be consistent with Coq *)
842 | he::tl -> proof'',he::fresh_meta::tl
846 let exact = PrimitiveTactics.exact_tac;;
848 let tac_use h ~status:(proof,goal as status) =
849 debug("Inizio TC_USE\n");
850 let curi,metasenv,pbo,pty = proof in
851 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
852 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
853 debug ("ty = "^ CicPp.ppterm ty^"\n");
857 "Rlt" -> exact ~term:h.hname ~status
858 |"Rle" -> exact ~term:h.hname ~status
859 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
860 ~term:_Rfourier_gt_to_lt)
861 ~continuation:(exact ~term:h.hname)) ~status
862 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
863 ~term:_Rfourier_ge_to_le)
864 ~continuation:(exact ~term:h.hname)) ~status
865 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
866 ~term:_Rfourier_eqLR_to_le)
867 ~continuation:(exact ~term:h.hname)) ~status
868 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
869 ~term:_Rfourier_eqRL_to_le)
870 ~continuation:(exact ~term:h.hname)) ~status
873 debug("Fine TAC_USE\n");
881 Cic.Appl ( Cic.Const(u,boh)::next) ->
882 (match (UriManager.string_of_uri u) with
883 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
884 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
885 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
886 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
887 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
888 (match (List.hd next) with
889 Cic.Const (uri,_) when
890 UriManager.string_of_uri uri =
891 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
897 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
900 Cic.Appl(Array.to_list a)
903 (* Résolution d'inéquations linéaires dans R *)
904 let rec strip_outer_cast c = match c with
905 | Cic.Cast (c,_) -> strip_outer_cast c
909 (*let find_in_context id context =
910 let rec find_in_context_aux c n =
912 [] -> failwith (id^" not found in context")
913 | a::next -> (match a with
914 Some (Cic.Name(name),_) when name = id -> n
915 (*? magari al posto di _ qualcosaltro?*)
916 | _ -> find_in_context_aux next (n+1))
918 find_in_context_aux context 1
921 (* mi sembra quadratico *)
922 let rec filter_real_hyp context cont =
925 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
926 let n = find_in_context h cont in
927 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
928 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
929 | a::next -> debug(" no\n"); filter_real_hyp next cont
931 let filter_real_hyp context _ =
932 let rec filter_aux context num =
935 | Some(Cic.Name(h),Cic.Decl(t))::next ->
937 (*let n = find_in_context h cont in*)
938 debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
939 [(Cic.Rel(num),t)] @ filter_aux next (num+1)
941 | a::next -> filter_aux next (num+1)
947 (* lifts everithing at the conclusion level *)
948 let rec superlift c n=
951 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
952 CicSubstitution.lift n a))] @ superlift next (n+1)
953 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
954 CicSubstitution.lift n a))] @ superlift next (n+1)
955 | _::next -> superlift next (n+1) (*?? ??*)
959 let equality_replace a b ~status =
960 debug("inizio EQ\n");
961 let module C = Cic in
962 let proof,goal = status in
963 let curi,metasenv,pbo,pty = proof in
964 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
965 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
966 let fresh_meta = ProofEngineHelpers.new_meta proof in
968 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
969 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
970 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
972 EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
973 ~status:((curi,metasenv',pbo,pty),goal)
975 let new_goals = fresh_meta::goals in
976 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
977 ^string_of_int( List.length goals)^"+ meta\n");
981 let tcl_fail a ~status:(proof,goal) =
983 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
987 (* Galla: moved in variousTactics.ml
988 let assumption_tac ~status:(proof,goal)=
989 let curi,metasenv,pbo,pty = proof in
990 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
992 let tac_list = List.map
993 ( fun x -> num := !num + 1;
995 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
996 | _ -> ("fake",tcl_fail 1)
1000 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
1003 (* Galla: moved in negationTactics.ml
1004 (* !!!!! fix !!!!!!!!!! *)
1005 let contradiction_tac ~status:(proof,goal)=
1007 (*inutile sia questo che quello prima della chiamata*)
1008 ~start:PrimitiveTactics.intros_tac
1009 ~continuation:(Tacticals.then_
1010 ~start:(VariousTactics.elim_type_tac ~term:_False)
1011 ~continuation:(assumption_tac))
1012 ~status:(proof,goal)
1016 (* ********************* TATTICA ******************************** *)
1018 let rec fourier ~status:(s_proof,s_goal)=
1019 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
1020 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
1023 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
1024 debug_pcontext s_context;
1026 let fhyp = String.copy "new_hyp_for_fourier" in
1028 (* here we need to negate the thesis, but to do this we need to apply the right
1029 theoreme,so let's parse our thesis *)
1031 let th_to_appl = ref _Rfourier_not_le_gt in
1033 Cic.Appl ( Cic.Const(u,boh)::args) ->
1034 (match UriManager.string_of_uri u with
1035 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
1037 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
1039 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
1041 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
1043 |_-> failwith "fourier can't be applyed")
1044 |_-> failwith "fourier can't be applyed");
1045 (* fix maybe strip_outer_cast goes here?? *)
1047 (* now let's change our thesis applying the th and put it with hp *)
1051 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
1052 ~continuation:(PrimitiveTactics.intros_tac ())
1053 ~status:(s_proof,s_goal) in
1054 let goal = if List.length gl = 1 then List.hd gl
1055 else failwith "a new goal" in
1057 debug ("port la tesi sopra e la nego. contesto :\n");
1058 debug_pcontext s_context;
1060 (* now we have all the right environment *)
1062 let curi,metasenv,pbo,pty = proof in
1063 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1066 (* now we want to convert hp to inequations, but first we must lift
1067 everyting to thesis level, so that a variable has the save Rel(n)
1068 in each hp ( needed by ineq1_of_term ) *)
1070 (* ? fix if None ?????*)
1071 (* fix change superlift with a real name *)
1073 let l_context = superlift context 1 in
1074 let hyps = filter_real_hyp l_context l_context in
1076 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
1078 let lineq =ref [] in
1080 (* transform hyps into inequations *)
1082 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1087 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1090 let res=fourier_lineq (!lineq) in
1091 let tac=ref Tacticals.id_tac in
1093 (print_string "Tactic Fourier fails.\n";flush stdout;
1094 failwith "fourier_tac fails")
1097 match res with (*match res*)
1100 (* in lc we have the coefficient to "reduce" the system *)
1102 print_string "Fourier's method can prove the goal...\n";flush stdout;
1104 debug "I coeff di moltiplicazione rit sono: ";
1108 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1109 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1111 (List.combine (!lineq) lc);
1113 print_string (" quindi lutil e' lunga "^
1114 string_of_int (List.length (!lutil))^"\n");
1116 (* on construit la combinaison linéaire des inéquation *)
1118 (match (!lutil) with (*match (!lutil) *)
1120 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1122 let s=ref (h1.hstrict) in
1125 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1126 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1128 List.iter (fun (h,c) ->
1129 s:=(!s)||(h.hstrict);
1130 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1131 [_Rmult;rational_to_real c;h.hleft ] ]);
1132 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1133 [_Rmult;rational_to_real c;h.hright] ]))
1136 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1137 let tc=rational_to_real cres in
1140 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1142 debug "inizio a costruire tac1\n";
1143 Fourier.print_rational(c1);
1145 let tac1=ref ( fun ~status ->
1150 debug ("inizio t1 strict\n");
1151 let curi,metasenv,pbo,pty = proof in
1152 let metano,context,ty = List.find
1153 (function (m,_,_) -> m=goal) metasenv in
1154 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1155 debug ("ty = "^ CicPp.ppterm ty^"\n");
1156 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1157 ~continuations:[tac_use h1;tac_zero_inf_pos
1158 (rational_to_fraction c1)]
1163 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1164 ~continuations:[tac_use h1;tac_zero_inf_pos
1165 (rational_to_fraction c1)] ~status
1171 List.iter (fun (h,c) ->
1175 tac1:=(Tacticals.thens
1176 ~start:(PrimitiveTactics.apply_tac
1177 ~term:_Rfourier_lt_lt)
1178 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1179 (rational_to_fraction c)])
1183 Fourier.print_rational(c1);
1184 tac1:=(Tacticals.thens
1187 debug("INIZIO TAC 1 2\n");
1188 let curi,metasenv,pbo,pty = proof in
1189 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1191 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1192 debug ("ty = "^ CicPp.ppterm ty^"\n");
1193 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1194 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1195 (rational_to_fraction c)])
1201 tac1:=(Tacticals.thens
1202 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1203 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1204 (rational_to_fraction c)])
1208 tac1:=(Tacticals.thens
1209 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1210 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1211 (rational_to_fraction c)])
1215 s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1219 tac_zero_inf_false goal (rational_to_fraction cres)
1221 tac_zero_infeq_false goal (rational_to_fraction cres)
1223 tac:=(Tacticals.thens
1224 ~start:(my_cut ~term:ineq)
1225 ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
1226 ~start:(fun ~status:(proof,goal as status) ->
1227 let curi,metasenv,pbo,pty = proof in
1228 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1230 PrimitiveTactics.change_tac ~what:ty
1231 ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1232 ~continuation:(Tacticals.then_
1233 ~start:(PrimitiveTactics.apply_tac ~term:
1234 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1235 ~continuation:(Tacticals.thens
1238 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1239 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1242 (match r with (p,gl) ->
1243 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1245 ~continuations:[(Tacticals.thens
1248 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1249 (match r with (p,gl) ->
1250 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1253 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1254 ;Tacticals.try_tactics
1255 ~tactics:[ "ring", (fun ~status ->
1256 debug("begin RING\n");
1257 let r = Ring.ring_tac ~status in
1258 debug ("end RING\n");
1260 ; "id", Tacticals.id_tac]
1262 ;(*Tacticals.id_tac*)
1266 fun ~status:(proof,goal as status) ->
1267 let curi,metasenv,pbo,pty = proof in
1268 let metano,context,ty = List.find (function (m,_,_) -> m=
1270 (* check if ty is of type *)
1272 debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1274 Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1277 let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1278 debug("fine MY_CHNGE\n");
1282 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1283 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1285 |_-> assert false)(*match (!lutil) *)
1286 |_-> assert false); (*match res*)
1287 debug ("finalmente applico tac\n");
1289 let r = !tac ~status:(proof,goal) in
1290 debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1295 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;