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 Fourier
  33
  34
  35 let debug x = print_string x ; flush stdout;;
  36
  37 (******************************************************************************
  38 Operations on linear combinations.
  39
  40 Opérations sur les combinaisons linéaires affines.
  41 La partie homogène d'une combinaison linéaire est en fait une table de hash
  42 qui donne le coefficient d'un terme du calcul des constructions,
  43 qui est zéro si le terme n'y est pas.
  44 *)
  45
  46
  47
  48 (**
  49         The type for linear combinations
  50 *)
  51 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
  52 ;;
  53
  54 (**
  55         @return an empty flin
  56 *)
  57 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
  58 ;;
  59
  60 (**
  61         @param f a flin
  62         @param x a Cic.term
  63         @return the rational associated with x (coefficient)
  64 *)
  65 let flin_coef f x =
  66         try
  67                 (Hashtbl.find f.fhom x)
  68         with
  69                 _ -> r0
  70 ;;
  71
  72 (**
  73         Adds c to the coefficient of x
  74         @param f a flin
  75         @param x a Cic.term
  76         @param c a rational
  77         @return the new flin
  78 *)
  79 let flin_add f x c =
  80     let cx = flin_coef f x in
  81     Hashtbl.remove f.fhom x;
  82     Hashtbl.add f.fhom x (rplus cx c);
  83     f
  84 ;;
  85 (**
  86         Adds c to f.fcste
  87         @param f a flin
  88         @param c a rational
  89         @return the new flin
  90 *)
  91 let flin_add_cste f c =
  92     {fhom=f.fhom;
  93      fcste=rplus f.fcste c}
  94 ;;
  95
  96 (**
  97         @return a empty flin with r1 in fcste
  98 *)
  99 let flin_one () = flin_add_cste (flin_zero()) r1;;
 100
 101 (**
 102         Adds two flin
 103 *)
 104 let flin_plus f1 f2 =
 105     let f3 = flin_zero() in
 106     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
 107     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
 108     flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
 109 ;;
 110
 111 (**
 112         Substracts two flin
 113 *)
 114 let flin_minus f1 f2 =
 115     let f3 = flin_zero() in
 116     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
 117     Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
 118     flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
 119 ;;
 120
 121 (**
 122         @return f times a
 123 *)
 124 let flin_emult a f =
 125     let f2 = flin_zero() in
 126     Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
 127     flin_add_cste f2 (rmult a f.fcste);
 128 ;;
 129
 130
 131 (*****************************************************************************)
 132
 133
 134 (**
 135         @param t a term
 136         @return proiection on string of t
 137 *)
 138 let rec string_of_term t =
 139  match t with
 140    Cic.Cast  (t1,t2) -> string_of_term t1
 141   |Cic.Const (u,boh) -> UriManager.string_of_uri u
 142   |Cic.Var       (u) -> UriManager.string_of_uri u
 143   | _ -> "not_of_constant"
 144 ;;
 145
 146 (* coq wrapper
 147 let string_of_constr = string_of_term
 148 ;;
 149 *)
 150
 151 (**
 152         @param t a term
 153         @raise Failure if conversion is impossible
 154         @return rational proiection of t
 155 *)
 156 let rec rational_of_term t =
 157   (* fun to apply f to the first and second rational-term of l *)
 158   let rat_of_binop f l =
 159         let a = List.hd l and
 160             b = List.hd(List.tl l) in
 161         f (rational_of_term a) (rational_of_term b)
 162   in
 163   (* as before, but f is unary *)
 164   let rat_of_unop f l =
 165         f (rational_of_term (List.hd l))
 166   in
 167   match t with
 168   | Cic.Cast (t1,t2) -> (rational_of_term t1)
 169   | Cic.Appl (t1::next) ->
 170         (match t1 with
 171            Cic.Const (u,boh) ->
 172                (match (UriManager.string_of_uri u) with
 173                  "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
 174                       rat_of_unop rop next
 175                 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
 176                       rat_of_unop rinv next
 177                 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
 178                       rat_of_binop rmult next
 179                 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
 180                       rat_of_binop rdiv next
 181                 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
 182                       rat_of_binop rplus next
 183                 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
 184                       rat_of_binop rminus next
 185                 | _ -> failwith "not a rational")
 186           | _ -> failwith "not a rational")
 187   | Cic.Const (u,boh) ->
 188         (match (UriManager.string_of_uri u) with
 189                "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
 190               |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
 191               |  _ -> failwith "not a rational")
 192   |  _ -> failwith "not a rational"
 193 ;;
 194
 195 (* coq wrapper
 196 let rational_of_const = rational_of_term;;
 197 *)
 198
 199
 200 let rec flin_of_term t =
 201         let fl_of_binop f l =
 202                 let a = List.hd l and
 203                     b = List.hd(List.tl l) in
 204                 f (flin_of_term a)  (flin_of_term b)
 205         in
 206   try(
 207     match t with
 208   | Cic.Cast (t1,t2) -> (flin_of_term t1)
 209   | Cic.Appl (t1::next) ->
 210         begin
 211         match t1 with
 212         Cic.Const (u,boh) ->
 213             begin
 214             match (UriManager.string_of_uri u) with
 215              "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
 216                   flin_emult (rop r1) (flin_of_term (List.hd next))
 217             |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
 218                   fl_of_binop flin_plus next
 219             |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
 220                   fl_of_binop flin_minus next
 221             |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
 222                 begin
 223                 let arg1 = (List.hd next) and
 224                     arg2 = (List.hd(List.tl next))
 225                 in
 226                 try
 227                         begin
 228                         let a = rational_of_term arg1 in
 229                         try
 230                                 begin
 231                                 let b = (rational_of_term arg2) in
 232                                 (flin_add_cste (flin_zero()) (rmult a b))
 233                                 end
 234                         with
 235                                 _ -> (flin_add (flin_zero()) arg2 a)
 236                         end
 237                 with
 238                         _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
 239                 end
 240             |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
 241                let a=(rational_of_term (List.hd next)) in
 242                flin_add_cste (flin_zero()) (rinv a)
 243             |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
 244                 begin
 245                 let b=(rational_of_term (List.hd(List.tl next))) in
 246                 try
 247                         begin
 248                         let a = (rational_of_term (List.hd next)) in
 249                         (flin_add_cste (flin_zero()) (rdiv a b))
 250                         end
 251                 with
 252                         _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
 253                 end
 254             |_->assert false
 255             end
 256         |_ -> assert false
 257         end
 258   | Cic.Const (u,boh) ->
 259         begin
 260         match (UriManager.string_of_uri u) with
 261          "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
 262         |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
 263         |_-> assert false
 264         end
 265   |_-> assert false)
 266   with _ -> flin_add (flin_zero()) t r1
 267 ;;
 268
 269 (* coq wrapper
 270 let flin_of_constr = flin_of_term;;
 271 *)
 272
 273 (**
 274         Translates a flin to (c,x) list
 275         @param f a flin
 276         @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
 277 *)
 278 let flin_to_alist f =
 279     let res=ref [] in
 280     Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
 281     !res
 282 ;;
 283
 284 (* Représentation des hypothèses qui sont des inéquations ou des équations.
 285 *)
 286
 287 (**
 288         The structure for ineq
 289 *)
 290 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
 291             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
 292             hleft:Cic.term;
 293             hright:Cic.term;
 294             hflin:flin;
 295             hstrict:bool}
 296 ;;
 297
 298 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 299 *)
 300
 301 let ineq1_of_term (h,t) =
 302     match t with
 303        Cic.Appl (t1::next) ->
 304          let arg1= List.hd next in
 305          let arg2= List.hd(List.tl next) in
 306          (match t1 with
 307            Cic.Const (u,boh) ->
 308             (match UriManager.string_of_uri u with
 309                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
 310                            htype="Rlt";
 311                            hleft=arg1;
 312                            hright=arg2;
 313                            hflin= flin_minus (flin_of_term arg1)
 314                                              (flin_of_term arg2);
 315                            hstrict=true}]
 316                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h;
 317                            htype="Rgt";
 318                            hleft=arg2;
 319                            hright=arg1;
 320                            hflin= flin_minus (flin_of_term arg2)
 321                                              (flin_of_term arg1);
 322                            hstrict=true}]
 323                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h;
 324                            htype="Rle";
 325                            hleft=arg1;
 326                            hright=arg2;
 327                            hflin= flin_minus (flin_of_term arg1)
 328                                              (flin_of_term arg2);
 329                            hstrict=false}]
 330                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h;
 331                            htype="Rge";
 332                            hleft=arg2;
 333                            hright=arg1;
 334                            hflin= flin_minus (flin_of_term arg2)
 335                                              (flin_of_term arg1);
 336                            hstrict=false}]
 337                 |_->assert false)
 338           | Cic.MutInd (u,i,o) ->
 339               (match UriManager.string_of_uri u with
 340                  "cic:/Coq/Init/Logic_Type/eqT.con" ->
 341                            let t0= arg1 in
 342                            let arg1= arg2 in
 343                            let arg2= List.hd(List.tl (List.tl next)) in
 344                     (match t0 with
 345                          Cic.Const (u,boh) ->
 346                            (match UriManager.string_of_uri u with
 347                               "cic:/Coq/Reals/Rdefinitions/R.con"->
 348                          [{hname=h;
 349                            htype="eqTLR";
 350                            hleft=arg1;
 351                            hright=arg2;
 352                            hflin= flin_minus (flin_of_term arg1)
 353                                              (flin_of_term arg2);
 354                            hstrict=false};
 355                           {hname=h;
 356                            htype="eqTRL";
 357                            hleft=arg2;
 358                            hright=arg1;
 359                            hflin= flin_minus (flin_of_term arg2)
 360                                              (flin_of_term arg1);
 361                            hstrict=false}]
 362                            |_-> assert false)
 363                          |_-> assert false)
 364                    |_-> assert false)
 365           |_-> assert false)
 366         |_-> assert false
 367 ;;
 368 (* coq wrapper
 369 let ineq1_of_constr = ineq1_of_term;;
 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    debug ("chiamo unsolvable sul sistema di "^ string_of_int (List.length sys) ^"\n");
 392    unsolvable sys
 393 ;;
 394
 395 (******************************************************************************
 396 Construction de la preuve en cas de succès de la méthode de Fourier,
 397 i.e. on obtient une contradiction.
 398 *)
 399
 400 let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
 401 let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
 402 let _Rinv  = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
 403 let _Rle_mult_inv_pos =  Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
 404 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
 405 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
 406 let _Rle_zero_pos_plus1 =  Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
 407 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
 408 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
 409 let _Rlt_not_le =  Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
 410 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
 411 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
 412 let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
 413 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
 414 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
 415 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
 416 let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
 417 let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
 418 let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
 419 let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
 420 let _Rfourier_gt_to_lt  =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
 421
 422 let _Rfourier_ge_to_le  =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
 423
 424 let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
 425
 426 let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
 427
 428
 429 let is_int x = (x.den)=1
 430 ;;
 431
 432 (* fraction = couple (num,den) *)
 433 let rec rational_to_fraction x= (x.num,x.den)
 434 ;;
 435
 436 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 437 *)
 438
 439 let rec int_to_real_aux n =
 440   match n with
 441     0 -> _R0 (* o forse R0 + R0 ????? *)
 442   | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
 443 ;;
 444
 445
 446 let int_to_real n =
 447    let x = int_to_real_aux (abs n) in
 448    if n < 0 then
 449         Cic.Appl [ _Ropp ; x ]
 450    else
 451         x
 452 ;;
 453
 454
 455 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 456 *)
 457
 458 let rational_to_real x =
 459    let (n,d)=rational_to_fraction x in
 460    Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ]  ]
 461 ;;
 462
 463 (* preuve que 0<n*1/d
 464 *)
 465
 466 let tac_zero_inf_pos gl (n,d) =
 467    (*let cste = pf_parse_constr gl in*)
 468    let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 469    let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 470    for i=1 to n-1 do
 471        tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
 472    for i=1 to d-1 do
 473        tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
 474    (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
 475 ;;
 476
 477 (* preuve que 0<=n*1/d
 478 *)
 479
 480 let tac_zero_infeq_pos gl (n,d) =
 481    (*let cste = pf_parse_constr gl in*)
 482    let tacn = ref (if n=0 then
 483         (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
 484         else
 485         (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ))
 486    in
 487    let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 488    for i=1 to n-1 do
 489        tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); done;
 490    for i=1 to d-1 do
 491        tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
 492    (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd])
 493 ;;
 494
 495
 496
 497 (* preuve que 0<(-n)*(1/d) => False
 498 *)
 499
 500 let tac_zero_inf_false gl (n,d) =
 501     if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0)
 502     else
 503      (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt)
 504               ~continuation:(tac_zero_infeq_pos gl (-n,d)))
 505 ;;
 506
 507 (* preuve que 0<=(-n)*(1/d) => False
 508 *)
 509
 510 let tac_zero_infeq_false gl (n,d) =
 511      (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
 512               ~continuation:(tac_zero_inf_pos gl (-n,d)))
 513 ;;
 514
 515
 516 (* *********** ********** ******** ??????????????? *********** **************
 517
 518 let mkMeta proof  = Cic.Meta (ProofEngineHelpers.new_meta proof) (ProofEngineHelpers.identity_relocation_list_for_metavariable []);;
 519
 520 let apply_type_tac t al (proof,goals) =
 521    let new_m = mkMeta proof in
 522    PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast new_m t)::al))
 523 ;;
 524
 525
 526
 527
 528 let create_meta () = mkMeta(new_meta());;
 529
 530 let my_cut c gl=
 531      let concl = pf_concl gl in
 532        apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
 533 ;;
 534
 535 *********** * ********************************* ***************************** *)
 536
 537 let exact = PrimitiveTactics.exact_tac;;
 538
 539 let tac_use h = match h.htype with
 540                "Rlt" -> exact ~term:h.hname
 541               |"Rle" -> exact ~term:h.hname
 542               |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
 543                                 ~continuation:(exact ~term:h.hname))
 544               |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
 545                                 ~continuation:(exact ~term:h.hname))
 546               |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
 547                                 ~continuation:(exact ~term:h.hname))
 548               |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
 549                                 ~continuation:(exact ~term:h.hname))
 550               |_->assert false
 551 ;;
 552
 553
 554
 555 let is_ineq (h,t) =
 556     match t with
 557        Cic.Appl ( Cic.Const(u,boh)::next) ->
 558          (match (UriManager.string_of_uri u) with
 559                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
 560                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
 561                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
 562                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
 563                 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
 564                    (match (List.hd next) with
 565                        Cic.Const (uri,_) when
 566                         UriManager.string_of_uri uri =
 567                         "cic:/Coq/Reals/Rdefinitions/R.con" -> true
 568                      | _ -> false)
 569                 |_->false)
 570      |_->false
 571 ;;
 572
 573 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 574
 575 let mkAppL a =
 576    Cic.Appl(Array.to_list a)
 577 ;;
 578
 579 (* Résolution d'inéquations linéaires dans R *)
 580 let rec strip_outer_cast c = match c with
 581   | Cic.Cast (c,_) -> strip_outer_cast c
 582   | _ -> c
 583 ;;
 584
 585 let find_in_context id context =
 586   let rec find_in_context_aux c n =
 587         match c with
 588         [] -> failwith (id^" not found in context")
 589         | a::next -> (match a with
 590                         Some (Cic.Name(name),Cic.Decl(t)) when name = id -> n
 591                         | _ -> find_in_context_aux next (n+1))
 592   in find_in_context_aux context 1 (*?? bisogna invertire il contesto? ??*)
 593 ;;
 594
 595 (* mi sembra quadratico *)
 596 let rec filter_real_hyp context =
 597   match context with
 598   [] -> []
 599   | Some(Cic.Name(h),Cic.Def(t))::next -> [(Cic.Rel(find_in_context h next),t)] @
 600                                                 filter_real_hyp next
 601   | a::next -> filter_real_hyp next
 602 ;;
 603
 604
 605
 606 (* se pf_concl estrae la concl*)
 607 let rec fourier ~status:(proof,goal)=
 608         debug ("invoco fourier_tac sul goal"^string_of_int(goal)^"\n");
 609         let curi,metasenv,pbo,pty = proof in
 610         let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 611
 612         (* il goal di prima dovrebbe essere ty
 613         let goal = strip_outer_cast (pf_concl gl) in*)
 614
 615         let fhyp = String.copy "new_hyp_for_fourier" in
 616     (* si le but est une inéquation, on introduit son contraire,
 617        et le but à prouver devient False *)
 618
 619     try (let tac =
 620      match ty with
 621       Cic.Appl ( Cic.Const(u,boh)::args) ->
 622       (match UriManager.string_of_uri u with
 623              "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
 624              (Tacticals.then_
 625               ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_ge_lt)
 626                         ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
 627                          ~continuation:fourier)
 628             |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
 629              (Tacticals.then_
 630               ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_gt_le)
 631                        ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
 632                         ~continuation:fourier)
 633             |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
 634              (Tacticals.then_
 635               ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_le_gt)
 636                        ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
 637                         ~continuation:fourier)
 638             |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
 639              (Tacticals.then_
 640               ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_lt_ge)
 641                        ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
 642                         ~continuation:fourier)
 643             |_->assert false)
 644         |_->assert false
 645       in tac (proof,goal) )
 646      with _ ->
 647
 648     (* les hypothèses *)
 649
 650
 651     (* ? fix if None  ?????*)
 652     debug ("estraggo hp da context "^ string_of_int(List.length context)^"\n");
 653     let hyps = filter_real_hyp context in
 654     debug ("trasformo in eq "^ string_of_int (List.length hyps)^"\n");
 655     let lineq =ref [] in
 656     List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
 657                         with _-> ())
 658               hyps;
 659
 660
 661     (* lineq = les inéquations découlant des hypothèses *)
 662
 663     debug ("applico fourier a "^ string_of_int (List.length !lineq)^"\n");
 664
 665     let res=fourier_lineq (!lineq) in
 666     (*let tac=ref tclIDTAC in*)
 667     if res=[]
 668     then (print_string "Tactic Fourier fails.\n";
 669                        flush stdout)
 670 ;debug "fine\n";
 671 ;(proof,[goal])
 672 ;;
 673     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
 674
 675 (*
 676     else (match res with
 677         [(cres,sres,lc)]->
 678 *)
 679     (* lc=coefficients multiplicateurs des inéquations
 680        qui donnent 0<cres ou 0<=cres selon sres *)
 681         (*print_string "Fourier's method can prove the goal...";flush stdout;*)
 682
 683
 684 (*
 685           let lutil=ref [] in
 686           List.iter
 687             (fun (h,c) ->
 688                           if c<>r0
 689                           then (lutil:=(h,c)::(!lutil)(*;
 690                                 print_rational(c);print_string " "*)))
 691                     (List.combine (!lineq) lc);
 692
 693 *)
 694        (* on construit la combinaison linéaire des inéquation *)
 695
 696 (*
 697              (match (!lutil) with
 698           (h1,c1)::lutil ->
 699           let s=ref (h1.hstrict) in
 700           let t1=ref (mkAppL [|parse "Rmult";
 701                           parse (rational_to_real c1);
 702                           h1.hleft|]) in
 703           let t2=ref (mkAppL [|parse "Rmult";
 704                           parse (rational_to_real c1);
 705                           h1.hright|]) in
 706           List.iter (fun (h,c) ->
 707                s:=(!s)||(h.hstrict);
 708                t1:=(mkAppL [|parse "Rplus";
 709                              !t1;
 710                              mkAppL [|parse "Rmult";
 711                                       parse (rational_to_real c);
 712                                       h.hleft|] |]);
 713                t2:=(mkAppL [|parse "Rplus";
 714                              !t2;
 715                              mkAppL [|parse "Rmult";
 716                                       parse (rational_to_real c);
 717                                       h.hright|] |]))
 718                lutil;
 719           let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
 720                               !t1;
 721                               !t2 |] in
 722            let tc=parse (rational_to_real cres) in
 723 *)
 724        (* puis sa preuve *)
 725 (*
 726            let tac1=ref (if h1.hstrict
 727                          then (tclTHENS (apply (parse "Rfourier_lt"))
 728                                  [tac_use h1;
 729                                   tac_zero_inf_pos  gl
 730                                       (rational_to_fraction c1)])
 731                          else (tclTHENS (apply (parse "Rfourier_le"))
 732                                  [tac_use h1;
 733                                   tac_zero_inf_pos  gl
 734                                       (rational_to_fraction c1)])) in
 735            s:=h1.hstrict;
 736            List.iter (fun (h,c)->
 737              (if (!s)
 738               then (if h.hstrict
 739                     then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
 740                                [!tac1;tac_use h;
 741                                 tac_zero_inf_pos  gl
 742                                       (rational_to_fraction c)])
 743                     else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
 744                                [!tac1;tac_use h;
 745                                 tac_zero_inf_pos  gl
 746                                       (rational_to_fraction c)]))
 747               else (if h.hstrict
 748                     then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
 749                                [!tac1;tac_use h;
 750                                 tac_zero_inf_pos  gl
 751                                       (rational_to_fraction c)])
 752                     else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
 753                                [!tac1;tac_use h;
 754                                 tac_zero_inf_pos  gl
 755                                       (rational_to_fraction c)])));
 756              s:=(!s)||(h.hstrict))
 757               lutil;
 758            let tac2= if sres
 759                       then tac_zero_inf_false gl (rational_to_fraction cres)
 760                       else tac_zero_infeq_false gl (rational_to_fraction cres)
 761            in
 762            tac:=(tclTHENS (my_cut ineq)
 763                      [tclTHEN (change_in_concl
 764                                (mkAppL [| parse "not"; ineq|]
 765                                        ))
 766                       (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
 767                                                else parse "Rnot_le_le"))
 768                             (tclTHENS (Equality.replace
 769                                        (mkAppL [|parse "Rminus";!t2;!t1|]
 770                                                )
 771                                        tc)
 772                                [tac2;
 773                                 (tclTHENS (Equality.replace (parse "(Rinv R1)")
 774                                                            (parse "R1"))
 775 *)
 776 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...    *)
 777 (*
 778                                 [tclORELSE
 779                                    (Ring.polynom [])
 780                                    tclIDTAC;
 781                                           (tclTHEN (apply (parse "sym_eqT"))
 782                                                 (apply (parse "Rinv_R1")))]
 783
 784                                          )
 785                                 ]));
 786                        !tac1]);
 787            tac:=(tclTHENS (cut (parse "False"))
 788                                   [tclTHEN intro contradiction;
 789                                    !tac])
 790       |_-> assert false) |_-> assert false
 791           );
 792     ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
 793       (!tac gl)
 794       ((tclABSTRACT None !tac) gl)
 795
 796 ;;
 797
 798 let fourier_tac x gl =
 799      fourier gl
 800 ;;
 801
 802 let v_fourier = add_tactic "Fourier" fourier_tac
 803 *)
 804
 805 (*open CicReduction*)
 806 (*open PrimitiveTactics*)
 807 (*open ProofEngineTypes*)
 808 let fourier_tac ~status:(proof,goal) = ignore(fourier (proof,goal)) ; (proof,[goal]) ;;
 809