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.con" ->
 186                       rat_of_unop rop next
 187                 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
 188                       rat_of_unop rinv next
 189                 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
 190                       rat_of_binop rmult next
 191                 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
 192                       rat_of_binop rdiv next
 193                 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
 194                       rat_of_binop rplus next
 195                 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
 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.con" -> r1
 202               |"cic:/Coq/Reals/Rdefinitions/R0.con" -> 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.con" ->
 228                   flin_emult (rop r1) (flin_of_term (List.hd next))
 229             |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
 230                   fl_of_binop flin_plus next
 231             |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
 232                   fl_of_binop flin_minus next
 233             |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
 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.con"->
 253                let a=(rational_of_term (List.hd next)) in
 254                flin_add_cste (flin_zero()) (rinv a)
 255             |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
 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.con" -> flin_one ()
 274         |"cic:/Coq/Reals/Rdefinitions/R0.con" -> 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         Translates a flin to (c,x) list
 287         @param f a flin
 288         @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
 289 *)
 290 let flin_to_alist f =
 291     let res=ref [] in
 292     Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
 293     !res
 294 ;;
 295
 296 (* Représentation des hypothèses qui sont des inéquations ou des équations.
 297 *)
 298
 299 (**
 300         The structure for ineq
 301 *)
 302 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
 303             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
 304             hleft:Cic.term;
 305             hright:Cic.term;
 306             hflin:flin;
 307             hstrict:bool}
 308 ;;
 309
 310 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 311 *)
 312
 313 let ineq1_of_term (h,t) =
 314     match t with
 315        Cic.Appl (t1::next) ->
 316          let arg1= List.hd next in
 317          let arg2= List.hd(List.tl next) in
 318          (match t1 with
 319            Cic.Const (u,boh) ->
 320             (match UriManager.string_of_uri u with
 321                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
 322                            htype="Rlt";
 323                            hleft=arg1;
 324                            hright=arg2;
 325                            hflin= flin_minus (flin_of_term arg1)
 326                                              (flin_of_term arg2);
 327                            hstrict=true}]
 328                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h;
 329                            htype="Rgt";
 330                            hleft=arg2;
 331                            hright=arg1;
 332                            hflin= flin_minus (flin_of_term arg2)
 333                                              (flin_of_term arg1);
 334                            hstrict=true}]
 335                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h;
 336                            htype="Rle";
 337                            hleft=arg1;
 338                            hright=arg2;
 339                            hflin= flin_minus (flin_of_term arg1)
 340                                              (flin_of_term arg2);
 341                            hstrict=false}]
 342                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h;
 343                            htype="Rge";
 344                            hleft=arg2;
 345                            hright=arg1;
 346                            hflin= flin_minus (flin_of_term arg2)
 347                                              (flin_of_term arg1);
 348                            hstrict=false}]
 349                 |_->assert false)
 350           | Cic.MutInd (u,i,o) ->
 351               (match UriManager.string_of_uri u with
 352                  "cic:/Coq/Init/Logic_Type/eqT.con" ->
 353                            let t0= arg1 in
 354                            let arg1= arg2 in
 355                            let arg2= List.hd(List.tl (List.tl next)) in
 356                     (match t0 with
 357                          Cic.Const (u,boh) ->
 358                            (match UriManager.string_of_uri u with
 359                               "cic:/Coq/Reals/Rdefinitions/R.con"->
 360                          [{hname=h;
 361                            htype="eqTLR";
 362                            hleft=arg1;
 363                            hright=arg2;
 364                            hflin= flin_minus (flin_of_term arg1)
 365                                              (flin_of_term arg2);
 366                            hstrict=false};
 367                           {hname=h;
 368                            htype="eqTRL";
 369                            hleft=arg2;
 370                            hright=arg1;
 371                            hflin= flin_minus (flin_of_term arg2)
 372                                              (flin_of_term arg1);
 373                            hstrict=false}]
 374                            |_-> assert false)
 375                          |_-> assert false)
 376                    |_-> assert false)
 377           |_-> assert false)
 378         |_-> assert false
 379 ;;
 380 (* coq wrapper
 381 let ineq1_of_constr = ineq1_of_term;;
 382 *)
 383
 384 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 385 *)
 386
 387 let fourier_lineq lineq1 =
 388    let nvar=ref (-1) in
 389    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
 390    List.iter (fun f ->
 391                Hashtbl.iter (fun x c ->
 392                                  try (Hashtbl.find hvar x;())
 393                                  with _-> nvar:=(!nvar)+1;
 394                                           Hashtbl.add hvar x (!nvar))
 395                             f.hflin.fhom)
 396              lineq1;
 397    let sys= List.map (fun h->
 398                let v=Array.create ((!nvar)+1) r0 in
 399                Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
 400                   h.hflin.fhom;
 401                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
 402              lineq1 in
 403    unsolvable sys
 404 ;;
 405
 406 (******************************************************************************
 407 Construction de la preuve en cas de succès de la méthode de Fourier,
 408 i.e. on obtient une contradiction.
 409 *)
 410
 411 let is_int x = (x.den)=1
 412 ;;
 413
 414 (* fraction = couple (num,den) *)
 415 let rec rational_to_fraction x= (x.num,x.den)
 416 ;;
 417
 418 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 419 *)
 420 let int_to_real n =
 421    let nn=abs n in
 422    let s=ref "" in
 423    if nn=0
 424    then s:="R0"
 425    else (s:="R1";
 426         for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
 427    if n<0 then s:="(Ropp "^(!s)^")";
 428    !s
 429 ;;
 430
 431 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 432 *)
 433 let rational_to_real x =
 434    let (n,d)=rational_to_fraction x in
 435    ("(Rmult "^(int_to_real n)^" (Rinv "^(int_to_real d)^"))")
 436 ;;
 437
 438 (* preuve que 0<n*1/d
 439 *)
 440 (*let tac_zero_inf_pos gl (n,d) =
 441    let cste = pf_parse_constr gl in
 442    let tacn=ref (apply (cste "Rlt_zero_1")) in
 443    let tacd=ref (apply (cste "Rlt_zero_1")) in
 444    for i=1 to n-1 do
 445        tacn:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacn); done;
 446    for i=1 to d-1 do
 447        tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
 448    (tclTHENS (apply (cste "Rlt_mult_inv_pos")) [!tacn;!tacd])
 449 ;;*)
 450
 451 (* preuve que 0<=n*1/d
 452 *)
 453 (*let tac_zero_infeq_pos gl (n,d)=
 454    let cste = pf_parse_constr gl in
 455    let tacn=ref (if n=0
 456                  then (apply (cste "Rle_zero_zero"))
 457                  else (apply (cste "Rle_zero_1"))) in
 458    let tacd=ref (apply (cste "Rlt_zero_1")) in
 459    for i=1 to n-1 do
 460        tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
 461    for i=1 to d-1 do
 462        tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
 463    (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
 464 ;;*)
 465
 466 (* preuve que 0<(-n)*(1/d) => False
 467 *)
 468 (*let tac_zero_inf_false gl (n,d) =
 469    let cste = pf_parse_constr gl in
 470     if n=0 then (apply (cste "Rnot_lt0"))
 471     else
 472      (tclTHEN (apply (cste "Rle_not_lt"))
 473               (tac_zero_infeq_pos gl (-n,d)))
 474 ;;*)
 475
 476 (* preuve que 0<=(-n)*(1/d) => False
 477 *)
 478 (*let tac_zero_infeq_false gl (n,d) =
 479    let cste = pf_parse_constr gl in
 480      (tclTHEN (apply (cste "Rlt_not_le"))
 481               (tac_zero_inf_pos gl (-n,d)))
 482 ;;
 483
 484 let create_meta () = mkMeta(new_meta());;
 485
 486 let my_cut c gl=
 487      let concl = pf_concl gl in
 488        apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
 489 ;;
 490 let exact = exact_check;;
 491
 492 let tac_use h = match h.htype with
 493                "Rlt" -> exact h.hname
 494               |"Rle" -> exact h.hname
 495               |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
 496                                 (exact h.hname))
 497               |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
 498                                 (exact h.hname))
 499               |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
 500                                 (exact h.hname))
 501               |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
 502                                 (exact h.hname))
 503               |_->assert false
 504 ;;
 505
 506 let is_ineq (h,t) =
 507     match (kind_of_term t) with
 508        App (f,args) ->
 509          (match (string_of_constr f) with
 510                  "Coq.Reals.Rdefinitions.Rlt" -> true
 511                 |"Coq.Reals.Rdefinitions.Rgt" -> true
 512                 |"Coq.Reals.Rdefinitions.Rle" -> true
 513                 |"Coq.Reals.Rdefinitions.Rge" -> true
 514                 |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
 515                             "Coq.Reals.Rdefinitions.R"->true
 516                             |_->false)
 517                 |_->false)
 518      |_->false
 519 ;;
 520
 521 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 522
 523 let mkAppL a =
 524    let l = Array.to_list a in
 525    mkApp(List.hd l, Array.of_list (List.tl l))
 526 ;;*)
 527
 528 (* Résolution d'inéquations linéaires dans R *)
 529
 530 (*
 531 let rec fourier gl=
 532     let parse = pf_parse_constr gl in
 533     let goal = strip_outer_cast (pf_concl gl) in
 534     let fhyp=id_of_string "new_hyp_for_fourier" in
 535     (* si le but est une inéquation, on introduit son contraire,
 536        et le but à prouver devient False *)
 537     try (let tac =
 538      match (kind_of_term goal) with
 539       App (f,args) ->
 540       (match (string_of_constr f) with
 541              "Coq.Reals.Rdefinitions.Rlt" ->
 542                (tclTHEN
 543                  (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
 544                           (intro_using  fhyp))
 545                  fourier)
 546             |"Coq.Reals.Rdefinitions.Rle" ->
 547              (tclTHEN
 548               (tclTHEN (apply (parse "Rfourier_not_gt_le"))
 549                        (intro_using  fhyp))
 550                         fourier)
 551             |"Coq.Reals.Rdefinitions.Rgt" ->
 552              (tclTHEN
 553               (tclTHEN (apply (parse "Rfourier_not_le_gt"))
 554                        (intro_using  fhyp))
 555               fourier)
 556             |"Coq.Reals.Rdefinitions.Rge" ->
 557              (tclTHEN
 558               (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
 559                        (intro_using  fhyp))
 560               fourier)
 561             |_->assert false)
 562         |_->assert false
 563       in tac gl)
 564      with _ ->
 565 *)
 566     (* les hypothèses *)
 567
 568 (*
 569     let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
 570                         (list_of_sign (pf_hyps gl)) in
 571     let lineq =ref [] in
 572     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
 573                         with _-> ())
 574               hyps;
 575 *)
 576
 577     (* lineq = les inéquations découlant des hypothèses *)
 578
 579
 580 (*
 581     let res=fourier_lineq (!lineq) in
 582     let tac=ref tclIDTAC in
 583     if res=[]
 584     then (print_string "Tactic Fourier fails.\n";
 585                        flush stdout)
 586
 587 *)
 588     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
 589
 590 (*
 591     else (match res with
 592         [(cres,sres,lc)]->
 593 *)
 594     (* lc=coefficients multiplicateurs des inéquations
 595        qui donnent 0<cres ou 0<=cres selon sres *)
 596         (*print_string "Fourier's method can prove the goal...";flush stdout;*)
 597
 598
 599 (*
 600           let lutil=ref [] in
 601           List.iter
 602             (fun (h,c) ->
 603                           if c<>r0
 604                           then (lutil:=(h,c)::(!lutil)(*;
 605                                 print_rational(c);print_string " "*)))
 606                     (List.combine (!lineq) lc);
 607
 608 *)
 609        (* on construit la combinaison linéaire des inéquation *)
 610
 611 (*
 612              (match (!lutil) with
 613           (h1,c1)::lutil ->
 614           let s=ref (h1.hstrict) in
 615           let t1=ref (mkAppL [|parse "Rmult";
 616                           parse (rational_to_real c1);
 617                           h1.hleft|]) in
 618           let t2=ref (mkAppL [|parse "Rmult";
 619                           parse (rational_to_real c1);
 620                           h1.hright|]) in
 621           List.iter (fun (h,c) ->
 622                s:=(!s)||(h.hstrict);
 623                t1:=(mkAppL [|parse "Rplus";
 624                              !t1;
 625                              mkAppL [|parse "Rmult";
 626                                       parse (rational_to_real c);
 627                                       h.hleft|] |]);
 628                t2:=(mkAppL [|parse "Rplus";
 629                              !t2;
 630                              mkAppL [|parse "Rmult";
 631                                       parse (rational_to_real c);
 632                                       h.hright|] |]))
 633                lutil;
 634           let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
 635                               !t1;
 636                               !t2 |] in
 637            let tc=parse (rational_to_real cres) in
 638 *)
 639        (* puis sa preuve *)
 640 (*
 641            let tac1=ref (if h1.hstrict
 642                          then (tclTHENS (apply (parse "Rfourier_lt"))
 643                                  [tac_use h1;
 644                                   tac_zero_inf_pos  gl
 645                                       (rational_to_fraction c1)])
 646                          else (tclTHENS (apply (parse "Rfourier_le"))
 647                                  [tac_use h1;
 648                                   tac_zero_inf_pos  gl
 649                                       (rational_to_fraction c1)])) in
 650            s:=h1.hstrict;
 651            List.iter (fun (h,c)->
 652              (if (!s)
 653               then (if h.hstrict
 654                     then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
 655                                [!tac1;tac_use h;
 656                                 tac_zero_inf_pos  gl
 657                                       (rational_to_fraction c)])
 658                     else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
 659                                [!tac1;tac_use h;
 660                                 tac_zero_inf_pos  gl
 661                                       (rational_to_fraction c)]))
 662               else (if h.hstrict
 663                     then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
 664                                [!tac1;tac_use h;
 665                                 tac_zero_inf_pos  gl
 666                                       (rational_to_fraction c)])
 667                     else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
 668                                [!tac1;tac_use h;
 669                                 tac_zero_inf_pos  gl
 670                                       (rational_to_fraction c)])));
 671              s:=(!s)||(h.hstrict))
 672               lutil;
 673            let tac2= if sres
 674                       then tac_zero_inf_false gl (rational_to_fraction cres)
 675                       else tac_zero_infeq_false gl (rational_to_fraction cres)
 676            in
 677            tac:=(tclTHENS (my_cut ineq)
 678                      [tclTHEN (change_in_concl
 679                                (mkAppL [| parse "not"; ineq|]
 680                                        ))
 681                       (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
 682                                                else parse "Rnot_le_le"))
 683                             (tclTHENS (Equality.replace
 684                                        (mkAppL [|parse "Rminus";!t2;!t1|]
 685                                                )
 686                                        tc)
 687                                [tac2;
 688                                 (tclTHENS (Equality.replace (parse "(Rinv R1)")
 689                                                            (parse "R1"))
 690 *)
 691 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...    *)
 692 (*
 693                                 [tclORELSE
 694                                    (Ring.polynom [])
 695                                    tclIDTAC;
 696                                           (tclTHEN (apply (parse "sym_eqT"))
 697                                                 (apply (parse "Rinv_R1")))]
 698
 699                                          )
 700                                 ]));
 701                        !tac1]);
 702            tac:=(tclTHENS (cut (parse "False"))
 703                                   [tclTHEN intro contradiction;
 704                                    !tac])
 705       |_-> assert false) |_-> assert false
 706           );
 707     ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
 708       (!tac gl)
 709       ((tclABSTRACT None !tac) gl)
 710
 711 ;;
 712
 713 let fourier_tac x gl =
 714      fourier gl
 715 ;;
 716
 717 let v_fourier = add_tactic "Fourier" fourier_tac
 718 *)
 719
 720 (*open CicReduction*)
 721 (*open PrimitiveTactics*)
 722 (*open ProofEngineTypes*)
 723 let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;
 724