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/Equality/eq.ind") ->
40 (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
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",0)
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
61 (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
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) ;
84 let simpl_tac ~status:(proof,goal) =
85 let curi,metasenv,pbo,pty = proof in
86 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
88 prerr_endline("simpl_tac su "^CicPp.ppterm ty);
90 let new_ty = ProofEngineReduction.simpl context ty in
92 prerr_endline("ritorna "^CicPp.ppterm new_ty);
97 (n,_,_) when n = metano -> (metano,context,new_ty)
101 (curi,new_metasenv,pbo,pty), [metano]
105 let rewrite_simpl_tac ~term ~status =
107 Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status
111 (******************** THE FOURIER TACTIC ***********************)
113 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
114 des inéquations et équations sont entiers. En attendant la tactique Field.
120 let debug x = print_string ("____ "^x) ; flush stdout;;
122 let debug_pcontext x =
124 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
125 a ^ " " | _ ->()) x ;
126 debug ("contesto : "^ (!str) ^ "\n")
129 (******************************************************************************
130 Operations on linear combinations.
132 Opérations sur les combinaisons linéaires affines.
133 La partie homogène d'une combinaison linéaire est en fait une table de hash
134 qui donne le coefficient d'un terme du calcul des constructions,
135 qui est zéro si le terme n'y est pas.
141 The type for linear combinations
143 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
147 @return an empty flin
149 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
155 @return the rational associated with x (coefficient)
159 (Hashtbl.find f.fhom x)
165 Adds c to the coefficient of x
172 let cx = flin_coef f x in
173 Hashtbl.remove f.fhom x;
174 Hashtbl.add f.fhom x (rplus cx c);
183 let flin_add_cste f c =
185 fcste=rplus f.fcste c}
189 @return a empty flin with r1 in fcste
191 let flin_one () = flin_add_cste (flin_zero()) r1;;
196 let flin_plus f1 f2 =
197 let f3 = flin_zero() in
198 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
199 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
200 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
206 let flin_minus f1 f2 =
207 let f3 = flin_zero() in
208 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
209 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
210 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
217 let f2 = flin_zero() in
218 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
219 flin_add_cste f2 (rmult a f.fcste);
223 (*****************************************************************************)
228 @return proiection on string of t
230 let rec string_of_term t =
232 Cic.Cast (t1,t2) -> string_of_term t1
233 |Cic.Const (u,boh) -> UriManager.string_of_uri u
234 |Cic.Var (u) -> UriManager.string_of_uri u
235 | _ -> "not_of_constant"
239 let string_of_constr = string_of_term
245 @raise Failure if conversion is impossible
246 @return rational proiection of t
248 let rec rational_of_term t =
249 (* fun to apply f to the first and second rational-term of l *)
250 let rat_of_binop f l =
251 let a = List.hd l and
252 b = List.hd(List.tl l) in
253 f (rational_of_term a) (rational_of_term b)
255 (* as before, but f is unary *)
256 let rat_of_unop f l =
257 f (rational_of_term (List.hd l))
260 | Cic.Cast (t1,t2) -> (rational_of_term t1)
261 | Cic.Appl (t1::next) ->
264 (match (UriManager.string_of_uri u) with
265 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
267 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
268 rat_of_unop rinv next
269 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
270 rat_of_binop rmult next
271 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
272 rat_of_binop rdiv next
273 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
274 rat_of_binop rplus next
275 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
276 rat_of_binop rminus next
277 | _ -> failwith "not a rational")
278 | _ -> failwith "not a rational")
279 | Cic.Const (u,boh) ->
280 (match (UriManager.string_of_uri u) with
281 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
282 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
283 | _ -> failwith "not a rational")
284 | _ -> failwith "not a rational"
288 let rational_of_const = rational_of_term;;
292 let rec flin_of_term t =
293 let fl_of_binop f l =
294 let a = List.hd l and
295 b = List.hd(List.tl l) in
296 f (flin_of_term a) (flin_of_term b)
300 | Cic.Cast (t1,t2) -> (flin_of_term t1)
301 | Cic.Appl (t1::next) ->
306 match (UriManager.string_of_uri u) with
307 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
308 flin_emult (rop r1) (flin_of_term (List.hd next))
309 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
310 fl_of_binop flin_plus next
311 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
312 fl_of_binop flin_minus next
313 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
315 let arg1 = (List.hd next) and
316 arg2 = (List.hd(List.tl next))
320 let a = rational_of_term arg1 in
323 let b = (rational_of_term arg2) in
324 (flin_add_cste (flin_zero()) (rmult a b))
327 _ -> (flin_add (flin_zero()) arg2 a)
330 _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
332 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
333 let a=(rational_of_term (List.hd next)) in
334 flin_add_cste (flin_zero()) (rinv a)
335 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
337 let b=(rational_of_term (List.hd(List.tl next))) in
340 let a = (rational_of_term (List.hd next)) in
341 (flin_add_cste (flin_zero()) (rdiv a b))
344 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
350 | Cic.Const (u,boh) ->
352 match (UriManager.string_of_uri u) with
353 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
354 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
358 with _ -> flin_add (flin_zero()) t r1
362 let flin_of_constr = flin_of_term;;
366 Translates a flin to (c,x) list
368 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
370 let flin_to_alist f =
372 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
376 (* Représentation des hypothèses qui sont des inéquations ou des équations.
380 The structure for ineq
382 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
383 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
390 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
393 let ineq1_of_term (h,t) =
394 match t with (* match t *)
395 Cic.Appl (t1::next) ->
396 let arg1= List.hd next in
397 let arg2= List.hd(List.tl next) in
398 (match t1 with (* match t1 *)
400 (match UriManager.string_of_uri u with (* match u *)
401 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
406 hflin= flin_minus (flin_of_term arg1)
409 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
414 hflin= flin_minus (flin_of_term arg2)
417 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
422 hflin= flin_minus (flin_of_term arg1)
425 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
430 hflin= flin_minus (flin_of_term arg2)
433 |_->assert false)(* match u *)
434 | Cic.MutInd (u,i,o) ->
435 (match UriManager.string_of_uri u with
436 "cic:/Coq/Init/Logic_Type/eqT.con" ->
439 let arg2= List.hd(List.tl (List.tl next)) in
442 (match UriManager.string_of_uri u with
443 "cic:/Coq/Reals/Rdefinitions/R.con"->
448 hflin= flin_minus (flin_of_term arg1)
455 hflin= flin_minus (flin_of_term arg2)
461 |_-> assert false)(* match t1 *)
462 |_-> assert false (* match t *)
465 let ineq1_of_constr = ineq1_of_term;;
468 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
474 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
477 let rec print_sys l =
480 | (a,b)::next -> (print_rl a;
481 print_string (if b=true then "strict\n"else"\n");
486 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
489 let fourier_lineq lineq1 =
491 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
493 Hashtbl.iter (fun x c ->
494 try (Hashtbl.find hvar x;())
495 with _-> nvar:=(!nvar)+1;
496 Hashtbl.add hvar x (!nvar))
500 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
501 let sys= List.map (fun h->
502 let v=Array.create ((!nvar)+1) r0 in
503 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
505 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
507 debug ("chiamo unsolvable sul sistema di "^
508 string_of_int (List.length sys) ^"\n");
513 (*****************************************************************************
514 Construction de la preuve en cas de succès de la méthode de Fourier,
515 i.e. on obtient une contradiction.
519 let _eqT = Cic.MutInd(UriManager.uri_of_string
520 "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
521 let _False = Cic.MutInd (UriManager.uri_of_string
522 "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
523 let _not = Cic.Const (UriManager.uri_of_string
524 "cic:/Coq/Init/Logic/not.con") 0;;
525 let _R0 = Cic.Const (UriManager.uri_of_string
526 "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
527 let _R1 = Cic.Const (UriManager.uri_of_string
528 "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
529 let _R = Cic.Const (UriManager.uri_of_string
530 "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
531 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
532 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
533 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
534 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
535 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
536 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
537 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
538 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
539 let _Rfourier_le=Cic.Const (UriManager.uri_of_string
540 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
541 let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
542 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
543 let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
544 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
545 let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
546 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
547 let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
548 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
549 let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
550 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
551 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
552 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
553 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
554 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
555 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
556 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
557 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
558 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
559 let _Rinv = Cic.Const (UriManager.uri_of_string
560 "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
561 let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
562 "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
563 let _Rle = Cic.Const (UriManager.uri_of_string
564 "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
565 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
566 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
567 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
568 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
569 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
570 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
571 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
572 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
573 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
574 "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
575 let _Rlt = Cic.Const (UriManager.uri_of_string
576 "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
577 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
578 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
579 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
580 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
581 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
582 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
583 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
584 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
585 let _Rminus = Cic.Const (UriManager.uri_of_string
586 "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
587 let _Rmult = Cic.Const (UriManager.uri_of_string
588 "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
589 let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
590 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
591 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
592 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
593 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
594 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
595 let _Ropp = Cic.Const (UriManager.uri_of_string
596 "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
597 let _Rplus = Cic.Const (UriManager.uri_of_string
598 "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
599 let _sym_eqT = Cic.Const(UriManager.uri_of_string
600 "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
602 (******************************************************************************)
604 let is_int x = (x.den)=1
607 (* fraction = couple (num,den) *)
608 let rec rational_to_fraction x= (x.num,x.den)
611 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
614 let rec int_to_real_aux n =
616 0 -> _R0 (* o forse R0 + R0 ????? *)
618 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
623 let x = int_to_real_aux (abs n) in
625 Cic.Appl [ _Ropp ; x ]
631 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
634 let rational_to_real x =
635 let (n,d)=rational_to_fraction x in
636 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
639 (* preuve que 0<n*1/d
642 let tac_zero_inf_pos (n,d) ~status =
643 (*let cste = pf_parse_constr gl in*)
644 let pall str ~status:(proof,goal) t =
645 debug ("tac "^str^" :\n" );
646 let curi,metasenv,pbo,pty = proof in
647 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
648 debug ("th = "^ CicPp.ppterm t ^"\n");
649 debug ("ty = "^ CicPp.ppterm ty^"\n");
652 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
653 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
655 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
656 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
660 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
661 ~status _Rlt_zero_pos_plus1;
662 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
663 ~continuation:!tacn);
666 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
667 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
668 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
673 debug("TAC ZERO INF POS\n");
675 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
684 (* preuve que 0<=n*1/d
687 let tac_zero_infeq_pos gl (n,d) ~status =
688 (*let cste = pf_parse_constr gl in*)
689 debug("inizio tac_zero_infeq_pos\n");
692 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
694 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
697 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
699 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
700 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
703 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
704 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
707 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
708 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
709 debug("fine tac_zero_infeq_pos\n");
715 (* preuve que 0<(-n)*(1/d) => False
718 let tac_zero_inf_false gl (n,d) ~status=
719 debug("inizio tac_zero_inf_false\n");
721 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
725 (debug "2\n";let r = (Tacticals.then_ ~start:(
726 fun ~status:(proof,goal as status) ->
727 let curi,metasenv,pbo,pty = proof in
728 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
729 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
730 ^ CicPp.ppterm ty ^"\n");
731 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
732 debug("!!!!!!!!!2\n");
735 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
741 (* preuve que 0<=(-n)*(1/d) => False
744 let tac_zero_infeq_false gl (n,d) ~status=
745 debug("stat tac_zero_infeq_false");
747 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
748 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
749 debug("stat tac_zero_infeq_false");
754 (* *********** ********** ******** ??????????????? *********** **************)
756 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
757 let curi,metasenv,pbo,pty = proof in
758 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
759 let fresh_meta = ProofEngineHelpers.new_meta proof in
761 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
762 let metasenv' = (fresh_meta,context,t)::metasenv in
763 let proof' = curi,metasenv',pbo,pty in
765 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta
766 (fresh_meta,irl),t))::al)) ~status:(proof',goal)
768 proof'',fresh_meta::goals
775 let my_cut ~term:c ~status:(proof,goal)=
776 let curi,metasenv,pbo,pty = proof in
777 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
779 let fresh_meta = ProofEngineHelpers.new_meta proof in
781 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
782 let metasenv' = (fresh_meta,context,c)::metasenv in
783 let proof' = curi,metasenv',pbo,pty in
785 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
786 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
787 ~status:(proof',goal)
789 (* We permute the generated goals to be consistent with Coq *)
792 | he::tl -> proof'',he::fresh_meta::tl
796 let exact = PrimitiveTactics.exact_tac;;
798 let tac_use h ~status:(proof,goal as status) =
799 debug("Inizio TC_USE\n");
800 let curi,metasenv,pbo,pty = proof in
801 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
802 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
803 debug ("ty = "^ CicPp.ppterm ty^"\n");
807 "Rlt" -> exact ~term:h.hname ~status
808 |"Rle" -> exact ~term:h.hname ~status
809 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
810 ~term:_Rfourier_gt_to_lt)
811 ~continuation:(exact ~term:h.hname)) ~status
812 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
813 ~term:_Rfourier_ge_to_le)
814 ~continuation:(exact ~term:h.hname)) ~status
815 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
816 ~term:_Rfourier_eqLR_to_le)
817 ~continuation:(exact ~term:h.hname)) ~status
818 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
819 ~term:_Rfourier_eqRL_to_le)
820 ~continuation:(exact ~term:h.hname)) ~status
823 debug("Fine TAC_USE\n");
831 Cic.Appl ( Cic.Const(u,boh)::next) ->
832 (match (UriManager.string_of_uri u) with
833 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
834 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
835 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
836 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
837 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
838 (match (List.hd next) with
839 Cic.Const (uri,_) when
840 UriManager.string_of_uri uri =
841 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
847 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
850 Cic.Appl(Array.to_list a)
853 (* Résolution d'inéquations linéaires dans R *)
854 let rec strip_outer_cast c = match c with
855 | Cic.Cast (c,_) -> strip_outer_cast c
859 let find_in_context id context =
860 let rec find_in_context_aux c n =
862 [] -> failwith (id^" not found in context")
863 | a::next -> (match a with
864 Some (Cic.Name(name),_) when name = id -> n
865 (*? magari al posto di _ qualcosaltro?*)
866 | _ -> find_in_context_aux next (n+1))
868 find_in_context_aux context 1
871 (* mi sembra quadratico *)
872 let rec filter_real_hyp context cont =
875 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
876 let n = find_in_context h cont in
877 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
878 | a::next -> debug(" no\n"); filter_real_hyp next cont
881 (* lifts everithing at the conclusion level *)
882 let rec superlift c n=
885 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
886 CicSubstitution.lift n a))] @ superlift next (n+1)
887 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
888 CicSubstitution.lift n a))] @ superlift next (n+1)
889 | _::next -> superlift next (n+1) (*?? ??*)
893 let equality_replace a b ~status =
894 debug("inizio EQ\n");
895 let module C = Cic in
896 let proof,goal = status in
897 let curi,metasenv,pbo,pty = proof in
898 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
899 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
900 let fresh_meta = ProofEngineHelpers.new_meta proof in
902 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
903 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
904 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
906 rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
907 ~status:((curi,metasenv',pbo,pty),goal)
909 let new_goals = fresh_meta::goals in
910 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
911 ^string_of_int( List.length goals)^"+ meta\n");
915 let tcl_fail a ~status:(proof,goal) =
917 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
922 let assumption_tac ~status:(proof,goal)=
923 let curi,metasenv,pbo,pty = proof in
924 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
926 let tac_list = List.map
927 ( fun x -> num := !num + 1;
929 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
930 | _ -> ("fake",tcl_fail 1)
934 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
937 (* !!!!! fix !!!!!!!!!! *)
938 let contradiction_tac ~status:(proof,goal)=
940 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
941 ~continuation:(Tacticals.then_
942 ~start:(Ring.elim_type_tac ~term:_False)
943 ~continuation:(assumption_tac))
947 (* ********************* TATTICA ******************************** *)
949 let rec fourier ~status:(s_proof,s_goal)=
950 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
951 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
954 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
955 debug_pcontext s_context;
957 let fhyp = String.copy "new_hyp_for_fourier" in
959 (* here we need to negate the thesis, but to do this we need to apply the right
960 theoreme,so let's parse our thesis *)
962 let th_to_appl = ref _Rfourier_not_le_gt in
964 Cic.Appl ( Cic.Const(u,boh)::args) ->
965 (match UriManager.string_of_uri u with
966 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
968 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
970 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
972 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
974 |_-> failwith "fourier can't be applyed")
975 |_-> failwith "fourier can't be applyed");
976 (* fix maybe strip_outer_cast goes here?? *)
978 (* now let's change our thesis applying the th and put it with hp *)
980 let proof,gl = Tacticals.then_
981 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
982 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
983 ~status:(s_proof,s_goal) in
984 let goal = if List.length gl = 1 then List.hd gl
985 else failwith "a new goal" in
987 debug ("port la tesi sopra e la nego. contesto :\n");
988 debug_pcontext s_context;
990 (* now we have all the right environment *)
992 let curi,metasenv,pbo,pty = proof in
993 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
996 (* now we want to convert hp to inequations, but first we must lift
997 everyting to thesis level, so that a variable has the save Rel(n)
998 in each hp ( needed by ineq1_of_term ) *)
1000 (* ? fix if None ?????*)
1001 (* fix change superlift with a real name *)
1003 let l_context = superlift context 1 in
1004 let hyps = filter_real_hyp l_context l_context in
1006 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
1008 let lineq =ref [] in
1010 (* transform hyps into inequations *)
1012 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1017 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1020 let res=fourier_lineq (!lineq) in
1021 let tac=ref Ring.id_tac in
1023 (print_string "Tactic Fourier fails.\n";flush stdout;
1024 failwith "fourier_tac fails")
1027 match res with (*match res*)
1030 (* in lc we have the coefficient to "reduce" the system *)
1032 print_string "Fourier's method can prove the goal...\n";flush stdout;
1034 debug "I coeff di moltiplicazione rit sono: ";
1038 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1039 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1041 (List.combine (!lineq) lc);
1043 print_string (" quindi lutil e' lunga "^
1044 string_of_int (List.length (!lutil))^"\n");
1046 (* on construit la combinaison linéaire des inéquation *)
1048 (match (!lutil) with (*match (!lutil) *)
1050 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1052 let s=ref (h1.hstrict) in
1055 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1056 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1058 List.iter (fun (h,c) ->
1059 s:=(!s)||(h.hstrict);
1060 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1061 [_Rmult;rational_to_real c;h.hleft ] ]);
1062 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1063 [_Rmult;rational_to_real c;h.hright] ]))
1066 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1067 let tc=rational_to_real cres in
1070 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1072 debug "inizio a costruire tac1\n";
1073 Fourier.print_rational(c1);
1075 let tac1=ref ( fun ~status ->
1080 debug ("inizio t1 strict\n");
1081 let curi,metasenv,pbo,pty = proof in
1082 let metano,context,ty = List.find
1083 (function (m,_,_) -> m=goal) metasenv in
1084 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1085 debug ("ty = "^ CicPp.ppterm ty^"\n");
1086 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1087 ~continuations:[tac_use h1;tac_zero_inf_pos
1088 (rational_to_fraction c1)]
1093 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1094 ~continuations:[tac_use h1;tac_zero_inf_pos
1095 (rational_to_fraction c1)] ~status
1101 List.iter (fun (h,c) ->
1105 tac1:=(Tacticals.thens
1106 ~start:(PrimitiveTactics.apply_tac
1107 ~term:_Rfourier_lt_lt)
1108 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1109 (rational_to_fraction c)])
1113 Fourier.print_rational(c1);
1114 tac1:=(Tacticals.thens
1117 debug("INIZIO TAC 1 2\n");
1118 let curi,metasenv,pbo,pty = proof in
1119 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1121 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1122 debug ("ty = "^ CicPp.ppterm ty^"\n");
1123 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1124 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1125 (rational_to_fraction c)])
1131 tac1:=(Tacticals.thens
1132 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1133 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1134 (rational_to_fraction c)])
1138 tac1:=(Tacticals.thens
1139 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1140 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1141 (rational_to_fraction c)])
1145 s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1149 tac_zero_inf_false goal (rational_to_fraction cres)
1151 tac_zero_infeq_false goal (rational_to_fraction cres)
1153 tac:=(Tacticals.thens
1154 ~start:(my_cut ~term:ineq)
1155 ~continuations:[Tacticals.then_
1156 ~start:(fun ~status:(proof,goal as status) ->
1157 let curi,metasenv,pbo,pty = proof in
1158 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1160 PrimitiveTactics.change_tac ~what:ty
1161 ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1162 ~continuation:(Tacticals.then_
1163 ~start:(PrimitiveTactics.apply_tac ~term:
1164 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1165 ~continuation:(Tacticals.thens
1168 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1171 (match r with (p,gl) ->
1172 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1174 ~continuations:[(Tacticals.thens
1177 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1178 (match r with (p,gl) ->
1179 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1182 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1183 (* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
1184 di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
1185 parametri della equality_replace vengono passati al contrario? Oppure la
1186 tattica usa i parametri al contrario?
1187 ~continuations:[Tacticals.then_
1189 fun ~status:(proof,goal as status) ->
1191 let curi,metasenv,pbo,pty = proof in
1192 let metano,context,ty = List.find (function (m,_,_) -> m=
1194 debug("ty = "^CicPp.ppterm ty^"\n");
1195 let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
1197 debug("fine ECCOCI\n");
1199 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1201 ;Tacticals.try_tactics
1202 ~tactics:[ "ring", (fun ~status ->
1203 debug("begin RING\n");
1204 let r = Ring.ring_tac ~status in
1205 debug ("end RING\n");
1207 ; "id", Ring.id_tac]
1209 (* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
1211 ;!tac1]);(*end tac:=*)
1212 tac:=(Tacticals.thens
1213 ~start:(PrimitiveTactics.cut_tac ~term:_False)
1214 ~continuations:[Tacticals.then_
1215 ~start:(PrimitiveTactics.intros_tac ~name:"??")
1216 ~continuation:contradiction_tac
1220 |_-> assert false)(*match (!lutil) *)
1221 |_-> assert false); (*match res*)
1222 debug ("finalmente applico tac\n");
1223 (!tac ~status:(proof,goal))
1226 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;