1 (* Copyright (C) 2002, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
27 (******************** OTHER USEFUL TACTICS **********************)
29 let rewrite_tac ~term:equality ~status:(proof,goal) =
31 let module U = UriManager in
32 let curi,metasenv,pbo,pty = proof in
33 let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
34 let eq_ind_r,ty,t1,t2 =
35 match CicTypeChecker.type_of_aux' metasenv context equality with
36 C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
37 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") ->
40 (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
43 | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
44 when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
47 (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0)
52 (ProofEngineTypes.Fail
53 "Rewrite: the argument is not a proof of an equality")
56 let gty' = CicSubstitution.lift 1 gty in
57 let t1' = CicSubstitution.lift 1 t1 in
59 ProofEngineReduction.replace_lifting
61 (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
62 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
64 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
66 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
67 let fresh_meta = ProofEngineHelpers.new_meta proof in
69 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
70 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
73 PrimitiveTactics.exact_tac
75 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
76 ~status:((curi,metasenv',pbo,pty),goal)
78 assert (List.length goals = 0) ;
82 (******************** THE FOURIER TACTIC ***********************)
84 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
85 des inéquations et équations sont entiers. En attendant la tactique Field.
91 let debug x = print_string ("____ "^x) ; flush stdout;;
93 let debug_pcontext x =
95 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^ a ^ " " | _ ->()) x ;
96 debug ("contesto : "^ (!str) ^ "\n")
99 (******************************************************************************
100 Operations on linear combinations.
102 Opérations sur les combinaisons linéaires affines.
103 La partie homogène d'une combinaison linéaire est en fait une table de hash
104 qui donne le coefficient d'un terme du calcul des constructions,
105 qui est zéro si le terme n'y est pas.
111 The type for linear combinations
113 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
117 @return an empty flin
119 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
125 @return the rational associated with x (coefficient)
129 (Hashtbl.find f.fhom x)
135 Adds c to the coefficient of x
142 let cx = flin_coef f x in
143 Hashtbl.remove f.fhom x;
144 Hashtbl.add f.fhom x (rplus cx c);
153 let flin_add_cste f c =
155 fcste=rplus f.fcste c}
159 @return a empty flin with r1 in fcste
161 let flin_one () = flin_add_cste (flin_zero()) r1;;
166 let flin_plus f1 f2 =
167 let f3 = flin_zero() in
168 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
169 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
170 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
176 let flin_minus f1 f2 =
177 let f3 = flin_zero() in
178 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
179 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
180 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
187 let f2 = flin_zero() in
188 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
189 flin_add_cste f2 (rmult a f.fcste);
193 (*****************************************************************************)
198 @return proiection on string of t
200 let rec string_of_term t =
202 Cic.Cast (t1,t2) -> string_of_term t1
203 |Cic.Const (u,boh) -> UriManager.string_of_uri u
204 |Cic.Var (u) -> UriManager.string_of_uri u
205 | _ -> "not_of_constant"
209 let string_of_constr = string_of_term
215 @raise Failure if conversion is impossible
216 @return rational proiection of t
218 let rec rational_of_term t =
219 (* fun to apply f to the first and second rational-term of l *)
220 let rat_of_binop f l =
221 let a = List.hd l and
222 b = List.hd(List.tl l) in
223 f (rational_of_term a) (rational_of_term b)
225 (* as before, but f is unary *)
226 let rat_of_unop f l =
227 f (rational_of_term (List.hd l))
230 | Cic.Cast (t1,t2) -> (rational_of_term t1)
231 | Cic.Appl (t1::next) ->
234 (match (UriManager.string_of_uri u) with
235 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
237 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
238 rat_of_unop rinv next
239 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
240 rat_of_binop rmult next
241 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
242 rat_of_binop rdiv next
243 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
244 rat_of_binop rplus next
245 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
246 rat_of_binop rminus next
247 | _ -> failwith "not a rational")
248 | _ -> failwith "not a rational")
249 | Cic.Const (u,boh) ->
250 (match (UriManager.string_of_uri u) with
251 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
252 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
253 | _ -> failwith "not a rational")
254 | _ -> failwith "not a rational"
258 let rational_of_const = rational_of_term;;
262 let rec flin_of_term t =
263 let fl_of_binop f l =
264 let a = List.hd l and
265 b = List.hd(List.tl l) in
266 f (flin_of_term a) (flin_of_term b)
270 | Cic.Cast (t1,t2) -> (flin_of_term t1)
271 | Cic.Appl (t1::next) ->
276 match (UriManager.string_of_uri u) with
277 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
278 flin_emult (rop r1) (flin_of_term (List.hd next))
279 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
280 fl_of_binop flin_plus next
281 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
282 fl_of_binop flin_minus next
283 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
285 let arg1 = (List.hd next) and
286 arg2 = (List.hd(List.tl next))
290 let a = rational_of_term arg1 in
293 let b = (rational_of_term arg2) in
294 (flin_add_cste (flin_zero()) (rmult a b))
297 _ -> (flin_add (flin_zero()) arg2 a)
300 _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
302 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
303 let a=(rational_of_term (List.hd next)) in
304 flin_add_cste (flin_zero()) (rinv a)
305 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
307 let b=(rational_of_term (List.hd(List.tl next))) in
310 let a = (rational_of_term (List.hd next)) in
311 (flin_add_cste (flin_zero()) (rdiv a b))
314 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
320 | Cic.Const (u,boh) ->
322 match (UriManager.string_of_uri u) with
323 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
324 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
328 with _ -> flin_add (flin_zero()) t r1
332 let flin_of_constr = flin_of_term;;
336 Translates a flin to (c,x) list
338 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
340 let flin_to_alist f =
342 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
346 (* Représentation des hypothèses qui sont des inéquations ou des équations.
350 The structure for ineq
352 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
353 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
360 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
363 let ineq1_of_term (h,t) =
364 match t with (* match t *)
365 Cic.Appl (t1::next) ->
366 let arg1= List.hd next in
367 let arg2= List.hd(List.tl next) in
368 (match t1 with (* match t1 *)
370 (match UriManager.string_of_uri u with (* match u *)
371 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
376 hflin= flin_minus (flin_of_term arg1)
379 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
384 hflin= flin_minus (flin_of_term arg2)
387 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
392 hflin= flin_minus (flin_of_term arg1)
395 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
400 hflin= flin_minus (flin_of_term arg2)
403 |_->assert false)(* match u *)
404 | Cic.MutInd (u,i,o) ->
405 (match UriManager.string_of_uri u with
406 "cic:/Coq/Init/Logic_Type/eqT.con" ->
409 let arg2= List.hd(List.tl (List.tl next)) in
412 (match UriManager.string_of_uri u with
413 "cic:/Coq/Reals/Rdefinitions/R.con"->
418 hflin= flin_minus (flin_of_term arg1)
425 hflin= flin_minus (flin_of_term arg2)
431 |_-> assert false)(* match t1 *)
432 |_-> assert false (* match t *)
435 let ineq1_of_constr = ineq1_of_term;;
438 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
444 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
447 let rec print_sys l =
450 | (a,b)::next -> (print_rl a;
451 print_string (if b=true then "strict\n"else"\n");
456 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
459 let fourier_lineq lineq1 =
461 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
463 Hashtbl.iter (fun x c ->
464 try (Hashtbl.find hvar x;())
465 with _-> nvar:=(!nvar)+1;
466 Hashtbl.add hvar x (!nvar))
470 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
471 let sys= List.map (fun h->
472 let v=Array.create ((!nvar)+1) r0 in
473 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
475 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
477 debug ("chiamo unsolvable sul sistema di "^ string_of_int (List.length sys) ^"\n");
482 (******************************************************************************
483 Construction de la preuve en cas de succès de la méthode de Fourier,
484 i.e. on obtient une contradiction.
488 let _eqT = Cic.MutInd(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
489 let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
490 let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;;
491 let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
492 let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
493 let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
494 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
495 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
496 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
497 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
498 let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
499 let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
500 let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
501 let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
502 let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
503 let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
504 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
505 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
506 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
507 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
508 let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
509 let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
510 let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
511 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
512 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
513 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
514 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
515 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
516 let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
517 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
518 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
519 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
520 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
521 let _Rminus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
522 let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
523 let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
524 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
525 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
526 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
527 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
528 let _sym_eqT = Cic.Const(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
529 (*****************************************************************************************************)
530 let is_int x = (x.den)=1
533 (* fraction = couple (num,den) *)
534 let rec rational_to_fraction x= (x.num,x.den)
537 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
540 let rec int_to_real_aux n =
542 0 -> _R0 (* o forse R0 + R0 ????? *)
544 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
549 let x = int_to_real_aux (abs n) in
551 Cic.Appl [ _Ropp ; x ]
557 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
560 let rational_to_real x =
561 let (n,d)=rational_to_fraction x in
562 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
565 (* preuve que 0<n*1/d
570 let tac_zero_inf_pos gl (n,d) =
571 (*let cste = pf_parse_constr gl in*)
572 let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
573 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
575 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
577 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
578 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
580 let tac_zero_inf_pos (n,d) ~status =
581 (*let cste = pf_parse_constr gl in*)
582 let pall str ~status:(proof,goal) t =
583 debug ("tac "^str^" :\n" );
584 let curi,metasenv,pbo,pty = proof in
585 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
586 debug ("th = "^ CicPp.ppterm t ^"\n");
587 debug ("ty = "^ CicPp.ppterm ty^"\n");
590 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
592 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
596 tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) ~status _Rlt_zero_pos_plus1;PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacn); done;
598 tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); done;
602 debug("TAC ZERO INF POS\n");
604 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
613 (* preuve que 0<=n*1/d
616 let tac_zero_infeq_pos gl (n,d) =
617 (*let cste = pf_parse_constr gl in*)
618 let tacn = ref (if n=0 then
619 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
621 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ))
623 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
625 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); done;
627 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
628 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd])
633 (* preuve que 0<(-n)*(1/d) => False
636 let tac_zero_inf_false gl (n,d) =
637 if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0)
639 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt)
640 ~continuation:(tac_zero_infeq_pos gl (-n,d)))
643 (* preuve que 0<=(-n)*(1/d) => False
646 let tac_zero_infeq_false gl (n,d) =
647 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
648 ~continuation:(tac_zero_inf_pos (-n,d)))
652 (* *********** ********** ******** ??????????????? *********** **************)
654 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
655 let curi,metasenv,pbo,pty = proof in
656 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
657 let fresh_meta = ProofEngineHelpers.new_meta proof in
659 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
660 let metasenv' = (fresh_meta,context,t)::metasenv in
661 let proof' = curi,metasenv',pbo,pty in
663 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) ~status:(proof',goal)
665 proof'',fresh_meta::goals
672 let my_cut ~term:c ~status:(proof,goal)=
673 let curi,metasenv,pbo,pty = proof in
674 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
676 let fresh_meta = ProofEngineHelpers.new_meta proof in
678 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
679 let metasenv' = (fresh_meta,context,c)::metasenv in
680 let proof' = curi,metasenv',pbo,pty in
682 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] ~status:(proof',goal)
684 (* We permute the generated goals to be consistent with Coq *)
687 | he::tl -> proof'',he::fresh_meta::tl
691 let exact = PrimitiveTactics.exact_tac;;
693 let tac_use h ~status:(proof,goal as status) =
694 debug("Inizio TC_USE\n");
695 let curi,metasenv,pbo,pty = proof in
696 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
697 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
698 debug ("ty = "^ CicPp.ppterm ty^"\n");
702 "Rlt" -> exact ~term:h.hname ~status
703 |"Rle" -> exact ~term:h.hname ~status
704 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
705 ~continuation:(exact ~term:h.hname)) ~status
706 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
707 ~continuation:(exact ~term:h.hname)) ~status
708 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
709 ~continuation:(exact ~term:h.hname)) ~status
710 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
711 ~continuation:(exact ~term:h.hname)) ~status
714 debug("Fine TAC_USE\n");
722 Cic.Appl ( Cic.Const(u,boh)::next) ->
723 (match (UriManager.string_of_uri u) with
724 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
725 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
726 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
727 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
728 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
729 (match (List.hd next) with
730 Cic.Const (uri,_) when
731 UriManager.string_of_uri uri =
732 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
738 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
741 Cic.Appl(Array.to_list a)
744 (* Résolution d'inéquations linéaires dans R *)
745 let rec strip_outer_cast c = match c with
746 | Cic.Cast (c,_) -> strip_outer_cast c
750 let find_in_context id context =
751 let rec find_in_context_aux c n =
753 [] -> failwith (id^" not found in context")
754 | a::next -> (match a with
755 Some (Cic.Name(name),_) when name = id -> n
756 (*? magari al posto di _ qualcosaltro?*)
757 | _ -> find_in_context_aux next (n+1))
759 find_in_context_aux context 1
762 (* mi sembra quadratico *)
763 let rec filter_real_hyp context cont =
766 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
767 let n = find_in_context h cont in
768 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
769 | a::next -> debug(" no\n"); filter_real_hyp next cont
772 (* lifts everithing at the conclusion level *)
773 let rec superlift c n=
776 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(CicSubstitution.lift n a))] @ superlift next (n+1)
777 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(CicSubstitution.lift n a))] @ superlift next (n+1)
778 | _::next -> superlift next (n+1) (*?? ??*)
782 let equality_replace a b ~status =
783 let module C = Cic in
784 let proof,goal = status in
785 let curi,metasenv,pbo,pty = proof in
786 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
787 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
788 let fresh_meta = ProofEngineHelpers.new_meta proof in
790 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
791 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
793 rewrite_tac ~term:(C.Meta (fresh_meta,irl))
794 ~status:((curi,metasenv',pbo,pty),goal)
796 (proof,fresh_meta::goals)
799 let tcl_fail a ~status:(proof,goal) =
801 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
806 let assumption_tac ~status:(proof,goal)=
807 let curi,metasenv,pbo,pty = proof in
808 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
810 let tac_list = List.map
811 ( fun x -> num := !num + 1;
813 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
814 | _ -> ("fake",tcl_fail 1)
818 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
821 (* !!!!! fix !!!!!!!!!! *)
822 let contradiction_tac ~status:(proof,goal)=
824 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
825 ~continuation:(Tacticals.then_
826 ~start:(Ring.elim_type_tac ~term:_False)
827 ~continuation:(assumption_tac))
831 (* ********************* TATTICA ******************************** *)
833 let rec fourier ~status:(s_proof,s_goal)=
834 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
835 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) s_metasenv in
837 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
838 debug_pcontext s_context;
840 let fhyp = String.copy "new_hyp_for_fourier" in
842 (* here we need to negate the thesis, but to do this we nned to apply the right theoreme,
843 so let's parse our thesis *)
845 let th_to_appl = ref _Rfourier_not_le_gt in
847 Cic.Appl ( Cic.Const(u,boh)::args) ->
848 (match UriManager.string_of_uri u with
849 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := _Rfourier_not_ge_lt
850 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := _Rfourier_not_gt_le
851 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := _Rfourier_not_le_gt
852 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := _Rfourier_not_lt_ge
853 |_-> failwith "fourier can't be applyed")
854 |_-> failwith "fourier can't be applyed"); (* fix maybe strip_outer_cast goes here?? *)
856 (* now let's change our thesis applying the th and put it with hp *)
858 let proof,gl = Tacticals.then_
859 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
860 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
861 ~status:(s_proof,s_goal) in
862 let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in
864 debug ("port la tesi sopra e la nego. contesto :\n");
865 debug_pcontext s_context;
867 (* now we have all the right environment *)
869 let curi,metasenv,pbo,pty = proof in
870 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
873 (* now we want to convert hp to inequations, but first we must lift
874 everyting to thesis level, so that a variable has the save Rel(n)
875 in each hp ( needed by ineq1_of_term ) *)
877 (* ? fix if None ?????*)
878 (* fix change superlift with a real name *)
880 let l_context = superlift context 1 in
881 let hyps = filter_real_hyp l_context l_context in
883 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
887 (* transform hyps into inequations *)
889 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
894 debug ("applico fourier a "^ string_of_int (List.length !lineq)^" disequazioni\n");
896 let res=fourier_lineq (!lineq) in
897 let tac=ref Ring.id_tac in
899 (print_string "Tactic Fourier fails.\n";flush stdout;failwith "fourier_tac fails")
902 match res with (*match res*)
905 (* in lc we have the coefficient to "reduce" the system *)
907 print_string "Fourier's method can prove the goal...\n";flush stdout;
909 debug "I coeff di moltiplicazione rit sono: ";
913 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
914 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
916 (List.combine (!lineq) lc);
918 print_string (" quindi lutil e' lunga "^string_of_int (List.length (!lutil))^"\n");
920 (* on construit la combinaison linéaire des inéquation *)
922 (match (!lutil) with (*match (!lutil) *)
925 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
927 let s=ref (h1.hstrict) in
929 (* let t1=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hleft|]) in
930 let t2=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hright|]) in
933 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
934 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
936 List.iter (fun (h,c) ->
937 s:=(!s)||(h.hstrict);
938 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl [_Rmult;rational_to_real c;h.hleft ] ]);
939 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl [_Rmult;rational_to_real c;h.hright] ]))
942 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
943 let tc=rational_to_real cres in
946 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
948 debug "inizio a costruire tac1\n";
949 Fourier.print_rational(c1);
951 let tac1=ref ( fun ~status ->
952 debug ("Sotto tattica t1 "^(if h1.hstrict then "strict" else "lasc")^"\n");
954 (Tacticals.thens ~start:(
956 debug ("inizio t1 strict\n");
957 let curi,metasenv,pbo,pty = proof in
958 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
959 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
960 debug ("ty = "^ CicPp.ppterm ty^"\n");
962 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
963 ~continuations:[tac_use h1;
965 tac_zero_inf_pos (rational_to_fraction c1)] ~status
969 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
970 ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status))
975 List.iter (fun (h,c) ->
979 tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
980 ~term:_Rfourier_lt_lt)
981 ~continuations:[!tac1;tac_use h;
983 (rational_to_fraction c)]))
987 Fourier.print_rational(c1);
988 tac1:=(Tacticals.thens ~start:(
990 debug("INIZIO TAC 1 2\n");
992 let curi,metasenv,pbo,pty = proof in
993 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
994 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
995 debug ("ty = "^ CicPp.ppterm ty^"\n");
997 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status
1000 ~continuations:[!tac1;tac_use h;
1002 tac_zero_inf_pos (rational_to_fraction c)
1011 tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1012 ~continuations:[!tac1;tac_use h;
1014 (rational_to_fraction c)]))
1018 tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1019 ~continuations:[!tac1;tac_use h;
1021 (rational_to_fraction c)]))
1025 s:=(!s)||(h.hstrict))
1026 lutil;(*end List.iter*)
1028 let tac2= if sres then
1029 tac_zero_inf_false goal (rational_to_fraction cres)
1031 tac_zero_infeq_false goal (rational_to_fraction cres)
1033 tac:=(Tacticals.thens ~start:(my_cut ~term:ineq)
1034 ~continuations:[Tacticals.then_ (* ?????????????????????????????? *)
1035 ~start:(fun ~status:(proof,goal as status) ->
1036 let curi,metasenv,pbo,pty = proof in
1037 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1038 PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1039 ~continuation:(Tacticals.then_
1040 ~start:(PrimitiveTactics.apply_tac
1041 ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
1042 ~continuation:(Tacticals.thens
1043 ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
1044 ~continuations:[(*tac2;*)(Tacticals.thens
1045 ~start:(equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
1049 Tacticals.try_tactics
1050 (* ???????????????????????????? *)
1051 ~tactics:[ "ring", Ring.ring_tac ; "id", Ring.id_tac]
1054 ~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
1055 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1057 Tacticals.try_tactics
1058 (* ???????????????????????????? *)
1059 ~tactics:[ "ring", Ring.ring_tac ; "id", Ring.id_tac]
1064 ;tac2 ] (* end continuations before comment *)
1069 tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False)
1070 ~continuations:[Tacticals.then_
1071 (* ???????????????????????????????
1073 ~start:(PrimitiveTactics.intros_tac ~name:(String.copy "??"))
1074 (* ????????????????????????????? *)
1076 ~continuation:contradiction_tac;!tac])
1079 |_-> assert false)(*match (!lutil) *)
1080 |_-> assert false); (*match res*)
1082 debug ("finalmente applico tac\n");
1083 (!tac ~status:(proof,goal))
1087 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;