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.
34 (******************************************************************************
35 Operations on linear combinations.
37 Opérations sur les combinaisons linéaires affines.
38 La partie homogène d'une combinaison linéaire est en fait une table de hash
39 qui donne le coefficient d'un terme du calcul des constructions,
40 qui est zéro si le terme n'y est pas.
46 The type for linear combinations
48 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
54 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
60 @return the rational associated with x (coefficient)
64 (Hashtbl.find f.fhom x)
70 Adds c to the coefficient of x
77 let cx = flin_coef f x in
78 Hashtbl.remove f.fhom x;
79 Hashtbl.add f.fhom x (rplus cx c);
88 let flin_add_cste f c =
90 fcste=rplus f.fcste c}
94 @return a empty flin with r1 in fcste
96 let flin_one () = flin_add_cste (flin_zero()) r1;;
101 let flin_plus f1 f2 =
102 let f3 = flin_zero() in
103 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
104 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
105 flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
111 let flin_minus f1 f2 =
112 let f3 = flin_zero() in
113 Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
114 Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
115 flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
122 let f2 = flin_zero() in
123 Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
124 flin_add_cste f2 (rmult a f.fcste);
128 (*****************************************************************************)
133 @return proiection on string of t
135 let rec string_of_term t =
137 Cic.Cast (t1,t2) -> string_of_term t1
138 |Cic.Const (u,boh) -> UriManager.string_of_uri u
139 |Cic.Var (u) -> UriManager.string_of_uri u
140 | _ -> "not_of_constant"
144 let string_of_constr = string_of_term
150 @raise Failure if conversion is impossible
151 @return rational proiection of t
153 let rec rational_of_term t =
154 (* fun to apply f to the first and second rational-term of l *)
155 let rat_of_binop f l =
156 let a = List.hd l and
157 b = List.hd(List.tl l) in
158 f (rational_of_term a) (rational_of_term b)
160 (* as before, but f is unary *)
161 let rat_of_unop f l =
162 f (rational_of_term (List.hd l))
165 | Cic.Cast (t1,t2) -> (rational_of_term t1)
166 | Cic.Appl (t1::next) ->
169 (match (UriManager.string_of_uri u) with
170 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
172 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
173 rat_of_unop rinv next
174 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
175 rat_of_binop rmult next
176 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
177 rat_of_binop rdiv next
178 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
179 rat_of_binop rplus next
180 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
181 rat_of_binop rminus next
182 | _ -> failwith "not a rational")
183 | _ -> failwith "not a rational")
184 | Cic.Const (u,boh) ->
185 (match (UriManager.string_of_uri u) with
186 "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
187 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
188 | _ -> failwith "not a rational")
189 | _ -> failwith "not a rational"
193 let rational_of_const = rational_of_term;;
197 let rec flin_of_term t =
198 let fl_of_binop f l =
199 let a = List.hd l and
200 b = List.hd(List.tl l) in
201 f (flin_of_term a) (flin_of_term b)
205 | Cic.Cast (t1,t2) -> (flin_of_term t1)
206 | Cic.Appl (t1::next) ->
211 match (UriManager.string_of_uri u) with
212 "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
213 flin_emult (rop r1) (flin_of_term (List.hd next))
214 |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
215 fl_of_binop flin_plus next
216 |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
217 fl_of_binop flin_minus next
218 |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
220 let arg1 = (List.hd next) and
221 arg2 = (List.hd(List.tl next))
225 let a = rational_of_term arg1 in
228 let b = (rational_of_term arg2) in
229 (flin_add_cste (flin_zero()) (rmult a b))
232 _ -> (flin_add (flin_zero()) arg2 a)
235 _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
237 |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
238 let a=(rational_of_term (List.hd next)) in
239 flin_add_cste (flin_zero()) (rinv a)
240 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
242 let b=(rational_of_term (List.hd(List.tl next))) in
245 let a = (rational_of_term (List.hd next)) in
246 (flin_add_cste (flin_zero()) (rdiv a b))
249 _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
255 | Cic.Const (u,boh) ->
257 match (UriManager.string_of_uri u) with
258 "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
259 |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
263 with _ -> flin_add (flin_zero()) t r1
267 let flin_of_constr = flin_of_term;;
271 Translates a flin to (c,x) list
273 @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
275 let flin_to_alist f =
277 Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
281 (* Représentation des hypothèses qui sont des inéquations ou des équations.
285 The structure for ineq
287 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
288 htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
295 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
298 let ineq1_of_term (h,t) =
300 Cic.Appl (t1::next) ->
301 let arg1= List.hd next in
302 let arg2= List.hd(List.tl next) in
305 (match UriManager.string_of_uri u with
306 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
310 hflin= flin_minus (flin_of_term arg1)
313 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h;
317 hflin= flin_minus (flin_of_term arg2)
320 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h;
324 hflin= flin_minus (flin_of_term arg1)
327 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h;
331 hflin= flin_minus (flin_of_term arg2)
335 | Cic.MutInd (u,i,o) ->
336 (match UriManager.string_of_uri u with
337 "cic:/Coq/Init/Logic_Type/eqT.con" ->
340 let arg2= List.hd(List.tl (List.tl next)) in
343 (match UriManager.string_of_uri u with
344 "cic:/Coq/Reals/Rdefinitions/R.con"->
349 hflin= flin_minus (flin_of_term arg1)
356 hflin= flin_minus (flin_of_term arg2)
366 let ineq1_of_constr = ineq1_of_term;;
369 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
372 let fourier_lineq lineq1 =
374 let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
376 Hashtbl.iter (fun x c ->
377 try (Hashtbl.find hvar x;())
378 with _-> nvar:=(!nvar)+1;
379 Hashtbl.add hvar x (!nvar))
382 let sys= List.map (fun h->
383 let v=Array.create ((!nvar)+1) r0 in
384 Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
386 ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
391 (******************************************************************************
392 Construction de la preuve en cas de succès de la méthode de Fourier,
393 i.e. on obtient une contradiction.
396 let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
397 let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
398 let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
399 let _Rle_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
400 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
401 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
402 let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
403 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
404 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
405 let _Rlt_not_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
406 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
407 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
408 let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
409 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
410 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
411 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
412 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
413 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
414 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
415 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
416 let _Rfourier_gt_to_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
418 let _Rfourier_ge_to_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
420 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
422 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
425 let is_int x = (x.den)=1
428 (* fraction = couple (num,den) *)
429 let rec rational_to_fraction x= (x.num,x.den)
432 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
435 let rec int_to_real_aux n =
437 0 -> _R0 (* o forse R0 + R0 ????? *)
438 | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
443 let x = int_to_real_aux (abs n) in
445 Cic.Appl [ _Ropp ; x ]
451 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
454 let rational_to_real x =
455 let (n,d)=rational_to_fraction x in
456 Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ] ]
459 (* preuve que 0<n*1/d
462 let tac_zero_inf_pos gl (n,d) =
463 (*let cste = pf_parse_constr gl in*)
464 let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
465 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
467 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
469 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
470 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
473 (* preuve que 0<=n*1/d
476 let tac_zero_infeq_pos gl (n,d) =
477 (*let cste = pf_parse_constr gl in*)
478 let tacn = ref (if n=0 then
479 (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
481 (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ))
483 let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
485 tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); done;
487 tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
488 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd])
493 (* preuve que 0<(-n)*(1/d) => False
496 let tac_zero_inf_false gl (n,d) =
497 if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0)
499 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt)
500 ~continuation:(tac_zero_infeq_pos gl (-n,d)))
503 (* preuve que 0<=(-n)*(1/d) => False
506 let tac_zero_infeq_false gl (n,d) =
507 (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
508 ~continuation:(tac_zero_inf_pos gl (-n,d)))
512 (* *********** ********** ******** ??????????????? *********** **************
514 let mkMeta proof = Cic.Meta (ProofEngineHelpers.new_meta proof) (ProofEngineHelpers.identity_relocation_list_for_metavariable []);;
516 let apply_type_tac t al (proof,goals) =
517 let new_m = mkMeta proof in
518 PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast new_m t)::al))
524 let create_meta () = mkMeta(new_meta());;
527 let concl = pf_concl gl in
528 apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
531 *********** * ********************************* ***************************** *)
533 let exact = PrimitiveTactics.exact_tac;;
535 let tac_use h = match h.htype with
536 "Rlt" -> exact ~term:h.hname
537 |"Rle" -> exact ~term:h.hname
538 |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
539 ~continuation:(exact ~term:h.hname))
540 |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
541 ~continuation:(exact ~term:h.hname))
542 |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
543 ~continuation:(exact ~term:h.hname))
544 |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
545 ~continuation:(exact ~term:h.hname))
553 Cic.Appl ( Cic.Const(u,boh)::next) ->
554 (match (UriManager.string_of_uri u) with
555 "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
556 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
557 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
558 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
559 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
560 (match (List.hd next) with
561 Cic.Const (uri,_) when
562 UriManager.string_of_uri uri =
563 "cic:/Coq/Reals/Rdefinitions/R.con" -> true
569 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
572 Cic.Appl(Array.to_list a)
575 (* Résolution d'inéquations linéaires dans R *)
576 let rec strip_outer_cast c = match c with
577 | Cic.Cast (c,_) -> strip_outer_cast c
580 (* se pf_concl estrae la concl*)
581 (*let rec fourier ~status:(((p_uri,p_meta,p_incom,p_tes) as proof,goal) as status)=
582 let goal = strip_outer_cast p_tes in
583 let fhyp = String.copy "new_hyp_for_fourier" in *)
584 (* si le but est une inéquation, on introduit son contraire,
585 et le but à prouver devient False *)
588 Cic.Appl ( Cic.Const(u,boh)::args) ->
589 (match UriManager.string_of_uri u with
590 "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
592 ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_ge_lt)
593 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
594 ~continuation:fourier)
595 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
597 ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_gt_le)
598 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
599 ~continuation:fourier)
600 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
602 ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_le_gt)
603 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
604 ~continuation:fourier)
605 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
607 ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_lt_ge)
608 ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
609 ~continuation:fourier)
617 (***** Come estraggo pf_hyps?????????????? *******)
618 (* let hyps = List.map (fun (h,t) -> (Cic.Var(h),t))
619 (list_of_sign (pf_hyps gl)) in
621 List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
626 (* lineq = les inéquations découlant des hypothèses *)
630 let res=fourier_lineq (!lineq) in
631 let tac=ref tclIDTAC in
633 then (print_string "Tactic Fourier fails.\n";
637 (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
643 (* lc=coefficients multiplicateurs des inéquations
644 qui donnent 0<cres ou 0<=cres selon sres *)
645 (*print_string "Fourier's method can prove the goal...";flush stdout;*)
653 then (lutil:=(h,c)::(!lutil)(*;
654 print_rational(c);print_string " "*)))
655 (List.combine (!lineq) lc);
658 (* on construit la combinaison linéaire des inéquation *)
663 let s=ref (h1.hstrict) in
664 let t1=ref (mkAppL [|parse "Rmult";
665 parse (rational_to_real c1);
667 let t2=ref (mkAppL [|parse "Rmult";
668 parse (rational_to_real c1);
670 List.iter (fun (h,c) ->
671 s:=(!s)||(h.hstrict);
672 t1:=(mkAppL [|parse "Rplus";
674 mkAppL [|parse "Rmult";
675 parse (rational_to_real c);
677 t2:=(mkAppL [|parse "Rplus";
679 mkAppL [|parse "Rmult";
680 parse (rational_to_real c);
683 let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
686 let tc=parse (rational_to_real cres) in
690 let tac1=ref (if h1.hstrict
691 then (tclTHENS (apply (parse "Rfourier_lt"))
694 (rational_to_fraction c1)])
695 else (tclTHENS (apply (parse "Rfourier_le"))
698 (rational_to_fraction c1)])) in
700 List.iter (fun (h,c)->
703 then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
706 (rational_to_fraction c)])
707 else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
710 (rational_to_fraction c)]))
712 then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
715 (rational_to_fraction c)])
716 else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
719 (rational_to_fraction c)])));
720 s:=(!s)||(h.hstrict))
723 then tac_zero_inf_false gl (rational_to_fraction cres)
724 else tac_zero_infeq_false gl (rational_to_fraction cres)
726 tac:=(tclTHENS (my_cut ineq)
727 [tclTHEN (change_in_concl
728 (mkAppL [| parse "not"; ineq|]
730 (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
731 else parse "Rnot_le_le"))
732 (tclTHENS (Equality.replace
733 (mkAppL [|parse "Rminus";!t2;!t1|]
737 (tclTHENS (Equality.replace (parse "(Rinv R1)")
740 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
745 (tclTHEN (apply (parse "sym_eqT"))
746 (apply (parse "Rinv_R1")))]
751 tac:=(tclTHENS (cut (parse "False"))
752 [tclTHEN intro contradiction;
754 |_-> assert false) |_-> assert false
756 ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
758 ((tclABSTRACT None !tac) gl)
762 let fourier_tac x gl =
766 let v_fourier = add_tactic "Fourier" fourier_tac
769 (*open CicReduction*)
770 (*open PrimitiveTactics*)
771 (*open ProofEngineTypes*)
772 let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;