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