helm/gTopLevel/fourierR.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   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.
   6  *
   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.
  11  *
  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.
  16  *
  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,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26
  27
  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.
  30 *)
  31
  32 (*open Term    // in coq/kernel
  33 open Tactics
  34 open Clenv
  35 open Names
  36 open Tacmach*)
  37 open Fourier
  38
  39 (******************************************************************************
  40 Operations on linear combinations.
  41
  42 Opérations sur les combinaisons linéaires affines.
  43 La partie homogène d'une combinaison linéaire est en fait une table de hash
  44 qui donne le coefficient d'un terme du calcul des constructions,
  45 qui est zéro si le terme n'y est pas.
  46 *)
  47
  48
  49
  50 (**
  51         The type for linear combinations
  52 *)
  53 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
  54 ;;
  55
  56 (**
  57         @return an empty flin
  58 *)
  59 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
  60 ;;
  61
  62 (**
  63         @param f a flin
  64         @param x a Cic.term
  65         @return the rational associated with x (coefficient)
  66 *)
  67 let flin_coef f x =
  68         try
  69                 (Hashtbl.find f.fhom x)
  70         with
  71                 _ -> r0
  72 ;;
  73
  74 (**
  75         Adds c to the coefficient of x
  76         @param f a flin
  77         @param x a Cic.term
  78         @param c a rational
  79         @return the new flin
  80 *)
  81 let flin_add f x c =
  82     let cx = flin_coef f x in
  83     Hashtbl.remove f.fhom x;
  84     Hashtbl.add f.fhom x (rplus cx c);
  85     f
  86 ;;
  87 (**
  88         Adds c to f.fcste
  89         @param f a flin
  90         @param c a rational
  91         @return the new flin
  92 *)
  93 let flin_add_cste f c =
  94     {fhom=f.fhom;
  95      fcste=rplus f.fcste c}
  96 ;;
  97
  98 (**
  99         @return a empty flin with r1 in fcste
 100 *)
 101 let flin_one () = flin_add_cste (flin_zero()) r1;;
 102
 103 (**
 104         Adds two flin
 105 *)
 106 let flin_plus f1 f2 =
 107     let f3 = flin_zero() in
 108     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
 109     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
 110     flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
 111 ;;
 112
 113 (**
 114         Substracts two flin
 115 *)
 116 let flin_minus f1 f2 =
 117     let f3 = flin_zero() in
 118     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
 119     Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
 120     flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
 121 ;;
 122
 123 (**
 124         @return f times a
 125 *)
 126 let flin_emult a f =
 127     let f2 = flin_zero() in
 128     Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
 129     flin_add_cste f2 (rmult a f.fcste);
 130 ;;
 131
 132
 133 (*****************************************************************************)
 134
 135 (*
 136
 137         no idea about helm parser ??????????????????????????????
 138
 139 let parse_ast   = Pcoq.parse_string Pcoq.Constr.constr;;
 140 let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
 141 let pf_parse_constr gl s =
 142    Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
 143 *)
 144
 145
 146 (**
 147         @param t a term
 148         @return proiection on string of t
 149 *)
 150 let rec string_of_term t =
 151  match t with
 152    Cic.Cast  (t1,t2) -> string_of_term t1
 153   |Cic.Const (u,boh) -> UriManager.string_of_uri u
 154   |Cic.Var       (u) -> UriManager.string_of_uri u
 155   | _ -> "not_of_constant"
 156 ;;
 157
 158 (* coq wrapper
 159 let string_of_constr = string_of_term
 160 ;;
 161 *)
 162
 163 (**
 164         @param t a term
 165         @raise Failure if conversion is impossible
 166         @return rational proiection of t
 167 *)
 168 let rec rational_of_term t =
 169   (* fun to apply f to the first and second rational-term of l *)
 170   let rat_of_binop f l =
 171         let a = List.hd l and
 172             b = List.hd(List.tl l) in
 173         f (rational_of_term a) (rational_of_term b)
 174   in
 175   (* as before, but f is unary *)
 176   let rat_of_unop f l =
 177         f (rational_of_term (List.hd l))
 178   in
 179   match t with
 180   | Cic.Cast (t1,t2) -> (rational_of_term t1)
 181   | Cic.Appl (t1::next) ->
 182         (match t1 with
 183            Cic.Const (u,boh) ->
 184                (match (UriManager.string_of_uri u) with
 185                  "cic:/Coq/Reals/Rdefinitions/Ropp" ->
 186                       rat_of_unop rop next
 187                 |"cic:/Coq/Reals/Rdefinitions/Rinv" ->
 188                       rat_of_unop rinv next
 189                 |"cic:/Coq/Reals/Rdefinitions/Rmult" ->
 190                       rat_of_binop rmult next
 191                 |"cic:/Coq/Reals/Rdefinitions/Rdiv" ->
 192                       rat_of_binop rdiv next
 193                 |"cic:/Coq/Reals/Rdefinitions/Rplus" ->
 194                       rat_of_binop rplus next
 195                 |"cic:/Coq/Reals/Rdefinitions/Rminus" ->
 196                       rat_of_binop rminus next
 197                 | _ -> failwith "not a rational")
 198           | _ -> failwith "not a rational")
 199   | Cic.Const (u,boh) ->
 200         (match (UriManager.string_of_uri u) with
 201                "cic:/Coq/Reals/Rdefinitions/R1" -> r1
 202               |"cic:/Coq/Reals/Rdefinitions/R0" -> r0
 203               |  _ -> failwith "not a rational")
 204   |  _ -> failwith "not a rational"
 205 ;;
 206
 207 (* coq wrapper
 208 let rational_of_const = rational_of_term;;
 209 *)
 210
 211
 212 let rec flin_of_term t =
 213         let fl_of_binop f l =
 214                 let a = List.hd l and
 215                     b = List.hd(List.tl l) in
 216                 f (flin_of_term a)  (flin_of_term b)
 217         in
 218   try(
 219     match t with
 220   | Cic.Cast (t1,t2) -> (flin_of_term t1)
 221   | Cic.Appl (t1::next) ->
 222         begin
 223         match t1 with
 224         Cic.Const (u,boh) ->
 225             begin
 226             match (UriManager.string_of_uri u) with
 227              "cic:/Coq/Reals/Rdefinitions/Ropp" ->
 228                   flin_emult (rop r1) (flin_of_term (List.hd next))
 229             |"cic:/Coq/Reals/Rdefinitions/Rplus"->
 230                   fl_of_binop flin_plus next
 231             |"cic:/Coq/Reals/Rdefinitions/Rminus"->
 232                   fl_of_binop flin_minus next
 233             |"cic:/Coq/Reals/Rdefinitions/Rmult"->
 234                 begin
 235                 let arg1 = (List.hd next) and
 236                     arg2 = (List.hd(List.tl next))
 237                 in
 238                 try
 239                         begin
 240                         let a = rational_of_term arg1 in
 241                         try
 242                                 begin
 243                                 let b = (rational_of_term arg2) in
 244                                 (flin_add_cste (flin_zero()) (rmult a b))
 245                                 end
 246                         with
 247                                 _ -> (flin_add (flin_zero()) arg2 a)
 248                         end
 249                 with
 250                         _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
 251                 end
 252             |"cic:/Coq/Reals/Rdefinitions/Rinv"->
 253                let a=(rational_of_term (List.hd next)) in
 254                flin_add_cste (flin_zero()) (rinv a)
 255             |"cic:/Coq/Reals/Rdefinitions/Rdiv"->
 256                 begin
 257                 let b=(rational_of_term (List.hd(List.tl next))) in
 258                 try
 259                         begin
 260                         let a = (rational_of_term (List.hd next)) in
 261                         (flin_add_cste (flin_zero()) (rdiv a b))
 262                         end
 263                 with
 264                         _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
 265                 end
 266             |_->assert false
 267             end
 268         |_ -> assert false
 269         end
 270   | Cic.Const (u,boh) ->
 271         begin
 272         match (UriManager.string_of_uri u) with
 273          "cic:/Coq/Reals/Rdefinitions/R1" -> flin_one ()
 274         |"cic:/Coq/Reals/Rdefinitions/R0" -> flin_zero ()
 275         |_-> assert false
 276         end
 277   |_-> assert false)
 278   with _ -> flin_add (flin_zero()) t r1
 279 ;;
 280
 281 (* coq wrapper
 282 let flin_of_constr = flin_of_term;;
 283 *)
 284
 285 (*
 286 let flin_to_alist f =
 287     let res=ref [] in
 288     Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
 289     !res
 290 ;;*)
 291
 292 (* Représentation des hypothèses qui sont des inéquations ou des équations.
 293 *)
 294 (*
 295 type hineq={hname:constr; (* le nom de l'hypothèse *)
 296             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
 297             hleft:constr;
 298             hright:constr;
 299             hflin:flin;
 300             hstrict:bool}
 301 ;;*)
 302
 303 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 304 *)
 305 (*let ineq1_of_constr (h,t) =
 306     match (kind_of_term t) with
 307        App (f,args) ->
 308          let t1= args.(0) in
 309          let t2= args.(1) in
 310          (match kind_of_term f with
 311            Const c ->
 312             (match (string_of_path c) with
 313                  "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h;
 314                            htype="Rlt";
 315                            hleft=t1;
 316                            hright=t2;
 317                            hflin= flin_minus (flin_of_constr t1)
 318                                              (flin_of_constr t2);
 319                            hstrict=true}]
 320                 |"Coq.Reals.Rdefinitions.Rgt" -> [{hname=h;
 321                            htype="Rgt";
 322                            hleft=t2;
 323                            hright=t1;
 324                            hflin= flin_minus (flin_of_constr t2)
 325                                              (flin_of_constr t1);
 326                            hstrict=true}]
 327                 |"Coq.Reals.Rdefinitions.Rle" -> [{hname=h;
 328                            htype="Rle";
 329                            hleft=t1;
 330                            hright=t2;
 331                            hflin= flin_minus (flin_of_constr t1)
 332                                              (flin_of_constr t2);
 333                            hstrict=false}]
 334                 |"Coq.Reals.Rdefinitions.Rge" -> [{hname=h;
 335                            htype="Rge";
 336                            hleft=t2;
 337                            hright=t1;
 338                            hflin= flin_minus (flin_of_constr t2)
 339                                              (flin_of_constr t1);
 340                            hstrict=false}]
 341                 |_->assert false)
 342           | Ind (sp,i) ->
 343               (match (string_of_path sp) with
 344                  "Coq.Init.Logic_Type.eqT" ->  let t0= args.(0) in
 345                            let t1= args.(1) in
 346                            let t2= args.(2) in
 347                     (match (kind_of_term t0) with
 348                          Const c ->
 349                            (match (string_of_path c) with
 350                               "Coq.Reals.Rdefinitions.R"->
 351                          [{hname=h;
 352                            htype="eqTLR";
 353                            hleft=t1;
 354                            hright=t2;
 355                            hflin= flin_minus (flin_of_constr t1)
 356                                              (flin_of_constr t2);
 357                            hstrict=false};
 358                           {hname=h;
 359                            htype="eqTRL";
 360                            hleft=t2;
 361                            hright=t1;
 362                            hflin= flin_minus (flin_of_constr t2)
 363                                              (flin_of_constr t1);
 364                            hstrict=false}]
 365                            |_-> assert false)
 366                          |_-> assert false)
 367                    |_-> assert false)
 368           |_-> assert false)
 369         |_-> assert false
 370 ;;*)
 371
 372 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 373 *)
 374
 375 (*let fourier_lineq lineq1 =
 376    let nvar=ref (-1) in
 377    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
 378    List.iter (fun f ->
 379                Hashtbl.iter (fun x c ->
 380                                  try (Hashtbl.find hvar x;())
 381                                  with _-> nvar:=(!nvar)+1;
 382                                           Hashtbl.add hvar x (!nvar))
 383                             f.hflin.fhom)
 384              lineq1;
 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)
 388                   h.hflin.fhom;
 389                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
 390              lineq1 in
 391    unsolvable sys
 392 ;;*)
 393
 394 (******************************************************************************
 395 Construction de la preuve en cas de succès de la méthode de Fourier,
 396 i.e. on obtient une contradiction.
 397 *)
 398
 399 (*let is_int x = (x.den)=1
 400 ;;*)
 401
 402 (* fraction = couple (num,den) *)
 403 (*let rec rational_to_fraction x= (x.num,x.den)
 404 ;;*)
 405
 406 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 407 *)
 408 (*let int_to_real n =
 409    let nn=abs n in
 410    let s=ref "" in
 411    if nn=0
 412    then s:="R0"
 413    else (s:="R1";
 414         for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
 415    if n<0 then s:="(Ropp "^(!s)^")";
 416    !s
 417 ;;*)
 418 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 419 *)
 420 (*let rational_to_real x =
 421    let (n,d)=rational_to_fraction x in
 422    ("(Rmult "^(int_to_real n)^" (Rinv "^(int_to_real d)^"))")
 423 ;;*)
 424
 425 (* preuve que 0<n*1/d
 426 *)
 427 (*let tac_zero_inf_pos gl (n,d) =
 428    let cste = pf_parse_constr gl in
 429    let tacn=ref (apply (cste "Rlt_zero_1")) in
 430    let tacd=ref (apply (cste "Rlt_zero_1")) in
 431    for i=1 to n-1 do
 432        tacn:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacn); done;
 433    for i=1 to d-1 do
 434        tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
 435    (tclTHENS (apply (cste "Rlt_mult_inv_pos")) [!tacn;!tacd])
 436 ;;*)
 437
 438 (* preuve que 0<=n*1/d
 439 *)
 440 (*let tac_zero_infeq_pos gl (n,d)=
 441    let cste = pf_parse_constr gl in
 442    let tacn=ref (if n=0
 443                  then (apply (cste "Rle_zero_zero"))
 444                  else (apply (cste "Rle_zero_1"))) in
 445    let tacd=ref (apply (cste "Rlt_zero_1")) in
 446    for i=1 to n-1 do
 447        tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
 448    for i=1 to d-1 do
 449        tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
 450    (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
 451 ;;*)
 452
 453 (* preuve que 0<(-n)*(1/d) => False
 454 *)
 455 (*let tac_zero_inf_false gl (n,d) =
 456    let cste = pf_parse_constr gl in
 457     if n=0 then (apply (cste "Rnot_lt0"))
 458     else
 459      (tclTHEN (apply (cste "Rle_not_lt"))
 460               (tac_zero_infeq_pos gl (-n,d)))
 461 ;;*)
 462
 463 (* preuve que 0<=(-n)*(1/d) => False
 464 *)
 465 (*let tac_zero_infeq_false gl (n,d) =
 466    let cste = pf_parse_constr gl in
 467      (tclTHEN (apply (cste "Rlt_not_le"))
 468               (tac_zero_inf_pos gl (-n,d)))
 469 ;;
 470
 471 let create_meta () = mkMeta(new_meta());;
 472
 473 let my_cut c gl=
 474      let concl = pf_concl gl in
 475        apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
 476 ;;
 477 let exact = exact_check;;
 478
 479 let tac_use h = match h.htype with
 480                "Rlt" -> exact h.hname
 481               |"Rle" -> exact h.hname
 482               |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
 483                                 (exact h.hname))
 484               |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
 485                                 (exact h.hname))
 486               |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
 487                                 (exact h.hname))
 488               |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
 489                                 (exact h.hname))
 490               |_->assert false
 491 ;;
 492
 493 let is_ineq (h,t) =
 494     match (kind_of_term t) with
 495        App (f,args) ->
 496          (match (string_of_constr f) with
 497                  "Coq.Reals.Rdefinitions.Rlt" -> true
 498                 |"Coq.Reals.Rdefinitions.Rgt" -> true
 499                 |"Coq.Reals.Rdefinitions.Rle" -> true
 500                 |"Coq.Reals.Rdefinitions.Rge" -> true
 501                 |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
 502                             "Coq.Reals.Rdefinitions.R"->true
 503                             |_->false)
 504                 |_->false)
 505      |_->false
 506 ;;
 507
 508 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 509
 510 let mkAppL a =
 511    let l = Array.to_list a in
 512    mkApp(List.hd l, Array.of_list (List.tl l))
 513 ;;*)
 514
 515 (* Résolution d'inéquations linéaires dans R *)
 516
 517 (*
 518 let rec fourier gl=
 519     let parse = pf_parse_constr gl in
 520     let goal = strip_outer_cast (pf_concl gl) in
 521     let fhyp=id_of_string "new_hyp_for_fourier" in
 522     (* si le but est une inéquation, on introduit son contraire,
 523        et le but à prouver devient False *)
 524     try (let tac =
 525      match (kind_of_term goal) with
 526       App (f,args) ->
 527       (match (string_of_constr f) with
 528              "Coq.Reals.Rdefinitions.Rlt" ->
 529                (tclTHEN
 530                  (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
 531                           (intro_using  fhyp))
 532                  fourier)
 533             |"Coq.Reals.Rdefinitions.Rle" ->
 534              (tclTHEN
 535               (tclTHEN (apply (parse "Rfourier_not_gt_le"))
 536                        (intro_using  fhyp))
 537                         fourier)
 538             |"Coq.Reals.Rdefinitions.Rgt" ->
 539              (tclTHEN
 540               (tclTHEN (apply (parse "Rfourier_not_le_gt"))
 541                        (intro_using  fhyp))
 542               fourier)
 543             |"Coq.Reals.Rdefinitions.Rge" ->
 544              (tclTHEN
 545               (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
 546                        (intro_using  fhyp))
 547               fourier)
 548             |_->assert false)
 549         |_->assert false
 550       in tac gl)
 551      with _ ->
 552 *)
 553     (* les hypothèses *)
 554
 555 (*
 556     let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
 557                         (list_of_sign (pf_hyps gl)) in
 558     let lineq =ref [] in
 559     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
 560                         with _-> ())
 561               hyps;
 562 *)
 563
 564     (* lineq = les inéquations découlant des hypothèses *)
 565
 566
 567 (*
 568     let res=fourier_lineq (!lineq) in
 569     let tac=ref tclIDTAC in
 570     if res=[]
 571     then (print_string "Tactic Fourier fails.\n";
 572                        flush stdout)
 573
 574 *)
 575     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
 576
 577 (*
 578     else (match res with
 579         [(cres,sres,lc)]->
 580 *)
 581     (* lc=coefficients multiplicateurs des inéquations
 582        qui donnent 0<cres ou 0<=cres selon sres *)
 583         (*print_string "Fourier's method can prove the goal...";flush stdout;*)
 584
 585
 586 (*
 587           let lutil=ref [] in
 588           List.iter
 589             (fun (h,c) ->
 590                           if c<>r0
 591                           then (lutil:=(h,c)::(!lutil)(*;
 592                                 print_rational(c);print_string " "*)))
 593                     (List.combine (!lineq) lc);
 594
 595 *)
 596        (* on construit la combinaison linéaire des inéquation *)
 597
 598 (*
 599              (match (!lutil) with
 600           (h1,c1)::lutil ->
 601           let s=ref (h1.hstrict) in
 602           let t1=ref (mkAppL [|parse "Rmult";
 603                           parse (rational_to_real c1);
 604                           h1.hleft|]) in
 605           let t2=ref (mkAppL [|parse "Rmult";
 606                           parse (rational_to_real c1);
 607                           h1.hright|]) in
 608           List.iter (fun (h,c) ->
 609                s:=(!s)||(h.hstrict);
 610                t1:=(mkAppL [|parse "Rplus";
 611                              !t1;
 612                              mkAppL [|parse "Rmult";
 613                                       parse (rational_to_real c);
 614                                       h.hleft|] |]);
 615                t2:=(mkAppL [|parse "Rplus";
 616                              !t2;
 617                              mkAppL [|parse "Rmult";
 618                                       parse (rational_to_real c);
 619                                       h.hright|] |]))
 620                lutil;
 621           let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
 622                               !t1;
 623                               !t2 |] in
 624            let tc=parse (rational_to_real cres) in
 625 *)
 626        (* puis sa preuve *)
 627 (*
 628            let tac1=ref (if h1.hstrict
 629                          then (tclTHENS (apply (parse "Rfourier_lt"))
 630                                  [tac_use h1;
 631                                   tac_zero_inf_pos  gl
 632                                       (rational_to_fraction c1)])
 633                          else (tclTHENS (apply (parse "Rfourier_le"))
 634                                  [tac_use h1;
 635                                   tac_zero_inf_pos  gl
 636                                       (rational_to_fraction c1)])) in
 637            s:=h1.hstrict;
 638            List.iter (fun (h,c)->
 639              (if (!s)
 640               then (if h.hstrict
 641                     then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
 642                                [!tac1;tac_use h;
 643                                 tac_zero_inf_pos  gl
 644                                       (rational_to_fraction c)])
 645                     else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
 646                                [!tac1;tac_use h;
 647                                 tac_zero_inf_pos  gl
 648                                       (rational_to_fraction c)]))
 649               else (if h.hstrict
 650                     then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
 651                                [!tac1;tac_use h;
 652                                 tac_zero_inf_pos  gl
 653                                       (rational_to_fraction c)])
 654                     else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
 655                                [!tac1;tac_use h;
 656                                 tac_zero_inf_pos  gl
 657                                       (rational_to_fraction c)])));
 658              s:=(!s)||(h.hstrict))
 659               lutil;
 660            let tac2= if sres
 661                       then tac_zero_inf_false gl (rational_to_fraction cres)
 662                       else tac_zero_infeq_false gl (rational_to_fraction cres)
 663            in
 664            tac:=(tclTHENS (my_cut ineq)
 665                      [tclTHEN (change_in_concl
 666                                (mkAppL [| parse "not"; ineq|]
 667                                        ))
 668                       (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
 669                                                else parse "Rnot_le_le"))
 670                             (tclTHENS (Equality.replace
 671                                        (mkAppL [|parse "Rminus";!t2;!t1|]
 672                                                )
 673                                        tc)
 674                                [tac2;
 675                                 (tclTHENS (Equality.replace (parse "(Rinv R1)")
 676                                                            (parse "R1"))
 677 *)
 678 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...    *)
 679 (*
 680                                 [tclORELSE
 681                                    (Ring.polynom [])
 682                                    tclIDTAC;
 683                                           (tclTHEN (apply (parse "sym_eqT"))
 684                                                 (apply (parse "Rinv_R1")))]
 685
 686                                          )
 687                                 ]));
 688                        !tac1]);
 689            tac:=(tclTHENS (cut (parse "False"))
 690                                   [tclTHEN intro contradiction;
 691                                    !tac])
 692       |_-> assert false) |_-> assert false
 693           );
 694     ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
 695       (!tac gl)
 696       ((tclABSTRACT None !tac) gl)
 697
 698 ;;
 699
 700 let fourier_tac x gl =
 701      fourier gl
 702 ;;
 703
 704 let v_fourier = add_tactic "Fourier" fourier_tac
 705 *)
 706
 707 (*open CicReduction*)
 708 (*open PrimitiveTactics*)
 709 (*open ProofEngineTypes*)
 710 let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;
 711