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) ~continuation:ReductionTactics.simpl_tac ~status
86 (******************** THE FOURIER TACTIC ***********************)
88 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
89 des inéquations et équations sont entiers. En attendant la tactique Field.
95 let debug x = print_string ("____ "^x) ; flush stdout;;
97 let debug_pcontext x =
99 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
100 a ^ " " | _ ->()) x ;
101 debug ("contesto : "^ (!str) ^ "\n")
104 (******************************************************************************
105 Operations on linear combinations.
107 Opérations sur les combinaisons linéaires affines.
108 La partie homogène d'une combinaison linéaire est en fait une table de hash
109 qui donne le coefficient d'un terme du calcul des constructions,
110 qui est zéro si le terme n'y est pas.
116 The type for linear combinations
118 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
122 @return an empty flin
124 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
130 @return the rational associated with x (coefficient)
134 (Hashtbl.find f.fhom x)
140 Adds c to the coefficient of x
147 let cx = flin_coef f x in
148 Hashtbl.remove f.fhom x;
149 Hashtbl.add f.fhom x (rplus cx c);
158 let flin_add_cste f c =
160 fcste=rplus f.fcste c}
164 @return a empty flin with r1 in fcste
166 let flin_one () = flin_add_cste (flin_zero()) r1;;
171 let flin_plus f1 f2 =
172 let f3 = flin_zero() in
173 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
174 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
175 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
181 let flin_minus f1 f2 =
182 let f3 = flin_zero() in
183 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
184 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
185 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
192 let f2 = flin_zero() in
193 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
194 flin_add_cste f2 (rmult a f.fcste);
198 (*****************************************************************************)
203 @raise Failure if conversion is impossible
204 @return rational proiection of t
206 let rec rational_of_term t =
207 (* fun to apply f to the first and second rational-term of l *)
208 let rat_of_binop f l =
209 let a = List.hd l and
210 b = List.hd(List.tl l) in
211 f (rational_of_term a) (rational_of_term b)
213 (* as before, but f is unary *)
214 let rat_of_unop f l =
215 f (rational_of_term (List.hd l))
218 | Cic.Cast (t1,t2) -> (rational_of_term t1)
219 | Cic.Appl (t1::next) ->
222 (match (UriManager.string_of_uri u) with
223 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
225 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
226 rat_of_unop rinv next
227 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
228 rat_of_binop rmult next
229 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
230 rat_of_binop rdiv next
231 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
232 rat_of_binop rplus next
233 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
234 rat_of_binop rminus next
235 | _ -> failwith "not a rational")
236 | _ -> failwith "not a rational")
237 | Cic.Const (u,boh) ->
238 (match (UriManager.string_of_uri u) with
239 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
240 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
241 | _ -> failwith "not a rational")
242 | _ -> failwith "not a rational"
246 let rational_of_const = rational_of_term;;
250 let rec flin_of_term t =
251 let fl_of_binop f l =
252 let a = List.hd l and
253 b = List.hd(List.tl l) in
254 f (flin_of_term a) (flin_of_term b)
258 | Cic.Cast (t1,t2) -> (flin_of_term t1)
259 | Cic.Appl (t1::next) ->
264 match (UriManager.string_of_uri u) with
265 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
266 flin_emult (rop r1) (flin_of_term (List.hd next))
267 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
268 fl_of_binop flin_plus next
269 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
270 fl_of_binop flin_minus next
271 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
273 let arg1 = (List.hd next) and
274 arg2 = (List.hd(List.tl next))
278 let a = rational_of_term arg1 in
281 let b = (rational_of_term arg2) in
282 (flin_add_cste (flin_zero()) (rmult a b))
285 _ -> (flin_add (flin_zero()) arg2 a)
288 _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
290 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
291 let a=(rational_of_term (List.hd next)) in
292 flin_add_cste (flin_zero()) (rinv a)
293 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
295 let b=(rational_of_term (List.hd(List.tl next))) in
298 let a = (rational_of_term (List.hd next)) in
299 (flin_add_cste (flin_zero()) (rdiv a b))
302 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
308 | Cic.Const (u,boh) ->
310 match (UriManager.string_of_uri u) with
311 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
312 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
316 with _ -> flin_add (flin_zero()) t r1
320 let flin_of_constr = flin_of_term;;
324 Translates a flin to (c,x) list
326 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
328 let flin_to_alist f =
330 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
334 (* Représentation des hypothèses qui sont des inéquations ou des équations.
338 The structure for ineq
340 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
341 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
348 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
351 let ineq1_of_term (h,t) =
352 match t with (* match t *)
353 Cic.Appl (t1::next) ->
354 let arg1= List.hd next in
355 let arg2= List.hd(List.tl next) in
356 (match t1 with (* match t1 *)
358 (match UriManager.string_of_uri u with (* match u *)
359 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
364 hflin= flin_minus (flin_of_term arg1)
367 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
372 hflin= flin_minus (flin_of_term arg2)
375 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
380 hflin= flin_minus (flin_of_term arg1)
383 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
388 hflin= flin_minus (flin_of_term arg2)
391 |_->assert false)(* match u *)
392 | Cic.MutInd (u,i,o) ->
393 (match UriManager.string_of_uri u with
394 "cic:/Coq/Init/Logic_Type/eqT.con" ->
397 let arg2= List.hd(List.tl (List.tl next)) in
400 (match UriManager.string_of_uri u with
401 "cic:/Coq/Reals/Rdefinitions/R.con"->
406 hflin= flin_minus (flin_of_term arg1)
413 hflin= flin_minus (flin_of_term arg2)
419 |_-> assert false)(* match t1 *)
420 |_-> assert false (* match t *)
423 let ineq1_of_constr = ineq1_of_term;;
426 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
432 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
435 let rec print_sys l =
438 | (a,b)::next -> (print_rl a;
439 print_string (if b=true then "strict\n"else"\n");
444 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
447 let fourier_lineq lineq1 =
449 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
451 Hashtbl.iter (fun x c ->
452 try (Hashtbl.find hvar x;())
453 with _-> nvar:=(!nvar)+1;
454 Hashtbl.add hvar x (!nvar))
458 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
459 let sys= List.map (fun h->
460 let v=Array.create ((!nvar)+1) r0 in
461 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
463 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
465 debug ("chiamo unsolvable sul sistema di "^
466 string_of_int (List.length sys) ^"\n");
471 (*****************************************************************************
472 Construction de la preuve en cas de succès de la méthode de Fourier,
473 i.e. on obtient une contradiction.
477 let _eqT = Cic.MutInd(UriManager.uri_of_string
478 "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [] ;;
479 let _False = Cic.MutInd (UriManager.uri_of_string
480 "cic:/Coq/Init/Logic/False.ind") 0 [] ;;
481 let _not = Cic.Const (UriManager.uri_of_string
482 "cic:/Coq/Init/Logic/not.con") [];;
483 let _R0 = Cic.Const (UriManager.uri_of_string
484 "cic:/Coq/Reals/Rdefinitions/R0.con") [] ;;
485 let _R1 = Cic.Const (UriManager.uri_of_string
486 "cic:/Coq/Reals/Rdefinitions/R1.con") [] ;;
487 let _R = Cic.Const (UriManager.uri_of_string
488 "cic:/Coq/Reals/Rdefinitions/R.con") [] ;;
489 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string
490 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [] ;;
491 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string
492 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [] ;;
493 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string
494 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [] ;;
495 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string
496 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [] ;;
497 let _Rfourier_le=Cic.Const (UriManager.uri_of_string
498 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") [] ;;
499 let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string
500 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") [] ;;
501 let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string
502 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") [] ;;
503 let _Rfourier_lt=Cic.Const (UriManager.uri_of_string
504 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") [] ;;
505 let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string
506 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") [] ;;
507 let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string
508 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") [] ;;
509 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string
510 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [] ;;
511 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string
512 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [] ;;
513 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string
514 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [] ;;
515 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string
516 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [] ;;
517 let _Rinv = Cic.Const (UriManager.uri_of_string
518 "cic:/Coq/Reals/Rdefinitions/Rinv.con") [] ;;
519 let _Rinv_R1 = Cic.Const(UriManager.uri_of_string
520 "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [] ;;
521 let _Rle = Cic.Const (UriManager.uri_of_string
522 "cic:/Coq/Reals/Rdefinitions/Rle.con") [] ;;
523 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string
524 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [] ;;
525 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string
526 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [] ;;
527 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string
528 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [] ;;
529 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
530 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [] ;;
531 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string
532 "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;
533 let _Rlt = Cic.Const (UriManager.uri_of_string
534 "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;;
535 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string
536 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [] ;;
537 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string
538 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [] ;;
539 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string
540 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [] ;;
541 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string
542 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [] ;;
543 let _Rminus = Cic.Const (UriManager.uri_of_string
544 "cic:/Coq/Reals/Rdefinitions/Rminus.con") [] ;;
545 let _Rmult = Cic.Const (UriManager.uri_of_string
546 "cic:/Coq/Reals/Rdefinitions/Rmult.con") [] ;;
547 let _Rnot_le_le =Cic.Const (UriManager.uri_of_string
548 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [] ;;
549 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string
550 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [] ;;
551 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string
552 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [] ;;
553 let _Ropp = Cic.Const (UriManager.uri_of_string
554 "cic:/Coq/Reals/Rdefinitions/Ropp.con") [] ;;
555 let _Rplus = Cic.Const (UriManager.uri_of_string
556 "cic:/Coq/Reals/Rdefinitions/Rplus.con") [] ;;
558 (******************************************************************************)
560 let is_int x = (x.den)=1
563 (* fraction = couple (num,den) *)
564 let rec rational_to_fraction x= (x.num,x.den)
567 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
570 let rec int_to_real_aux n =
572 0 -> _R0 (* o forse R0 + R0 ????? *)
574 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
579 let x = int_to_real_aux (abs n) in
581 Cic.Appl [ _Ropp ; x ]
587 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
590 let rational_to_real x =
591 let (n,d)=rational_to_fraction x in
592 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
595 (* preuve que 0<n*1/d
598 let tac_zero_inf_pos (n,d) ~status =
599 (*let cste = pf_parse_constr gl in*)
600 let pall str ~status:(proof,goal) t =
601 debug ("tac "^str^" :\n" );
602 let curi,metasenv,pbo,pty = proof in
603 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
604 debug ("th = "^ CicPp.ppterm t ^"\n");
605 debug ("ty = "^ CicPp.ppterm ty^"\n");
608 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
609 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
611 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
612 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
616 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
617 ~status _Rlt_zero_pos_plus1;
618 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
619 ~continuation:!tacn);
622 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
623 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
624 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
629 debug("TAC ZERO INF POS\n");
631 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
640 (* preuve que 0<=n*1/d
643 let tac_zero_infeq_pos gl (n,d) ~status =
644 (*let cste = pf_parse_constr gl in*)
645 debug("inizio tac_zero_infeq_pos\n");
648 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
650 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
653 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
655 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
656 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
659 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
660 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
663 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
664 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
665 debug("fine tac_zero_infeq_pos\n");
671 (* preuve que 0<(-n)*(1/d) => False
674 let tac_zero_inf_false gl (n,d) ~status=
675 debug("inizio tac_zero_inf_false\n");
677 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
681 (debug "2\n";let r = (Tacticals.then_ ~start:(
682 fun ~status:(proof,goal as status) ->
683 let curi,metasenv,pbo,pty = proof in
684 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
685 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
686 ^ CicPp.ppterm ty ^"\n");
687 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
688 debug("!!!!!!!!!2\n");
691 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
697 (* preuve que 0<=n*(1/d) => False ; n est negatif
700 let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
701 debug("stat tac_zero_infeq_false\n");
703 let curi,metasenv,pbo,pty = proof in
704 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
706 debug("faccio fold di " ^ CicPp.ppterm
710 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
713 debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
714 (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
717 (ReductionTactics.fold_tac ~also_in_hypotheses:false
722 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
727 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
728 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
729 debug("end tac_zero_infeq_false\n");
732 Tacticals.id_tac ~status
737 (* *********** ********** ******** ??????????????? *********** **************)
739 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
740 let curi,metasenv,pbo,pty = proof in
741 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
742 let fresh_meta = ProofEngineHelpers.new_meta proof in
744 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
745 let metasenv' = (fresh_meta,context,t)::metasenv in
746 let proof' = curi,metasenv',pbo,pty in
748 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta
749 (fresh_meta,irl),t))::al)) ~status:(proof',goal)
751 proof'',fresh_meta::goals
758 let my_cut ~term:c ~status:(proof,goal)=
759 let curi,metasenv,pbo,pty = proof in
760 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
762 let fresh_meta = ProofEngineHelpers.new_meta proof in
764 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
765 let metasenv' = (fresh_meta,context,c)::metasenv in
766 let proof' = curi,metasenv',pbo,pty in
768 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
769 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
770 ~status:(proof',goal)
772 (* We permute the generated goals to be consistent with Coq *)
775 | he::tl -> proof'',he::fresh_meta::tl
779 let exact = PrimitiveTactics.exact_tac;;
781 let tac_use h ~status:(proof,goal as status) =
782 debug("Inizio TC_USE\n");
783 let curi,metasenv,pbo,pty = proof in
784 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
785 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
786 debug ("ty = "^ CicPp.ppterm ty^"\n");
790 "Rlt" -> exact ~term:h.hname ~status
791 |"Rle" -> exact ~term:h.hname ~status
792 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
793 ~term:_Rfourier_gt_to_lt)
794 ~continuation:(exact ~term:h.hname)) ~status
795 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
796 ~term:_Rfourier_ge_to_le)
797 ~continuation:(exact ~term:h.hname)) ~status
798 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
799 ~term:_Rfourier_eqLR_to_le)
800 ~continuation:(exact ~term:h.hname)) ~status
801 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
802 ~term:_Rfourier_eqRL_to_le)
803 ~continuation:(exact ~term:h.hname)) ~status
806 debug("Fine TAC_USE\n");
814 Cic.Appl ( Cic.Const(u,boh)::next) ->
815 (match (UriManager.string_of_uri u) with
816 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
817 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
818 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
819 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
820 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
821 (match (List.hd next) with
822 Cic.Const (uri,_) when
823 UriManager.string_of_uri uri =
824 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
830 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
833 Cic.Appl(Array.to_list a)
836 (* Résolution d'inéquations linéaires dans R *)
837 let rec strip_outer_cast c = match c with
838 | Cic.Cast (c,_) -> strip_outer_cast c
842 let find_in_context id context =
843 let rec find_in_context_aux c n =
845 [] -> failwith (id^" not found in context")
846 | a::next -> (match a with
847 Some (Cic.Name(name),_) when name = id -> n
848 (*? magari al posto di _ qualcosaltro?*)
849 | _ -> find_in_context_aux next (n+1))
851 find_in_context_aux context 1
854 (* mi sembra quadratico *)
855 let rec filter_real_hyp context cont =
858 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
859 let n = find_in_context h cont in
860 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
861 | a::next -> debug(" no\n"); filter_real_hyp next cont
864 (* lifts everithing at the conclusion level *)
865 let rec superlift c n=
868 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
869 CicSubstitution.lift n a))] @ superlift next (n+1)
870 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
871 CicSubstitution.lift n a))] @ superlift next (n+1)
872 | _::next -> superlift next (n+1) (*?? ??*)
876 let equality_replace a b ~status =
877 debug("inizio EQ\n");
878 let module C = Cic in
879 let proof,goal = status in
880 let curi,metasenv,pbo,pty = proof in
881 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
882 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
883 let fresh_meta = ProofEngineHelpers.new_meta proof in
885 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
886 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
887 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
889 rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
890 ~status:((curi,metasenv',pbo,pty),goal)
892 let new_goals = fresh_meta::goals in
893 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
894 ^string_of_int( List.length goals)^"+ meta\n");
898 let tcl_fail a ~status:(proof,goal) =
900 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
905 let assumption_tac ~status:(proof,goal)=
906 let curi,metasenv,pbo,pty = proof in
907 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
909 let tac_list = List.map
910 ( fun x -> num := !num + 1;
912 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
913 | _ -> ("fake",tcl_fail 1)
917 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
920 (* !!!!! fix !!!!!!!!!! *)
921 let contradiction_tac ~status:(proof,goal)=
923 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
924 ~continuation:(Tacticals.then_
925 ~start:(Ring.elim_type_tac ~term:_False)
926 ~continuation:(assumption_tac))
930 (* ********************* TATTICA ******************************** *)
932 let rec fourier ~status:(s_proof,s_goal)=
933 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
934 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
937 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
938 debug_pcontext s_context;
940 let fhyp = String.copy "new_hyp_for_fourier" in
942 (* here we need to negate the thesis, but to do this we need to apply the right
943 theoreme,so let's parse our thesis *)
945 let th_to_appl = ref _Rfourier_not_le_gt in
947 Cic.Appl ( Cic.Const(u,boh)::args) ->
948 (match UriManager.string_of_uri u with
949 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
951 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
953 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
955 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
957 |_-> failwith "fourier can't be applyed")
958 |_-> failwith "fourier can't be applyed");
959 (* fix maybe strip_outer_cast goes here?? *)
961 (* now let's change our thesis applying the th and put it with hp *)
963 let proof,gl = Tacticals.then_
964 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
965 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
966 ~status:(s_proof,s_goal) in
967 let goal = if List.length gl = 1 then List.hd gl
968 else failwith "a new goal" in
970 debug ("port la tesi sopra e la nego. contesto :\n");
971 debug_pcontext s_context;
973 (* now we have all the right environment *)
975 let curi,metasenv,pbo,pty = proof in
976 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
979 (* now we want to convert hp to inequations, but first we must lift
980 everyting to thesis level, so that a variable has the save Rel(n)
981 in each hp ( needed by ineq1_of_term ) *)
983 (* ? fix if None ?????*)
984 (* fix change superlift with a real name *)
986 let l_context = superlift context 1 in
987 let hyps = filter_real_hyp l_context l_context in
989 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
993 (* transform hyps into inequations *)
995 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1000 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1003 let res=fourier_lineq (!lineq) in
1004 let tac=ref Tacticals.id_tac in
1006 (print_string "Tactic Fourier fails.\n";flush stdout;
1007 failwith "fourier_tac fails")
1010 match res with (*match res*)
1013 (* in lc we have the coefficient to "reduce" the system *)
1015 print_string "Fourier's method can prove the goal...\n";flush stdout;
1017 debug "I coeff di moltiplicazione rit sono: ";
1021 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1022 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1024 (List.combine (!lineq) lc);
1026 print_string (" quindi lutil e' lunga "^
1027 string_of_int (List.length (!lutil))^"\n");
1029 (* on construit la combinaison linéaire des inéquation *)
1031 (match (!lutil) with (*match (!lutil) *)
1033 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1035 let s=ref (h1.hstrict) in
1038 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1039 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1041 List.iter (fun (h,c) ->
1042 s:=(!s)||(h.hstrict);
1043 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1044 [_Rmult;rational_to_real c;h.hleft ] ]);
1045 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1046 [_Rmult;rational_to_real c;h.hright] ]))
1049 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1050 let tc=rational_to_real cres in
1053 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1055 debug "inizio a costruire tac1\n";
1056 Fourier.print_rational(c1);
1058 let tac1=ref ( fun ~status ->
1063 debug ("inizio t1 strict\n");
1064 let curi,metasenv,pbo,pty = proof in
1065 let metano,context,ty = List.find
1066 (function (m,_,_) -> m=goal) metasenv in
1067 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1068 debug ("ty = "^ CicPp.ppterm ty^"\n");
1069 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1070 ~continuations:[tac_use h1;tac_zero_inf_pos
1071 (rational_to_fraction c1)]
1076 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1077 ~continuations:[tac_use h1;tac_zero_inf_pos
1078 (rational_to_fraction c1)] ~status
1084 List.iter (fun (h,c) ->
1088 tac1:=(Tacticals.thens
1089 ~start:(PrimitiveTactics.apply_tac
1090 ~term:_Rfourier_lt_lt)
1091 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1092 (rational_to_fraction c)])
1096 Fourier.print_rational(c1);
1097 tac1:=(Tacticals.thens
1100 debug("INIZIO TAC 1 2\n");
1101 let curi,metasenv,pbo,pty = proof in
1102 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1104 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1105 debug ("ty = "^ CicPp.ppterm ty^"\n");
1106 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1107 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1108 (rational_to_fraction c)])
1114 tac1:=(Tacticals.thens
1115 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1116 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1117 (rational_to_fraction c)])
1121 tac1:=(Tacticals.thens
1122 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1123 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1124 (rational_to_fraction c)])
1128 s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1132 tac_zero_inf_false goal (rational_to_fraction cres)
1134 tac_zero_infeq_false goal (rational_to_fraction cres)
1136 tac:=(Tacticals.thens
1137 ~start:(my_cut ~term:ineq)
1138 ~continuations:[Tacticals.then_
1139 ~start:(fun ~status:(proof,goal as status) ->
1140 let curi,metasenv,pbo,pty = proof in
1141 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1143 PrimitiveTactics.change_tac ~what:ty
1144 ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1145 ~continuation:(Tacticals.then_
1146 ~start:(PrimitiveTactics.apply_tac ~term:
1147 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1148 ~continuation:(Tacticals.thens
1151 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1154 (match r with (p,gl) ->
1155 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1157 ~continuations:[(Tacticals.thens
1160 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1161 (match r with (p,gl) ->
1162 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1165 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1166 (* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
1167 di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
1168 parametri della equality_replace vengono passati al contrario? Oppure la
1169 tattica usa i parametri al contrario?
1170 CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac
1171 ~continuations:[Tacticals.then_
1173 fun ~status:(proof,goal as status) ->
1175 let curi,metasenv,pbo,pty = proof in
1176 let metano,context,ty = List.find (function (m,_,_) -> m=
1178 debug("ty = "^CicPp.ppterm ty^"\n");
1179 let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
1181 debug("fine ECCOCI\n");
1183 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1185 ;Tacticals.try_tactics
1186 ~tactics:[ "ring", (fun ~status ->
1187 debug("begin RING\n");
1188 let r = Ring.ring_tac ~status in
1189 debug ("end RING\n");
1191 ; "id", Tacticals.id_tac]
1196 fun ~status:(proof,goal as status) ->
1197 let curi,metasenv,pbo,pty = proof in
1198 let metano,context,ty = List.find (function (m,_,_) -> m=
1200 (* check if ty is of type *)
1202 debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1204 (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*)
1205 Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1208 let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1209 debug("fine MY_CHNGE\n");
1212 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1213 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1214 tac:=(Tacticals.thens
1215 ~start:(PrimitiveTactics.cut_tac ~term:_False)
1216 ~continuations:[Tacticals.then_
1217 ~start:(PrimitiveTactics.intros_tac ~name:"??")
1218 ~continuation:contradiction_tac
1222 |_-> assert false)(*match (!lutil) *)
1223 |_-> assert false); (*match res*)
1224 debug ("finalmente applico tac\n");
1225 (!tac ~status:(proof,goal))
1228 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;