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) ;
81 let rewrite_simpl_tac ~term =
82 Tacticals.then_ ~start:(rewrite_tac ~term)
83 ~continuation:ReductionTactics.simpl_tac
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 @return proiection on string of t
205 let rec string_of_term t =
207 Cic.Cast (t,_) -> string_of_term t
208 |Cic.Const (u,_) -> UriManager.string_of_uri u
209 |Cic.Var (u,_) -> UriManager.string_of_uri u
210 | _ -> "not_of_constant"
214 let string_of_constr = string_of_term
220 @raise Failure if conversion is impossible
221 @return rational proiection of t
223 let rec rational_of_term t =
224 (* fun to apply f to the first and second rational-term of l *)
225 let rat_of_binop f l =
226 let a = List.hd l and
227 b = List.hd(List.tl l) in
228 f (rational_of_term a) (rational_of_term b)
230 (* as before, but f is unary *)
231 let rat_of_unop f l =
232 f (rational_of_term (List.hd l))
235 | Cic.Cast (t1,t2) -> (rational_of_term t1)
236 | Cic.Appl (t1::next) ->
239 (match (UriManager.string_of_uri u) with
240 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
242 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
243 rat_of_unop rinv next
244 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
245 rat_of_binop rmult next
246 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
247 rat_of_binop rdiv next
248 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
249 rat_of_binop rplus next
250 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
251 rat_of_binop rminus next
252 | _ -> failwith "not a rational")
253 | _ -> failwith "not a rational")
254 | Cic.Const (u,boh) ->
255 (match (UriManager.string_of_uri u) with
256 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
257 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
258 | _ -> failwith "not a rational")
259 | _ -> failwith "not a rational"
263 let rational_of_const = rational_of_term;;
267 let rec flin_of_term t =
268 let fl_of_binop f l =
269 let a = List.hd l and
270 b = List.hd(List.tl l) in
271 f (flin_of_term a) (flin_of_term b)
275 | Cic.Cast (t1,t2) -> (flin_of_term t1)
276 | Cic.Appl (t1::next) ->
281 match (UriManager.string_of_uri u) with
282 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
283 flin_emult (rop r1) (flin_of_term (List.hd next))
284 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
285 fl_of_binop flin_plus next
286 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
287 fl_of_binop flin_minus next
288 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
290 let arg1 = (List.hd next) and
291 arg2 = (List.hd(List.tl next))
295 let a = rational_of_term arg1 in
298 let b = (rational_of_term arg2) in
299 (flin_add_cste (flin_zero()) (rmult a b))
302 _ -> (flin_add (flin_zero()) arg2 a)
305 _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
307 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
308 let a=(rational_of_term (List.hd next)) in
309 flin_add_cste (flin_zero()) (rinv a)
310 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
312 let b=(rational_of_term (List.hd(List.tl next))) in
315 let a = (rational_of_term (List.hd next)) in
316 (flin_add_cste (flin_zero()) (rdiv a b))
319 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
325 | Cic.Const (u,boh) ->
327 match (UriManager.string_of_uri u) with
328 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
329 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
333 with _ -> flin_add (flin_zero()) t r1
337 let flin_of_constr = flin_of_term;;
341 Translates a flin to (c,x) list
343 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
345 let flin_to_alist f =
347 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
351 (* Représentation des hypothèses qui sont des inéquations ou des équations.
355 The structure for ineq
357 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
358 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
365 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
368 let ineq1_of_term (h,t) =
369 match t with (* match t *)
370 Cic.Appl (t1::next) ->
371 let arg1= List.hd next in
372 let arg2= List.hd(List.tl next) in
373 (match t1 with (* match t1 *)
375 (match UriManager.string_of_uri u with (* match u *)
376 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
381 hflin= flin_minus (flin_of_term arg1)
384 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
389 hflin= flin_minus (flin_of_term arg2)
392 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
397 hflin= flin_minus (flin_of_term arg1)
400 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
405 hflin= flin_minus (flin_of_term arg2)
408 |_->assert false)(* match u *)
409 | Cic.MutInd (u,i,o) ->
410 (match UriManager.string_of_uri u with
411 "cic:/Coq/Init/Logic_Type/eqT.con" ->
414 let arg2= List.hd(List.tl (List.tl next)) in
417 (match UriManager.string_of_uri u with
418 "cic:/Coq/Reals/Rdefinitions/R.con"->
423 hflin= flin_minus (flin_of_term arg1)
430 hflin= flin_minus (flin_of_term arg2)
436 |_-> assert false)(* match t1 *)
437 |_-> assert false (* match t *)
440 let ineq1_of_constr = ineq1_of_term;;
443 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
449 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
452 let rec print_sys l =
455 | (a,b)::next -> (print_rl a;
456 print_string (if b=true then "strict\n"else"\n");
461 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
464 let fourier_lineq lineq1 =
466 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
468 Hashtbl.iter (fun x c ->
469 try (Hashtbl.find hvar x;())
470 with _-> nvar:=(!nvar)+1;
471 Hashtbl.add hvar x (!nvar))
475 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
476 let sys= List.map (fun h->
477 let v=Array.create ((!nvar)+1) r0 in
478 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
480 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
482 debug ("chiamo unsolvable sul sistema di "^
483 string_of_int (List.length sys) ^"\n");
488 (*****************************************************************************
489 Construction de la preuve en cas de succès de la méthode de Fourier,
490 i.e. on obtient une contradiction.
495 Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [];;
497 Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [];;
499 Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") [];;
501 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") [];;
503 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") [];;
505 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") [];;
506 let _Rfourier_eqLR_to_le=
508 (UriManager.uri_of_string
509 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [];;
510 let _Rfourier_eqRL_to_le =
512 (UriManager.uri_of_string
513 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [];;
514 let _Rfourier_ge_to_le =
516 (UriManager.uri_of_string
517 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [];;
518 let _Rfourier_gt_to_lt =
520 (UriManager.uri_of_string
521 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [];;
524 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con")[];;
525 let _Rfourier_le_le =
527 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con")
529 let _Rfourier_le_lt =
531 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con")
535 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") []
537 let _Rfourier_lt_le =
539 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con")
542 let _Rfourier_lt_lt =
544 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con")
547 let _Rfourier_not_ge_lt =
549 (UriManager.uri_of_string
550 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [];;
551 let _Rfourier_not_gt_le =
553 (UriManager.uri_of_string
554 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [];;
555 let _Rfourier_not_le_gt =
557 (UriManager.uri_of_string
558 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [];;
559 let _Rfourier_not_lt_ge =
561 (UriManager.uri_of_string
562 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [];;
564 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con")[];;
566 Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [];;
568 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") [];;
569 let _Rle_mult_inv_pos =
571 (UriManager.uri_of_string
572 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [];;
575 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [];;
578 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [];;
579 let _Rle_zero_pos_plus1 =
581 (UriManager.uri_of_string
582 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [];;
585 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con")
589 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") [];;
590 let _Rlt_mult_inv_pos =
592 (UriManager.uri_of_string
593 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [];;
596 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [];;
599 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [];;
600 let _Rlt_zero_pos_plus1 =
602 (UriManager.uri_of_string
603 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [];;
605 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con")
609 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con")
614 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [];;
617 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [];;
620 (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [];;
622 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") []
625 Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") []
629 (UriManager.uri_of_string
630 "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") [];;
632 (******************************************************************************)
634 let is_int x = (x.den)=1
637 (* fraction = couple (num,den) *)
638 let rec rational_to_fraction x= (x.num,x.den)
641 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
644 let rec int_to_real_aux n =
646 0 -> _R0 (* o forse R0 + R0 ????? *)
648 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
653 let x = int_to_real_aux (abs n) in
655 Cic.Appl [ _Ropp ; x ]
661 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
664 let rational_to_real x =
665 let (n,d)=rational_to_fraction x in
666 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
669 (* preuve que 0<n*1/d
672 let tac_zero_inf_pos (n,d) ~status =
673 (*let cste = pf_parse_constr gl in*)
674 let pall str ~status:(proof,goal) t =
675 debug ("tac "^str^" :\n" );
676 let curi,metasenv,pbo,pty = proof in
677 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
678 debug ("th = "^ CicPp.ppterm t ^"\n");
679 debug ("ty = "^ CicPp.ppterm ty^"\n");
682 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
683 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
685 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
686 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
690 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
691 ~status _Rlt_zero_pos_plus1;
692 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
693 ~continuation:!tacn);
696 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
697 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
698 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
703 debug("TAC ZERO INF POS\n");
705 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
714 (* preuve que 0<=n*1/d
717 let tac_zero_infeq_pos gl (n,d) ~status =
718 (*let cste = pf_parse_constr gl in*)
719 debug("inizio tac_zero_infeq_pos\n");
722 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
724 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
727 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
729 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
730 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
733 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
734 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
737 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
738 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
739 debug("fine tac_zero_infeq_pos\n");
745 (* preuve que 0<(-n)*(1/d) => False
748 let tac_zero_inf_false gl (n,d) ~status=
749 debug("inizio tac_zero_inf_false\n");
751 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
755 (debug "2\n";let r = (Tacticals.then_ ~start:(
756 fun ~status:(proof,goal as status) ->
757 let curi,metasenv,pbo,pty = proof in
758 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
759 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
760 ^ CicPp.ppterm ty ^"\n");
761 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
762 debug("!!!!!!!!!2\n");
765 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
771 (* preuve que 0<=(-n)*(1/d) => False
774 let tac_zero_infeq_false gl (n,d) ~status=
775 debug("stat tac_zero_infeq_false");
777 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
778 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
779 debug("stat tac_zero_infeq_false");
784 (* *********** ********** ******** ??????????????? *********** **************)
786 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
787 let curi,metasenv,pbo,pty = proof in
788 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
789 let fresh_meta = ProofEngineHelpers.new_meta proof in
791 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
792 let metasenv' = (fresh_meta,context,t)::metasenv in
793 let proof' = curi,metasenv',pbo,pty in
795 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta
796 (fresh_meta,irl),t))::al)) ~status:(proof',goal)
798 proof'',fresh_meta::goals
805 let my_cut ~term:c ~status:(proof,goal)=
806 let curi,metasenv,pbo,pty = proof in
807 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
809 let fresh_meta = ProofEngineHelpers.new_meta proof in
811 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
812 let metasenv' = (fresh_meta,context,c)::metasenv in
813 let proof' = curi,metasenv',pbo,pty in
815 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
816 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
817 ~status:(proof',goal)
819 (* We permute the generated goals to be consistent with Coq *)
822 | he::tl -> proof'',he::fresh_meta::tl
826 let exact = PrimitiveTactics.exact_tac;;
828 let tac_use h ~status:(proof,goal as status) =
829 debug("Inizio TC_USE\n");
830 let curi,metasenv,pbo,pty = proof in
831 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
832 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
833 debug ("ty = "^ CicPp.ppterm ty^"\n");
837 "Rlt" -> exact ~term:h.hname ~status
838 |"Rle" -> exact ~term:h.hname ~status
839 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
840 ~term:_Rfourier_gt_to_lt)
841 ~continuation:(exact ~term:h.hname)) ~status
842 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
843 ~term:_Rfourier_ge_to_le)
844 ~continuation:(exact ~term:h.hname)) ~status
845 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
846 ~term:_Rfourier_eqLR_to_le)
847 ~continuation:(exact ~term:h.hname)) ~status
848 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
849 ~term:_Rfourier_eqRL_to_le)
850 ~continuation:(exact ~term:h.hname)) ~status
853 debug("Fine TAC_USE\n");
861 Cic.Appl ( Cic.Const(u,boh)::next) ->
862 (match (UriManager.string_of_uri u) with
863 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
864 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
865 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
866 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
867 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
868 (match (List.hd next) with
869 Cic.Const (uri,_) when
870 UriManager.string_of_uri uri =
871 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
877 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
880 Cic.Appl(Array.to_list a)
883 (* Résolution d'inéquations linéaires dans R *)
884 let rec strip_outer_cast c = match c with
885 | Cic.Cast (c,_) -> strip_outer_cast c
889 let find_in_context id context =
890 let rec find_in_context_aux c n =
892 [] -> failwith (id^" not found in context")
893 | a::next -> (match a with
894 Some (Cic.Name(name),_) when name = id -> n
895 (*? magari al posto di _ qualcosaltro?*)
896 | _ -> find_in_context_aux next (n+1))
898 find_in_context_aux context 1
901 (* mi sembra quadratico *)
902 let rec filter_real_hyp context cont =
905 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
906 let n = find_in_context h cont in
907 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
908 | a::next -> debug(" no\n"); filter_real_hyp next cont
911 (* lifts everithing at the conclusion level *)
912 let rec superlift c n=
915 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
916 CicSubstitution.lift n a))] @ superlift next (n+1)
917 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
918 CicSubstitution.lift n a))] @ superlift next (n+1)
919 | _::next -> superlift next (n+1) (*?? ??*)
923 let equality_replace a b ~status =
924 debug("inizio EQ\n");
925 let module C = Cic in
926 let proof,goal = status in
927 let curi,metasenv,pbo,pty = proof in
928 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
929 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
930 let fresh_meta = ProofEngineHelpers.new_meta proof in
932 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
933 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
934 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
936 rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
937 ~status:((curi,metasenv',pbo,pty),goal)
939 let new_goals = fresh_meta::goals in
940 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
941 ^string_of_int( List.length goals)^"+ meta\n");
945 let tcl_fail a ~status:(proof,goal) =
947 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
952 let assumption_tac ~status:(proof,goal)=
953 let curi,metasenv,pbo,pty = proof in
954 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
956 let tac_list = List.map
957 ( fun x -> num := !num + 1;
959 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
960 | _ -> ("fake",tcl_fail 1)
964 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
967 (* !!!!! fix !!!!!!!!!! *)
968 let contradiction_tac ~status:(proof,goal)=
970 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
971 ~continuation:(Tacticals.then_
972 ~start:(Ring.elim_type_tac ~term:_False)
973 ~continuation:(assumption_tac))
977 (* ********************* TATTICA ******************************** *)
979 let rec fourier ~status:(s_proof,s_goal)=
980 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
981 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
984 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
985 debug_pcontext s_context;
987 let fhyp = String.copy "new_hyp_for_fourier" in
989 (* here we need to negate the thesis, but to do this we need to apply the right
990 theoreme,so let's parse our thesis *)
992 let th_to_appl = ref _Rfourier_not_le_gt in
994 Cic.Appl ( Cic.Const(u,boh)::args) ->
995 (match UriManager.string_of_uri u with
996 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
998 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
1000 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
1002 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
1004 |_-> failwith "fourier can't be applyed")
1005 |_-> failwith "fourier can't be applyed");
1006 (* fix maybe strip_outer_cast goes here?? *)
1008 (* now let's change our thesis applying the th and put it with hp *)
1010 let proof,gl = Tacticals.then_
1011 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
1012 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
1013 ~status:(s_proof,s_goal) in
1014 let goal = if List.length gl = 1 then List.hd gl
1015 else failwith "a new goal" in
1017 debug ("port la tesi sopra e la nego. contesto :\n");
1018 debug_pcontext s_context;
1020 (* now we have all the right environment *)
1022 let curi,metasenv,pbo,pty = proof in
1023 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1026 (* now we want to convert hp to inequations, but first we must lift
1027 everyting to thesis level, so that a variable has the save Rel(n)
1028 in each hp ( needed by ineq1_of_term ) *)
1030 (* ? fix if None ?????*)
1031 (* fix change superlift with a real name *)
1033 let l_context = superlift context 1 in
1034 let hyps = filter_real_hyp l_context l_context in
1036 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
1038 let lineq =ref [] in
1040 (* transform hyps into inequations *)
1042 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1047 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1050 let res=fourier_lineq (!lineq) in
1051 let tac=ref Ring.id_tac in
1053 (print_string "Tactic Fourier fails.\n";flush stdout;
1054 failwith "fourier_tac fails")
1057 match res with (*match res*)
1060 (* in lc we have the coefficient to "reduce" the system *)
1062 print_string "Fourier's method can prove the goal...\n";flush stdout;
1064 debug "I coeff di moltiplicazione rit sono: ";
1068 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1069 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1071 (List.combine (!lineq) lc);
1073 print_string (" quindi lutil e' lunga "^
1074 string_of_int (List.length (!lutil))^"\n");
1076 (* on construit la combinaison linéaire des inéquation *)
1078 (match (!lutil) with (*match (!lutil) *)
1080 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1082 let s=ref (h1.hstrict) in
1085 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1086 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1088 List.iter (fun (h,c) ->
1089 s:=(!s)||(h.hstrict);
1090 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1091 [_Rmult;rational_to_real c;h.hleft ] ]);
1092 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1093 [_Rmult;rational_to_real c;h.hright] ]))
1096 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1097 let tc=rational_to_real cres in
1100 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1102 debug "inizio a costruire tac1\n";
1103 Fourier.print_rational(c1);
1105 let tac1=ref ( fun ~status ->
1110 debug ("inizio t1 strict\n");
1111 let curi,metasenv,pbo,pty = proof in
1112 let metano,context,ty = List.find
1113 (function (m,_,_) -> m=goal) metasenv in
1114 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1115 debug ("ty = "^ CicPp.ppterm ty^"\n");
1116 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1117 ~continuations:[tac_use h1;tac_zero_inf_pos
1118 (rational_to_fraction c1)]
1123 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1124 ~continuations:[tac_use h1;tac_zero_inf_pos
1125 (rational_to_fraction c1)] ~status
1131 List.iter (fun (h,c) ->
1135 tac1:=(Tacticals.thens
1136 ~start:(PrimitiveTactics.apply_tac
1137 ~term:_Rfourier_lt_lt)
1138 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1139 (rational_to_fraction c)])
1143 Fourier.print_rational(c1);
1144 tac1:=(Tacticals.thens
1147 debug("INIZIO TAC 1 2\n");
1148 let curi,metasenv,pbo,pty = proof in
1149 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1151 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1152 debug ("ty = "^ CicPp.ppterm ty^"\n");
1153 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1154 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1155 (rational_to_fraction c)])
1161 tac1:=(Tacticals.thens
1162 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1163 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1164 (rational_to_fraction c)])
1168 tac1:=(Tacticals.thens
1169 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1170 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1171 (rational_to_fraction c)])
1175 s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1179 tac_zero_inf_false goal (rational_to_fraction cres)
1181 tac_zero_infeq_false goal (rational_to_fraction cres)
1183 tac:=(Tacticals.thens
1184 ~start:(my_cut ~term:ineq)
1185 ~continuations:[Tacticals.then_
1186 ~start:(fun ~status:(proof,goal as status) ->
1187 let curi,metasenv,pbo,pty = proof in
1188 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1190 PrimitiveTactics.change_tac ~what:ty
1191 ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1192 ~continuation:(Tacticals.then_
1193 ~start:(PrimitiveTactics.apply_tac ~term:
1194 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1195 ~continuation:(Tacticals.thens
1198 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1201 (match r with (p,gl) ->
1202 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1204 ~continuations:[(Tacticals.thens
1207 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1208 (match r with (p,gl) ->
1209 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1212 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1213 (* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
1214 di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i
1215 parametri della equality_replace vengono passati al contrario? Oppure la
1216 tattica usa i parametri al contrario?
1217 ~continuations:[Tacticals.then_
1219 fun ~status:(proof,goal as status) ->
1221 let curi,metasenv,pbo,pty = proof in
1222 let metano,context,ty = List.find (function (m,_,_) -> m=
1224 debug("ty = "^CicPp.ppterm ty^"\n");
1225 let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
1227 debug("fine ECCOCI\n");
1229 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1231 ;Tacticals.try_tactics
1232 ~tactics:[ "ring", (fun ~status ->
1233 debug("begin RING\n");
1234 let r = Ring.ring_tac ~status in
1235 debug ("end RING\n");
1237 ; "id", Ring.id_tac]
1239 (* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
1241 ;!tac1]);(*end tac:=*)
1242 tac:=(Tacticals.thens
1243 ~start:(PrimitiveTactics.cut_tac ~term:_False)
1244 ~continuations:[Tacticals.then_
1245 ~start:(PrimitiveTactics.intros_tac ~name:"??")
1246 ~continuation:contradiction_tac
1250 |_-> assert false)(*match (!lutil) *)
1251 |_-> assert false); (*match res*)
1252 debug ("finalmente applico tac\n");
1253 (!tac ~status:(proof,goal))
1256 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;