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 (match (UriManager.string_of_uri u) with
171 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
173 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
174 rat_of_unop rinv next
175 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
176 rat_of_binop rmult next
177 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
178 rat_of_binop rdiv next
179 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
180 rat_of_binop rplus next
181 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
182 rat_of_binop rminus next
183 | _ -> failwith "not a rational")
184 | _ -> failwith "not a rational")
185 | Cic.Const (u,boh) ->
186 (match (UriManager.string_of_uri u) with
187 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
188 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
189 | _ -> failwith "not a rational")
190 | _ -> failwith "not a rational"
194 let rational_of_const = rational_of_term;;
204 let rec flin_of_term t =
205 let fl_of_binop f l =
206 let a = List.hd l and
207 b = List.hd(List.tl l) in
208 f (flin_of_term a) (flin_of_term b)
212 | Cic.Cast (t1,t2) -> (flin_of_term t1)
213 | Cic.Appl (t1::next) ->
218 match (UriManager.string_of_uri u) with
219 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
220 flin_emult (rop r1) (flin_of_term (List.hd next))
221 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
222 fl_of_binop flin_plus next
223 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
224 fl_of_binop flin_minus next
225 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
227 let arg1 = (List.hd next) and
228 arg2 = (List.hd(List.tl next))
230 if fails rational_of_term arg1
232 if fails rational_of_term arg2
234 ( (* prodotto tra 2 incognite ????? impossibile*)
235 failwith "Sistemi lineari!!!!\n"
240 Cic.Rel(n) -> (*trasformo al volo*)
241 (flin_add (flin_zero()) arg1 (rational_of_term arg2))
243 let tmp = flin_of_term arg1 in
244 flin_emult (rational_of_term arg2) (tmp)
247 if fails rational_of_term arg2
251 Cic.Rel(n) -> (*trasformo al volo*)
252 (flin_add (flin_zero()) arg2 (rational_of_term arg1))
254 let tmp = flin_of_term arg2 in
255 flin_emult (rational_of_term arg1) (tmp)
259 ( (*prodotto tra razionali*)
260 (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
264 (*let a = rational_of_term arg1 in
265 debug("ho fatto rational of term di "^CicPp.ppterm arg1^
266 " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
267 let a = flin_of_term arg1
270 let b = (rational_of_term arg2) in
271 debug("ho fatto rational of term di "^CicPp.ppterm arg2^
272 " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
273 (flin_add_cste (flin_zero()) (rmult a b))
276 _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
277 (flin_add (flin_zero()) arg2 a)
280 _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
281 (flin_add(flin_zero()) arg1 (rational_of_term arg2))
284 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
285 let a=(rational_of_term (List.hd next)) in
286 flin_add_cste (flin_zero()) (rinv a)
287 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
289 let b=(rational_of_term (List.hd(List.tl next))) in
292 let a = (rational_of_term (List.hd next)) in
293 (flin_add_cste (flin_zero()) (rdiv a b))
296 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
302 | Cic.Const (u,boh) ->
304 match (UriManager.string_of_uri u) with
305 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
306 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
310 with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
314 let flin_of_constr = flin_of_term;;
318 Translates a flin to (c,x) list
320 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
322 let flin_to_alist f =
324 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
328 (* Représentation des hypothèses qui sont des inéquations ou des équations.
332 The structure for ineq
334 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
335 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
342 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
345 let ineq1_of_term (h,t) =
346 match t with (* match t *)
347 Cic.Appl (t1::next) ->
348 let arg1= List.hd next in
349 let arg2= List.hd(List.tl next) in
350 (match t1 with (* match t1 *)
352 (match UriManager.string_of_uri u with (* match u *)
353 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
358 hflin= flin_minus (flin_of_term arg1)
361 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
366 hflin= flin_minus (flin_of_term arg2)
369 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
374 hflin= flin_minus (flin_of_term arg1)
377 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
382 hflin= flin_minus (flin_of_term arg2)
385 |_->assert false)(* match u *)
386 | Cic.MutInd (u,i,o) ->
387 (match UriManager.string_of_uri u with
388 "cic:/Coq/Init/Logic_Type/eqT.ind" ->
391 let arg2= List.hd(List.tl (List.tl next)) in
394 (match UriManager.string_of_uri u with
395 "cic:/Coq/Reals/Rdefinitions/R.con"->
400 hflin= flin_minus (flin_of_term arg1)
407 hflin= flin_minus (flin_of_term arg2)
413 |_-> assert false)(* match t1 *)
414 |_-> assert false (* match t *)
417 let ineq1_of_constr = ineq1_of_term;;
420 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
426 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
429 let rec print_sys l =
432 | (a,b)::next -> (print_rl a;
433 print_string (if b=true then "strict\n"else"\n");
438 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
441 let fourier_lineq lineq1 =
443 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
445 Hashtbl.iter (fun x c ->
446 try (Hashtbl.find hvar x;())
447 with _-> nvar:=(!nvar)+1;
448 Hashtbl.add hvar x (!nvar);
449 debug("aggiungo una var "^
450 string_of_int !nvar^" per "^
451 CicPp.ppterm x^"\n"))
455 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
456 let sys= List.map (fun h->
457 let v=Array.create ((!nvar)+1) r0 in
458 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c)
460 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
462 debug ("chiamo unsolvable sul sistema di "^
463 string_of_int (List.length sys) ^"\n");
468 (*****************************************************************************
469 Construction de la preuve en cas de succès de la méthode de Fourier,
470 i.e. on obtient une contradiction.
474 let _eqT = Cic.MutInd((UriManager.uri_of_string
475 "cic:/Coq/Init/Logic_Type/eqT.ind"), 0, []) ;;
476 let _False = Cic.MutInd ((UriManager.uri_of_string
477 "cic:/Coq/Init/Logic/False.ind"), 0, []) ;;
478 let _not = Cic.Const ((UriManager.uri_of_string
479 "cic:/Coq/Init/Logic/not.con"), []);;
480 let _R0 = Cic.Const ((UriManager.uri_of_string
481 "cic:/Coq/Reals/Rdefinitions/R0.con"), []) ;;
482 let _R1 = Cic.Const ((UriManager.uri_of_string
483 "cic:/Coq/Reals/Rdefinitions/R1.con"), []) ;;
484 let _R = Cic.Const ((UriManager.uri_of_string
485 "cic:/Coq/Reals/Rdefinitions/R.con"), []) ;;
486 let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string
487 "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;;
488 let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string
489 "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;;
490 let _Rfourier_ge_to_le =Cic.Const ((UriManager.uri_of_string
491 "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;;
492 let _Rfourier_gt_to_lt =Cic.Const ((UriManager.uri_of_string
493 "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;;
494 let _Rfourier_le=Cic.Const ((UriManager.uri_of_string
495 "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;;
496 let _Rfourier_le_le =Cic.Const ((UriManager.uri_of_string
497 "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con"), []) ;;
498 let _Rfourier_le_lt =Cic.Const ((UriManager.uri_of_string
499 "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con"), []) ;;
500 let _Rfourier_lt=Cic.Const ((UriManager.uri_of_string
501 "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con"), []) ;;
502 let _Rfourier_lt_le =Cic.Const ((UriManager.uri_of_string
503 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con"), []) ;;
504 let _Rfourier_lt_lt =Cic.Const ((UriManager.uri_of_string
505 "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con"), []) ;;
506 let _Rfourier_not_ge_lt = Cic.Const ((UriManager.uri_of_string
507 "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con"), []) ;;
508 let _Rfourier_not_gt_le = Cic.Const ((UriManager.uri_of_string
509 "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con"), []) ;;
510 let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string
511 "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;;
512 let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string
513 "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;;
514 let _Rinv = Cic.Const ((UriManager.uri_of_string
515 "cic:/Coq/Reals/Rdefinitions/Rinv.con"), []) ;;
516 let _Rinv_R1 = Cic.Const((UriManager.uri_of_string
517 "cic:/Coq/Reals/Rbase/Rinv_R1.con" ), []) ;;
518 let _Rle = Cic.Const ((UriManager.uri_of_string
519 "cic:/Coq/Reals/Rdefinitions/Rle.con"), []) ;;
520 let _Rle_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
521 "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;;
522 let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string
523 "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con"), []) ;;
524 let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string
525 "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;;
526 let _Rle_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
527 "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;;
528 (*let _Rle_zero_zero = Cic.Const ((UriManager.uri_of_string
529 "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con"), []) ;;*)
530 let _Rlt = Cic.Const ((UriManager.uri_of_string
531 "cic:/Coq/Reals/Rdefinitions/Rlt.con"), []) ;;
532 let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
533 "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;;
534 let _Rlt_not_le = Cic.Const ((UriManager.uri_of_string
535 "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con"), []) ;;
536 let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string
537 "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;;
538 let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
539 "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;;
540 let _Rminus = Cic.Const ((UriManager.uri_of_string
541 "cic:/Coq/Reals/Rdefinitions/Rminus.con"), []) ;;
542 let _Rmult = Cic.Const ((UriManager.uri_of_string
543 "cic:/Coq/Reals/Rdefinitions/Rmult.con"), []) ;;
544 let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string
545 "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;;
546 let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string
547 "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;;
548 let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string
549 "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;;
550 let _Ropp = Cic.Const ((UriManager.uri_of_string
551 "cic:/Coq/Reals/Rdefinitions/Ropp.con"), []) ;;
552 let _Rplus = Cic.Const ((UriManager.uri_of_string
553 "cic:/Coq/Reals/Rdefinitions/Rplus.con"), []) ;;
555 (******************************************************************************)
557 let is_int x = (x.den)=1
560 (* fraction = couple (num,den) *)
561 let rec rational_to_fraction x= (x.num,x.den)
564 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
567 let rec int_to_real_aux n =
569 0 -> _R0 (* o forse R0 + R0 ????? *)
571 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
576 let x = int_to_real_aux (abs n) in
578 Cic.Appl [ _Ropp ; x ]
584 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
587 let rational_to_real x =
588 let (n,d)=rational_to_fraction x in
589 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
592 (* preuve que 0<n*1/d
595 let tac_zero_inf_pos (n,d) ~status =
596 (*let cste = pf_parse_constr gl in*)
597 let pall str ~status:(proof,goal) t =
598 debug ("tac "^str^" :\n" );
599 let curi,metasenv,pbo,pty = proof in
600 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
601 debug ("th = "^ CicPp.ppterm t ^"\n");
602 debug ("ty = "^ CicPp.ppterm ty^"\n");
605 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
606 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
608 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
609 PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
613 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
614 ~status _Rlt_zero_pos_plus1;
615 PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
616 ~continuation:!tacn);
619 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
620 ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
621 ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
626 debug("TAC ZERO INF POS\n");
628 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
637 (* preuve que 0<=n*1/d
640 let tac_zero_infeq_pos gl (n,d) ~status =
641 (*let cste = pf_parse_constr gl in*)
642 debug("inizio tac_zero_infeq_pos\n");
645 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
647 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
650 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
652 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
653 ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
656 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
657 ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
660 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
661 ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
662 debug("fine tac_zero_infeq_pos\n");
668 (* preuve que 0<(-n)*(1/d) => False
671 let tac_zero_inf_false gl (n,d) ~status=
672 debug("inizio tac_zero_inf_false\n");
674 (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
678 (debug "2\n";let r = (Tacticals.then_ ~start:(
679 fun ~status:(proof,goal as status) ->
680 let curi,metasenv,pbo,pty = proof in
681 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
682 debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
683 ^ CicPp.ppterm ty ^"\n");
684 let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
685 debug("!!!!!!!!!2\n");
688 ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
694 (* preuve que 0<=n*(1/d) => False ; n est negatif
697 let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
698 debug("stat tac_zero_infeq_false\n");
700 let curi,metasenv,pbo,pty = proof in
701 let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
703 debug("faccio fold di " ^ CicPp.ppterm
707 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
710 debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
711 (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
714 (ReductionTactics.fold_tac ~reduction:CicReduction.whd
715 ~also_in_hypotheses:false
720 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
725 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
726 ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
727 debug("end tac_zero_infeq_false\n");
730 Tacticals.id_tac ~status
735 (* *********** ********** ******** ??????????????? *********** **************)
737 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
738 let curi,metasenv,pbo,pty = proof in
739 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
740 let fresh_meta = ProofEngineHelpers.new_meta proof in
742 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
743 let metasenv' = (fresh_meta,context,t)::metasenv in
744 let proof' = curi,metasenv',pbo,pty in
746 PrimitiveTactics.apply_tac
747 (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
748 ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
749 ~status:(proof',goal)
751 proof'',fresh_meta::goals
758 let my_cut ~term:c ~status:(proof,goal)=
759 let curi,metasenv,pbo,pty = proof in
760 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
762 debug("my_cut di "^CicPp.ppterm c^"\n");
765 let fresh_meta = ProofEngineHelpers.new_meta proof in
767 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
768 let metasenv' = (fresh_meta,context,c)::metasenv in
769 let proof' = curi,metasenv',pbo,pty in
771 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
772 CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
773 ~status:(proof',goal)
775 (* We permute the generated goals to be consistent with Coq *)
778 | he::tl -> proof'',he::fresh_meta::tl
782 let exact = PrimitiveTactics.exact_tac;;
784 let tac_use h ~status:(proof,goal as status) =
785 debug("Inizio TC_USE\n");
786 let curi,metasenv,pbo,pty = proof in
787 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
788 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
789 debug ("ty = "^ CicPp.ppterm ty^"\n");
793 "Rlt" -> exact ~term:h.hname ~status
794 |"Rle" -> exact ~term:h.hname ~status
795 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
796 ~term:_Rfourier_gt_to_lt)
797 ~continuation:(exact ~term:h.hname)) ~status
798 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
799 ~term:_Rfourier_ge_to_le)
800 ~continuation:(exact ~term:h.hname)) ~status
801 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
802 ~term:_Rfourier_eqLR_to_le)
803 ~continuation:(exact ~term:h.hname)) ~status
804 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
805 ~term:_Rfourier_eqRL_to_le)
806 ~continuation:(exact ~term:h.hname)) ~status
809 debug("Fine TAC_USE\n");
817 Cic.Appl ( Cic.Const(u,boh)::next) ->
818 (match (UriManager.string_of_uri u) with
819 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
820 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
821 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
822 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
823 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
824 (match (List.hd next) with
825 Cic.Const (uri,_) when
826 UriManager.string_of_uri uri =
827 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
833 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
836 Cic.Appl(Array.to_list a)
839 (* Résolution d'inéquations linéaires dans R *)
840 let rec strip_outer_cast c = match c with
841 | Cic.Cast (c,_) -> strip_outer_cast c
845 (*let find_in_context id context =
846 let rec find_in_context_aux c n =
848 [] -> failwith (id^" not found in context")
849 | a::next -> (match a with
850 Some (Cic.Name(name),_) when name = id -> n
851 (*? magari al posto di _ qualcosaltro?*)
852 | _ -> find_in_context_aux next (n+1))
854 find_in_context_aux context 1
857 (* mi sembra quadratico *)
858 let rec filter_real_hyp context cont =
861 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
862 let n = find_in_context h cont in
863 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
864 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
865 | a::next -> debug(" no\n"); filter_real_hyp next cont
867 let filter_real_hyp context _ =
868 let rec filter_aux context num =
871 | Some(Cic.Name(h),Cic.Decl(t))::next ->
873 (*let n = find_in_context h cont in*)
874 debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
875 [(Cic.Rel(num),t)] @ filter_aux next (num+1)
877 | a::next -> filter_aux next (num+1)
883 (* lifts everithing at the conclusion level *)
884 let rec superlift c n=
887 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
888 CicSubstitution.lift n a))] @ superlift next (n+1)
889 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
890 CicSubstitution.lift n a))] @ superlift next (n+1)
891 | _::next -> superlift next (n+1) (*?? ??*)
895 let equality_replace a b ~status =
896 debug("inizio EQ\n");
897 let module C = Cic in
898 let proof,goal = status in
899 let curi,metasenv,pbo,pty = proof in
900 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
901 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
902 let fresh_meta = ProofEngineHelpers.new_meta proof in
904 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
905 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
906 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
908 EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
909 ~status:((curi,metasenv',pbo,pty),goal)
911 let new_goals = fresh_meta::goals in
912 debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
913 ^string_of_int( List.length goals)^"+ meta\n");
917 let tcl_fail a ~status:(proof,goal) =
919 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
923 (* Galla: moved in variousTactics.ml
924 let assumption_tac ~status:(proof,goal)=
925 let curi,metasenv,pbo,pty = proof in
926 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
928 let tac_list = List.map
929 ( fun x -> num := !num + 1;
931 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
932 | _ -> ("fake",tcl_fail 1)
936 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
939 (* Galla: moved in negationTactics.ml
940 (* !!!!! fix !!!!!!!!!! *)
941 let contradiction_tac ~status:(proof,goal)=
943 (*inutile sia questo che quello prima della chiamata*)
944 ~start:PrimitiveTactics.intros_tac
945 ~continuation:(Tacticals.then_
946 ~start:(VariousTactics.elim_type_tac ~term:_False)
947 ~continuation:(assumption_tac))
952 (* ********************* TATTICA ******************************** *)
954 let rec fourier ~status:(s_proof,s_goal)=
955 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
956 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
959 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
960 debug_pcontext s_context;
962 let fhyp = String.copy "new_hyp_for_fourier" in
964 (* here we need to negate the thesis, but to do this we need to apply the right
965 theoreme,so let's parse our thesis *)
967 let th_to_appl = ref _Rfourier_not_le_gt in
969 Cic.Appl ( Cic.Const(u,boh)::args) ->
970 (match UriManager.string_of_uri u with
971 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
973 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
975 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
977 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
979 |_-> failwith "fourier can't be applyed")
980 |_-> failwith "fourier can't be applyed");
981 (* fix maybe strip_outer_cast goes here?? *)
983 (* now let's change our thesis applying the th and put it with hp *)
987 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
988 ~continuation:(PrimitiveTactics.intros_tac ())
989 ~status:(s_proof,s_goal) in
990 let goal = if List.length gl = 1 then List.hd gl
991 else failwith "a new goal" in
993 debug ("port la tesi sopra e la nego. contesto :\n");
994 debug_pcontext s_context;
996 (* now we have all the right environment *)
998 let curi,metasenv,pbo,pty = proof in
999 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1002 (* now we want to convert hp to inequations, but first we must lift
1003 everyting to thesis level, so that a variable has the save Rel(n)
1004 in each hp ( needed by ineq1_of_term ) *)
1006 (* ? fix if None ?????*)
1007 (* fix change superlift with a real name *)
1009 let l_context = superlift context 1 in
1010 let hyps = filter_real_hyp l_context l_context in
1012 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
1014 let lineq =ref [] in
1016 (* transform hyps into inequations *)
1018 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1023 debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1026 let res=fourier_lineq (!lineq) in
1027 let tac=ref Tacticals.id_tac in
1029 (print_string "Tactic Fourier fails.\n";flush stdout;
1030 failwith "fourier_tac fails")
1033 match res with (*match res*)
1036 (* in lc we have the coefficient to "reduce" the system *)
1038 print_string "Fourier's method can prove the goal...\n";flush stdout;
1040 debug "I coeff di moltiplicazione rit sono: ";
1044 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1045 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1047 (List.combine (!lineq) lc);
1049 print_string (" quindi lutil e' lunga "^
1050 string_of_int (List.length (!lutil))^"\n");
1052 (* on construit la combinaison linéaire des inéquation *)
1054 (match (!lutil) with (*match (!lutil) *)
1056 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1058 let s=ref (h1.hstrict) in
1061 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1062 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1064 List.iter (fun (h,c) ->
1065 s:=(!s)||(h.hstrict);
1066 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1067 [_Rmult;rational_to_real c;h.hleft ] ]);
1068 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1069 [_Rmult;rational_to_real c;h.hright] ]))
1072 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1073 let tc=rational_to_real cres in
1076 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1078 debug "inizio a costruire tac1\n";
1079 Fourier.print_rational(c1);
1081 let tac1=ref ( fun ~status ->
1086 debug ("inizio t1 strict\n");
1087 let curi,metasenv,pbo,pty = proof in
1088 let metano,context,ty = List.find
1089 (function (m,_,_) -> m=goal) metasenv in
1090 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1091 debug ("ty = "^ CicPp.ppterm ty^"\n");
1092 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1093 ~continuations:[tac_use h1;tac_zero_inf_pos
1094 (rational_to_fraction c1)]
1099 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1100 ~continuations:[tac_use h1;tac_zero_inf_pos
1101 (rational_to_fraction c1)] ~status
1107 List.iter (fun (h,c) ->
1111 tac1:=(Tacticals.thens
1112 ~start:(PrimitiveTactics.apply_tac
1113 ~term:_Rfourier_lt_lt)
1114 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1115 (rational_to_fraction c)])
1119 Fourier.print_rational(c1);
1120 tac1:=(Tacticals.thens
1123 debug("INIZIO TAC 1 2\n");
1124 let curi,metasenv,pbo,pty = proof in
1125 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1127 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1128 debug ("ty = "^ CicPp.ppterm ty^"\n");
1129 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1130 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1131 (rational_to_fraction c)])
1137 tac1:=(Tacticals.thens
1138 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1139 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1140 (rational_to_fraction c)])
1144 tac1:=(Tacticals.thens
1145 ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1146 ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1147 (rational_to_fraction c)])
1151 s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1155 tac_zero_inf_false goal (rational_to_fraction cres)
1157 tac_zero_infeq_false goal (rational_to_fraction cres)
1159 tac:=(Tacticals.thens
1160 ~start:(my_cut ~term:ineq)
1161 ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
1162 ~start:(fun ~status:(proof,goal as status) ->
1163 let curi,metasenv,pbo,pty = proof in
1164 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1166 PrimitiveTactics.change_tac ~what:ty
1167 ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1168 ~continuation:(Tacticals.then_
1169 ~start:(PrimitiveTactics.apply_tac ~term:
1170 (if sres then _Rnot_lt_lt else _Rnot_le_le))
1171 ~continuation:(Tacticals.thens
1174 debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1175 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1178 (match r with (p,gl) ->
1179 debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1181 ~continuations:[(Tacticals.thens
1184 let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1185 (match r with (p,gl) ->
1186 debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1189 [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1190 ;Tacticals.try_tactics
1191 ~tactics:[ "ring", (fun ~status ->
1192 debug("begin RING\n");
1193 let r = Ring.ring_tac ~status in
1194 debug ("end RING\n");
1196 ; "id", Tacticals.id_tac]
1198 ;(*Tacticals.id_tac*)
1202 fun ~status:(proof,goal as status) ->
1203 let curi,metasenv,pbo,pty = proof in
1204 let metano,context,ty = List.find (function (m,_,_) -> m=
1206 (* check if ty is of type *)
1208 debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1210 Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1213 let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1214 debug("fine MY_CHNGE\n");
1218 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1219 ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1221 |_-> assert false)(*match (!lutil) *)
1222 |_-> assert false); (*match res*)
1223 debug ("finalmente applico tac\n");
1225 let r = !tac ~status:(proof,goal) in
1226 debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1231 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;