1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
27 (******************** OTHER USEFUL TACTICS **********************)
29 let rewrite_tac ~term:equality ~status:(proof,goal) =
31 let module U = UriManager in
32 let curi,metasenv,pbo,pty = proof in
33 let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
34 let eq_ind_r,ty,t1,t2 =
35 match CicTypeChecker.type_of_aux' metasenv context equality with
36 C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
37 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
40 (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
43 | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
44 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
47 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",[])
52 (ProofEngineTypes.Fail
53 "Rewrite: the argument is not a proof of an equality")
56 let gty' = CicSubstitution.lift 1 gty in
57 let t1' = CicSubstitution.lift 1 t1 in
59 ProofEngineReduction.replace_lifting
60 ~equality:ProofEngineReduction.alpha_equivalence
61 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
63 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
65 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
66 let fresh_meta = ProofEngineHelpers.new_meta proof in
68 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
69 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
72 PrimitiveTactics.exact_tac
74 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
75 ~status:((curi,metasenv',pbo,pty),goal)
77 assert (List.length goals = 0) ;
82 let rewrite_simpl_tac ~term ~status =
83 Tacticals.then_ ~start:(rewrite_tac ~term)
85 (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
89 (******************** THE FOURIER TACTIC ***********************)
91 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
92 des inéquations et équations sont entiers. En attendant la tactique Field.
98 let debug x = print_string ("____ "^x) ; flush stdout;;
100 let debug_pcontext x =
102 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
103 a ^ " " | _ ->()) x ;
104 debug ("contesto : "^ (!str) ^ "\n")
107 (******************************************************************************
108 Operations on linear combinations.
110 Opérations sur les combinaisons linéaires affines.
111 La partie homogène d'une combinaison linéaire est en fait une table de hash
112 qui donne le coefficient d'un terme du calcul des constructions,
113 qui est zéro si le terme n'y est pas.
119 The type for linear combinations
121 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
125 @return an empty flin
127 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
133 @return the rational associated with x (coefficient)
137 (Hashtbl.find f.fhom x)
143 Adds c to the coefficient of x
150 let cx = flin_coef f x in
151 Hashtbl.remove f.fhom x;
152 Hashtbl.add f.fhom x (rplus cx c);
161 let flin_add_cste f c =
163 fcste=rplus f.fcste c}
167 @return a empty flin with r1 in fcste
169 let flin_one () = flin_add_cste (flin_zero()) r1;;
174 let flin_plus f1 f2 =
175 let f3 = flin_zero() in
176 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
177 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
178 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
184 let flin_minus f1 f2 =
185 let f3 = flin_zero() in
186 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
187 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
188 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
195 let f2 = flin_zero() in
196 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
197 flin_add_cste f2 (rmult a f.fcste);
201 (*****************************************************************************)
206 @raise Failure if conversion is impossible
207 @return rational proiection of t
209 let rec rational_of_term t =
210 (* fun to apply f to the first and second rational-term of l *)
211 let rat_of_binop f l =
212 let a = List.hd l and
213 b = List.hd(List.tl l) in
214 f (rational_of_term a) (rational_of_term b)
216 (* as before, but f is unary *)
217 let rat_of_unop f l =
218 f (rational_of_term (List.hd l))
221 | Cic.Cast (t1,t2) -> (rational_of_term t1)
222 | Cic.Appl (t1::next) ->
225 (match (UriManager.string_of_uri u) with
226 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
228 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
229 rat_of_unop rinv next
230 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
231 rat_of_binop rmult next
232 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
233 rat_of_binop rdiv next
234 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
235 rat_of_binop rplus next
236 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
237 rat_of_binop rminus next
238 | _ -> failwith "not a rational")
239 | _ -> failwith "not a rational")
240 | Cic.Const (u,boh) ->
241 (match (UriManager.string_of_uri u) with
242 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
243 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
244 | _ -> failwith "not a rational")
245 | _ -> failwith "not a rational"
249 let rational_of_const = rational_of_term;;
253 let rec flin_of_term t =
254 let fl_of_binop f l =
255 let a = List.hd l and
256 b = List.hd(List.tl l) in
257 f (flin_of_term a) (flin_of_term b)
261 | Cic.Cast (t1,t2) -> (flin_of_term t1)
262 | Cic.Appl (t1::next) ->
267 match (UriManager.string_of_uri u) with
268 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
269 flin_emult (rop r1) (flin_of_term (List.hd next))
270 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
271 fl_of_binop flin_plus next
272 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
273 fl_of_binop flin_minus next
274 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
276 let arg1 = (List.hd next) and
277 arg2 = (List.hd(List.tl next))
281 let a = rational_of_term arg1 in
284 let b = (rational_of_term arg2) in
285 (flin_add_cste (flin_zero()) (rmult a b))
288 _ -> (flin_add (flin_zero()) arg2 a)
291 _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
293 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
294 let a=(rational_of_term (List.hd next)) in
295 flin_add_cste (flin_zero()) (rinv a)
296 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
298 let b=(rational_of_term (List.hd(List.tl next))) in
301 let a = (rational_of_term (List.hd next)) in
302 (flin_add_cste (flin_zero()) (rdiv a b))
305 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
311 | Cic.Const (u,boh) ->
313 match (UriManager.string_of_uri u) with
314 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
315 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
319 with _ -> flin_add (flin_zero()) t r1
323 let flin_of_constr = flin_of_term;;
327 Translates a flin to (c,x) list
329 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
331 let flin_to_alist f =
333 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
337 (* Représentation des hypothèses qui sont des inéquations ou des équations.
341 The structure for ineq
343 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
344 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
351 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
354 let ineq1_of_term (h,t) =
355 match t with (* match t *)
356 Cic.Appl (t1::next) ->
357 let arg1= List.hd next in
358 let arg2= List.hd(List.tl next) in
359 (match t1 with (* match t1 *)
361 (match UriManager.string_of_uri u with (* match u *)
362 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
367 hflin= flin_minus (flin_of_term arg1)
370 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
375 hflin= flin_minus (flin_of_term arg2)
378 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
383 hflin= flin_minus (flin_of_term arg1)
386 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
391 hflin= flin_minus (flin_of_term arg2)
394 |_->assert false)(* match u *)
395 | Cic.MutInd (u,i,o) ->
396 (match UriManager.string_of_uri u with
397 "cic:/Coq/Init/Logic_Type/eqT.ind" ->
400 let arg2= List.hd(List.tl (List.tl next)) in
403 (match UriManager.string_of_uri u with
404 "cic:/Coq/Reals/Rdefinitions/R.con"->
409 hflin= flin_minus (flin_of_term arg1)
416 hflin= flin_minus (flin_of_term arg2)
422 |_-> assert false)(* match t1 *)
423 |_-> assert false (* match t *)
426 let ineq1_of_constr = ineq1_of_term;;
429 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
435 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
438 let rec print_sys l =
441 | (a,b)::next -> (print_rl a;
442 print_string (if b=true then "strict\n"else"\n");
447 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
450 let fourier_lineq lineq1 =
452 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
454 Hashtbl.iter (fun x c ->
455 try (Hashtbl.find hvar x;())
456 with _-> nvar:=(!nvar)+1;
457 Hashtbl.add hvar x (!nvar))
461 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
462 let sys= List.map (fun h->
463 let v=Array.create ((!nvar)+1) r0 in
464 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
466 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
468 debug ("chiamo unsolvable sul sistema di "^
469 string_of_int (List.length sys) ^"\n");
474 (*****************************************************************************
475 Construction de la preuve en cas de succès de la méthode de Fourier,
476 i.e. on obtient une contradiction.
480 let _eqT = Cic.MutInd(UriManager.uri_of_string
481 "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [] ;;
482 let _False = Cic.MutInd (UriManager.uri_of_string
483 "cic:/Coq/Init/Logic/False.ind") 0 [] ;;
484 let _not = Cic.Const (UriManager.uri_of_string
485 "cic:/Coq/Init/Logic/not.con") [];;
486 let _R0 = Cic.Const (UriManager.uri_of_string
487 "cic:/Coq/Reals/Rdefinitions/R0.con") [] ;;
488 let _R1 = Cic.Const (UriManager.uri_of_string
489 "cic:/Coq/Reals/Rdefinitions/R1.con") [] ;;
490 let _R = Cic.Const (UriManager.uri_of_string
491 "cic:/Coq/Reals/Rdefinitions/R.con") [] ;;
492 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
493 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [] ;;
494 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
495 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [] ;;
496 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
497 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [] ;;
498 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
499 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [] ;;
500 let _Rfourier_le=Cic.Const (UriManager.uri_of_string
501 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") [] ;;
502 let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
503 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") [] ;;
504 let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
505 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") [] ;;
506 let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
507 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") [] ;;
508 let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
509 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") [] ;;
510 let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
511 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") [] ;;
512 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
513 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [] ;;
514 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
515 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [] ;;
516 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
517 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [] ;;
518 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
519 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [] ;;
520 let _Rinv = Cic.Const (UriManager.uri_of_string
521 "cic:/Coq/Reals/Rdefinitions/Rinv.con") [] ;;
522 let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
523 "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [] ;;
524 let _Rle = Cic.Const (UriManager.uri_of_string
525 "cic:/Coq/Reals/Rdefinitions/Rle.con") [] ;;
526 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
527 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [] ;;
528 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
529 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [] ;;
530 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
531 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [] ;;
532 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
533 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [] ;;
534 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
535 "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;
536 let _Rlt = Cic.Const (UriManager.uri_of_string
537 "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;;
538 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
539 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [] ;;
540 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
541 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [] ;;
542 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
543 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [] ;;
544 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
545 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [] ;;
546 let _Rminus = Cic.Const (UriManager.uri_of_string
547 "cic:/Coq/Reals/Rdefinitions/Rminus.con") [] ;;
548 let _Rmult = Cic.Const (UriManager.uri_of_string
549 "cic:/Coq/Reals/Rdefinitions/Rmult.con") [] ;;
550 let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
551 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [] ;;
552 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
553 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [] ;;
554 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
555 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [] ;;
556 let _Ropp = Cic.Const (UriManager.uri_of_string
557 "cic:/Coq/Reals/Rdefinitions/Ropp.con") [] ;;
558 let _Rplus = Cic.Const (UriManager.uri_of_string
559 "cic:/Coq/Reals/Rdefinitions/Rplus.con") [] ;;
561 (******************************************************************************)
563 let is_int x = (x.den)=1
566 (* fraction = couple (num,den) *)
567 let rec rational_to_fraction x= (x.num,x.den)
570 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
573 let rec int_to_real_aux n =
575 0 -> _R0 (* o forse R0 + R0 ????? *)
577 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
582 let x = int_to_real_aux (abs n) in
584 Cic.Appl [ _Ropp ; x ]
590 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
593 let rational_to_real x =
594 let (n,d)=rational_to_fraction x in
595 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
598 (* preuve que 0<n*1/d
601 let tac_zero_inf_pos (n,d) ~status =
602 (*let cste = pf_parse_constr gl in*)
603 let pall str ~status:(proof,goal) t =
604 debug ("tac "^str^" :\n" );
605 let curi,metasenv,pbo,pty = proof in
606 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
607 debug ("th = "^ CicPp.ppterm t ^"\n");
608 debug ("ty = "^ CicPp.ppterm ty^"\n");
611 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
612 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
614 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
615 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
619 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
620 ~status _Rlt_zero_pos_plus1;
621 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
622 ~continuation:!tacn);
625 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
626 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
627 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
632 debug("TAC ZERO INF POS\n");
634 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
643 (* preuve que 0<=n*1/d
646 let tac_zero_infeq_pos gl (n,d) ~status =
647 (*let cste = pf_parse_constr gl in*)
648 debug("inizio tac_zero_infeq_pos\n");
651 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
653 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
656 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
658 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
659 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
662 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
663 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
666 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
667 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
668 debug("fine tac_zero_infeq_pos\n");
674 (* preuve que 0<(-n)*(1/d) => False
677 let tac_zero_inf_false gl (n,d) ~status=
678 debug("inizio tac_zero_inf_false\n");
680 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
684 (debug "2\n";let r = (Tacticals.then_ ~start:(
685 fun ~status:(proof,goal as status) ->
686 let curi,metasenv,pbo,pty = proof in
687 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
688 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
689 ^ CicPp.ppterm ty ^"\n");
690 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
691 debug("!!!!!!!!!2\n");
694 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
700 (* preuve que 0<=n*(1/d) => False ; n est negatif
703 let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
704 debug("stat tac_zero_infeq_false\n");
706 let curi,metasenv,pbo,pty = proof in
707 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
709 debug("faccio fold di " ^ CicPp.ppterm
713 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
716 debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
717 (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
720 (ReductionTactics.fold_tac ~also_in_hypotheses:false
725 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
730 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
731 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
732 debug("end tac_zero_infeq_false\n");
735 Tacticals.id_tac ~status
740 (* *********** ********** ******** ??????????????? *********** **************)
742 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
743 let curi,metasenv,pbo,pty = proof in
744 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
745 let fresh_meta = ProofEngineHelpers.new_meta proof in
747 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
748 let metasenv' = (fresh_meta,context,t)::metasenv in
749 let proof' = curi,metasenv',pbo,pty in
751 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta
752 (fresh_meta,irl),t))::al)) ~status:(proof',goal)
754 proof'',fresh_meta::goals
761 let my_cut ~term:c ~status:(proof,goal)=
762 let curi,metasenv,pbo,pty = proof in
763 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
765 debug("my_cut di "^CicPp.ppterm c^"\n");
768 let fresh_meta = ProofEngineHelpers.new_meta proof in
770 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
771 let metasenv' = (fresh_meta,context,c)::metasenv in
772 let proof' = curi,metasenv',pbo,pty in
774 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
775 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
776 ~status:(proof',goal)
778 (* We permute the generated goals to be consistent with Coq *)
781 | he::tl -> proof'',he::fresh_meta::tl
785 let exact = PrimitiveTactics.exact_tac;;
787 let tac_use h ~status:(proof,goal as status) =
788 debug("Inizio TC_USE\n");
789 let curi,metasenv,pbo,pty = proof in
790 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
791 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
792 debug ("ty = "^ CicPp.ppterm ty^"\n");
796 "Rlt" -> exact ~term:h.hname ~status
797 |"Rle" -> exact ~term:h.hname ~status
798 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
799 ~term:_Rfourier_gt_to_lt)
800 ~continuation:(exact ~term:h.hname)) ~status
801 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
802 ~term:_Rfourier_ge_to_le)
803 ~continuation:(exact ~term:h.hname)) ~status
804 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
805 ~term:_Rfourier_eqLR_to_le)
806 ~continuation:(exact ~term:h.hname)) ~status
807 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
808 ~term:_Rfourier_eqRL_to_le)
809 ~continuation:(exact ~term:h.hname)) ~status
812 debug("Fine TAC_USE\n");
820 Cic.Appl ( Cic.Const(u,boh)::next) ->
821 (match (UriManager.string_of_uri u) with
822 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
823 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
824 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
825 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
826 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
827 (match (List.hd next) with
828 Cic.Const (uri,_) when
829 UriManager.string_of_uri uri =
830 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
836 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
839 Cic.Appl(Array.to_list a)
842 (* Résolution d'inéquations linéaires dans R *)
843 let rec strip_outer_cast c = match c with
844 | Cic.Cast (c,_) -> strip_outer_cast c
848 let find_in_context id context =
849 let rec find_in_context_aux c n =
851 [] -> failwith (id^" not found in context")
852 | a::next -> (match a with
853 Some (Cic.Name(name),_) when name = id -> n
854 (*? magari al posto di _ qualcosaltro?*)
855 | _ -> find_in_context_aux next (n+1))
857 find_in_context_aux context 1
860 (* mi sembra quadratico *)
861 let rec filter_real_hyp context cont =
864 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
865 let n = find_in_context h cont in
866 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
867 | a::next -> debug(" no\n"); filter_real_hyp next cont
870 (* lifts everithing at the conclusion level *)
871 let rec superlift c n=
874 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
875 CicSubstitution.lift n a))] @ superlift next (n+1)
876 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
877 CicSubstitution.lift n a))] @ superlift next (n+1)
878 | _::next -> superlift next (n+1) (*?? ??*)
882 let equality_replace a b ~status =
883 debug("inizio EQ\n");
884 let module C = Cic in
885 let proof,goal = status in
886 let curi,metasenv,pbo,pty = proof in
887 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
888 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
889 let fresh_meta = ProofEngineHelpers.new_meta proof in
891 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
892 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
893 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
895 rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
896 ~status:((curi,metasenv',pbo,pty),goal)
898 let new_goals = fresh_meta::goals in
899 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
900 ^string_of_int( List.length goals)^"+ meta\n");
904 let tcl_fail a ~status:(proof,goal) =
906 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
911 let assumption_tac ~status:(proof,goal)=
912 let curi,metasenv,pbo,pty = proof in
913 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
915 let tac_list = List.map
916 ( fun x -> num := !num + 1;
918 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
919 | _ -> ("fake",tcl_fail 1)
923 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
926 (* !!!!! fix !!!!!!!!!! *)
927 let contradiction_tac ~status:(proof,goal)=
929 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
930 ~continuation:(Tacticals.then_
931 ~start:(Ring.elim_type_tac ~term:_False)
932 ~continuation:(assumption_tac))
936 (* ********************* TATTICA ******************************** *)
938 let rec fourier ~status:(s_proof,s_goal)=
939 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
940 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
943 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
944 debug_pcontext s_context;
946 let fhyp = String.copy "new_hyp_for_fourier" in
948 (* here we need to negate the thesis, but to do this we need to apply the right
949 theoreme,so let's parse our thesis *)
951 let th_to_appl = ref _Rfourier_not_le_gt in
953 Cic.Appl ( Cic.Const(u,boh)::args) ->
954 (match UriManager.string_of_uri u with
955 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
957 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
959 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
961 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
963 |_-> failwith "fourier can't be applyed")
964 |_-> failwith "fourier can't be applyed");
965 (* fix maybe strip_outer_cast goes here?? *)
967 (* now let's change our thesis applying the th and put it with hp *)
969 let proof,gl = Tacticals.then_
970 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
971 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
972 ~status:(s_proof,s_goal) in
973 let goal = if List.length gl = 1 then List.hd gl
974 else failwith "a new goal" in
976 debug ("port la tesi sopra e la nego. contesto :\n");
977 debug_pcontext s_context;
979 (* now we have all the right environment *)
981 let curi,metasenv,pbo,pty = proof in
982 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
985 (* now we want to convert hp to inequations, but first we must lift
986 everyting to thesis level, so that a variable has the save Rel(n)
987 in each hp ( needed by ineq1_of_term ) *)
989 (* ? fix if None ?????*)
990 (* fix change superlift with a real name *)
992 let l_context = superlift context 1 in
993 let hyps = filter_real_hyp l_context l_context in
995 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
999 (* transform hyps into inequations *)
1001 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1006 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1009 let res=fourier_lineq (!lineq) in
1010 let tac=ref Tacticals.id_tac in
1012 (print_string "Tactic Fourier fails.\n";flush stdout;
1013 failwith "fourier_tac fails")
1016 match res with (*match res*)
1019 (* in lc we have the coefficient to "reduce" the system *)
1021 print_string "Fourier's method can prove the goal...\n";flush stdout;
1023 debug "I coeff di moltiplicazione rit sono: ";
1027 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1028 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1030 (List.combine (!lineq) lc);
1032 print_string (" quindi lutil e' lunga "^
1033 string_of_int (List.length (!lutil))^"\n");
1035 (* on construit la combinaison linéaire des inéquation *)
1037 (match (!lutil) with (*match (!lutil) *)
1039 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1041 let s=ref (h1.hstrict) in
1044 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1045 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1047 List.iter (fun (h,c) ->
1048 s:=(!s)||(h.hstrict);
1049 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1050 [_Rmult;rational_to_real c;h.hleft ] ]);
1051 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1052 [_Rmult;rational_to_real c;h.hright] ]))
1055 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1056 let tc=rational_to_real cres in
1059 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1061 debug "inizio a costruire tac1\n";
1062 Fourier.print_rational(c1);
1064 let tac1=ref ( fun ~status ->
1069 debug ("inizio t1 strict\n");
1070 let curi,metasenv,pbo,pty = proof in
1071 let metano,context,ty = List.find
1072 (function (m,_,_) -> m=goal) metasenv in
1073 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1074 debug ("ty = "^ CicPp.ppterm ty^"\n");
1075 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1076 ~continuations:[tac_use h1;tac_zero_inf_pos
1077 (rational_to_fraction c1)]
1082 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1083 ~continuations:[tac_use h1;tac_zero_inf_pos
1084 (rational_to_fraction c1)] ~status
1090 List.iter (fun (h,c) ->
1094 tac1:=(Tacticals.thens
1095 ~start:(PrimitiveTactics.apply_tac
1096 ~term:_Rfourier_lt_lt)
1097 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1098 (rational_to_fraction c)])
1102 Fourier.print_rational(c1);
1103 tac1:=(Tacticals.thens
1106 debug("INIZIO TAC 1 2\n");
1107 let curi,metasenv,pbo,pty = proof in
1108 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1110 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1111 debug ("ty = "^ CicPp.ppterm ty^"\n");
1112 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1113 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1114 (rational_to_fraction c)])
1120 tac1:=(Tacticals.thens
1121 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1122 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1123 (rational_to_fraction c)])
1127 tac1:=(Tacticals.thens
1128 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1129 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1130 (rational_to_fraction c)])
1134 s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1138 tac_zero_inf_false goal (rational_to_fraction cres)
1140 tac_zero_infeq_false goal (rational_to_fraction cres)
1142 tac:=(Tacticals.thens
1143 ~start:(my_cut ~term:ineq)
1144 ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)Tacticals.then_
1145 ~start:(fun ~status:(proof,goal as status) ->
1146 let curi,metasenv,pbo,pty = proof in
1147 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1149 PrimitiveTactics.change_tac ~what:ty
1150 ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1151 ~continuation:(Tacticals.then_
1152 ~start:(PrimitiveTactics.apply_tac ~term:
1153 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1154 ~continuation:(Tacticals.thens
1157 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1158 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1161 (match r with (p,gl) ->
1162 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1164 ~continuations:[(Tacticals.thens
1167 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1168 (match r with (p,gl) ->
1169 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1172 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1173 (* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
1174 di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
1175 parametri della equality_replace vengono passati al contrario? Oppure la
1176 tattica usa i parametri al contrario?
1177 CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac
1178 ~continuations:[Tacticals.then_
1180 fun ~status:(proof,goal as status) ->
1182 let curi,metasenv,pbo,pty = proof in
1183 let metano,context,ty = List.find (function (m,_,_) -> m=
1185 debug("ty = "^CicPp.ppterm ty^"\n");
1186 let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
1188 debug("fine ECCOCI\n");
1190 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1192 ;Tacticals.try_tactics
1193 ~tactics:[ "ring", (fun ~status ->
1194 debug("begin RING\n");
1195 let r = Ring.ring_tac ~status in
1196 debug ("end RING\n");
1198 ; "id", Tacticals.id_tac]
1203 fun ~status:(proof,goal as status) ->
1204 let curi,metasenv,pbo,pty = proof in
1205 let metano,context,ty = List.find (function (m,_,_) -> m=
1207 (* check if ty is of type *)
1209 debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1211 (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*)
1212 Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1215 let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1216 debug("fine MY_CHNGE\n");
1219 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1220 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1221 (*tac:=(Tacticals.thens
1222 ~start:(PrimitiveTactics.cut_tac ~term:_False)
1223 ~continuations:[Tacticals.then_
1224 ~start:(PrimitiveTactics.intros_tac ~name:"??")
1225 ~continuation:contradiction_tac
1230 |_-> assert false)(*match (!lutil) *)
1231 |_-> assert false); (*match res*)
1232 debug ("finalmente applico tac\n");
1233 (!tac ~status:(proof,goal))
1236 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;