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/.
28 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
29 des inéquations et équations sont entiers. En attendant la tactique Field.
35 let debug x = print_string x ; flush stdout;;
37 (******************************************************************************
38 Operations on linear combinations.
40 Opérations sur les combinaisons linéaires affines.
41 La partie homogène d'une combinaison linéaire est en fait une table de hash
42 qui donne le coefficient d'un terme du calcul des constructions,
43 qui est zéro si le terme n'y est pas.
49 The type for linear combinations
51 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
57 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
63 @return the rational associated with x (coefficient)
67 (Hashtbl.find f.fhom x)
73 Adds c to the coefficient of x
80 let cx = flin_coef f x in
81 Hashtbl.remove f.fhom x;
82 Hashtbl.add f.fhom x (rplus cx c);
91 let flin_add_cste f c =
93 fcste=rplus f.fcste c}
97 @return a empty flin with r1 in fcste
99 let flin_one () = flin_add_cste (flin_zero()) r1;;
104 let flin_plus f1 f2 =
105 let f3 = flin_zero() in
106 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
107 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
108 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
114 let flin_minus f1 f2 =
115 let f3 = flin_zero() in
116 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
117 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
118 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
125 let f2 = flin_zero() in
126 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
127 flin_add_cste f2 (rmult a f.fcste);
131 (*****************************************************************************)
136 @return proiection on string of t
138 let rec string_of_term t =
140 Cic.Cast (t1,t2) -> string_of_term t1
141 |Cic.Const (u,boh) -> UriManager.string_of_uri u
142 |Cic.Var (u) -> UriManager.string_of_uri u
143 | _ -> "not_of_constant"
147 let string_of_constr = string_of_term
153 @raise Failure if conversion is impossible
154 @return rational proiection of t
156 let rec rational_of_term t =
157 (* fun to apply f to the first and second rational-term of l *)
158 let rat_of_binop f l =
159 let a = List.hd l and
160 b = List.hd(List.tl l) in
161 f (rational_of_term a) (rational_of_term b)
163 (* as before, but f is unary *)
164 let rat_of_unop f l =
165 f (rational_of_term (List.hd l))
168 | Cic.Cast (t1,t2) -> (rational_of_term t1)
169 | Cic.Appl (t1::next) ->
172 (match (UriManager.string_of_uri u) with
173 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
175 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
176 rat_of_unop rinv next
177 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
178 rat_of_binop rmult next
179 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
180 rat_of_binop rdiv next
181 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
182 rat_of_binop rplus next
183 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
184 rat_of_binop rminus next
185 | _ -> failwith "not a rational")
186 | _ -> failwith "not a rational")
187 | Cic.Const (u,boh) ->
188 (match (UriManager.string_of_uri u) with
189 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
190 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
191 | _ -> failwith "not a rational")
192 | _ -> failwith "not a rational"
196 let rational_of_const = rational_of_term;;
200 let rec flin_of_term t =
201 let fl_of_binop f l =
202 let a = List.hd l and
203 b = List.hd(List.tl l) in
204 f (flin_of_term a) (flin_of_term b)
208 | Cic.Cast (t1,t2) -> (flin_of_term t1)
209 | Cic.Appl (t1::next) ->
214 match (UriManager.string_of_uri u) with
215 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
216 flin_emult (rop r1) (flin_of_term (List.hd next))
217 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
218 fl_of_binop flin_plus next
219 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
220 fl_of_binop flin_minus next
221 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
223 let arg1 = (List.hd next) and
224 arg2 = (List.hd(List.tl next))
228 let a = rational_of_term arg1 in
231 let b = (rational_of_term arg2) in
232 (flin_add_cste (flin_zero()) (rmult a b))
235 _ -> (flin_add (flin_zero()) arg2 a)
238 _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
240 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
241 let a=(rational_of_term (List.hd next)) in
242 flin_add_cste (flin_zero()) (rinv a)
243 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
245 let b=(rational_of_term (List.hd(List.tl next))) in
248 let a = (rational_of_term (List.hd next)) in
249 (flin_add_cste (flin_zero()) (rdiv a b))
252 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
258 | Cic.Const (u,boh) ->
260 match (UriManager.string_of_uri u) with
261 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
262 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
266 with _ -> flin_add (flin_zero()) t r1
270 let flin_of_constr = flin_of_term;;
274 Translates a flin to (c,x) list
276 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
278 let flin_to_alist f =
280 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
284 (* Représentation des hypothèses qui sont des inéquations ou des équations.
288 The structure for ineq
290 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
291 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
298 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
301 let ineq1_of_term (h,t) =
303 Cic.Appl (t1::next) ->
304 let arg1= List.hd next in
305 let arg2= List.hd(List.tl next) in
308 (match UriManager.string_of_uri u with
309 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
313 hflin= flin_minus (flin_of_term arg1)
316 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h;
320 hflin= flin_minus (flin_of_term arg2)
323 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h;
327 hflin= flin_minus (flin_of_term arg1)
330 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h;
334 hflin= flin_minus (flin_of_term arg2)
338 | Cic.MutInd (u,i,o) ->
339 (match UriManager.string_of_uri u with
340 "cic:/Coq/Init/Logic_Type/eqT.con" ->
343 let arg2= List.hd(List.tl (List.tl next)) in
346 (match UriManager.string_of_uri u with
347 "cic:/Coq/Reals/Rdefinitions/R.con"->
352 hflin= flin_minus (flin_of_term arg1)
359 hflin= flin_minus (flin_of_term arg2)
369 let ineq1_of_constr = ineq1_of_term;;
372 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
375 let fourier_lineq lineq1 =
377 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
379 Hashtbl.iter (fun x c ->
380 try (Hashtbl.find hvar x;())
381 with _-> nvar:=(!nvar)+1;
382 Hashtbl.add hvar x (!nvar))
385 let sys= List.map (fun h->
386 let v=Array.create ((!nvar)+1) r0 in
387 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
389 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
391 debug ("chiamo unsolvable sul sistema di "^ string_of_int (List.length sys) ^"\n");
395 (******************************************************************************
396 Construction de la preuve en cas de succès de la méthode de Fourier,
397 i.e. on obtient une contradiction.
400 let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
401 let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
402 let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
403 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
404 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
405 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
406 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
407 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
408 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
409 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
410 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
411 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
412 let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
413 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
414 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
415 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
416 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
417 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
418 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
419 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
420 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
422 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
424 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
426 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
429 let is_int x = (x.den)=1
432 (* fraction = couple (num,den) *)
433 let rec rational_to_fraction x= (x.num,x.den)
436 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
439 let rec int_to_real_aux n =
441 0 -> _R0 (* o forse R0 + R0 ????? *)
442 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
447 let x = int_to_real_aux (abs n) in
449 Cic.Appl [ _Ropp ; x ]
455 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
458 let rational_to_real x =
459 let (n,d)=rational_to_fraction x in
460 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
463 (* preuve que 0<n*1/d
466 let tac_zero_inf_pos gl (n,d) =
467 (*let cste = pf_parse_constr gl in*)
468 let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
469 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
471 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
473 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
474 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
477 (* preuve que 0<=n*1/d
480 let tac_zero_infeq_pos gl (n,d) =
481 (*let cste = pf_parse_constr gl in*)
482 let tacn = ref (if n=0 then
483 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
485 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ))
487 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
489 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); done;
491 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
492 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd])
497 (* preuve que 0<(-n)*(1/d) => False
500 let tac_zero_inf_false gl (n,d) =
501 if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0)
503 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt)
504 ~continuation:(tac_zero_infeq_pos gl (-n,d)))
507 (* preuve que 0<=(-n)*(1/d) => False
510 let tac_zero_infeq_false gl (n,d) =
511 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
512 ~continuation:(tac_zero_inf_pos gl (-n,d)))
516 (* *********** ********** ******** ??????????????? *********** **************
518 let mkMeta proof = Cic.Meta (ProofEngineHelpers.new_meta proof) (ProofEngineHelpers.identity_relocation_list_for_metavariable []);;
520 let apply_type_tac t al (proof,goals) =
521 let new_m = mkMeta proof in
522 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast new_m t)::al))
528 let create_meta () = mkMeta(new_meta());;
531 let concl = pf_concl gl in
532 apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
535 *********** * ********************************* ***************************** *)
537 let exact = PrimitiveTactics.exact_tac;;
539 let tac_use h = match h.htype with
540 "Rlt" -> exact ~term:h.hname
541 |"Rle" -> exact ~term:h.hname
542 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
543 ~continuation:(exact ~term:h.hname))
544 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
545 ~continuation:(exact ~term:h.hname))
546 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
547 ~continuation:(exact ~term:h.hname))
548 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
549 ~continuation:(exact ~term:h.hname))
557 Cic.Appl ( Cic.Const(u,boh)::next) ->
558 (match (UriManager.string_of_uri u) with
559 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
560 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
561 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
562 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
563 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
564 (match (List.hd next) with
565 Cic.Const (uri,_) when
566 UriManager.string_of_uri uri =
567 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
573 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
576 Cic.Appl(Array.to_list a)
579 (* Résolution d'inéquations linéaires dans R *)
580 let rec strip_outer_cast c = match c with
581 | Cic.Cast (c,_) -> strip_outer_cast c
585 let find_in_context id context =
586 let rec find_in_context_aux c n =
588 [] -> failwith (id^" not found in context")
589 | a::next -> (match a with
590 Some (Cic.Name(name),Cic.Decl(t)) when name = id -> n
591 | _ -> find_in_context_aux next (n+1))
592 in find_in_context_aux context 1 (*?? bisogna invertire il contesto? ??*)
595 (* mi sembra quadratico *)
596 let rec filter_real_hyp context =
599 | Some(Cic.Name(h),Cic.Def(t))::next -> [(Cic.Rel(find_in_context h next),t)] @
601 | a::next -> filter_real_hyp next
606 (* se pf_concl estrae la concl*)
607 let rec fourier ~status:(proof,goal)=
608 debug ("invoco fourier_tac sul goal"^string_of_int(goal)^"\n");
609 let curi,metasenv,pbo,pty = proof in
610 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
612 (* il goal di prima dovrebbe essere ty
613 let goal = strip_outer_cast (pf_concl gl) in*)
615 let fhyp = String.copy "new_hyp_for_fourier" in
616 (* si le but est une inéquation, on introduit son contraire,
617 et le but à prouver devient False *)
621 Cic.Appl ( Cic.Const(u,boh)::args) ->
622 (match UriManager.string_of_uri u with
623 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
625 ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_ge_lt)
626 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
627 ~continuation:fourier)
628 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
630 ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_gt_le)
631 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
632 ~continuation:fourier)
633 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
635 ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_le_gt)
636 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
637 ~continuation:fourier)
638 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
640 ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_lt_ge)
641 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
642 ~continuation:fourier)
645 in tac (proof,goal) )
651 (* ? fix if None ?????*)
652 debug ("estraggo hp da context "^ string_of_int(List.length context)^"\n");
653 let hyps = filter_real_hyp context in
654 debug ("trasformo in eq "^ string_of_int (List.length hyps)^"\n");
656 List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
661 (* lineq = les inéquations découlant des hypothèses *)
663 debug ("applico fourier a "^ string_of_int (List.length !lineq)^"\n");
665 let res=fourier_lineq (!lineq) in
666 (*let tac=ref tclIDTAC in*)
668 then (print_string "Tactic Fourier fails.\n";
673 (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
679 (* lc=coefficients multiplicateurs des inéquations
680 qui donnent 0<cres ou 0<=cres selon sres *)
681 (*print_string "Fourier's method can prove the goal...";flush stdout;*)
689 then (lutil:=(h,c)::(!lutil)(*;
690 print_rational(c);print_string " "*)))
691 (List.combine (!lineq) lc);
694 (* on construit la combinaison linéaire des inéquation *)
699 let s=ref (h1.hstrict) in
700 let t1=ref (mkAppL [|parse "Rmult";
701 parse (rational_to_real c1);
703 let t2=ref (mkAppL [|parse "Rmult";
704 parse (rational_to_real c1);
706 List.iter (fun (h,c) ->
707 s:=(!s)||(h.hstrict);
708 t1:=(mkAppL [|parse "Rplus";
710 mkAppL [|parse "Rmult";
711 parse (rational_to_real c);
713 t2:=(mkAppL [|parse "Rplus";
715 mkAppL [|parse "Rmult";
716 parse (rational_to_real c);
719 let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
722 let tc=parse (rational_to_real cres) in
726 let tac1=ref (if h1.hstrict
727 then (tclTHENS (apply (parse "Rfourier_lt"))
730 (rational_to_fraction c1)])
731 else (tclTHENS (apply (parse "Rfourier_le"))
734 (rational_to_fraction c1)])) in
736 List.iter (fun (h,c)->
739 then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
742 (rational_to_fraction c)])
743 else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
746 (rational_to_fraction c)]))
748 then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
751 (rational_to_fraction c)])
752 else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
755 (rational_to_fraction c)])));
756 s:=(!s)||(h.hstrict))
759 then tac_zero_inf_false gl (rational_to_fraction cres)
760 else tac_zero_infeq_false gl (rational_to_fraction cres)
762 tac:=(tclTHENS (my_cut ineq)
763 [tclTHEN (change_in_concl
764 (mkAppL [| parse "not"; ineq|]
766 (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
767 else parse "Rnot_le_le"))
768 (tclTHENS (Equality.replace
769 (mkAppL [|parse "Rminus";!t2;!t1|]
773 (tclTHENS (Equality.replace (parse "(Rinv R1)")
776 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
781 (tclTHEN (apply (parse "sym_eqT"))
782 (apply (parse "Rinv_R1")))]
787 tac:=(tclTHENS (cut (parse "False"))
788 [tclTHEN intro contradiction;
790 |_-> assert false) |_-> assert false
792 ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
794 ((tclABSTRACT None !tac) gl)
798 let fourier_tac x gl =
802 let v_fourier = add_tactic "Fourier" fourier_tac
805 (*open CicReduction*)
806 (*open PrimitiveTactics*)
807 (*open ProofEngineTypes*)
808 let fourier_tac ~status:(proof,goal) = ignore(fourier (proof,goal)) ; (proof,[goal]) ;;