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 tac_zero_inf_pos gl (n,d) =
 465    (*let cste = pf_parse_constr gl in*)
 466    let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 467    let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 468    for i=1 to n-1 do
 469        tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
 470    for i=1 to d-1 do
 471        tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
 472    (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
 473 ;;
 474
 475 (* preuve que 0<=n*1/d
 476 *)
 477 (*let tac_zero_infeq_pos gl (n,d)=
 478    let cste = pf_parse_constr gl in
 479    let tacn=ref (if n=0
 480                  then (apply (cste "Rle_zero_zero"))
 481                  else (apply (cste "Rle_zero_1"))) in
 482    let tacd=ref (apply (cste "Rlt_zero_1")) in
 483    for i=1 to n-1 do
 484        tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
 485    for i=1 to d-1 do
 486        tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
 487    (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
 488 ;;*)
 489
 490 (* preuve que 0<(-n)*(1/d) => False
 491 *)
 492 (*let tac_zero_inf_false gl (n,d) =
 493    let cste = pf_parse_constr gl in
 494     if n=0 then (apply (cste "Rnot_lt0"))
 495     else
 496      (tclTHEN (apply (cste "Rle_not_lt"))
 497               (tac_zero_infeq_pos gl (-n,d)))
 498 ;;*)
 499
 500 (* preuve que 0<=(-n)*(1/d) => False
 501 *)
 502 (*let tac_zero_infeq_false gl (n,d) =
 503    let cste = pf_parse_constr gl in
 504      (tclTHEN (apply (cste "Rlt_not_le"))
 505               (tac_zero_inf_pos gl (-n,d)))
 506 ;;
 507
 508 let create_meta () = mkMeta(new_meta());;
 509
 510 let my_cut c gl=
 511      let concl = pf_concl gl in
 512        apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
 513 ;;
 514 let exact = exact_check;;
 515
 516 let tac_use h = match h.htype with
 517                "Rlt" -> exact h.hname
 518               |"Rle" -> exact h.hname
 519               |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
 520                                 (exact h.hname))
 521               |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
 522                                 (exact h.hname))
 523               |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
 524                                 (exact h.hname))
 525               |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
 526                                 (exact h.hname))
 527               |_->assert false
 528 ;;
 529
 530 let is_ineq (h,t) =
 531     match (kind_of_term t) with
 532        App (f,args) ->
 533          (match (string_of_constr f) with
 534                  "Coq.Reals.Rdefinitions.Rlt" -> true
 535                 |"Coq.Reals.Rdefinitions.Rgt" -> true
 536                 |"Coq.Reals.Rdefinitions.Rle" -> true
 537                 |"Coq.Reals.Rdefinitions.Rge" -> true
 538                 |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
 539                             "Coq.Reals.Rdefinitions.R"->true
 540                             |_->false)
 541                 |_->false)
 542      |_->false
 543 ;;
 544
 545 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 546
 547 let mkAppL a =
 548    let l = Array.to_list a in
 549    mkApp(List.hd l, Array.of_list (List.tl l))
 550 ;;*)
 551
 552 (* Résolution d'inéquations linéaires dans R *)
 553
 554 (*
 555 let rec fourier gl=
 556     let parse = pf_parse_constr gl in
 557     let goal = strip_outer_cast (pf_concl gl) in
 558     let fhyp=id_of_string "new_hyp_for_fourier" in
 559     (* si le but est une inéquation, on introduit son contraire,
 560        et le but à prouver devient False *)
 561     try (let tac =
 562      match (kind_of_term goal) with
 563       App (f,args) ->
 564       (match (string_of_constr f) with
 565              "Coq.Reals.Rdefinitions.Rlt" ->
 566                (tclTHEN
 567                  (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
 568                           (intro_using  fhyp))
 569                  fourier)
 570             |"Coq.Reals.Rdefinitions.Rle" ->
 571              (tclTHEN
 572               (tclTHEN (apply (parse "Rfourier_not_gt_le"))
 573                        (intro_using  fhyp))
 574                         fourier)
 575             |"Coq.Reals.Rdefinitions.Rgt" ->
 576              (tclTHEN
 577               (tclTHEN (apply (parse "Rfourier_not_le_gt"))
 578                        (intro_using  fhyp))
 579               fourier)
 580             |"Coq.Reals.Rdefinitions.Rge" ->
 581              (tclTHEN
 582               (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
 583                        (intro_using  fhyp))
 584               fourier)
 585             |_->assert false)
 586         |_->assert false
 587       in tac gl)
 588      with _ ->
 589 *)
 590     (* les hypothèses *)
 591
 592 (*
 593     let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
 594                         (list_of_sign (pf_hyps gl)) in
 595     let lineq =ref [] in
 596     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
 597                         with _-> ())
 598               hyps;
 599 *)
 600
 601     (* lineq = les inéquations découlant des hypothèses *)
 602
 603
 604 (*
 605     let res=fourier_lineq (!lineq) in
 606     let tac=ref tclIDTAC in
 607     if res=[]
 608     then (print_string "Tactic Fourier fails.\n";
 609                        flush stdout)
 610
 611 *)
 612     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
 613
 614 (*
 615     else (match res with
 616         [(cres,sres,lc)]->
 617 *)
 618     (* lc=coefficients multiplicateurs des inéquations
 619        qui donnent 0<cres ou 0<=cres selon sres *)
 620         (*print_string "Fourier's method can prove the goal...";flush stdout;*)
 621
 622
 623 (*
 624           let lutil=ref [] in
 625           List.iter
 626             (fun (h,c) ->
 627                           if c<>r0
 628                           then (lutil:=(h,c)::(!lutil)(*;
 629                                 print_rational(c);print_string " "*)))
 630                     (List.combine (!lineq) lc);
 631
 632 *)
 633        (* on construit la combinaison linéaire des inéquation *)
 634
 635 (*
 636              (match (!lutil) with
 637           (h1,c1)::lutil ->
 638           let s=ref (h1.hstrict) in
 639           let t1=ref (mkAppL [|parse "Rmult";
 640                           parse (rational_to_real c1);
 641                           h1.hleft|]) in
 642           let t2=ref (mkAppL [|parse "Rmult";
 643                           parse (rational_to_real c1);
 644                           h1.hright|]) in
 645           List.iter (fun (h,c) ->
 646                s:=(!s)||(h.hstrict);
 647                t1:=(mkAppL [|parse "Rplus";
 648                              !t1;
 649                              mkAppL [|parse "Rmult";
 650                                       parse (rational_to_real c);
 651                                       h.hleft|] |]);
 652                t2:=(mkAppL [|parse "Rplus";
 653                              !t2;
 654                              mkAppL [|parse "Rmult";
 655                                       parse (rational_to_real c);
 656                                       h.hright|] |]))
 657                lutil;
 658           let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
 659                               !t1;
 660                               !t2 |] in
 661            let tc=parse (rational_to_real cres) in
 662 *)
 663        (* puis sa preuve *)
 664 (*
 665            let tac1=ref (if h1.hstrict
 666                          then (tclTHENS (apply (parse "Rfourier_lt"))
 667                                  [tac_use h1;
 668                                   tac_zero_inf_pos  gl
 669                                       (rational_to_fraction c1)])
 670                          else (tclTHENS (apply (parse "Rfourier_le"))
 671                                  [tac_use h1;
 672                                   tac_zero_inf_pos  gl
 673                                       (rational_to_fraction c1)])) in
 674            s:=h1.hstrict;
 675            List.iter (fun (h,c)->
 676              (if (!s)
 677               then (if h.hstrict
 678                     then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
 679                                [!tac1;tac_use h;
 680                                 tac_zero_inf_pos  gl
 681                                       (rational_to_fraction c)])
 682                     else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
 683                                [!tac1;tac_use h;
 684                                 tac_zero_inf_pos  gl
 685                                       (rational_to_fraction c)]))
 686               else (if h.hstrict
 687                     then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
 688                                [!tac1;tac_use h;
 689                                 tac_zero_inf_pos  gl
 690                                       (rational_to_fraction c)])
 691                     else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
 692                                [!tac1;tac_use h;
 693                                 tac_zero_inf_pos  gl
 694                                       (rational_to_fraction c)])));
 695              s:=(!s)||(h.hstrict))
 696               lutil;
 697            let tac2= if sres
 698                       then tac_zero_inf_false gl (rational_to_fraction cres)
 699                       else tac_zero_infeq_false gl (rational_to_fraction cres)
 700            in
 701            tac:=(tclTHENS (my_cut ineq)
 702                      [tclTHEN (change_in_concl
 703                                (mkAppL [| parse "not"; ineq|]
 704                                        ))
 705                       (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
 706                                                else parse "Rnot_le_le"))
 707                             (tclTHENS (Equality.replace
 708                                        (mkAppL [|parse "Rminus";!t2;!t1|]
 709                                                )
 710                                        tc)
 711                                [tac2;
 712                                 (tclTHENS (Equality.replace (parse "(Rinv R1)")
 713                                                            (parse "R1"))
 714 *)
 715 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...    *)
 716 (*
 717                                 [tclORELSE
 718                                    (Ring.polynom [])
 719                                    tclIDTAC;
 720                                           (tclTHEN (apply (parse "sym_eqT"))
 721                                                 (apply (parse "Rinv_R1")))]
 722
 723                                          )
 724                                 ]));
 725                        !tac1]);
 726            tac:=(tclTHENS (cut (parse "False"))
 727                                   [tclTHEN intro contradiction;
 728                                    !tac])
 729       |_-> assert false) |_-> assert false
 730           );
 731     ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
 732       (!tac gl)
 733       ((tclABSTRACT None !tac) gl)
 734
 735 ;;
 736
 737 let fourier_tac x gl =
 738      fourier gl
 739 ;;
 740
 741 let v_fourier = add_tactic "Fourier" fourier_tac
 742 *)
 743
 744 (*open CicReduction*)
 745 (*open PrimitiveTactics*)
 746 (*open ProofEngineTypes*)
 747 let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;
 748