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
60 ~equality:ProofEngineReduction.syntactic_equality
61 ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
63 C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
65 prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
66 let fresh_meta = ProofEngineHelpers.new_meta proof in
68 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
69 let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
70 PrimitiveTactics.exact_tac
72 [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
73 ((curi,metasenv',pbo,pty),goal)
76 (******************** THE FOURIER TACTIC ***********************)
78 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
79 des inéquations et équations sont entiers. En attendant la tactique Field.
85 let debug x = print_string ("____ "^x) ; flush stdout;;
87 let debug_pcontext x =
89 List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^ a ^ " " | _ ->()) x ;
90 debug ("contesto : "^ (!str) ^ "\n")
93 (******************************************************************************
94 Operations on linear combinations.
96 Opérations sur les combinaisons linéaires affines.
97 La partie homogène d'une combinaison linéaire est en fait une table de hash
98 qui donne le coefficient d'un terme du calcul des constructions,
99 qui est zéro si le terme n'y est pas.
105 The type for linear combinations
107 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
111 @return an empty flin
113 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
119 @return the rational associated with x (coefficient)
123 (Hashtbl.find f.fhom x)
129 Adds c to the coefficient of x
136 let cx = flin_coef f x in
137 Hashtbl.remove f.fhom x;
138 Hashtbl.add f.fhom x (rplus cx c);
147 let flin_add_cste f c =
149 fcste=rplus f.fcste c}
153 @return a empty flin with r1 in fcste
155 let flin_one () = flin_add_cste (flin_zero()) r1;;
160 let flin_plus f1 f2 =
161 let f3 = flin_zero() in
162 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
163 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
164 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
170 let flin_minus f1 f2 =
171 let f3 = flin_zero() in
172 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
173 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
174 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
181 let f2 = flin_zero() in
182 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
183 flin_add_cste f2 (rmult a f.fcste);
187 (*****************************************************************************)
192 @return proiection on string of t
194 let rec string_of_term t =
196 Cic.Cast (t1,t2) -> string_of_term t1
197 |Cic.Const (u,boh) -> UriManager.string_of_uri u
198 |Cic.Var (u) -> UriManager.string_of_uri u
199 | _ -> "not_of_constant"
203 let string_of_constr = string_of_term
209 @raise Failure if conversion is impossible
210 @return rational proiection of t
212 let rec rational_of_term t =
213 (* fun to apply f to the first and second rational-term of l *)
214 let rat_of_binop f l =
215 let a = List.hd l and
216 b = List.hd(List.tl l) in
217 f (rational_of_term a) (rational_of_term b)
219 (* as before, but f is unary *)
220 let rat_of_unop f l =
221 f (rational_of_term (List.hd l))
224 | Cic.Cast (t1,t2) -> (rational_of_term t1)
225 | Cic.Appl (t1::next) ->
228 (match (UriManager.string_of_uri u) with
229 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
231 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
232 rat_of_unop rinv next
233 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
234 rat_of_binop rmult next
235 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
236 rat_of_binop rdiv next
237 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
238 rat_of_binop rplus next
239 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
240 rat_of_binop rminus next
241 | _ -> failwith "not a rational")
242 | _ -> failwith "not a rational")
243 | Cic.Const (u,boh) ->
244 (match (UriManager.string_of_uri u) with
245 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
246 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
247 | _ -> failwith "not a rational")
248 | _ -> failwith "not a rational"
252 let rational_of_const = rational_of_term;;
256 let rec flin_of_term t =
257 let fl_of_binop f l =
258 let a = List.hd l and
259 b = List.hd(List.tl l) in
260 f (flin_of_term a) (flin_of_term b)
264 | Cic.Cast (t1,t2) -> (flin_of_term t1)
265 | Cic.Appl (t1::next) ->
270 match (UriManager.string_of_uri u) with
271 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
272 flin_emult (rop r1) (flin_of_term (List.hd next))
273 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
274 fl_of_binop flin_plus next
275 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
276 fl_of_binop flin_minus next
277 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
279 let arg1 = (List.hd next) and
280 arg2 = (List.hd(List.tl next))
284 let a = rational_of_term arg1 in
287 let b = (rational_of_term arg2) in
288 (flin_add_cste (flin_zero()) (rmult a b))
291 _ -> (flin_add (flin_zero()) arg2 a)
294 _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
296 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
297 let a=(rational_of_term (List.hd next)) in
298 flin_add_cste (flin_zero()) (rinv a)
299 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
301 let b=(rational_of_term (List.hd(List.tl next))) in
304 let a = (rational_of_term (List.hd next)) in
305 (flin_add_cste (flin_zero()) (rdiv a b))
308 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
314 | Cic.Const (u,boh) ->
316 match (UriManager.string_of_uri u) with
317 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
318 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
322 with _ -> flin_add (flin_zero()) t r1
326 let flin_of_constr = flin_of_term;;
330 Translates a flin to (c,x) list
332 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
334 let flin_to_alist f =
336 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
340 (* Représentation des hypothèses qui sont des inéquations ou des équations.
344 The structure for ineq
346 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
347 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
354 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
357 let ineq1_of_term (h,t) =
358 match t with (* match t *)
359 Cic.Appl (t1::next) ->
360 let arg1= List.hd next in
361 let arg2= List.hd(List.tl next) in
362 (match t1 with (* match t1 *)
364 (match UriManager.string_of_uri u with (* match u *)
365 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
370 hflin= flin_minus (flin_of_term arg1)
373 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
378 hflin= flin_minus (flin_of_term arg2)
381 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
386 hflin= flin_minus (flin_of_term arg1)
389 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
394 hflin= flin_minus (flin_of_term arg2)
397 |_->assert false)(* match u *)
398 | Cic.MutInd (u,i,o) ->
399 (match UriManager.string_of_uri u with
400 "cic:/Coq/Init/Logic_Type/eqT.con" ->
403 let arg2= List.hd(List.tl (List.tl next)) in
406 (match UriManager.string_of_uri u with
407 "cic:/Coq/Reals/Rdefinitions/R.con"->
412 hflin= flin_minus (flin_of_term arg1)
419 hflin= flin_minus (flin_of_term arg2)
425 |_-> assert false)(* match t1 *)
426 |_-> assert false (* match t *)
429 let ineq1_of_constr = ineq1_of_term;;
432 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
438 | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
441 let rec print_sys l =
444 | (a,b)::next -> (print_rl a;
445 print_string (if b=true then "strict\n"else"\n");
450 Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
453 let fourier_lineq lineq1 =
455 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
457 Hashtbl.iter (fun x c ->
458 try (Hashtbl.find hvar x;())
459 with _-> nvar:=(!nvar)+1;
460 Hashtbl.add hvar x (!nvar))
464 debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
465 let sys= List.map (fun h->
466 let v=Array.create ((!nvar)+1) r0 in
467 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
469 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
471 debug ("chiamo unsolvable sul sistema di "^ string_of_int (List.length sys) ^"\n");
476 (******************************************************************************
477 Construction de la preuve en cas de succès de la méthode de Fourier,
478 i.e. on obtient une contradiction.
482 let _eqT = Cic.MutInd(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
483 let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
484 let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;;
485 let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
486 let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
487 let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
488 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
489 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
490 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
491 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
492 let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
493 let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
494 let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
495 let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
496 let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
497 let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
498 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
499 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
500 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
501 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
502 let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
503 let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
504 let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
505 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
506 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
507 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
508 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
509 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
510 let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
511 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
512 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
513 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
514 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
515 let _Rminus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
516 let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
517 let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
518 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
519 let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
520 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
521 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
522 let _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
523 (*****************************************************************************************************)
524 let is_int x = (x.den)=1
527 (* fraction = couple (num,den) *)
528 let rec rational_to_fraction x= (x.num,x.den)
531 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
534 let rec int_to_real_aux n =
536 0 -> _R0 (* o forse R0 + R0 ????? *)
538 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
543 let x = int_to_real_aux (abs n) in
545 Cic.Appl [ _Ropp ; x ]
551 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
554 let rational_to_real x =
555 let (n,d)=rational_to_fraction x in
556 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
559 (* preuve que 0<n*1/d
564 let tac_zero_inf_pos gl (n,d) =
565 (*let cste = pf_parse_constr gl in*)
566 let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
567 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
569 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
571 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
572 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
574 let tac_zero_inf_pos (n,d) ~status =
575 (*let cste = pf_parse_constr gl in*)
576 let pall str ~status:(proof,goal) t =
577 debug ("tac "^str^" :\n" );
578 let curi,metasenv,pbo,pty = proof in
579 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
580 debug ("th = "^ CicPp.ppterm t ^"\n");
581 debug ("ty = "^ CicPp.ppterm ty^"\n");
584 (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
586 (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
590 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;
592 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;
596 debug("TAC ZERO INF POS\n");
598 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
607 (* preuve que 0<=n*1/d
610 let tac_zero_infeq_pos gl (n,d) =
611 (*let cste = pf_parse_constr gl in*)
612 let tacn = ref (if n=0 then
613 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
615 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ))
617 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
619 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); done;
621 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
622 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd])
627 (* preuve que 0<(-n)*(1/d) => False
630 let tac_zero_inf_false gl (n,d) =
631 if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0)
633 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt)
634 ~continuation:(tac_zero_infeq_pos gl (-n,d)))
637 (* preuve que 0<=(-n)*(1/d) => False
640 let tac_zero_infeq_false gl (n,d) =
641 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
642 ~continuation:(tac_zero_inf_pos (-n,d)))
646 (* *********** ********** ******** ??????????????? *********** **************)
648 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
649 let curi,metasenv,pbo,pty = proof in
650 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
651 let fresh_meta = ProofEngineHelpers.new_meta proof in
653 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
654 let metasenv' = (fresh_meta,context,t)::metasenv in
655 let proof' = curi,metasenv',pbo,pty in
657 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) ~status:(proof',goal)
659 proof'',fresh_meta::goals
666 let my_cut ~term:c ~status:(proof,goal)=
667 let curi,metasenv,pbo,pty = proof in
668 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
670 let fresh_meta = ProofEngineHelpers.new_meta proof in
672 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
673 let metasenv' = (fresh_meta,context,c)::metasenv in
674 let proof' = curi,metasenv',pbo,pty in
676 apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] ~status:(proof',goal)
678 (* We permute the generated goals to be consistent with Coq *)
681 | he::tl -> proof'',he::fresh_meta::tl
685 let exact = PrimitiveTactics.exact_tac;;
687 let tac_use h ~status:(proof,goal as status) =
688 debug("Inizio TC_USE\n");
689 let curi,metasenv,pbo,pty = proof in
690 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
691 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
692 debug ("ty = "^ CicPp.ppterm ty^"\n");
696 "Rlt" -> exact ~term:h.hname ~status
697 |"Rle" -> exact ~term:h.hname ~status
698 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
699 ~continuation:(exact ~term:h.hname)) ~status
700 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
701 ~continuation:(exact ~term:h.hname)) ~status
702 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
703 ~continuation:(exact ~term:h.hname)) ~status
704 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
705 ~continuation:(exact ~term:h.hname)) ~status
708 debug("Fine TAC_USE\n");
716 Cic.Appl ( Cic.Const(u,boh)::next) ->
717 (match (UriManager.string_of_uri u) with
718 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
719 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
720 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
721 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
722 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
723 (match (List.hd next) with
724 Cic.Const (uri,_) when
725 UriManager.string_of_uri uri =
726 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
732 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
735 Cic.Appl(Array.to_list a)
738 (* Résolution d'inéquations linéaires dans R *)
739 let rec strip_outer_cast c = match c with
740 | Cic.Cast (c,_) -> strip_outer_cast c
744 let find_in_context id context =
745 let rec find_in_context_aux c n =
747 [] -> failwith (id^" not found in context")
748 | a::next -> (match a with
749 Some (Cic.Name(name),_) when name = id -> n
750 (*? magari al posto di _ qualcosaltro?*)
751 | _ -> find_in_context_aux next (n+1))
753 find_in_context_aux context 1
756 (* mi sembra quadratico *)
757 let rec filter_real_hyp context cont =
760 | Some(Cic.Name(h),Cic.Decl(t))::next -> (
761 let n = find_in_context h cont in
762 [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
763 | a::next -> debug(" no\n"); filter_real_hyp next cont
766 (* lifts everithing at the conclusion level *)
767 let rec superlift c n=
770 | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(CicSubstitution.lift n a))] @ superlift next (n+1)
771 | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(CicSubstitution.lift n a))] @ superlift next (n+1)
772 | _::next -> superlift next (n+1) (*?? ??*)
776 let equality_replace a b ~status =
777 let module C = Cic in
778 let proof,goal = status in
779 let curi,metasenv,pbo,pty = proof in
780 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
781 let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
782 let fresh_meta = ProofEngineHelpers.new_meta proof in
784 ProofEngineHelpers.identity_relocation_list_for_metavariable context in
785 let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
787 rewrite_tac ~term:(C.Meta (fresh_meta,irl))
788 ~status:((curi,metasenv',pbo,pty),goal)
790 (proof,fresh_meta::goals)
793 let tcl_fail a ~status:(proof,goal) =
795 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
800 let assumption_tac ~status:(proof,goal)=
801 let curi,metasenv,pbo,pty = proof in
802 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
804 let tac_list = List.map
805 ( fun x -> num := !num + 1;
807 Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
808 | _ -> ("fake",tcl_fail 1)
812 Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
815 (* !!!!! fix !!!!!!!!!! *)
816 let contradiction_tac ~status:(proof,goal)=
818 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
819 ~continuation:(Tacticals.then_
820 ~start:(Ring.elim_type_tac ~term:_False)
821 ~continuation:(assumption_tac))
825 (* ********************* TATTICA ******************************** *)
827 let rec fourier ~status:(s_proof,s_goal)=
828 let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
829 let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) s_metasenv in
831 debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
832 debug_pcontext s_context;
834 let fhyp = String.copy "new_hyp_for_fourier" in
836 (* here we need to negate the thesis, but to do this we nned to apply the right theoreme,
837 so let's parse our thesis *)
839 let th_to_appl = ref _Rfourier_not_le_gt in
841 Cic.Appl ( Cic.Const(u,boh)::args) ->
842 (match UriManager.string_of_uri u with
843 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := _Rfourier_not_ge_lt
844 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := _Rfourier_not_gt_le
845 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := _Rfourier_not_le_gt
846 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := _Rfourier_not_lt_ge
847 |_-> failwith "fourier can't be applyed")
848 |_-> failwith "fourier can't be applyed"); (* fix maybe strip_outer_cast goes here?? *)
850 (* now let's change our thesis applying the th and put it with hp *)
852 let proof,gl = Tacticals.then_
853 ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
854 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
855 ~status:(s_proof,s_goal) in
856 let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in
858 debug ("port la tesi sopra e la nego. contesto :\n");
859 debug_pcontext s_context;
861 (* now we have all the right environment *)
863 let curi,metasenv,pbo,pty = proof in
864 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
867 (* now we want to convert hp to inequations, but first we must lift
868 everyting to thesis level, so that a variable has the save Rel(n)
869 in each hp ( needed by ineq1_of_term ) *)
871 (* ? fix if None ?????*)
872 (* fix change superlift with a real name *)
874 let l_context = superlift context 1 in
875 let hyps = filter_real_hyp l_context l_context in
877 debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
881 (* transform hyps into inequations *)
883 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
888 debug ("applico fourier a "^ string_of_int (List.length !lineq)^" disequazioni\n");
890 let res=fourier_lineq (!lineq) in
891 let tac=ref Ring.id_tac in
893 (print_string "Tactic Fourier fails.\n";flush stdout;failwith "fourier_tac fails")
896 match res with (*match res*)
899 (* in lc we have the coefficient to "reduce" the system *)
901 print_string "Fourier's method can prove the goal...\n";flush stdout;
903 debug "I coeff di moltiplicazione rit sono: ";
907 (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
908 (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
910 (List.combine (!lineq) lc);
912 print_string (" quindi lutil e' lunga "^string_of_int (List.length (!lutil))^"\n");
914 (* on construit la combinaison linéaire des inéquation *)
916 (match (!lutil) with (*match (!lutil) *)
919 debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
921 let s=ref (h1.hstrict) in
923 (* let t1=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hleft|]) in
924 let t2=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hright|]) in
927 let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
928 let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
930 List.iter (fun (h,c) ->
931 s:=(!s)||(h.hstrict);
932 t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl [_Rmult;rational_to_real c;h.hleft ] ]);
933 t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl [_Rmult;rational_to_real c;h.hright] ]))
936 let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
937 let tc=rational_to_real cres in
940 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
942 debug "inizio a costruire tac1\n";
943 Fourier.print_rational(c1);
945 let tac1=ref ( fun ~status ->
946 debug ("Sotto tattica t1 "^(if h1.hstrict then "strict" else "lasc")^"\n");
948 (Tacticals.thens ~start:(
950 debug ("inizio t1 strict\n");
951 let curi,metasenv,pbo,pty = proof in
952 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
953 debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
954 debug ("ty = "^ CicPp.ppterm ty^"\n");
956 PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
957 ~continuations:[tac_use h1;
959 tac_zero_inf_pos (rational_to_fraction c1)] ~status
963 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
964 ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status))
969 List.iter (fun (h,c) ->
973 tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
974 ~term:_Rfourier_lt_lt)
975 ~continuations:[!tac1;tac_use h;
977 (rational_to_fraction c)]))
981 Fourier.print_rational(c1);
982 tac1:=(Tacticals.thens ~start:(
984 debug("INIZIO TAC 1 2\n");
986 let curi,metasenv,pbo,pty = proof in
987 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
988 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
989 debug ("ty = "^ CicPp.ppterm ty^"\n");
991 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status
994 ~continuations:[!tac1;tac_use h;
996 tac_zero_inf_pos (rational_to_fraction c)
1005 tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1006 ~continuations:[!tac1;tac_use h;
1008 (rational_to_fraction c)]))
1012 tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1013 ~continuations:[!tac1;tac_use h;
1015 (rational_to_fraction c)]))
1019 s:=(!s)||(h.hstrict))
1020 lutil;(*end List.iter*)
1022 let tac2= if sres then
1023 tac_zero_inf_false goal (rational_to_fraction cres)
1025 tac_zero_infeq_false goal (rational_to_fraction cres)
1027 tac:=(Tacticals.thens ~start:(my_cut ~term:ineq)
1028 ~continuations:[Tacticals.then_ (* ?????????????????????????????? *)
1029 ~start:(fun ~status:(proof,goal as status) ->
1030 let curi,metasenv,pbo,pty = proof in
1031 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1032 PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1033 ~continuation:(Tacticals.then_
1034 ~start:(PrimitiveTactics.apply_tac
1035 ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
1036 ~continuation:(Tacticals.thens
1037 ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
1038 ~continuations:[tac2;(Tacticals.thens
1039 ~start:(equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
1041 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
1042 [Tacticals.try_tactics
1043 (* ???????????????????????????? *)
1044 ~tactics:[ "ring", Ring.ring_tac ; "id", Ring.id_tac]
1047 ~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
1048 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1052 ] (* end continuations before comment *)
1057 tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False)
1058 ~continuations:[Tacticals.then_
1059 (* ???????????????????????????????
1061 ~start:(PrimitiveTactics.intros_tac ~name:(String.copy "??"))
1062 (* ????????????????????????????? *)
1064 ~continuation:contradiction_tac;!tac])
1067 |_-> assert false)(*match (!lutil) *)
1068 |_-> assert false); (*match res*)
1070 debug ("finalmente applico tac\n");
1071 (!tac ~status:(proof,goal))
1075 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;