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) ;
82 (******************** THE FOURIER TACTIC ***********************)
84 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
85 des inéquations et équations sont entiers. En attendant la tactique Field.
91 let debug x = print_string ("____ "^x) ; flush stdout;;
93 let debug_pcontext x =
95 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
97 debug ("contesto : "^ (!str) ^ "\n")
100 (******************************************************************************
101 Operations on linear combinations.
103 Opérations sur les combinaisons linéaires affines.
104 La partie homogène d'une combinaison linéaire est en fait une table de hash
105 qui donne le coefficient d'un terme du calcul des constructions,
106 qui est zéro si le terme n'y est pas.
112 The type for linear combinations
114 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
118 @return an empty flin
120 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
126 @return the rational associated with x (coefficient)
130 (Hashtbl.find f.fhom x)
136 Adds c to the coefficient of x
143 let cx = flin_coef f x in
144 Hashtbl.remove f.fhom x;
145 Hashtbl.add f.fhom x (rplus cx c);
154 let flin_add_cste f c =
156 fcste=rplus f.fcste c}
160 @return a empty flin with r1 in fcste
162 let flin_one () = flin_add_cste (flin_zero()) r1;;
167 let flin_plus f1 f2 =
168 let f3 = flin_zero() in
169 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
170 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
171 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
177 let flin_minus f1 f2 =
178 let f3 = flin_zero() in
179 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
180 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
181 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
188 let f2 = flin_zero() in
189 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
190 flin_add_cste f2 (rmult a f.fcste);
194 (*****************************************************************************)
199 @return proiection on string of t
201 let rec string_of_term t =
203 Cic.Cast (t1,t2) -> string_of_term t1
204 |Cic.Const (u,boh) -> UriManager.string_of_uri u
205 |Cic.Var (u) -> UriManager.string_of_uri u
206 | _ -> "not_of_constant"
210 let string_of_constr = string_of_term
216 @raise Failure if conversion is impossible
217 @return rational proiection of t
219 let rec rational_of_term t =
220 (* fun to apply f to the first and second rational-term of l *)
221 let rat_of_binop f l =
222 let a = List.hd l and
223 b = List.hd(List.tl l) in
224 f (rational_of_term a) (rational_of_term b)
226 (* as before, but f is unary *)
227 let rat_of_unop f l =
228 f (rational_of_term (List.hd l))
231 | Cic.Cast (t1,t2) -> (rational_of_term t1)
232 | Cic.Appl (t1::next) ->
235 (match (UriManager.string_of_uri u) with
236 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
238 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
239 rat_of_unop rinv next
240 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
241 rat_of_binop rmult next
242 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
243 rat_of_binop rdiv next
244 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
245 rat_of_binop rplus next
246 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
247 rat_of_binop rminus next
248 | _ -> failwith "not a rational")
249 | _ -> failwith "not a rational")
250 | Cic.Const (u,boh) ->
251 (match (UriManager.string_of_uri u) with
252 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
253 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
254 | _ -> failwith "not a rational")
255 | _ -> failwith "not a rational"
259 let rational_of_const = rational_of_term;;
263 let rec flin_of_term t =
264 let fl_of_binop f l =
265 let a = List.hd l and
266 b = List.hd(List.tl l) in
267 f (flin_of_term a) (flin_of_term b)
271 | Cic.Cast (t1,t2) -> (flin_of_term t1)
272 | Cic.Appl (t1::next) ->
277 match (UriManager.string_of_uri u) with
278 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
279 flin_emult (rop r1) (flin_of_term (List.hd next))
280 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
281 fl_of_binop flin_plus next
282 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
283 fl_of_binop flin_minus next
284 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
286 let arg1 = (List.hd next) and
287 arg2 = (List.hd(List.tl next))
291 let a = rational_of_term arg1 in
294 let b = (rational_of_term arg2) in
295 (flin_add_cste (flin_zero()) (rmult a b))
298 _ -> (flin_add (flin_zero()) arg2 a)
301 _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
303 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
304 let a=(rational_of_term (List.hd next)) in
305 flin_add_cste (flin_zero()) (rinv a)
306 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
308 let b=(rational_of_term (List.hd(List.tl next))) in
311 let a = (rational_of_term (List.hd next)) in
312 (flin_add_cste (flin_zero()) (rdiv a b))
315 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
321 | Cic.Const (u,boh) ->
323 match (UriManager.string_of_uri u) with
324 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
325 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
329 with _ -> flin_add (flin_zero()) t r1
333 let flin_of_constr = flin_of_term;;
337 Translates a flin to (c,x) list
339 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
341 let flin_to_alist f =
343 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
347 (* Représentation des hypothèses qui sont des inéquations ou des équations.
351 The structure for ineq
353 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
354 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
361 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
364 let ineq1_of_term (h,t) =
365 match t with (* match t *)
366 Cic.Appl (t1::next) ->
367 let arg1= List.hd next in
368 let arg2= List.hd(List.tl next) in
369 (match t1 with (* match t1 *)
371 (match UriManager.string_of_uri u with (* match u *)
372 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
377 hflin= flin_minus (flin_of_term arg1)
380 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
385 hflin= flin_minus (flin_of_term arg2)
388 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
393 hflin= flin_minus (flin_of_term arg1)
396 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
401 hflin= flin_minus (flin_of_term arg2)
404 |_->assert false)(* match u *)
405 | Cic.MutInd (u,i,o) ->
406 (match UriManager.string_of_uri u with
407 "cic:/Coq/Init/Logic_Type/eqT.con" ->
410 let arg2= List.hd(List.tl (List.tl next)) in
413 (match UriManager.string_of_uri u with
414 "cic:/Coq/Reals/Rdefinitions/R.con"->
419 hflin= flin_minus (flin_of_term arg1)
426 hflin= flin_minus (flin_of_term arg2)
432 |_-> assert false)(* match t1 *)
433 |_-> assert false (* match t *)
436 let ineq1_of_constr = ineq1_of_term;;
439 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
445 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
448 let rec print_sys l =
451 | (a,b)::next -> (print_rl a;
452 print_string (if b=true then "strict\n"else"\n");
457 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
460 let fourier_lineq lineq1 =
462 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
464 Hashtbl.iter (fun x c ->
465 try (Hashtbl.find hvar x;())
466 with _-> nvar:=(!nvar)+1;
467 Hashtbl.add hvar x (!nvar))
471 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
472 let sys= List.map (fun h->
473 let v=Array.create ((!nvar)+1) r0 in
474 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
476 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
478 debug ("chiamo unsolvable sul sistema di "^
479 string_of_int (List.length sys) ^"\n");
484 (*****************************************************************************
485 Construction de la preuve en cas de succès de la méthode de Fourier,
486 i.e. on obtient une contradiction.
490 let _eqT = Cic.MutInd(UriManager.uri_of_string
491 "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
492 let _False = Cic.MutInd (UriManager.uri_of_string
493 "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
494 let _not = Cic.Const (UriManager.uri_of_string
495 "cic:/Coq/Init/Logic/not.con") 0;;
496 let _R0 = Cic.Const (UriManager.uri_of_string
497 "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
498 let _R1 = Cic.Const (UriManager.uri_of_string
499 "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
500 let _R = Cic.Const (UriManager.uri_of_string
501 "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
502 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
503 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
504 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
505 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
506 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
507 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
508 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
509 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
510 let _Rfourier_le=Cic.Const (UriManager.uri_of_string
511 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
512 let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
513 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
514 let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
515 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
516 let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
517 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
518 let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
519 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
520 let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
521 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
522 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
523 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
524 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
525 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
526 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
527 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
528 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
529 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
530 let _Rinv = Cic.Const (UriManager.uri_of_string
531 "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
532 let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
533 "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
534 let _Rle = Cic.Const (UriManager.uri_of_string
535 "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
536 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
537 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
538 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
539 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
540 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
541 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
542 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
543 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
544 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
545 "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
546 let _Rlt = Cic.Const (UriManager.uri_of_string
547 "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
548 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
549 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
550 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
551 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
552 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
553 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
554 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
555 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
556 let _Rminus = Cic.Const (UriManager.uri_of_string
557 "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
558 let _Rmult = Cic.Const (UriManager.uri_of_string
559 "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
560 let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
561 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
562 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
563 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
564 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
565 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
566 let _Ropp = Cic.Const (UriManager.uri_of_string
567 "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
568 let _Rplus = Cic.Const (UriManager.uri_of_string
569 "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
570 let _sym_eqT = Cic.Const(UriManager.uri_of_string
571 "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
573 (******************************************************************************)
575 let is_int x = (x.den)=1
578 (* fraction = couple (num,den) *)
579 let rec rational_to_fraction x= (x.num,x.den)
582 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
585 let rec int_to_real_aux n =
587 0 -> _R0 (* o forse R0 + R0 ????? *)
589 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
594 let x = int_to_real_aux (abs n) in
596 Cic.Appl [ _Ropp ; x ]
602 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
605 let rational_to_real x =
606 let (n,d)=rational_to_fraction x in
607 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
610 (* preuve que 0<n*1/d
613 let tac_zero_inf_pos (n,d) ~status =
614 (*let cste = pf_parse_constr gl in*)
615 let pall str ~status:(proof,goal) t =
616 debug ("tac "^str^" :\n" );
617 let curi,metasenv,pbo,pty = proof in
618 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
619 debug ("th = "^ CicPp.ppterm t ^"\n");
620 debug ("ty = "^ CicPp.ppterm ty^"\n");
623 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
624 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
626 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
627 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
631 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
632 ~status _Rlt_zero_pos_plus1;
633 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
634 ~continuation:!tacn);
637 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
638 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
639 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
644 debug("TAC ZERO INF POS\n");
646 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
655 (* preuve que 0<=n*1/d
658 let tac_zero_infeq_pos gl (n,d) ~status =
659 (*let cste = pf_parse_constr gl in*)
660 debug("inizio tac_zero_infeq_pos\n");
663 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
665 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
668 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
670 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
671 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
674 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
675 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
678 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
679 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
680 debug("fine tac_zero_infeq_pos\n");
686 (* preuve que 0<(-n)*(1/d) => False
689 let tac_zero_inf_false gl (n,d) ~status=
690 debug("inizio tac_zero_inf_false\n");
692 (debug "1\n";let r = (PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
696 (debug "2\n";let r = (Tacticals.then_ ~start:(
697 fun ~status:(proof,goal as status) ->
698 let curi,metasenv,pbo,pty = proof in
699 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
701 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
702 ^ CicPp.ppterm ty ^"\n");
704 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
706 debug("!!!!!!!!!2\n");
711 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
717 (* preuve que 0<=(-n)*(1/d) => False
720 let tac_zero_infeq_false gl (n,d) ~status=
721 debug("stat tac_zero_infeq_false");
723 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
724 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
725 debug("stat tac_zero_infeq_false");
730 (* *********** ********** ******** ??????????????? *********** **************)
732 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
733 let curi,metasenv,pbo,pty = proof in
734 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
735 let fresh_meta = ProofEngineHelpers.new_meta proof in
737 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
738 let metasenv' = (fresh_meta,context,t)::metasenv in
739 let proof' = curi,metasenv',pbo,pty in
741 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta
742 (fresh_meta,irl),t))::al)) ~status:(proof',goal)
744 proof'',fresh_meta::goals
751 let my_cut ~term:c ~status:(proof,goal)=
752 let curi,metasenv,pbo,pty = proof in
753 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
755 let fresh_meta = ProofEngineHelpers.new_meta proof in
757 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
758 let metasenv' = (fresh_meta,context,c)::metasenv in
759 let proof' = curi,metasenv',pbo,pty in
761 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
762 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
763 ~status:(proof',goal)
765 (* We permute the generated goals to be consistent with Coq *)
768 | he::tl -> proof'',he::fresh_meta::tl
772 let exact = PrimitiveTactics.exact_tac;;
774 let tac_use h ~status:(proof,goal as status) =
775 debug("Inizio TC_USE\n");
776 let curi,metasenv,pbo,pty = proof in
777 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
778 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
779 debug ("ty = "^ CicPp.ppterm ty^"\n");
783 "Rlt" -> exact ~term:h.hname ~status
784 |"Rle" -> exact ~term:h.hname ~status
785 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
786 ~term:_Rfourier_gt_to_lt)
787 ~continuation:(exact ~term:h.hname)) ~status
788 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
789 ~term:_Rfourier_ge_to_le)
790 ~continuation:(exact ~term:h.hname)) ~status
791 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
792 ~term:_Rfourier_eqLR_to_le)
793 ~continuation:(exact ~term:h.hname)) ~status
794 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
795 ~term:_Rfourier_eqRL_to_le)
796 ~continuation:(exact ~term:h.hname)) ~status
799 debug("Fine TAC_USE\n");
807 Cic.Appl ( Cic.Const(u,boh)::next) ->
808 (match (UriManager.string_of_uri u) with
809 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
810 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
811 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
812 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
813 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
814 (match (List.hd next) with
815 Cic.Const (uri,_) when
816 UriManager.string_of_uri uri =
817 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
823 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
826 Cic.Appl(Array.to_list a)
829 (* Résolution d'inéquations linéaires dans R *)
830 let rec strip_outer_cast c = match c with
831 | Cic.Cast (c,_) -> strip_outer_cast c
835 let find_in_context id context =
836 let rec find_in_context_aux c n =
838 [] -> failwith (id^" not found in context")
839 | a::next -> (match a with
840 Some (Cic.Name(name),_) when name = id -> n
841 (*? magari al posto di _ qualcosaltro?*)
842 | _ -> find_in_context_aux next (n+1))
844 find_in_context_aux context 1
847 (* mi sembra quadratico *)
848 let rec filter_real_hyp context cont =
851 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
852 let n = find_in_context h cont in
853 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
854 | a::next -> debug(" no\n"); filter_real_hyp next cont
857 (* lifts everithing at the conclusion level *)
858 let rec superlift c n=
861 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
862 CicSubstitution.lift n a))] @ superlift next (n+1)
863 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
864 CicSubstitution.lift n a))] @ superlift next (n+1)
865 | _::next -> superlift next (n+1) (*?? ??*)
869 let equality_replace a b ~status =
870 debug("inizio EQ\n");
871 let module C = Cic in
872 let proof,goal = status in
873 let curi,metasenv,pbo,pty = proof in
874 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
875 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
876 let fresh_meta = ProofEngineHelpers.new_meta proof in
878 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
879 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
880 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
882 rewrite_tac ~term:(C.Meta (fresh_meta,irl))
883 ~status:((curi,metasenv',pbo,pty),goal)
885 let new_goals = fresh_meta::goals in
886 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "^string_of_int( List.length goals)^"+ meta\n");
890 let tcl_fail a ~status:(proof,goal) =
892 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
897 let assumption_tac ~status:(proof,goal)=
898 let curi,metasenv,pbo,pty = proof in
899 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
901 let tac_list = List.map
902 ( fun x -> num := !num + 1;
904 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
905 | _ -> ("fake",tcl_fail 1)
909 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
912 (* !!!!! fix !!!!!!!!!! *)
913 let contradiction_tac ~status:(proof,goal)=
915 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
916 ~continuation:(Tacticals.then_
917 ~start:(Ring.elim_type_tac ~term:_False)
918 ~continuation:(assumption_tac))
922 (* ********************* TATTICA ******************************** *)
924 let rec fourier ~status:(s_proof,s_goal)=
925 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
926 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
929 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
930 debug_pcontext s_context;
932 let fhyp = String.copy "new_hyp_for_fourier" in
934 (* here we need to negate the thesis, but to do this we need to apply the right
935 theoreme,so let's parse our thesis *)
937 let th_to_appl = ref _Rfourier_not_le_gt in
939 Cic.Appl ( Cic.Const(u,boh)::args) ->
940 (match UriManager.string_of_uri u with
941 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
943 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
945 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
947 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
949 |_-> failwith "fourier can't be applyed")
950 |_-> failwith "fourier can't be applyed");
951 (* fix maybe strip_outer_cast goes here?? *)
953 (* now let's change our thesis applying the th and put it with hp *)
955 let proof,gl = Tacticals.then_
956 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
957 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
958 ~status:(s_proof,s_goal) in
959 let goal = if List.length gl = 1 then List.hd gl
960 else failwith "a new goal" in
962 debug ("port la tesi sopra e la nego. contesto :\n");
963 debug_pcontext s_context;
965 (* now we have all the right environment *)
967 let curi,metasenv,pbo,pty = proof in
968 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
971 (* now we want to convert hp to inequations, but first we must lift
972 everyting to thesis level, so that a variable has the save Rel(n)
973 in each hp ( needed by ineq1_of_term ) *)
975 (* ? fix if None ?????*)
976 (* fix change superlift with a real name *)
978 let l_context = superlift context 1 in
979 let hyps = filter_real_hyp l_context l_context in
981 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
985 (* transform hyps into inequations *)
987 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
992 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
995 let res=fourier_lineq (!lineq) in
996 let tac=ref Ring.id_tac in
998 (print_string "Tactic Fourier fails.\n";flush stdout;
999 failwith "fourier_tac fails")
1002 match res with (*match res*)
1005 (* in lc we have the coefficient to "reduce" the system *)
1007 print_string "Fourier's method can prove the goal...\n";flush stdout;
1009 debug "I coeff di moltiplicazione rit sono: ";
1013 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1014 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1016 (List.combine (!lineq) lc);
1018 print_string (" quindi lutil e' lunga "^
1019 string_of_int (List.length (!lutil))^"\n");
1021 (* on construit la combinaison linéaire des inéquation *)
1023 (match (!lutil) with (*match (!lutil) *)
1026 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1028 let s=ref (h1.hstrict) in
1031 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1032 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1034 List.iter (fun (h,c) ->
1035 s:=(!s)||(h.hstrict);
1036 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1037 [_Rmult;rational_to_real c;h.hleft ] ]);
1038 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1039 [_Rmult;rational_to_real c;h.hright] ]))
1042 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1043 let tc=rational_to_real cres in
1046 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1048 debug "inizio a costruire tac1\n";
1049 Fourier.print_rational(c1);
1051 let tac1=ref ( fun ~status ->
1052 debug ("Sotto tattica t1 "^(if h1.hstrict
1053 then "strict" else "lasc")^"\n");
1055 (Tacticals.thens ~start:(
1057 debug ("inizio t1 strict\n");
1058 let curi,metasenv,pbo,pty = proof in
1059 let metano,context,ty = List.find
1060 (function (m,_,_) -> m=goal) metasenv in
1061 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1062 debug ("ty = "^ CicPp.ppterm ty^"\n");
1064 PrimitiveTactics.apply_tac ~term:_Rfourier_lt
1066 ~continuations:[tac_use h1;
1069 (rational_to_fraction c1)] ~status
1073 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
1076 [tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status))
1081 List.iter (fun (h,c) ->
1085 tac1:=(Tacticals.thens
1086 ~start:(PrimitiveTactics.apply_tac
1087 ~term:_Rfourier_lt_lt)
1088 ~continuations:[!tac1;tac_use h;
1090 (rational_to_fraction c)]))
1094 Fourier.print_rational(c1);
1095 tac1:=(Tacticals.thens ~start:(
1097 debug("INIZIO TAC 1 2\n");
1099 let curi,metasenv,pbo,pty = proof in
1100 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1101 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1102 debug ("ty = "^ CicPp.ppterm ty^"\n");
1104 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status
1107 ~continuations:[!tac1;tac_use h;
1109 tac_zero_inf_pos (rational_to_fraction c)
1118 tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1119 ~continuations:[!tac1;tac_use h;
1121 (rational_to_fraction c)]))
1125 tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1126 ~continuations:[!tac1;tac_use h;
1128 (rational_to_fraction c)]))
1132 s:=(!s)||(h.hstrict))
1133 lutil;(*end List.iter*)
1135 let tac2= if sres then
1136 tac_zero_inf_false goal (rational_to_fraction cres)
1138 tac_zero_infeq_false goal (rational_to_fraction cres)
1140 tac:=(Tacticals.thens ~start:(my_cut ~term:ineq)
1141 ~continuations:[Tacticals.then_ (* ?????????????????????????????? *)
1142 ~start:(fun ~status:(proof,goal as status) ->
1143 let curi,metasenv,pbo,pty = proof in
1144 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1145 PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1146 ~continuation:(Tacticals.then_
1147 ~start:(PrimitiveTactics.apply_tac
1148 ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
1149 ~continuation:(Tacticals.thens
1153 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc ~status
1155 (match r with (p,gl) ->
1156 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1161 ~continuations:[(*tac2;*)(Tacticals.thens
1164 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1165 (match r with (p,gl) ->
1166 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));r
1174 fun ~status:(proof,goal as status) ->
1177 let curi,metasenv,pbo,pty = proof in
1178 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1180 debug("ty = "^CicPp.ppterm ty^"\n");
1182 let r = PrimitiveTactics.apply_tac ~term:_sym_eqT ~status in
1183 debug("fine ECCOCI\n");
1186 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1190 Tacticals.try_tactics
1191 (* ???????????????????????????? *)
1195 debug("begin RING\n");
1196 let r = Ring.ring_tac ~status in
1197 debug ("end RING\n");
1201 ; "id", Ring.id_tac]
1206 ] (* end continuations before comment *)
1211 tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False)
1212 ~continuations:[Tacticals.then_
1213 (* ???????????????????????????????
1215 ~start:(PrimitiveTactics.intros_tac ~name:"??")
1216 (* ????????????????????????????? *)
1218 ~continuation:contradiction_tac;!tac])
1221 |_-> assert false)(*match (!lutil) *)
1222 |_-> assert false); (*match res*)
1224 debug ("finalmente applico tac\n");
1225 (!tac ~status:(proof,goal))
1229 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
1232 let simpl_tac ~status:(proof,goal) =
1233 let curi,metasenv,pbo,pty = proof in
1234 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1236 prerr_endline("simpl_tac su "^CicPp.ppterm ty);
1238 let new_ty = ProofEngineReduction.simpl context ty in
1240 prerr_endline("ritorna "^CicPp.ppterm new_ty);
1245 (n,_,_) when n = metano -> (metano,context,new_ty)
1249 (curi,new_metasenv,pbo,pty), [metano]
1253 let rewrite_simpl_tac ~term ~status =
1255 Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status