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         @param t a term
 138         @return proiection on string of t
 139 *)
 140 let rec string_of_term t =
 141  match t with
 142    Cic.Cast  (t1,t2) -> string_of_term t1
 143   |Cic.Const (u,boh) -> UriManager.string_of_uri u
 144   |Cic.Var       (u) -> UriManager.string_of_uri u
 145   | _ -> "not_of_constant"
 146 ;;
 147
 148 (* coq wrapper
 149 let string_of_constr = string_of_term
 150 ;;
 151 *)
 152
 153 (**
 154         @param t a term
 155         @raise Failure if conversion is impossible
 156         @return rational proiection of t
 157 *)
 158 let rec rational_of_term t =
 159   (* fun to apply f to the first and second rational-term of l *)
 160   let rat_of_binop f l =
 161         let a = List.hd l and
 162             b = List.hd(List.tl l) in
 163         f (rational_of_term a) (rational_of_term b)
 164   in
 165   (* as before, but f is unary *)
 166   let rat_of_unop f l =
 167         f (rational_of_term (List.hd l))
 168   in
 169   match t with
 170   | Cic.Cast (t1,t2) -> (rational_of_term t1)
 171   | Cic.Appl (t1::next) ->
 172         (match t1 with
 173            Cic.Const (u,boh) ->
 174                (match (UriManager.string_of_uri u) with
 175                  "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
 176                       rat_of_unop rop next
 177                 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
 178                       rat_of_unop rinv next
 179                 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
 180                       rat_of_binop rmult next
 181                 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
 182                       rat_of_binop rdiv next
 183                 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
 184                       rat_of_binop rplus next
 185                 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
 186                       rat_of_binop rminus next
 187                 | _ -> failwith "not a rational")
 188           | _ -> failwith "not a rational")
 189   | Cic.Const (u,boh) ->
 190         (match (UriManager.string_of_uri u) with
 191                "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
 192               |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
 193               |  _ -> failwith "not a rational")
 194   |  _ -> failwith "not a rational"
 195 ;;
 196
 197 (* coq wrapper
 198 let rational_of_const = rational_of_term;;
 199 *)
 200
 201
 202 let rec flin_of_term t =
 203         let fl_of_binop f l =
 204                 let a = List.hd l and
 205                     b = List.hd(List.tl l) in
 206                 f (flin_of_term a)  (flin_of_term b)
 207         in
 208   try(
 209     match t with
 210   | Cic.Cast (t1,t2) -> (flin_of_term t1)
 211   | Cic.Appl (t1::next) ->
 212         begin
 213         match t1 with
 214         Cic.Const (u,boh) ->
 215             begin
 216             match (UriManager.string_of_uri u) with
 217              "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
 218                   flin_emult (rop r1) (flin_of_term (List.hd next))
 219             |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
 220                   fl_of_binop flin_plus next
 221             |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
 222                   fl_of_binop flin_minus next
 223             |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
 224                 begin
 225                 let arg1 = (List.hd next) and
 226                     arg2 = (List.hd(List.tl next))
 227                 in
 228                 try
 229                         begin
 230                         let a = rational_of_term arg1 in
 231                         try
 232                                 begin
 233                                 let b = (rational_of_term arg2) in
 234                                 (flin_add_cste (flin_zero()) (rmult a b))
 235                                 end
 236                         with
 237                                 _ -> (flin_add (flin_zero()) arg2 a)
 238                         end
 239                 with
 240                         _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
 241                 end
 242             |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
 243                let a=(rational_of_term (List.hd next)) in
 244                flin_add_cste (flin_zero()) (rinv a)
 245             |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
 246                 begin
 247                 let b=(rational_of_term (List.hd(List.tl next))) in
 248                 try
 249                         begin
 250                         let a = (rational_of_term (List.hd next)) in
 251                         (flin_add_cste (flin_zero()) (rdiv a b))
 252                         end
 253                 with
 254                         _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
 255                 end
 256             |_->assert false
 257             end
 258         |_ -> assert false
 259         end
 260   | Cic.Const (u,boh) ->
 261         begin
 262         match (UriManager.string_of_uri u) with
 263          "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
 264         |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
 265         |_-> assert false
 266         end
 267   |_-> assert false)
 268   with _ -> flin_add (flin_zero()) t r1
 269 ;;
 270
 271 (* coq wrapper
 272 let flin_of_constr = flin_of_term;;
 273 *)
 274
 275 (**
 276         Translates a flin to (c,x) list
 277         @param f a flin
 278         @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
 279 *)
 280 let flin_to_alist f =
 281     let res=ref [] in
 282     Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
 283     !res
 284 ;;
 285
 286 (* Représentation des hypothèses qui sont des inéquations ou des équations.
 287 *)
 288
 289 (**
 290         The structure for ineq
 291 *)
 292 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
 293             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
 294             hleft:Cic.term;
 295             hright:Cic.term;
 296             hflin:flin;
 297             hstrict:bool}
 298 ;;
 299
 300 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 301 *)
 302
 303 let ineq1_of_term (h,t) =
 304     match t with
 305        Cic.Appl (t1::next) ->
 306          let arg1= List.hd next in
 307          let arg2= List.hd(List.tl next) in
 308          (match t1 with
 309            Cic.Const (u,boh) ->
 310             (match UriManager.string_of_uri u with
 311                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
 312                            htype="Rlt";
 313                            hleft=arg1;
 314                            hright=arg2;
 315                            hflin= flin_minus (flin_of_term arg1)
 316                                              (flin_of_term arg2);
 317                            hstrict=true}]
 318                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h;
 319                            htype="Rgt";
 320                            hleft=arg2;
 321                            hright=arg1;
 322                            hflin= flin_minus (flin_of_term arg2)
 323                                              (flin_of_term arg1);
 324                            hstrict=true}]
 325                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h;
 326                            htype="Rle";
 327                            hleft=arg1;
 328                            hright=arg2;
 329                            hflin= flin_minus (flin_of_term arg1)
 330                                              (flin_of_term arg2);
 331                            hstrict=false}]
 332                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h;
 333                            htype="Rge";
 334                            hleft=arg2;
 335                            hright=arg1;
 336                            hflin= flin_minus (flin_of_term arg2)
 337                                              (flin_of_term arg1);
 338                            hstrict=false}]
 339                 |_->assert false)
 340           | Cic.MutInd (u,i,o) ->
 341               (match UriManager.string_of_uri u with
 342                  "cic:/Coq/Init/Logic_Type/eqT.con" ->
 343                            let t0= arg1 in
 344                            let arg1= arg2 in
 345                            let arg2= List.hd(List.tl (List.tl next)) in
 346                     (match t0 with
 347                          Cic.Const (u,boh) ->
 348                            (match UriManager.string_of_uri u with
 349                               "cic:/Coq/Reals/Rdefinitions/R.con"->
 350                          [{hname=h;
 351                            htype="eqTLR";
 352                            hleft=arg1;
 353                            hright=arg2;
 354                            hflin= flin_minus (flin_of_term arg1)
 355                                              (flin_of_term arg2);
 356                            hstrict=false};
 357                           {hname=h;
 358                            htype="eqTRL";
 359                            hleft=arg2;
 360                            hright=arg1;
 361                            hflin= flin_minus (flin_of_term arg2)
 362                                              (flin_of_term arg1);
 363                            hstrict=false}]
 364                            |_-> assert false)
 365                          |_-> assert false)
 366                    |_-> assert false)
 367           |_-> assert false)
 368         |_-> assert false
 369 ;;
 370 (* coq wrapper
 371 let ineq1_of_constr = ineq1_of_term;;
 372 *)
 373
 374 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 375 *)
 376
 377 let fourier_lineq lineq1 =
 378    let nvar=ref (-1) in
 379    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
 380    List.iter (fun f ->
 381                Hashtbl.iter (fun x c ->
 382                                  try (Hashtbl.find hvar x;())
 383                                  with _-> nvar:=(!nvar)+1;
 384                                           Hashtbl.add hvar x (!nvar))
 385                             f.hflin.fhom)
 386              lineq1;
 387    let sys= List.map (fun h->
 388                let v=Array.create ((!nvar)+1) r0 in
 389                Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
 390                   h.hflin.fhom;
 391                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
 392              lineq1 in
 393    unsolvable sys
 394 ;;
 395
 396 (******************************************************************************
 397 Construction de la preuve en cas de succès de la méthode de Fourier,
 398 i.e. on obtient une contradiction.
 399 *)
 400
 401 let is_int x = (x.den)=1
 402 ;;
 403
 404 (* fraction = couple (num,den) *)
 405 let rec rational_to_fraction x= (x.num,x.den)
 406 ;;
 407
 408 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 409 *)
 410 (*et int_to_real n =
 411    let nn=abs n in
 412    let s=ref Cic.term
 413    if nn=0
 414    then s:="R0"
 415    else (s:="R1";
 416         for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
 417    if n<0 then s:="(Ropp "^(!s)^")";
 418    !s
 419 ;;*)
 420 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
 421
 422 let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
 423 let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
 424 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
 425
 426
 427 let rec int_to_real_aux n =
 428   match n with
 429     0 -> _R0 (* o forse R0 + R0 ????? *)
 430   | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
 431 ;;
 432
 433
 434 let int_to_real n =
 435    let x = int_to_real_aux (abs n) in
 436    if n < 0 then
 437         Cic.Appl [ _Ropp ; x ]
 438    else
 439         x
 440 ;;
 441
 442
 443 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 444 *)
 445 let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
 446 let _Rinv  = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
 447
 448
 449 let rational_to_real x =
 450    let (n,d)=rational_to_fraction x in
 451    Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ]  ]
 452 ;;
 453
 454 (* preuve que 0<n*1/d
 455 *)
 456
 457 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
 458
 459 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
 460
 461 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
 462
 463
 464 let tcl_then ~start ~continuation ~status =
 465    let tcl_then_aux (proof,goals) goal =
 466       let (newproof,newgoals) = continuation ~status:(proof,goal) in
 467       (newproof, goals @ newgoals)
 468    in
 469    let (proof,new_goals) = start ~status in
 470    List.fold_left tcl_then_aux (proof,[]) new_goals
 471 ;;
 472
 473 let tac_zero_inf_pos gl (n,d) =
 474    (*let cste = pf_parse_constr gl in*)
 475    let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 476    let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 477    for i=1 to n-1 do
 478        tacn:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
 479    for i=1 to d-1 do
 480        tacd:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
 481    (Ring.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
 482 ;;
 483
 484 (* preuve que 0<=n*1/d
 485 *)
 486 (*let tac_zero_infeq_pos gl (n,d)=
 487    let cste = pf_parse_constr gl in
 488    let tacn=ref (if n=0
 489                  then (apply (cste "Rle_zero_zero"))
 490                  else (apply (cste "Rle_zero_1"))) in
 491    let tacd=ref (apply (cste "Rlt_zero_1")) in
 492    for i=1 to n-1 do
 493        tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
 494    for i=1 to d-1 do
 495        tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
 496    (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
 497 ;;*)
 498
 499 (* preuve que 0<(-n)*(1/d) => False
 500 *)
 501 (*let tac_zero_inf_false gl (n,d) =
 502    let cste = pf_parse_constr gl in
 503     if n=0 then (apply (cste "Rnot_lt0"))
 504     else
 505      (tclTHEN (apply (cste "Rle_not_lt"))
 506               (tac_zero_infeq_pos gl (-n,d)))
 507 ;;*)
 508
 509 (* preuve que 0<=(-n)*(1/d) => False
 510 *)
 511 (*let tac_zero_infeq_false gl (n,d) =
 512    let cste = pf_parse_constr gl in
 513      (tclTHEN (apply (cste "Rlt_not_le"))
 514               (tac_zero_inf_pos gl (-n,d)))
 515 ;;
 516
 517 let create_meta () = mkMeta(new_meta());;
 518
 519 let my_cut c gl=
 520      let concl = pf_concl gl in
 521        apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
 522 ;;
 523 let exact = exact_check;;
 524
 525 let tac_use h = match h.htype with
 526                "Rlt" -> exact h.hname
 527               |"Rle" -> exact h.hname
 528               |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
 529                                 (exact h.hname))
 530               |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
 531                                 (exact h.hname))
 532               |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
 533                                 (exact h.hname))
 534               |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
 535                                 (exact h.hname))
 536               |_->assert false
 537 ;;
 538
 539 let is_ineq (h,t) =
 540     match (kind_of_term t) with
 541        App (f,args) ->
 542          (match (string_of_constr f) with
 543                  "Coq.Reals.Rdefinitions.Rlt" -> true
 544                 |"Coq.Reals.Rdefinitions.Rgt" -> true
 545                 |"Coq.Reals.Rdefinitions.Rle" -> true
 546                 |"Coq.Reals.Rdefinitions.Rge" -> true
 547                 |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
 548                             "Coq.Reals.Rdefinitions.R"->true
 549                             |_->false)
 550                 |_->false)
 551      |_->false
 552 ;;
 553
 554 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 555
 556 let mkAppL a =
 557    let l = Array.to_list a in
 558    mkApp(List.hd l, Array.of_list (List.tl l))
 559 ;;*)
 560
 561 (* Résolution d'inéquations linéaires dans R *)
 562
 563 (*
 564 let rec fourier gl=
 565     let parse = pf_parse_constr gl in
 566     let goal = strip_outer_cast (pf_concl gl) in
 567     let fhyp=id_of_string "new_hyp_for_fourier" in
 568     (* si le but est une inéquation, on introduit son contraire,
 569        et le but à prouver devient False *)
 570     try (let tac =
 571      match (kind_of_term goal) with
 572       App (f,args) ->
 573       (match (string_of_constr f) with
 574              "Coq.Reals.Rdefinitions.Rlt" ->
 575                (tclTHEN
 576                  (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
 577                           (intro_using  fhyp))
 578                  fourier)
 579             |"Coq.Reals.Rdefinitions.Rle" ->
 580              (tclTHEN
 581               (tclTHEN (apply (parse "Rfourier_not_gt_le"))
 582                        (intro_using  fhyp))
 583                         fourier)
 584             |"Coq.Reals.Rdefinitions.Rgt" ->
 585              (tclTHEN
 586               (tclTHEN (apply (parse "Rfourier_not_le_gt"))
 587                        (intro_using  fhyp))
 588               fourier)
 589             |"Coq.Reals.Rdefinitions.Rge" ->
 590              (tclTHEN
 591               (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
 592                        (intro_using  fhyp))
 593               fourier)
 594             |_->assert false)
 595         |_->assert false
 596       in tac gl)
 597      with _ ->
 598 *)
 599     (* les hypothèses *)
 600
 601 (*
 602     let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
 603                         (list_of_sign (pf_hyps gl)) in
 604     let lineq =ref [] in
 605     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
 606                         with _-> ())
 607               hyps;
 608 *)
 609
 610     (* lineq = les inéquations découlant des hypothèses *)
 611
 612
 613 (*
 614     let res=fourier_lineq (!lineq) in
 615     let tac=ref tclIDTAC in
 616     if res=[]
 617     then (print_string "Tactic Fourier fails.\n";
 618                        flush stdout)
 619
 620 *)
 621     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
 622
 623 (*
 624     else (match res with
 625         [(cres,sres,lc)]->
 626 *)
 627     (* lc=coefficients multiplicateurs des inéquations
 628        qui donnent 0<cres ou 0<=cres selon sres *)
 629         (*print_string "Fourier's method can prove the goal...";flush stdout;*)
 630
 631
 632 (*
 633           let lutil=ref [] in
 634           List.iter
 635             (fun (h,c) ->
 636                           if c<>r0
 637                           then (lutil:=(h,c)::(!lutil)(*;
 638                                 print_rational(c);print_string " "*)))
 639                     (List.combine (!lineq) lc);
 640
 641 *)
 642        (* on construit la combinaison linéaire des inéquation *)
 643
 644 (*
 645              (match (!lutil) with
 646           (h1,c1)::lutil ->
 647           let s=ref (h1.hstrict) in
 648           let t1=ref (mkAppL [|parse "Rmult";
 649                           parse (rational_to_real c1);
 650                           h1.hleft|]) in
 651           let t2=ref (mkAppL [|parse "Rmult";
 652                           parse (rational_to_real c1);
 653                           h1.hright|]) in
 654           List.iter (fun (h,c) ->
 655                s:=(!s)||(h.hstrict);
 656                t1:=(mkAppL [|parse "Rplus";
 657                              !t1;
 658                              mkAppL [|parse "Rmult";
 659                                       parse (rational_to_real c);
 660                                       h.hleft|] |]);
 661                t2:=(mkAppL [|parse "Rplus";
 662                              !t2;
 663                              mkAppL [|parse "Rmult";
 664                                       parse (rational_to_real c);
 665                                       h.hright|] |]))
 666                lutil;
 667           let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
 668                               !t1;
 669                               !t2 |] in
 670            let tc=parse (rational_to_real cres) in
 671 *)
 672        (* puis sa preuve *)
 673 (*
 674            let tac1=ref (if h1.hstrict
 675                          then (tclTHENS (apply (parse "Rfourier_lt"))
 676                                  [tac_use h1;
 677                                   tac_zero_inf_pos  gl
 678                                       (rational_to_fraction c1)])
 679                          else (tclTHENS (apply (parse "Rfourier_le"))
 680                                  [tac_use h1;
 681                                   tac_zero_inf_pos  gl
 682                                       (rational_to_fraction c1)])) in
 683            s:=h1.hstrict;
 684            List.iter (fun (h,c)->
 685              (if (!s)
 686               then (if h.hstrict
 687                     then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
 688                                [!tac1;tac_use h;
 689                                 tac_zero_inf_pos  gl
 690                                       (rational_to_fraction c)])
 691                     else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
 692                                [!tac1;tac_use h;
 693                                 tac_zero_inf_pos  gl
 694                                       (rational_to_fraction c)]))
 695               else (if h.hstrict
 696                     then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
 697                                [!tac1;tac_use h;
 698                                 tac_zero_inf_pos  gl
 699                                       (rational_to_fraction c)])
 700                     else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
 701                                [!tac1;tac_use h;
 702                                 tac_zero_inf_pos  gl
 703                                       (rational_to_fraction c)])));
 704              s:=(!s)||(h.hstrict))
 705               lutil;
 706            let tac2= if sres
 707                       then tac_zero_inf_false gl (rational_to_fraction cres)
 708                       else tac_zero_infeq_false gl (rational_to_fraction cres)
 709            in
 710            tac:=(tclTHENS (my_cut ineq)
 711                      [tclTHEN (change_in_concl
 712                                (mkAppL [| parse "not"; ineq|]
 713                                        ))
 714                       (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
 715                                                else parse "Rnot_le_le"))
 716                             (tclTHENS (Equality.replace
 717                                        (mkAppL [|parse "Rminus";!t2;!t1|]
 718                                                )
 719                                        tc)
 720                                [tac2;
 721                                 (tclTHENS (Equality.replace (parse "(Rinv R1)")
 722                                                            (parse "R1"))
 723 *)
 724 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...    *)
 725 (*
 726                                 [tclORELSE
 727                                    (Ring.polynom [])
 728                                    tclIDTAC;
 729                                           (tclTHEN (apply (parse "sym_eqT"))
 730                                                 (apply (parse "Rinv_R1")))]
 731
 732                                          )
 733                                 ]));
 734                        !tac1]);
 735            tac:=(tclTHENS (cut (parse "False"))
 736                                   [tclTHEN intro contradiction;
 737                                    !tac])
 738       |_-> assert false) |_-> assert false
 739           );
 740     ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
 741       (!tac gl)
 742       ((tclABSTRACT None !tac) gl)
 743
 744 ;;
 745
 746 let fourier_tac x gl =
 747      fourier gl
 748 ;;
 749
 750 let v_fourier = add_tactic "Fourier" fourier_tac
 751 *)
 752
 753 (*open CicReduction*)
 754 (*open PrimitiveTactics*)
 755 (*open ProofEngineTypes*)
 756 let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;
 757