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.
37 let debug x = print_string ("____ "^x) ; flush stdout;;
39 let debug_pcontext x =
41 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
43 debug ("contesto : "^ (!str) ^ "\n")
46 (******************************************************************************
47 Operations on linear combinations.
49 Opérations sur les combinaisons linéaires affines.
50 La partie homogène d'une combinaison linéaire est en fait une table de hash
51 qui donne le coefficient d'un terme du calcul des constructions,
52 qui est zéro si le terme n'y est pas.
58 The type for linear combinations
60 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
66 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
72 @return the rational associated with x (coefficient)
76 (Hashtbl.find f.fhom x)
82 Adds c to the coefficient of x
91 let cx = flin_coef f x in
92 Hashtbl.remove f.fhom x;
93 Hashtbl.add f.fhom x (rplus cx c);
95 |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n");
96 let cx = flin_coef f x in
97 Hashtbl.remove f.fhom x;
98 Hashtbl.add f.fhom x (rplus cx c);
107 let flin_add_cste f c =
109 fcste=rplus f.fcste c}
113 @return a empty flin with r1 in fcste
115 let flin_one () = flin_add_cste (flin_zero()) r1;;
120 let flin_plus f1 f2 =
121 let f3 = flin_zero() in
122 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
123 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
124 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
130 let flin_minus f1 f2 =
131 let f3 = flin_zero() in
132 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
133 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
134 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
141 let f2 = flin_zero() in
142 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
143 flin_add_cste f2 (rmult a f.fcste);
147 (*****************************************************************************)
152 @raise Failure if conversion is impossible
153 @return rational proiection of t
155 let rec rational_of_term t =
156 (* fun to apply f to the first and second rational-term of l *)
157 let rat_of_binop f l =
158 let a = List.hd l and
159 b = List.hd(List.tl l) in
160 f (rational_of_term a) (rational_of_term b)
162 (* as before, but f is unary *)
163 let rat_of_unop f l =
164 f (rational_of_term (List.hd l))
167 | Cic.Cast (t1,t2) -> (rational_of_term t1)
168 | Cic.Appl (t1::next) ->
171 if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then
173 else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then
174 rat_of_unop rinv next
175 else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then
176 rat_of_binop rmult next
177 else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then
178 rat_of_binop rdiv next
179 else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then
180 rat_of_binop rplus next
181 else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then
182 rat_of_binop rminus next
183 else failwith "not a rational"
184 | _ -> failwith "not a rational")
185 | Cic.Const (u,boh) ->
186 if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then r1
187 else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then r0
188 else failwith "not a rational"
189 | _ -> failwith "not a rational"
193 let rational_of_const = rational_of_term;;
203 let rec flin_of_term t =
204 let fl_of_binop f l =
205 let a = List.hd l and
206 b = List.hd(List.tl l) in
207 f (flin_of_term a) (flin_of_term b)
211 | Cic.Cast (t1,t2) -> (flin_of_term t1)
212 | Cic.Appl (t1::next) ->
217 if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then
218 flin_emult (rop r1) (flin_of_term (List.hd next))
219 else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then
220 fl_of_binop flin_plus next
221 else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then
222 fl_of_binop flin_minus next
223 else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then
225 let arg1 = (List.hd next) and
226 arg2 = (List.hd(List.tl next))
228 if fails rational_of_term arg1
230 if fails rational_of_term arg2
232 ( (* prodotto tra 2 incognite ????? impossibile*)
233 failwith "Sistemi lineari!!!!\n"
238 Cic.Rel(n) -> (*trasformo al volo*)
239 (flin_add (flin_zero()) arg1 (rational_of_term arg2))
241 let tmp = flin_of_term arg1 in
242 flin_emult (rational_of_term arg2) (tmp)
245 if fails rational_of_term arg2
249 Cic.Rel(n) -> (*trasformo al volo*)
250 (flin_add (flin_zero()) arg2 (rational_of_term arg1))
252 let tmp = flin_of_term arg2 in
253 flin_emult (rational_of_term arg1) (tmp)
257 ( (*prodotto tra razionali*)
258 (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
262 (*let a = rational_of_term arg1 in
263 debug("ho fatto rational of term di "^CicPp.ppterm arg1^
264 " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
265 let a = flin_of_term arg1
268 let b = (rational_of_term arg2) in
269 debug("ho fatto rational of term di "^CicPp.ppterm arg2^
270 " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
271 (flin_add_cste (flin_zero()) (rmult a b))
274 _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
275 (flin_add (flin_zero()) arg2 a)
278 _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
279 (flin_add(flin_zero()) arg1 (rational_of_term arg2))
282 else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then
283 let a=(rational_of_term (List.hd next)) in
284 flin_add_cste (flin_zero()) (rinv a)
285 else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then
287 let b=(rational_of_term (List.hd(List.tl next))) in
290 let a = (rational_of_term (List.hd next)) in
291 (flin_add_cste (flin_zero()) (rdiv a b))
294 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
300 | Cic.Const (u,boh) ->
302 if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then flin_one ()
303 else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then flin_zero ()
307 with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
311 let flin_of_constr = flin_of_term;;
315 Translates a flin to (c,x) list
317 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
319 let flin_to_alist f =
321 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
325 (* Représentation des hypothèses qui sont des inéquations ou des équations.
329 The structure for ineq
331 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
332 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
339 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
342 let ineq1_of_term (h,t) =
343 match t with (* match t *)
344 Cic.Appl (t1::next) ->
345 let arg1= List.hd next in
346 let arg2= List.hd(List.tl next) in
347 (match t1 with (* match t1 *)
349 if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
354 hflin= flin_minus (flin_of_term arg1)
357 else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
362 hflin= flin_minus (flin_of_term arg2)
365 else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
370 hflin= flin_minus (flin_of_term arg1)
373 else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
378 hflin= flin_minus (flin_of_term arg2)
382 | Cic.MutInd (u,i,o) ->
383 if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then
386 let arg2= List.hd(List.tl (List.tl next)) in
389 if UriManager.eq u HelmLibraryObjects.Reals.r_URI then
394 hflin= flin_minus (flin_of_term arg1)
401 hflin= flin_minus (flin_of_term arg2)
407 |_-> assert false)(* match t1 *)
408 |_-> assert false (* match t *)
411 let ineq1_of_constr = ineq1_of_term;;
414 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
420 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
423 let rec print_sys l =
426 | (a,b)::next -> (print_rl a;
427 print_string (if b=true then "strict\n"else"\n");
432 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
435 let fourier_lineq lineq1 =
437 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
439 Hashtbl.iter (fun x c ->
440 try (Hashtbl.find hvar x;())
441 with _-> nvar:=(!nvar)+1;
442 Hashtbl.add hvar x (!nvar);
443 debug("aggiungo una var "^
444 string_of_int !nvar^" per "^
445 CicPp.ppterm x^"\n"))
449 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
450 let sys= List.map (fun h->
451 let v=Array.create ((!nvar)+1) r0 in
452 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c)
454 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
456 debug ("chiamo unsolvable sul sistema di "^
457 string_of_int (List.length sys) ^"\n");
462 (*****************************************************************************
463 Construction de la preuve en cas de succès de la méthode de Fourier,
464 i.e. on obtient une contradiction.
468 let _eqT = Cic.MutInd(HelmLibraryObjects.Logic.eq_URI, 0, []) ;;
469 let _False = Cic.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []) ;;
470 let _not = Cic.Const (HelmLibraryObjects.Logic.not_URI,[]);;
471 let _R0 = Cic.Const (HelmLibraryObjects.Reals.r0_URI,[]);;
472 let _R1 = Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);;
473 let _R = Cic.Const (HelmLibraryObjects.Reals.r_URI,[]);;
474 let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string
475 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;;
476 let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string
477 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;;
478 let _Rfourier_ge_to_le =Cic.Const ((UriManager.uri_of_string
479 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;;
480 let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string
481 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;;
482 let _Rfourier_le=Cic.Const ((UriManager.uri_of_string
483 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;;
484 let _Rfourier_le_le =Cic.Const ((UriManager.uri_of_string
485 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con"), []) ;;
486 let _Rfourier_le_lt =Cic.Const ((UriManager.uri_of_string
487 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con"), []) ;;
488 let _Rfourier_lt=Cic.Const ((UriManager.uri_of_string
489 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con"), []) ;;
490 let _Rfourier_lt_le =Cic.Const ((UriManager.uri_of_string
491 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con"), []) ;;
492 let _Rfourier_lt_lt =Cic.Const ((UriManager.uri_of_string
493 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con"), []) ;;
494 let _Rfourier_not_ge_lt = Cic.Const ((UriManager.uri_of_string
495 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con"), []) ;;
496 let _Rfourier_not_gt_le = Cic.Const ((UriManager.uri_of_string
497 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con"), []) ;;
498 let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string
499 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;;
500 let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string
501 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;;
502 let _Rinv = Cic.Const (HelmLibraryObjects.Reals.rinv_URI, []);;
503 let _Rinv_R1 = Cic.Const(HelmLibraryObjects.Reals.rinv_r1_URI, []);;
504 let _Rle = Cic.Const (HelmLibraryObjects.Reals.rle_URI, []);;
505 let _Rle_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
506 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;;
507 let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string
508 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con"), []) ;;
509 let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string
510 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;;
511 let _Rle_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
512 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;;
513 let _Rlt = Cic.Const (HelmLibraryObjects.Reals.rlt_URI, []);;
514 let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
515 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;;
516 let _Rlt_not_le = Cic.Const ((UriManager.uri_of_string
517 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con"), []) ;;
518 let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string
519 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;;
520 let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
521 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;;
522 let _Rminus = Cic.Const (HelmLibraryObjects.Reals.rminus_URI, []);;
523 let _Rmult = Cic.Const (HelmLibraryObjects.Reals.rmult_URI, []);;
524 let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string
525 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;;
526 let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string
527 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;;
528 let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string
529 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;;
530 let _Ropp = Cic.Const (HelmLibraryObjects.Reals.ropp_URI, []);;
531 let _Rplus = Cic.Const (HelmLibraryObjects.Reals.rplus_URI, []);;
533 (******************************************************************************)
535 let is_int x = (x.den)=1
538 (* fraction = couple (num,den) *)
539 let rec rational_to_fraction x= (x.num,x.den)
542 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
545 let rec int_to_real_aux n =
547 0 -> _R0 (* o forse R0 + R0 ????? *)
549 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
554 let x = int_to_real_aux (abs n) in
556 Cic.Appl [ _Ropp ; x ]
562 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
565 let rational_to_real x =
566 let (n,d)=rational_to_fraction x in
567 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
570 (* preuve que 0<n*1/d
573 let tac_zero_inf_pos (n,d) =
574 let tac_zero_inf_pos (n,d) status =
575 (*let cste = pf_parse_constr gl in*)
576 let pall str (proof,goal) t =
577 debug ("tac "^str^" :\n" );
578 let curi,metasenv,pbo,pty = proof in
579 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
580 debug ("th = "^ CicPp.ppterm t ^"\n");
581 debug ("ty = "^ CicPp.ppterm ty^"\n");
583 let tacn=ref (mk_tactic (fun status ->
584 pall "n0" status _Rlt_zero_1 ;
585 apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in
586 let tacd=ref (mk_tactic (fun status ->
587 pall "d0" status _Rlt_zero_1 ;
588 apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in
592 tacn:=(Tacticals.then_
593 ~start:(mk_tactic (fun status ->
594 pall ("n"^string_of_int i) status _Rlt_zero_pos_plus1;
596 (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1)
598 ~continuation:!tacn);
601 tacd:=(Tacticals.then_
602 ~start:(mk_tactic (fun status ->
603 pall "d" status _Rlt_zero_pos_plus1 ;
605 (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) status))
606 ~continuation:!tacd);
609 debug("TAC ZERO INF POS\n");
612 ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
613 ~continuations:[!tacn ;!tacd ] )
616 mk_tactic (tac_zero_inf_pos (n,d))
621 (* preuve que 0<=n*1/d
624 let tac_zero_infeq_pos gl (n,d) =
625 let tac_zero_infeq_pos gl (n,d) status =
626 (*let cste = pf_parse_constr gl in*)
627 debug("inizio tac_zero_infeq_pos\n");
630 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
632 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
635 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
637 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
638 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
641 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
642 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
646 ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos)
647 ~continuations:[!tacn;!tacd]) status
649 mk_tactic (tac_zero_infeq_pos gl (n,d))
654 (* preuve que 0<(-n)*(1/d) => False
657 let tac_zero_inf_false gl (n,d) =
658 let tac_zero_inf_false gl (n,d) status =
660 apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status
662 apply_tactic (Tacticals.then_
663 ~start:( mk_tactic (fun status ->
664 let (proof, goal) = status in
665 let curi,metasenv,pbo,pty = proof in
666 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
667 apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status))
668 ~continuation:(tac_zero_infeq_pos gl (-n,d)))
671 mk_tactic (tac_zero_inf_false gl (n,d))
674 (* preuve que 0<=n*(1/d) => False ; n est negatif
677 let tac_zero_infeq_false gl (n,d) =
678 let tac_zero_infeq_false gl (n,d) status =
679 let (proof, goal) = status in
680 let curi,metasenv,pbo,pty = proof in
681 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
683 debug("faccio fold di " ^ CicPp.ppterm
687 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
690 debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
691 (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
695 (ReductionTactics.fold_tac
696 ~reduction:(const_lazy_reduction CicReduction.whd)
697 ~pattern:(ProofEngineTypes.conclusion_pattern None)
703 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])))
706 ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
707 ~continuation:(tac_zero_inf_pos (-n,d))))
710 mk_tactic (tac_zero_infeq_false gl (n,d))
714 (* *********** ********** ******** ??????????????? *********** **************)
716 let apply_type_tac ~cast:t ~applist:al =
717 let apply_type_tac ~cast:t ~applist:al (proof,goal) =
718 let curi,metasenv,pbo,pty = proof in
719 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
720 let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
722 CicMkImplicit.identity_relocation_list_for_metavariable context in
723 let metasenv' = (fresh_meta,context,t)::metasenv in
724 let proof' = curi,metasenv',pbo,pty in
727 (PrimitiveTactics.apply_tac
728 (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) *)
729 ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al))) (* ??? *)
732 proof'',fresh_meta::goals
734 mk_tactic (apply_type_tac ~cast:t ~applist:al)
738 let my_cut ~term:c (proof,goal) =
739 let curi,metasenv,pbo,pty = proof in
740 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
741 let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
743 CicMkImplicit.identity_relocation_list_for_metavariable context in
744 let metasenv' = (fresh_meta,context,c)::metasenv in
745 let proof' = curi,metasenv',pbo,pty in
749 ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty))
750 ~applist:[Cic.Meta(fresh_meta,irl)])
753 (* We permute the generated goals to be consistent with Coq *)
756 | he::tl -> proof'',he::fresh_meta::tl
758 mk_tactic (my_cut ~term:c)
761 let exact = PrimitiveTactics.exact_tac;;
764 let tac_use h status =
765 let (proof, goal) = status in
766 debug("Inizio TC_USE\n");
767 let curi,metasenv,pbo,pty = proof in
768 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
769 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
770 debug ("ty = "^ CicPp.ppterm ty^"\n");
773 "Rlt" -> exact ~term:h.hname
774 | "Rle" -> exact ~term:h.hname
775 | "Rgt" -> (Tacticals.then_
776 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
777 ~continuation:(exact ~term:h.hname))
778 | "Rge" -> (Tacticals.then_
779 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
780 ~continuation:(exact ~term:h.hname))
781 | "eqTLR" -> (Tacticals.then_
782 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
783 ~continuation:(exact ~term:h.hname))
784 | "eqTRL" -> (Tacticals.then_
785 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
786 ~continuation:(exact ~term:h.hname))
790 mk_tactic (tac_use h)
795 Cic.Appl ( Cic.Const(u,boh)::next) ->
796 (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI or
797 UriManager.eq u HelmLibraryObjects.Reals.rgt_URI or
798 UriManager.eq u HelmLibraryObjects.Reals.rle_URI or
799 UriManager.eq u HelmLibraryObjects.Reals.rge_URI then true
800 else if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then
801 (match (List.hd next) with
802 Cic.Const (uri,_) when
803 UriManager.eq uri HelmLibraryObjects.Reals.r_URI
810 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
813 Cic.Appl(Array.to_list a)
816 (* Résolution d'inéquations linéaires dans R *)
817 let rec strip_outer_cast c = match c with
818 | Cic.Cast (c,_) -> strip_outer_cast c
822 (*let find_in_context id context =
823 let rec find_in_context_aux c n =
825 [] -> failwith (id^" not found in context")
826 | a::next -> (match a with
827 Some (Cic.Name(name),_) when name = id -> n
828 (*? magari al posto di _ qualcosaltro?*)
829 | _ -> find_in_context_aux next (n+1))
831 find_in_context_aux context 1
834 (* mi sembra quadratico *)
835 let rec filter_real_hyp context cont =
838 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
839 let n = find_in_context h cont in
840 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
841 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
842 | a::next -> debug(" no\n"); filter_real_hyp next cont
845 let filter_real_hyp context _ =
846 let rec filter_aux context num =
849 | Some(Cic.Name(h),Cic.Decl(t))::next ->
850 [(Cic.Rel(num),t)] @ filter_aux next (num+1)
851 | a::next -> filter_aux next (num+1)
857 (* lifts everithing at the conclusion level *)
858 let rec superlift c n=
861 | Some(name,Cic.Decl(a))::next ->
862 [Some(name,Cic.Decl(CicSubstitution.lift n a))]@ superlift next (n+1)
863 | Some(name,Cic.Def(a,None))::next ->
864 [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1)
865 | Some(name,Cic.Def(a,Some ty))::next ->
867 Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))
868 ] @ superlift next (n+1)
869 | _::next -> superlift next (n+1) (*?? ??*)
873 let equality_replace a b =
874 let equality_replace a b status =
875 debug("inizio EQ\n");
876 let module C = Cic in
877 let proof,goal = status in
878 let curi,metasenv,pbo,pty = proof in
879 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
880 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
881 let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
883 CicMkImplicit.identity_relocation_list_for_metavariable context in
884 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
885 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
886 let (proof,goals) = apply_tactic
887 (EqualityTactics.rewrite_simpl_tac
888 ~direction:`LeftToRight
889 ~pattern:(ProofEngineTypes.conclusion_pattern None)
890 (C.Meta (fresh_meta,irl)))
891 ((curi,metasenv',pbo,pty),goal)
893 let new_goals = fresh_meta::goals in
894 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
895 ^string_of_int( List.length goals)^"+ meta\n");
898 mk_tactic (equality_replace a b)
901 let tcl_fail a (proof,goal) =
903 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
904 | _ -> (proof,[goal])
907 (* Galla: moved in variousTactics.ml
908 let assumption_tac (proof,goal)=
909 let curi,metasenv,pbo,pty = proof in
910 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
912 let tac_list = List.map
913 ( fun x -> num := !num + 1;
915 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
916 | _ -> ("fake",tcl_fail 1)
920 Tacticals.first ~tactics:tac_list (proof,goal)
923 (* Galla: moved in negationTactics.ml
924 (* !!!!! fix !!!!!!!!!! *)
925 let contradiction_tac (proof,goal)=
927 (*inutile sia questo che quello prima della chiamata*)
928 ~start:PrimitiveTactics.intros_tac
929 ~continuation:(Tacticals.then_
930 ~start:(VariousTactics.elim_type_tac ~term:_False)
931 ~continuation:(assumption_tac))
936 (* ********************* TATTICA ******************************** *)
938 let rec fourier (s_proof,s_goal)=
939 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
940 let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
941 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
942 debug_pcontext s_context;
944 let fhyp = String.copy "new_hyp_for_fourier" in
946 (* here we need to negate the thesis, but to do this we need to apply the
947 right theoreme,so let's parse our thesis *)
949 let th_to_appl = ref _Rfourier_not_le_gt in
951 Cic.Appl ( Cic.Const(u,boh)::args) ->
953 (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
955 else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
957 else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
959 else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
961 else failwith "fourier can't be applyed")
962 |_-> failwith "fourier can't be applyed");
963 (* fix maybe strip_outer_cast goes here?? *)
965 (* now let's change our thesis applying the th and put it with hp *)
967 let proof,gl = apply_tactic
969 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
970 ~continuation:(PrimitiveTactics.intros_tac ()))
973 let goal = if List.length gl = 1 then List.hd gl
974 else failwith "a new goal" in
976 debug ("port la tesi sopra e la nego. contesto :\n");
977 debug_pcontext s_context;
979 (* now we have all the right environment *)
981 let curi,metasenv,pbo,pty = proof in
982 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
984 (* now we want to convert hp to inequations, but first we must lift
985 everyting to thesis level, so that a variable has the save Rel(n)
986 in each hp ( needed by ineq1_of_term ) *)
988 (* ? fix if None ?????*)
989 (* fix change superlift with a real name *)
991 let l_context = superlift context 1 in
992 let hyps = filter_real_hyp l_context l_context in
994 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
998 (* transform hyps into inequations *)
1000 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1004 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1007 let res=fourier_lineq (!lineq) in
1008 let tac=ref Tacticals.id_tac in
1010 (print_string "Tactic Fourier fails.\n";flush stdout;
1011 failwith "fourier_tac fails")
1014 match res with (*match res*)
1017 (* in lc we have the coefficient to "reduce" the system *)
1019 print_string "Fourier's method can prove the goal...\n";flush stdout;
1021 debug "I coeff di moltiplicazione rit sono: ";
1025 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1026 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1028 (List.combine (!lineq) lc);
1030 print_string (" quindi lutil e' lunga "^
1031 string_of_int (List.length (!lutil))^"\n");
1033 (* on construit la combinaison linéaire des inéquation *)
1035 (match (!lutil) with (*match (!lutil) *)
1037 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1039 let s=ref (h1.hstrict) in
1042 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1043 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1045 List.iter (fun (h,c) ->
1046 s:=(!s)||(h.hstrict);
1047 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1048 [_Rmult;rational_to_real c;h.hleft ] ]);
1049 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1050 [_Rmult;rational_to_real c;h.hright] ]))
1053 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1054 let tc=rational_to_real cres in
1057 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1059 debug "inizio a costruire tac1\n";
1060 Fourier.print_rational(c1);
1062 let tac1=ref ( mk_tactic (fun status ->
1066 ~start:(mk_tactic (fun status ->
1067 debug ("inizio t1 strict\n");
1068 let curi,metasenv,pbo,pty = proof in
1069 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1070 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1071 debug ("ty = "^ CicPp.ppterm ty^"\n");
1073 (PrimitiveTactics.apply_tac ~term:_Rfourier_lt) status))
1074 ~continuations:[tac_use h1;
1075 tac_zero_inf_pos (rational_to_fraction c1)])
1078 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1079 ~continuations:[tac_use h1;tac_zero_inf_pos
1080 (rational_to_fraction c1)]))
1085 List.iter (fun (h,c) ->
1089 tac1:=(Tacticals.thens
1090 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt_lt)
1091 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1092 (rational_to_fraction c)]))
1095 Fourier.print_rational(c1);
1096 tac1:=(Tacticals.thens
1097 ~start:(mk_tactic (fun status ->
1098 debug("INIZIO TAC 1 2\n");
1099 let curi,metasenv,pbo,pty = proof in
1100 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1101 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1102 debug ("ty = "^ CicPp.ppterm ty^"\n");
1104 (PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le)
1106 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1107 (rational_to_fraction c)])))
1111 tac1:=(Tacticals.thens
1112 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1113 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1114 (rational_to_fraction c)]))
1117 tac1:=(Tacticals.thens
1118 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1119 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1120 (rational_to_fraction c)]))));
1121 s:=(!s)||(h.hstrict)) (* end fun -> *)
1122 lutil;(*end List.iter*)
1126 tac_zero_inf_false goal (rational_to_fraction cres)
1128 tac_zero_infeq_false goal (rational_to_fraction cres)
1130 tac:=(Tacticals.thens
1131 ~start:(my_cut ~term:ineq)
1132 ~continuations:[Tacticals.then_
1133 ~start:( mk_tactic (fun status ->
1134 let (proof, goal) = status in
1135 let curi,metasenv,pbo,pty = proof in
1136 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1138 (ReductionTactics.change_tac
1139 ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
1140 (const_lazy_term (Cic.Appl [ _not; ineq])))
1142 ~continuation:(Tacticals.then_
1143 ~start:(PrimitiveTactics.apply_tac ~term:
1144 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1145 ~continuation:(Tacticals.thens
1146 ~start:(mk_tactic (fun status ->
1147 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^
1148 CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1149 let r = apply_tactic
1150 (equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
1153 (match r with (p,gl) ->
1154 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1156 ~continuations:[(Tacticals.thens
1157 ~start:(mk_tactic (fun status ->
1158 let r = apply_tactic
1159 (equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
1162 (match r with (p,gl) ->
1163 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1166 [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
1168 ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac]
1170 ;(*Tacticals.id_tac*)
1172 ~start:(mk_tactic (fun status ->
1173 let (proof, goal) = status in
1174 let curi,metasenv,pbo,pty = proof in
1175 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1176 (* check if ty is of type *)
1178 debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1180 Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1183 let r = apply_tactic
1184 (ReductionTactics.change_tac
1185 ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
1186 (const_lazy_term w1)) status
1188 debug("fine MY_CHNGE\n");
1190 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1191 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1193 |_-> assert false)(*match (!lutil) *)
1194 |_-> assert false); (*match res*)
1195 debug ("finalmente applico tac\n");
1197 let r = apply_tactic !tac (proof,goal) in
1198 debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1203 let fourier_tac = mk_tactic fourier