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 (******************** THE FOURIER TACTIC ***********************)
29 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
30 des inéquations et équations sont entiers. En attendant la tactique Field.
36 let debug x = print_string ("____ "^x) ; flush stdout;;
38 let debug_pcontext x =
40 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
42 debug ("contesto : "^ (!str) ^ "\n")
45 (******************************************************************************
46 Operations on linear combinations.
48 Opérations sur les combinaisons linéaires affines.
49 La partie homogène d'une combinaison linéaire est en fait une table de hash
50 qui donne le coefficient d'un terme du calcul des constructions,
51 qui est zéro si le terme n'y est pas.
57 The type for linear combinations
59 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
65 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
71 @return the rational associated with x (coefficient)
75 (Hashtbl.find f.fhom x)
81 Adds c to the coefficient of x
90 let cx = flin_coef f x in
91 Hashtbl.remove f.fhom x;
92 Hashtbl.add f.fhom x (rplus cx c);
94 |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n");
95 let cx = flin_coef f x in
96 Hashtbl.remove f.fhom x;
97 Hashtbl.add f.fhom x (rplus cx c);
106 let flin_add_cste f c =
108 fcste=rplus f.fcste c}
112 @return a empty flin with r1 in fcste
114 let flin_one () = flin_add_cste (flin_zero()) r1;;
119 let flin_plus f1 f2 =
120 let f3 = flin_zero() in
121 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
122 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
123 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
129 let flin_minus f1 f2 =
130 let f3 = flin_zero() in
131 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
132 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
133 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
140 let f2 = flin_zero() in
141 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
142 flin_add_cste f2 (rmult a f.fcste);
146 (*****************************************************************************)
151 @raise Failure if conversion is impossible
152 @return rational proiection of t
154 let rec rational_of_term t =
155 (* fun to apply f to the first and second rational-term of l *)
156 let rat_of_binop f l =
157 let a = List.hd l and
158 b = List.hd(List.tl l) in
159 f (rational_of_term a) (rational_of_term b)
161 (* as before, but f is unary *)
162 let rat_of_unop f l =
163 f (rational_of_term (List.hd l))
166 | Cic.Cast (t1,t2) -> (rational_of_term t1)
167 | Cic.Appl (t1::next) ->
170 if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then
172 else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then
173 rat_of_unop rinv next
174 else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then
175 rat_of_binop rmult next
176 else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then
177 rat_of_binop rdiv next
178 else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then
179 rat_of_binop rplus next
180 else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then
181 rat_of_binop rminus next
182 else failwith "not a rational"
183 | _ -> failwith "not a rational")
184 | Cic.Const (u,boh) ->
185 if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then r1
186 else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then r0
187 else failwith "not a rational"
188 | _ -> failwith "not a rational"
192 let rational_of_const = rational_of_term;;
202 let rec flin_of_term t =
203 let fl_of_binop f l =
204 let a = List.hd l and
205 b = List.hd(List.tl l) in
206 f (flin_of_term a) (flin_of_term b)
210 | Cic.Cast (t1,t2) -> (flin_of_term t1)
211 | Cic.Appl (t1::next) ->
216 if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then
217 flin_emult (rop r1) (flin_of_term (List.hd next))
218 else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then
219 fl_of_binop flin_plus next
220 else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then
221 fl_of_binop flin_minus next
222 else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then
224 let arg1 = (List.hd next) and
225 arg2 = (List.hd(List.tl next))
227 if fails rational_of_term arg1
229 if fails rational_of_term arg2
231 ( (* prodotto tra 2 incognite ????? impossibile*)
232 failwith "Sistemi lineari!!!!\n"
237 Cic.Rel(n) -> (*trasformo al volo*)
238 (flin_add (flin_zero()) arg1 (rational_of_term arg2))
240 let tmp = flin_of_term arg1 in
241 flin_emult (rational_of_term arg2) (tmp)
244 if fails rational_of_term arg2
248 Cic.Rel(n) -> (*trasformo al volo*)
249 (flin_add (flin_zero()) arg2 (rational_of_term arg1))
251 let tmp = flin_of_term arg2 in
252 flin_emult (rational_of_term arg1) (tmp)
256 ( (*prodotto tra razionali*)
257 (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
261 (*let a = rational_of_term arg1 in
262 debug("ho fatto rational of term di "^CicPp.ppterm arg1^
263 " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
264 let a = flin_of_term arg1
267 let b = (rational_of_term arg2) in
268 debug("ho fatto rational of term di "^CicPp.ppterm arg2^
269 " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
270 (flin_add_cste (flin_zero()) (rmult a b))
273 _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
274 (flin_add (flin_zero()) arg2 a)
277 _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
278 (flin_add(flin_zero()) arg1 (rational_of_term arg2))
281 else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then
282 let a=(rational_of_term (List.hd next)) in
283 flin_add_cste (flin_zero()) (rinv a)
284 else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then
286 let b=(rational_of_term (List.hd(List.tl next))) in
289 let a = (rational_of_term (List.hd next)) in
290 (flin_add_cste (flin_zero()) (rdiv a b))
293 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
299 | Cic.Const (u,boh) ->
301 if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then flin_one ()
302 else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then flin_zero ()
306 with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
310 let flin_of_constr = flin_of_term;;
314 Translates a flin to (c,x) list
316 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
318 let flin_to_alist f =
320 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
324 (* Représentation des hypothèses qui sont des inéquations ou des équations.
328 The structure for ineq
330 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
331 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
338 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
341 let ineq1_of_term (h,t) =
342 match t with (* match t *)
343 Cic.Appl (t1::next) ->
344 let arg1= List.hd next in
345 let arg2= List.hd(List.tl next) in
346 (match t1 with (* match t1 *)
348 if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
353 hflin= flin_minus (flin_of_term arg1)
356 else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
361 hflin= flin_minus (flin_of_term arg2)
364 else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
369 hflin= flin_minus (flin_of_term arg1)
372 else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
377 hflin= flin_minus (flin_of_term arg2)
381 | Cic.MutInd (u,i,o) ->
382 if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then
385 let arg2= List.hd(List.tl (List.tl next)) in
388 if UriManager.eq u HelmLibraryObjects.Reals.r_URI then
393 hflin= flin_minus (flin_of_term arg1)
400 hflin= flin_minus (flin_of_term arg2)
406 |_-> assert false)(* match t1 *)
407 |_-> assert false (* match t *)
410 let ineq1_of_constr = ineq1_of_term;;
413 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
419 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
422 let rec print_sys l =
425 | (a,b)::next -> (print_rl a;
426 print_string (if b=true then "strict\n"else"\n");
431 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
434 let fourier_lineq lineq1 =
436 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
438 Hashtbl.iter (fun x c ->
439 try (Hashtbl.find hvar x;())
440 with _-> nvar:=(!nvar)+1;
441 Hashtbl.add hvar x (!nvar);
442 debug("aggiungo una var "^
443 string_of_int !nvar^" per "^
444 CicPp.ppterm x^"\n"))
448 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
449 let sys= List.map (fun h->
450 let v=Array.create ((!nvar)+1) r0 in
451 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c)
453 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
455 debug ("chiamo unsolvable sul sistema di "^
456 string_of_int (List.length sys) ^"\n");
461 (*****************************************************************************
462 Construction de la preuve en cas de succès de la méthode de Fourier,
463 i.e. on obtient une contradiction.
467 let _eqT = Cic.MutInd(HelmLibraryObjects.Logic.eq_URI, 0, []) ;;
468 let _False = Cic.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []) ;;
469 let _not = Cic.Const (HelmLibraryObjects.Logic.not_URI,[]);;
470 let _R0 = Cic.Const (HelmLibraryObjects.Reals.r0_URI,[]);;
471 let _R1 = Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);;
472 let _R = Cic.Const (HelmLibraryObjects.Reals.r_URI,[]);;
473 let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string
474 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;;
475 let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string
476 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;;
477 let _Rfourier_ge_to_le =Cic.Const ((UriManager.uri_of_string
478 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;;
479 let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string
480 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;;
481 let _Rfourier_le=Cic.Const ((UriManager.uri_of_string
482 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;;
483 let _Rfourier_le_le =Cic.Const ((UriManager.uri_of_string
484 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con"), []) ;;
485 let _Rfourier_le_lt =Cic.Const ((UriManager.uri_of_string
486 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con"), []) ;;
487 let _Rfourier_lt=Cic.Const ((UriManager.uri_of_string
488 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con"), []) ;;
489 let _Rfourier_lt_le =Cic.Const ((UriManager.uri_of_string
490 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con"), []) ;;
491 let _Rfourier_lt_lt =Cic.Const ((UriManager.uri_of_string
492 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con"), []) ;;
493 let _Rfourier_not_ge_lt = Cic.Const ((UriManager.uri_of_string
494 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con"), []) ;;
495 let _Rfourier_not_gt_le = Cic.Const ((UriManager.uri_of_string
496 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con"), []) ;;
497 let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string
498 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;;
499 let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string
500 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;;
501 let _Rinv = Cic.Const (HelmLibraryObjects.Reals.rinv_URI, []);;
502 let _Rinv_R1 = Cic.Const(HelmLibraryObjects.Reals.rinv_r1_URI, []);;
503 let _Rle = Cic.Const (HelmLibraryObjects.Reals.rle_URI, []);;
504 let _Rle_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
505 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;;
506 let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string
507 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con"), []) ;;
508 let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string
509 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;;
510 let _Rle_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
511 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;;
512 let _Rlt = Cic.Const (HelmLibraryObjects.Reals.rlt_URI, []);;
513 let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
514 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;;
515 let _Rlt_not_le = Cic.Const ((UriManager.uri_of_string
516 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con"), []) ;;
517 let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string
518 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;;
519 let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
520 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;;
521 let _Rminus = Cic.Const (HelmLibraryObjects.Reals.rminus_URI, []);;
522 let _Rmult = Cic.Const (HelmLibraryObjects.Reals.rmult_URI, []);;
523 let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string
524 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;;
525 let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string
526 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;;
527 let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string
528 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;;
529 let _Ropp = Cic.Const (HelmLibraryObjects.Reals.ropp_URI, []);;
530 let _Rplus = Cic.Const (HelmLibraryObjects.Reals.rplus_URI, []);;
532 (******************************************************************************)
534 let is_int x = (x.den)=1
537 (* fraction = couple (num,den) *)
538 let rec rational_to_fraction x= (x.num,x.den)
541 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
544 let rec int_to_real_aux n =
546 0 -> _R0 (* o forse R0 + R0 ????? *)
548 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
553 let x = int_to_real_aux (abs n) in
555 Cic.Appl [ _Ropp ; x ]
561 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
564 let rational_to_real x =
565 let (n,d)=rational_to_fraction x in
566 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
569 (* preuve que 0<n*1/d
572 let tac_zero_inf_pos (n,d) status =
573 (*let cste = pf_parse_constr gl in*)
574 let pall str (proof,goal) t =
575 debug ("tac "^str^" :\n" );
576 let curi,metasenv,pbo,pty = proof in
577 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
578 debug ("th = "^ CicPp.ppterm t ^"\n");
579 debug ("ty = "^ CicPp.ppterm ty^"\n");
582 (fun status -> pall "n0" status _Rlt_zero_1 ;
583 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in
585 (fun status -> pall "d0" status _Rlt_zero_1 ;
586 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 status ) in
590 tacn:=(Tacticals.then_ ~start:(fun status -> pall ("n"^string_of_int i)
591 status _Rlt_zero_pos_plus1;
592 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 status)
593 ~continuation:!tacn);
596 tacd:=(Tacticals.then_ ~start:(fun status -> pall "d"
597 status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
598 ~term:_Rlt_zero_pos_plus1 status) ~continuation:!tacd);
603 debug("TAC ZERO INF POS\n");
605 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
614 (* preuve que 0<=n*1/d
617 let tac_zero_infeq_pos gl (n,d) status =
618 (*let cste = pf_parse_constr gl in*)
619 debug("inizio tac_zero_infeq_pos\n");
622 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
624 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
627 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
629 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
630 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
633 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
634 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
637 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
638 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) status in
639 debug("fine tac_zero_infeq_pos\n");
645 (* preuve que 0<(-n)*(1/d) => False
648 let tac_zero_inf_false gl (n,d) status=
649 debug("inizio tac_zero_inf_false\n");
651 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 status) in
655 (debug "2\n";let r = (Tacticals.then_ ~start:(
657 let (proof, goal) = status in
658 let curi,metasenv,pbo,pty = proof in
659 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
660 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
661 ^ CicPp.ppterm ty ^"\n");
662 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt status in
663 debug("!!!!!!!!!2\n");
666 ~continuation:(tac_zero_infeq_pos gl (-n,d))) status in
672 (* preuve que 0<=n*(1/d) => False ; n est negatif
675 let tac_zero_infeq_false gl (n,d) status=
676 let (proof, goal) = status in
677 debug("stat tac_zero_infeq_false\n");
679 let curi,metasenv,pbo,pty = proof in
680 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
682 debug("faccio fold di " ^ CicPp.ppterm
686 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
689 debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
690 (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
693 (ReductionTactics.fold_tac ~reduction:CicReduction.whd
694 ~also_in_hypotheses:false
699 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
704 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
705 ~continuation:(tac_zero_inf_pos (-n,d))) status in
706 debug("end tac_zero_infeq_false\n");
709 Tacticals.id_tac status
714 (* *********** ********** ******** ??????????????? *********** **************)
716 let apply_type_tac ~cast:t ~applist:al (proof,goal) =
717 let curi,metasenv,pbo,pty = proof in
718 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
719 let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
721 CicMkImplicit.identity_relocation_list_for_metavariable context in
722 let metasenv' = (fresh_meta,context,t)::metasenv in
723 let proof' = curi,metasenv',pbo,pty in
725 PrimitiveTactics.apply_tac
726 (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
727 ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
730 proof'',fresh_meta::goals
737 let my_cut ~term:c (proof,goal)=
738 let curi,metasenv,pbo,pty = proof in
739 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
741 debug("my_cut di "^CicPp.ppterm c^"\n");
744 let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
746 CicMkImplicit.identity_relocation_list_for_metavariable context in
747 let metasenv' = (fresh_meta,context,c)::metasenv in
748 let proof' = curi,metasenv',pbo,pty in
750 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
751 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
754 (* We permute the generated goals to be consistent with Coq *)
757 | he::tl -> proof'',he::fresh_meta::tl
761 let exact = PrimitiveTactics.exact_tac;;
763 let tac_use h status =
764 let (proof, goal) = status in
765 debug("Inizio TC_USE\n");
766 let curi,metasenv,pbo,pty = proof in
767 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
768 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
769 debug ("ty = "^ CicPp.ppterm ty^"\n");
773 "Rlt" -> exact ~term:h.hname status
774 |"Rle" -> exact ~term:h.hname status
775 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
776 ~term:_Rfourier_gt_to_lt)
777 ~continuation:(exact ~term:h.hname)) status
778 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
779 ~term:_Rfourier_ge_to_le)
780 ~continuation:(exact ~term:h.hname)) status
781 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
782 ~term:_Rfourier_eqLR_to_le)
783 ~continuation:(exact ~term:h.hname)) status
784 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
785 ~term:_Rfourier_eqRL_to_le)
786 ~continuation:(exact ~term:h.hname)) status
789 debug("Fine TAC_USE\n");
797 Cic.Appl ( Cic.Const(u,boh)::next) ->
798 (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI or
799 UriManager.eq u HelmLibraryObjects.Reals.rgt_URI or
800 UriManager.eq u HelmLibraryObjects.Reals.rle_URI or
801 UriManager.eq u HelmLibraryObjects.Reals.rge_URI then true
802 else if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then
803 (match (List.hd next) with
804 Cic.Const (uri,_) when
805 UriManager.eq uri HelmLibraryObjects.Reals.r_URI
812 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
815 Cic.Appl(Array.to_list a)
818 (* Résolution d'inéquations linéaires dans R *)
819 let rec strip_outer_cast c = match c with
820 | Cic.Cast (c,_) -> strip_outer_cast c
824 (*let find_in_context id context =
825 let rec find_in_context_aux c n =
827 [] -> failwith (id^" not found in context")
828 | a::next -> (match a with
829 Some (Cic.Name(name),_) when name = id -> n
830 (*? magari al posto di _ qualcosaltro?*)
831 | _ -> find_in_context_aux next (n+1))
833 find_in_context_aux context 1
836 (* mi sembra quadratico *)
837 let rec filter_real_hyp context cont =
840 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
841 let n = find_in_context h cont in
842 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
843 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
844 | a::next -> debug(" no\n"); filter_real_hyp next cont
846 let filter_real_hyp context _ =
847 let rec filter_aux context num =
850 | Some(Cic.Name(h),Cic.Decl(t))::next ->
852 (*let n = find_in_context h cont in*)
853 debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
854 [(Cic.Rel(num),t)] @ filter_aux next (num+1)
856 | a::next -> filter_aux next (num+1)
862 (* lifts everithing at the conclusion level *)
863 let rec superlift c n=
866 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
867 CicSubstitution.lift n a))] @ superlift next (n+1)
868 | Some(name,Cic.Def(a,None))::next -> [Some(name,Cic.Def((
869 CicSubstitution.lift n a),None))] @ superlift next (n+1)
870 | Some(name,Cic.Def(a,Some ty))::next -> [Some(name,Cic.Def((
871 CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ 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 = CicUtil.lookup_meta goal metasenv in
882 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
883 let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
885 CicMkImplicit.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 EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
890 ((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 (proof,goal) =
900 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
904 (* Galla: moved in variousTactics.ml
905 let assumption_tac (proof,goal)=
906 let curi,metasenv,pbo,pty = proof in
907 let metano,context,ty = CicUtil.lookup_meta 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 (proof,goal)
920 (* Galla: moved in negationTactics.ml
921 (* !!!!! fix !!!!!!!!!! *)
922 let contradiction_tac (proof,goal)=
924 (*inutile sia questo che quello prima della chiamata*)
925 ~start:PrimitiveTactics.intros_tac
926 ~continuation:(Tacticals.then_
927 ~start:(VariousTactics.elim_type_tac ~term:_False)
928 ~continuation:(assumption_tac))
933 (* ********************* TATTICA ******************************** *)
935 let rec fourier (s_proof,s_goal)=
936 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
937 let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
938 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
939 debug_pcontext s_context;
941 let fhyp = String.copy "new_hyp_for_fourier" in
943 (* here we need to negate the thesis, but to do this we need to apply the right
944 theoreme,so let's parse our thesis *)
946 let th_to_appl = ref _Rfourier_not_le_gt in
948 Cic.Appl ( Cic.Const(u,boh)::args) ->
950 (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
952 else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
954 else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
956 else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
958 else failwith "fourier can't be applyed")
959 |_-> failwith "fourier can't be applyed");
960 (* fix maybe strip_outer_cast goes here?? *)
962 (* now let's change our thesis applying the th and put it with hp *)
966 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
967 ~continuation:(PrimitiveTactics.intros_tac ())
969 let goal = if List.length gl = 1 then List.hd gl
970 else failwith "a new goal" in
972 debug ("port la tesi sopra e la nego. contesto :\n");
973 debug_pcontext s_context;
975 (* now we have all the right environment *)
977 let curi,metasenv,pbo,pty = proof in
978 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
981 (* now we want to convert hp to inequations, but first we must lift
982 everyting to thesis level, so that a variable has the save Rel(n)
983 in each hp ( needed by ineq1_of_term ) *)
985 (* ? fix if None ?????*)
986 (* fix change superlift with a real name *)
988 let l_context = superlift context 1 in
989 let hyps = filter_real_hyp l_context l_context in
991 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
995 (* transform hyps into inequations *)
997 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1002 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1005 let res=fourier_lineq (!lineq) in
1006 let tac=ref Tacticals.id_tac in
1008 (print_string "Tactic Fourier fails.\n";flush stdout;
1009 failwith "fourier_tac fails")
1012 match res with (*match res*)
1015 (* in lc we have the coefficient to "reduce" the system *)
1017 print_string "Fourier's method can prove the goal...\n";flush stdout;
1019 debug "I coeff di moltiplicazione rit sono: ";
1023 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1024 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1026 (List.combine (!lineq) lc);
1028 print_string (" quindi lutil e' lunga "^
1029 string_of_int (List.length (!lutil))^"\n");
1031 (* on construit la combinaison linéaire des inéquation *)
1033 (match (!lutil) with (*match (!lutil) *)
1035 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1037 let s=ref (h1.hstrict) in
1040 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1041 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1043 List.iter (fun (h,c) ->
1044 s:=(!s)||(h.hstrict);
1045 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1046 [_Rmult;rational_to_real c;h.hleft ] ]);
1047 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1048 [_Rmult;rational_to_real c;h.hright] ]))
1051 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1052 let tc=rational_to_real cres in
1055 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1057 debug "inizio a costruire tac1\n";
1058 Fourier.print_rational(c1);
1060 let tac1=ref ( fun status ->
1065 debug ("inizio t1 strict\n");
1066 let curi,metasenv,pbo,pty = proof in
1067 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1068 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1069 debug ("ty = "^ CicPp.ppterm ty^"\n");
1070 PrimitiveTactics.apply_tac ~term:_Rfourier_lt status)
1071 ~continuations:[tac_use h1;tac_zero_inf_pos
1072 (rational_to_fraction c1)]
1077 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1078 ~continuations:[tac_use h1;tac_zero_inf_pos
1079 (rational_to_fraction c1)] status
1085 List.iter (fun (h,c) ->
1089 tac1:=(Tacticals.thens
1090 ~start:(PrimitiveTactics.apply_tac
1091 ~term:_Rfourier_lt_lt)
1092 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1093 (rational_to_fraction c)])
1097 Fourier.print_rational(c1);
1098 tac1:=(Tacticals.thens
1101 debug("INIZIO TAC 1 2\n");
1102 let curi,metasenv,pbo,pty = proof in
1103 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
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.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
1139 ~start:(fun status ->
1140 let (proof, goal) = status in
1141 let curi,metasenv,pbo,pty = proof in
1142 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
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 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1152 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1155 (match r with (p,gl) ->
1156 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1158 ~continuations:[(Tacticals.thens
1161 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 status in
1162 (match r with (p,gl) ->
1163 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1166 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1167 ;Tacticals.try_tactics
1168 ~tactics:[ "ring", (fun status ->
1169 debug("begin RING\n");
1170 let r = Ring.ring_tac status in
1171 debug ("end RING\n");
1173 ; "id", Tacticals.id_tac]
1175 ;(*Tacticals.id_tac*)
1180 let (proof, goal) = status in
1181 let curi,metasenv,pbo,pty = proof in
1182 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1183 (* check if ty is of type *)
1185 debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1187 Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1190 let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 status in
1191 debug("fine MY_CHNGE\n");
1195 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1196 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1198 |_-> assert false)(*match (!lutil) *)
1199 |_-> assert false); (*match res*)
1200 debug ("finalmente applico tac\n");
1202 let r = !tac (proof,goal) in
1203 debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1208 let fourier_tac (proof,goal) = fourier (proof,goal);;