helm/ocaml/tactics/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 (******************** THE FOURIER TACTIC ***********************)
  28
  29 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
  30 des inéquations et équations sont entiers. En attendant la tactique Field.
  31 *)
  32
  33 open Fourier
  34
  35
  36 let debug x = print_string ("____ "^x) ; flush stdout;;
  37
  38 let debug_pcontext x =
  39  let str = ref "" in
  40  List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
  41   a ^ " " | _ ->()) x ;
  42  debug ("contesto : "^ (!str) ^ "\n")
  43 ;;
  44
  45 (******************************************************************************
  46 Operations on linear combinations.
  47
  48 Opérations sur les combinaisons linéaires affines.
  49 La partie homogène d'une combinaison linéaire est en fait une table de hash
  50 qui donne le coefficient d'un terme du calcul des constructions,
  51 qui est zéro si le terme n'y est pas.
  52 *)
  53
  54
  55
  56 (**
  57         The type for linear combinations
  58 *)
  59 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
  60 ;;
  61
  62 (**
  63         @return an empty flin
  64 *)
  65 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
  66 ;;
  67
  68 (**
  69         @param f a flin
  70         @param x a Cic.term
  71         @return the rational associated with x (coefficient)
  72 *)
  73 let flin_coef f x =
  74         try
  75                 (Hashtbl.find f.fhom x)
  76         with
  77                 _ -> r0
  78 ;;
  79
  80 (**
  81         Adds c to the coefficient of x
  82         @param f a flin
  83         @param x a Cic.term
  84         @param c a rational
  85         @return the new flin
  86 *)
  87 let flin_add f x c =
  88     match x with
  89     Cic.Rel(n) ->(
  90       let cx = flin_coef f x in
  91       Hashtbl.remove f.fhom x;
  92       Hashtbl.add f.fhom x (rplus cx c);
  93       f)
  94     |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n");
  95       let cx = flin_coef f x in
  96       Hashtbl.remove f.fhom x;
  97       Hashtbl.add f.fhom x (rplus cx c);
  98       f
  99 ;;
 100 (**
 101         Adds c to f.fcste
 102         @param f a flin
 103         @param c a rational
 104         @return the new flin
 105 *)
 106 let flin_add_cste f c =
 107     {fhom=f.fhom;
 108      fcste=rplus f.fcste c}
 109 ;;
 110
 111 (**
 112         @return a empty flin with r1 in fcste
 113 *)
 114 let flin_one () = flin_add_cste (flin_zero()) r1;;
 115
 116 (**
 117         Adds two flin
 118 *)
 119 let flin_plus f1 f2 =
 120     let f3 = flin_zero() in
 121     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
 122     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
 123     flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
 124 ;;
 125
 126 (**
 127         Substracts two flin
 128 *)
 129 let flin_minus f1 f2 =
 130     let f3 = flin_zero() in
 131     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
 132     Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
 133     flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
 134 ;;
 135
 136 (**
 137         @return a times f
 138 *)
 139 let flin_emult a f =
 140     let f2 = flin_zero() in
 141     Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
 142     flin_add_cste f2 (rmult a f.fcste);
 143 ;;
 144
 145
 146 (*****************************************************************************)
 147
 148
 149 (**
 150         @param t a term
 151         @raise Failure if conversion is impossible
 152         @return rational proiection of t
 153 *)
 154 let rec rational_of_term t =
 155   (* fun to apply f to the first and second rational-term of l *)
 156   let rat_of_binop f l =
 157         let a = List.hd l and
 158             b = List.hd(List.tl l) in
 159         f (rational_of_term a) (rational_of_term b)
 160   in
 161   (* as before, but f is unary *)
 162   let rat_of_unop f l =
 163         f (rational_of_term (List.hd l))
 164   in
 165   match t with
 166   | Cic.Cast (t1,t2) -> (rational_of_term t1)
 167   | Cic.Appl (t1::next) ->
 168         (match t1 with
 169            Cic.Const (u,boh) ->
 170                (match (UriManager.string_of_uri u) with
 171                  "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
 172                       rat_of_unop rop next
 173                 |"cic:/Coq/Reals/Rdefinitions/Rinv.con" ->
 174                       rat_of_unop rinv next
 175                 |"cic:/Coq/Reals/Rdefinitions/Rmult.con" ->
 176                       rat_of_binop rmult next
 177                 |"cic:/Coq/Reals/Rdefinitions/Rdiv.con" ->
 178                       rat_of_binop rdiv next
 179                 |"cic:/Coq/Reals/Rdefinitions/Rplus.con" ->
 180                       rat_of_binop rplus next
 181                 |"cic:/Coq/Reals/Rdefinitions/Rminus.con" ->
 182                       rat_of_binop rminus next
 183                 | _ -> failwith "not a rational")
 184           | _ -> failwith "not a rational")
 185   | Cic.Const (u,boh) ->
 186         (match (UriManager.string_of_uri u) with
 187                "cic:/Coq/Reals/Rdefinitions/R1.con" -> r1
 188               |"cic:/Coq/Reals/Rdefinitions/R0.con" -> r0
 189               |  _ -> failwith "not a rational")
 190   |  _ -> failwith "not a rational"
 191 ;;
 192
 193 (* coq wrapper
 194 let rational_of_const = rational_of_term;;
 195 *)
 196 let fails f a =
 197  try
 198    let tmp = (f a) in
 199    false
 200  with
 201    _-> true
 202  ;;
 203
 204 let rec flin_of_term t =
 205         let fl_of_binop f l =
 206                 let a = List.hd l and
 207                     b = List.hd(List.tl l) in
 208                 f (flin_of_term a)  (flin_of_term b)
 209         in
 210   try(
 211     match t with
 212   | Cic.Cast (t1,t2) -> (flin_of_term t1)
 213   | Cic.Appl (t1::next) ->
 214         begin
 215         match t1 with
 216         Cic.Const (u,boh) ->
 217             begin
 218             match (UriManager.string_of_uri u) with
 219              "cic:/Coq/Reals/Rdefinitions/Ropp.con" ->
 220                   flin_emult (rop r1) (flin_of_term (List.hd next))
 221             |"cic:/Coq/Reals/Rdefinitions/Rplus.con"->
 222                   fl_of_binop flin_plus next
 223             |"cic:/Coq/Reals/Rdefinitions/Rminus.con"->
 224                   fl_of_binop flin_minus next
 225             |"cic:/Coq/Reals/Rdefinitions/Rmult.con"->
 226                 begin
 227                 let arg1 = (List.hd next) and
 228                     arg2 = (List.hd(List.tl next))
 229                 in
 230                 if fails rational_of_term arg1
 231                    then
 232                    if fails rational_of_term arg2
 233                       then
 234                       ( (* prodotto tra 2 incognite ????? impossibile*)
 235                       failwith "Sistemi lineari!!!!\n"
 236                       )
 237                       else
 238                       (
 239                       match arg1 with
 240                       Cic.Rel(n) -> (*trasformo al volo*)
 241                                     (flin_add (flin_zero()) arg1 (rational_of_term arg2))
 242                       |_-> (* test this *)
 243                            let tmp = flin_of_term arg1 in
 244                            flin_emult  (rational_of_term arg2) (tmp)
 245                       )
 246                    else
 247                    if fails rational_of_term arg2
 248                       then
 249                       (
 250                       match arg2 with
 251                       Cic.Rel(n) -> (*trasformo al volo*)
 252                                     (flin_add (flin_zero()) arg2 (rational_of_term arg1))
 253                       |_-> (* test this *)
 254                            let tmp = flin_of_term arg2 in
 255                            flin_emult (rational_of_term arg1) (tmp)
 256
 257                       )
 258                       else
 259                       (  (*prodotto tra razionali*)
 260                       (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
 261                       )
 262                         (*try
 263                         begin
 264                         (*let a = rational_of_term arg1 in
 265                         debug("ho fatto rational of term di "^CicPp.ppterm arg1^
 266                          " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
 267                         let a = flin_of_term arg1
 268                         try
 269                                 begin
 270                                 let b = (rational_of_term arg2) in
 271                                 debug("ho fatto rational of term di "^CicPp.ppterm arg2^
 272                                  " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
 273                                 (flin_add_cste (flin_zero()) (rmult a b))
 274                                 end
 275                         with
 276                                 _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
 277                                      (flin_add (flin_zero()) arg2 a)
 278                         end
 279                 with
 280                         _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
 281                             (flin_add(flin_zero()) arg1 (rational_of_term arg2))
 282                             *)
 283                 end
 284             |"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
 285                let a=(rational_of_term (List.hd next)) in
 286                flin_add_cste (flin_zero()) (rinv a)
 287             |"cic:/Coq/Reals/Rdefinitions/Rdiv.con"->
 288                 begin
 289                 let b=(rational_of_term (List.hd(List.tl next))) in
 290                 try
 291                         begin
 292                         let a = (rational_of_term (List.hd next)) in
 293                         (flin_add_cste (flin_zero()) (rdiv a b))
 294                         end
 295                 with
 296                         _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
 297                 end
 298             |_->assert false
 299             end
 300         |_ -> assert false
 301         end
 302   | Cic.Const (u,boh) ->
 303         begin
 304         match (UriManager.string_of_uri u) with
 305          "cic:/Coq/Reals/Rdefinitions/R1.con" -> flin_one ()
 306         |"cic:/Coq/Reals/Rdefinitions/R0.con" -> flin_zero ()
 307         |_-> assert false
 308         end
 309   |_-> assert false)
 310   with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
 311 ;;
 312
 313 (* coq wrapper
 314 let flin_of_constr = flin_of_term;;
 315 *)
 316
 317 (**
 318         Translates a flin to (c,x) list
 319         @param f a flin
 320         @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
 321 *)
 322 let flin_to_alist f =
 323     let res=ref [] in
 324     Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
 325     !res
 326 ;;
 327
 328 (* Représentation des hypothèses qui sont des inéquations ou des équations.
 329 *)
 330
 331 (**
 332         The structure for ineq
 333 *)
 334 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
 335             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
 336             hleft:Cic.term;
 337             hright:Cic.term;
 338             hflin:flin;
 339             hstrict:bool}
 340 ;;
 341
 342 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 343 *)
 344
 345 let ineq1_of_term (h,t) =
 346     match t with (* match t *)
 347        Cic.Appl (t1::next) ->
 348          let arg1= List.hd next in
 349          let arg2= List.hd(List.tl next) in
 350          (match t1 with (* match t1 *)
 351            Cic.Const (u,boh) ->
 352             (match UriManager.string_of_uri u with (* match u *)
 353                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
 354                            [{hname=h;
 355                            htype="Rlt";
 356                            hleft=arg1;
 357                            hright=arg2;
 358                            hflin= flin_minus (flin_of_term arg1)
 359                                              (flin_of_term arg2);
 360                            hstrict=true}]
 361                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
 362                            [{hname=h;
 363                            htype="Rgt";
 364                            hleft=arg2;
 365                            hright=arg1;
 366                            hflin= flin_minus (flin_of_term arg2)
 367                                              (flin_of_term arg1);
 368                            hstrict=true}]
 369                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
 370                            [{hname=h;
 371                            htype="Rle";
 372                            hleft=arg1;
 373                            hright=arg2;
 374                            hflin= flin_minus (flin_of_term arg1)
 375                                              (flin_of_term arg2);
 376                            hstrict=false}]
 377                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
 378                            [{hname=h;
 379                            htype="Rge";
 380                            hleft=arg2;
 381                            hright=arg1;
 382                            hflin= flin_minus (flin_of_term arg2)
 383                                              (flin_of_term arg1);
 384                            hstrict=false}]
 385                 |_->assert false)(* match u *)
 386           | Cic.MutInd (u,i,o) ->
 387               (match UriManager.string_of_uri u with
 388                  "cic:/Coq/Init/Logic_Type/eqT.ind" ->
 389                            let t0= arg1 in
 390                            let arg1= arg2 in
 391                            let arg2= List.hd(List.tl (List.tl next)) in
 392                     (match t0 with
 393                          Cic.Const (u,boh) ->
 394                            (match UriManager.string_of_uri u with
 395                               "cic:/Coq/Reals/Rdefinitions/R.con"->
 396                          [{hname=h;
 397                            htype="eqTLR";
 398                            hleft=arg1;
 399                            hright=arg2;
 400                            hflin= flin_minus (flin_of_term arg1)
 401                                              (flin_of_term arg2);
 402                            hstrict=false};
 403                           {hname=h;
 404                            htype="eqTRL";
 405                            hleft=arg2;
 406                            hright=arg1;
 407                            hflin= flin_minus (flin_of_term arg2)
 408                                              (flin_of_term arg1);
 409                            hstrict=false}]
 410                            |_-> assert false)
 411                          |_-> assert false)
 412                    |_-> assert false)
 413           |_-> assert false)(* match t1 *)
 414         |_-> assert false (* match t *)
 415 ;;
 416 (* coq wrapper
 417 let ineq1_of_constr = ineq1_of_term;;
 418 *)
 419
 420 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 421 *)
 422
 423 let rec print_rl l =
 424  match l with
 425  []-> ()
 426  | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
 427 ;;
 428
 429 let rec print_sys l =
 430  match l with
 431  [] -> ()
 432  | (a,b)::next -> (print_rl a;
 433                 print_string (if b=true then "strict\n"else"\n");
 434                 print_sys next)
 435  ;;
 436
 437 (*let print_hash h =
 438         Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
 439 ;;*)
 440
 441 let fourier_lineq lineq1 =
 442    let nvar=ref (-1) in
 443    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
 444    List.iter (fun f ->
 445                Hashtbl.iter (fun x c ->
 446                                  try (Hashtbl.find hvar x;())
 447                                  with _-> nvar:=(!nvar)+1;
 448                                           Hashtbl.add hvar x (!nvar);
 449                                           debug("aggiungo una var "^
 450                                            string_of_int !nvar^" per "^
 451                                             CicPp.ppterm x^"\n"))
 452                             f.hflin.fhom)
 453              lineq1;
 454    (*print_hash hvar;*)
 455    debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
 456    let sys= List.map (fun h->
 457                let v=Array.create ((!nvar)+1) r0 in
 458                Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c)
 459                   h.hflin.fhom;
 460                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
 461              lineq1 in
 462    debug ("chiamo unsolvable sul sistema di "^
 463     string_of_int (List.length sys) ^"\n");
 464    print_sys sys;
 465    unsolvable sys
 466 ;;
 467
 468 (*****************************************************************************
 469 Construction de la preuve en cas de succès de la méthode de Fourier,
 470 i.e. on obtient une contradiction.
 471 *)
 472
 473
 474 let _eqT = Cic.MutInd((UriManager.uri_of_string
 475  "cic:/Coq/Init/Logic_Type/eqT.ind"), 0, []) ;;
 476 let _False = Cic.MutInd ((UriManager.uri_of_string
 477  "cic:/Coq/Init/Logic/False.ind"), 0, []) ;;
 478 let _not = Cic.Const ((UriManager.uri_of_string
 479  "cic:/Coq/Init/Logic/not.con"), []);;
 480 let _R0 = Cic.Const ((UriManager.uri_of_string
 481  "cic:/Coq/Reals/Rdefinitions/R0.con"), []) ;;
 482 let _R1 = Cic.Const ((UriManager.uri_of_string
 483  "cic:/Coq/Reals/Rdefinitions/R1.con"), []) ;;
 484 let _R = Cic.Const ((UriManager.uri_of_string
 485  "cic:/Coq/Reals/Rdefinitions/R.con"), []) ;;
 486 let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string
 487  "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;;
 488 let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string
 489  "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;;
 490 let _Rfourier_ge_to_le  =Cic.Const ((UriManager.uri_of_string
 491  "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;;
 492 let _Rfourier_gt_to_lt  =Cic.Const ((UriManager.uri_of_string
 493  "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;;
 494 let _Rfourier_le=Cic.Const ((UriManager.uri_of_string
 495  "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;;
 496 let _Rfourier_le_le =Cic.Const ((UriManager.uri_of_string
 497  "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con"), []) ;;
 498 let _Rfourier_le_lt =Cic.Const ((UriManager.uri_of_string
 499  "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con"), []) ;;
 500 let _Rfourier_lt=Cic.Const ((UriManager.uri_of_string
 501  "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con"), []) ;;
 502 let _Rfourier_lt_le =Cic.Const ((UriManager.uri_of_string
 503  "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con"), []) ;;
 504 let _Rfourier_lt_lt =Cic.Const ((UriManager.uri_of_string
 505  "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con"), []) ;;
 506 let _Rfourier_not_ge_lt = Cic.Const ((UriManager.uri_of_string
 507  "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con"), []) ;;
 508 let _Rfourier_not_gt_le = Cic.Const ((UriManager.uri_of_string
 509  "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con"), []) ;;
 510 let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string
 511  "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;;
 512 let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string
 513  "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;;
 514 let _Rinv  = Cic.Const ((UriManager.uri_of_string
 515  "cic:/Coq/Reals/Rdefinitions/Rinv.con"), []) ;;
 516 let _Rinv_R1 = Cic.Const((UriManager.uri_of_string
 517  "cic:/Coq/Reals/Rbase/Rinv_R1.con" ), []) ;;
 518 let _Rle = Cic.Const ((UriManager.uri_of_string
 519  "cic:/Coq/Reals/Rdefinitions/Rle.con"), []) ;;
 520 let _Rle_mult_inv_pos =  Cic.Const ((UriManager.uri_of_string
 521  "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;;
 522 let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string
 523  "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con"), []) ;;
 524 let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string
 525  "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;;
 526 let _Rle_zero_pos_plus1 =  Cic.Const ((UriManager.uri_of_string
 527  "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;;
 528 (*let _Rle_zero_zero = Cic.Const ((UriManager.uri_of_string
 529  "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con"), []) ;;*)
 530 let _Rlt = Cic.Const ((UriManager.uri_of_string
 531  "cic:/Coq/Reals/Rdefinitions/Rlt.con"), []) ;;
 532 let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
 533  "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;;
 534 let _Rlt_not_le =  Cic.Const ((UriManager.uri_of_string
 535  "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con"), []) ;;
 536 let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string
 537  "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;;
 538 let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
 539  "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;;
 540 let _Rminus = Cic.Const ((UriManager.uri_of_string
 541  "cic:/Coq/Reals/Rdefinitions/Rminus.con"), []) ;;
 542 let _Rmult = Cic.Const ((UriManager.uri_of_string
 543  "cic:/Coq/Reals/Rdefinitions/Rmult.con"), []) ;;
 544 let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string
 545  "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;;
 546 let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string
 547  "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;;
 548 let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string
 549  "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;;
 550 let _Ropp = Cic.Const ((UriManager.uri_of_string
 551  "cic:/Coq/Reals/Rdefinitions/Ropp.con"), []) ;;
 552 let _Rplus = Cic.Const ((UriManager.uri_of_string
 553  "cic:/Coq/Reals/Rdefinitions/Rplus.con"), []) ;;
 554
 555 (******************************************************************************)
 556
 557 let is_int x = (x.den)=1
 558 ;;
 559
 560 (* fraction = couple (num,den) *)
 561 let rec rational_to_fraction x= (x.num,x.den)
 562 ;;
 563
 564 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 565 *)
 566
 567 let rec int_to_real_aux n =
 568   match n with
 569     0 -> _R0 (* o forse R0 + R0 ????? *)
 570   | 1 -> _R1
 571   | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
 572 ;;
 573
 574
 575 let int_to_real n =
 576    let x = int_to_real_aux (abs n) in
 577    if n < 0 then
 578         Cic.Appl [ _Ropp ; x ]
 579    else
 580         x
 581 ;;
 582
 583
 584 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 585 *)
 586
 587 let rational_to_real x =
 588    let (n,d)=rational_to_fraction x in
 589    Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ]  ]
 590 ;;
 591
 592 (* preuve que 0<n*1/d
 593 *)
 594
 595 let tac_zero_inf_pos (n,d) ~status =
 596    (*let cste = pf_parse_constr gl in*)
 597    let pall str ~status:(proof,goal) t =
 598      debug ("tac "^str^" :\n" );
 599      let curi,metasenv,pbo,pty = proof in
 600      let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 601      debug ("th = "^ CicPp.ppterm t ^"\n");
 602      debug ("ty = "^ CicPp.ppterm ty^"\n");
 603    in
 604    let tacn=ref
 605      (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;
 606        PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
 607    let tacd=ref
 608      (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;
 609        PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
 610
 611
 612   for i=1 to n-1 do
 613        tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i)
 614         ~status _Rlt_zero_pos_plus1;
 615          PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status)
 616           ~continuation:!tacn);
 617   done;
 618   for i=1 to d-1 do
 619        tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d"
 620         ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac
 621          ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd);
 622   done;
 623
 624
 625
 626 debug("TAC ZERO INF POS\n");
 627
 628 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
 629   ~continuations:[
 630    !tacn ;
 631    !tacd ]
 632   ~status)
 633 ;;
 634
 635
 636
 637 (* preuve que 0<=n*1/d
 638 *)
 639
 640 let tac_zero_infeq_pos gl (n,d) ~status =
 641  (*let cste = pf_parse_constr gl in*)
 642  debug("inizio tac_zero_infeq_pos\n");
 643  let tacn = ref
 644   (*(if n=0 then
 645     (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
 646    else*)
 647     (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
 648  (* ) *)
 649   in
 650   let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 651   for i=1 to n-1 do
 652       tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 653        ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
 654   done;
 655   for i=1 to d-1 do
 656       tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 657        ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
 658   done;
 659   let r =
 660   (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
 661    ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
 662    debug("fine tac_zero_infeq_pos\n");
 663    r
 664 ;;
 665
 666
 667
 668 (* preuve que 0<(-n)*(1/d) => False
 669 *)
 670
 671 let tac_zero_inf_false gl (n,d) ~status=
 672   debug("inizio tac_zero_inf_false\n");
 673     if n=0 then
 674      (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
 675      debug("fine\n");
 676      r)
 677     else
 678      (debug "2\n";let r = (Tacticals.then_ ~start:(
 679        fun ~status:(proof,goal as status) ->
 680        let curi,metasenv,pbo,pty = proof in
 681        let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
 682          debug("!!!!!!!!!1: unify "^CicPp.ppterm _Rle_not_lt^" with "
 683          ^ CicPp.ppterm ty ^"\n");
 684        let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
 685        debug("!!!!!!!!!2\n");
 686        r
 687        )
 688      ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
 689      debug("fine\n");
 690      r
 691      )
 692 ;;
 693
 694 (* preuve que 0<=n*(1/d) => False ; n est negatif
 695 *)
 696
 697 let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
 698 debug("stat tac_zero_infeq_false\n");
 699 let r =
 700      let curi,metasenv,pbo,pty = proof in
 701      let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
 702
 703      debug("faccio fold di " ^ CicPp.ppterm
 704             (Cic.Appl
 705               [_Rle ; _R0 ;
 706                Cic.Appl
 707                 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
 708               ]
 709             ) ^ "\n") ;
 710      debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
 711      (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
 712      Tacticals.then_
 713       ~start:
 714         (ReductionTactics.fold_tac ~reduction:CicReduction.whd
 715           ~also_in_hypotheses:false
 716           ~term:
 717             (Cic.Appl
 718               [_Rle ; _R0 ;
 719                Cic.Appl
 720                 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
 721               ]
 722             )
 723         )
 724       ~continuation:
 725         (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
 726           ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
 727  debug("end tac_zero_infeq_false\n");
 728  r
 729 (*PORTING
 730  Tacticals.id_tac ~status
 731 *)
 732 ;;
 733
 734
 735 (* *********** ********** ******** ??????????????? *********** **************)
 736
 737 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
 738   let curi,metasenv,pbo,pty = proof in
 739   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 740   let fresh_meta = ProofEngineHelpers.new_meta proof in
 741   let irl =
 742    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 743   let metasenv' = (fresh_meta,context,t)::metasenv in
 744    let proof' = curi,metasenv',pbo,pty in
 745     let proof'',goals =
 746      PrimitiveTactics.apply_tac
 747       (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
 748       ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
 749        ~status:(proof',goal)
 750     in
 751      proof'',fresh_meta::goals
 752 ;;
 753
 754
 755
 756
 757
 758 let my_cut ~term:c ~status:(proof,goal)=
 759   let curi,metasenv,pbo,pty = proof in
 760   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 761
 762 debug("my_cut di "^CicPp.ppterm c^"\n");
 763
 764
 765   let fresh_meta = ProofEngineHelpers.new_meta proof in
 766   let irl =
 767    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 768   let metasenv' = (fresh_meta,context,c)::metasenv in
 769    let proof' = curi,metasenv',pbo,pty in
 770     let proof'',goals =
 771      apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
 772       CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
 773        ~status:(proof',goal)
 774     in
 775      (* We permute the generated goals to be consistent with Coq *)
 776      match goals with
 777         [] -> assert false
 778       | he::tl -> proof'',he::fresh_meta::tl
 779 ;;
 780
 781
 782 let exact = PrimitiveTactics.exact_tac;;
 783
 784 let tac_use h ~status:(proof,goal as status) =
 785 debug("Inizio TC_USE\n");
 786 let curi,metasenv,pbo,pty = proof in
 787 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 788 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
 789 debug ("ty = "^ CicPp.ppterm ty^"\n");
 790
 791 let res =
 792 match h.htype with
 793   "Rlt" -> exact ~term:h.hname ~status
 794   |"Rle" -> exact ~term:h.hname ~status
 795   |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 796              ~term:_Rfourier_gt_to_lt)
 797               ~continuation:(exact ~term:h.hname)) ~status
 798   |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 799              ~term:_Rfourier_ge_to_le)
 800               ~continuation:(exact ~term:h.hname)) ~status
 801   |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 802                ~term:_Rfourier_eqLR_to_le)
 803                 ~continuation:(exact ~term:h.hname)) ~status
 804   |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 805                ~term:_Rfourier_eqRL_to_le)
 806                 ~continuation:(exact ~term:h.hname)) ~status
 807   |_->assert false
 808 in
 809 debug("Fine TAC_USE\n");
 810 res
 811 ;;
 812
 813
 814
 815 let is_ineq (h,t) =
 816     match t with
 817        Cic.Appl ( Cic.Const(u,boh)::next) ->
 818          (match (UriManager.string_of_uri u) with
 819                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
 820                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
 821                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
 822                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
 823                 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
 824                    (match (List.hd next) with
 825                        Cic.Const (uri,_) when
 826                         UriManager.string_of_uri uri =
 827                         "cic:/Coq/Reals/Rdefinitions/R.con" -> true
 828                      | _ -> false)
 829                 |_->false)
 830      |_->false
 831 ;;
 832
 833 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 834
 835 let mkAppL a =
 836    Cic.Appl(Array.to_list a)
 837 ;;
 838
 839 (* Résolution d'inéquations linéaires dans R *)
 840 let rec strip_outer_cast c = match c with
 841   | Cic.Cast (c,_) -> strip_outer_cast c
 842   | _ -> c
 843 ;;
 844
 845 (*let find_in_context id context =
 846   let rec find_in_context_aux c n =
 847         match c with
 848         [] -> failwith (id^" not found in context")
 849         | a::next -> (match a with
 850                         Some (Cic.Name(name),_) when name = id -> n
 851                               (*? magari al posto di _ qualcosaltro?*)
 852                         | _ -> find_in_context_aux next (n+1))
 853   in
 854   find_in_context_aux context 1
 855 ;;
 856
 857 (* mi sembra quadratico *)
 858 let rec filter_real_hyp context cont =
 859   match context with
 860   [] -> []
 861   | Some(Cic.Name(h),Cic.Decl(t))::next -> (
 862                                 let n = find_in_context h cont in
 863                                 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
 864                         [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
 865   | a::next -> debug("  no\n"); filter_real_hyp next cont
 866 ;;*)
 867 let filter_real_hyp context _ =
 868   let rec filter_aux context num =
 869    match context with
 870   [] -> []
 871   | Some(Cic.Name(h),Cic.Decl(t))::next ->
 872                 (
 873                 (*let n = find_in_context h cont in*)
 874                 debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
 875                 [(Cic.Rel(num),t)] @ filter_aux next (num+1)
 876                 )
 877   | a::next -> filter_aux next (num+1)
 878   in
 879   filter_aux context 1
 880 ;;
 881
 882
 883 (* lifts everithing at the conclusion level *)
 884 let rec superlift c n=
 885   match c with
 886   [] -> []
 887   | Some(name,Cic.Decl(a))::next  -> [Some(name,Cic.Decl(
 888                   CicSubstitution.lift n a))] @ superlift next (n+1)
 889   | Some(name,Cic.Def(a,None))::next   -> [Some(name,Cic.Def((
 890                   CicSubstitution.lift n a),None))] @ superlift next (n+1)
 891   | Some(name,Cic.Def(a,Some ty))::next   -> [Some(name,Cic.Def((
 892                   CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1)
 893   | _::next -> superlift next (n+1) (*??  ??*)
 894
 895 ;;
 896
 897 let equality_replace a b ~status =
 898 debug("inizio EQ\n");
 899  let module C = Cic in
 900   let proof,goal = status in
 901   let curi,metasenv,pbo,pty = proof in
 902   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 903    let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
 904    let fresh_meta = ProofEngineHelpers.new_meta proof in
 905    let irl =
 906     ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 907    let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
 908 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
 909    let (proof,goals) =
 910     EqualityTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
 911      ~status:((curi,metasenv',pbo,pty),goal)
 912    in
 913    let new_goals = fresh_meta::goals in
 914 debug("fine EQ -> goals : "^string_of_int( List.length new_goals)  ^" = "
 915   ^string_of_int( List.length goals)^"+ meta\n");
 916     (proof,new_goals)
 917 ;;
 918
 919 let tcl_fail a ~status:(proof,goal) =
 920         match a with
 921         1 -> raise (ProofEngineTypes.Fail "fail-tactical")
 922         |_-> (proof,[goal])
 923 ;;
 924
 925 (* Galla: moved in variousTactics.ml
 926 let assumption_tac ~status:(proof,goal)=
 927   let curi,metasenv,pbo,pty = proof in
 928   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 929   let num = ref 0 in
 930   let tac_list = List.map
 931         ( fun x -> num := !num + 1;
 932                 match x with
 933                   Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
 934                   | _ -> ("fake",tcl_fail 1)
 935         )
 936         context
 937   in
 938   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
 939 ;;
 940 *)
 941 (* Galla: moved in negationTactics.ml
 942 (* !!!!! fix !!!!!!!!!! *)
 943 let contradiction_tac ~status:(proof,goal)=
 944         Tacticals.then_
 945                 (*inutile sia questo che quello prima  della chiamata*)
 946                 ~start:PrimitiveTactics.intros_tac
 947                 ~continuation:(Tacticals.then_
 948                         ~start:(VariousTactics.elim_type_tac ~term:_False)
 949                         ~continuation:(assumption_tac))
 950         ~status:(proof,goal)
 951 ;;
 952 *)
 953
 954 (* ********************* TATTICA ******************************** *)
 955
 956 let rec fourier ~status:(s_proof,s_goal)=
 957   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
 958   let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
 959    s_metasenv in
 960
 961   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
 962   debug_pcontext s_context;
 963
 964   let fhyp = String.copy "new_hyp_for_fourier" in
 965
 966 (* here we need to negate the thesis, but to do this we need to apply the right
 967 theoreme,so let's parse our thesis *)
 968
 969   let th_to_appl = ref _Rfourier_not_le_gt in
 970   (match s_ty with
 971    Cic.Appl ( Cic.Const(u,boh)::args) ->
 972     (match UriManager.string_of_uri u with
 973        "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
 974                _Rfourier_not_ge_lt
 975        |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
 976                _Rfourier_not_gt_le
 977        |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
 978                _Rfourier_not_le_gt
 979        |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
 980                _Rfourier_not_lt_ge
 981        |_-> failwith "fourier can't be applyed")
 982    |_-> failwith "fourier can't be applyed");
 983    (* fix maybe strip_outer_cast goes here?? *)
 984
 985    (* now let's change our thesis applying the th and put it with hp *)
 986
 987    let proof,gl =
 988     Tacticals.then_
 989      ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
 990      ~continuation:(PrimitiveTactics.intros_tac ())
 991      ~status:(s_proof,s_goal) in
 992    let goal = if List.length gl = 1 then List.hd gl
 993                                     else failwith "a new goal" in
 994
 995    debug ("port la tesi sopra e la nego. contesto :\n");
 996    debug_pcontext s_context;
 997
 998    (* now we have all the right environment *)
 999
1000    let curi,metasenv,pbo,pty = proof in
1001    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1002
1003
1004    (* now we want to convert hp to inequations, but first we must lift
1005       everyting to thesis level, so that a variable has the save Rel(n)
1006       in each hp ( needed by ineq1_of_term ) *)
1007
1008     (* ? fix if None  ?????*)
1009     (* fix change superlift with a real name *)
1010
1011   let l_context = superlift context 1 in
1012   let hyps = filter_real_hyp l_context l_context in
1013
1014   debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
1015
1016   let lineq =ref [] in
1017
1018   (* transform hyps into inequations *)
1019
1020   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1021                         with _-> ())
1022               hyps;
1023
1024
1025   debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1026          " disequazioni\n");
1027
1028   let res=fourier_lineq (!lineq) in
1029   let tac=ref Tacticals.id_tac in
1030   if res=[] then
1031         (print_string "Tactic Fourier fails.\n";flush stdout;
1032          failwith "fourier_tac fails")
1033   else
1034   (
1035   match res with (*match res*)
1036   [(cres,sres,lc)]->
1037
1038      (* in lc we have the coefficient to "reduce" the system *)
1039
1040      print_string "Fourier's method can prove the goal...\n";flush stdout;
1041
1042      debug "I coeff di moltiplicazione rit sono: ";
1043
1044      let lutil=ref [] in
1045      List.iter
1046         (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1047            (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1048                                      )
1049         (List.combine (!lineq) lc);
1050
1051      print_string (" quindi lutil e' lunga "^
1052       string_of_int (List.length (!lutil))^"\n");
1053
1054      (* on construit la combinaison linéaire des inéquation *)
1055
1056      (match (!lutil) with (*match (!lutil) *)
1057        (h1,c1)::lutil ->
1058        debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1059
1060        let s=ref (h1.hstrict) in
1061
1062
1063        let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1064        let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1065
1066        List.iter (fun (h,c) ->
1067                s:=(!s)||(h.hstrict);
1068                t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1069                      [_Rmult;rational_to_real c;h.hleft ]  ]);
1070                t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1071                      [_Rmult;rational_to_real c;h.hright]  ]))
1072                lutil;
1073
1074        let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1075        let tc=rational_to_real cres in
1076
1077
1078 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1079
1080        debug "inizio a costruire tac1\n";
1081        Fourier.print_rational(c1);
1082
1083        let tac1=ref ( fun ~status ->
1084          if h1.hstrict then
1085            (Tacticals.thens
1086              ~start:(
1087               fun ~status ->
1088               debug ("inizio t1 strict\n");
1089               let curi,metasenv,pbo,pty = proof in
1090               let metano,context,ty = List.find
1091                (function (m,_,_) -> m=goal) metasenv in
1092               debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1093               debug ("ty = "^ CicPp.ppterm ty^"\n");
1094               PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1095             ~continuations:[tac_use h1;tac_zero_inf_pos
1096              (rational_to_fraction c1)]
1097             ~status
1098            )
1099            else
1100            (Tacticals.thens
1101              ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1102              ~continuations:[tac_use h1;tac_zero_inf_pos
1103               (rational_to_fraction c1)] ~status
1104            )
1105          )
1106
1107        in
1108        s:=h1.hstrict;
1109        List.iter (fun (h,c) ->
1110          (if (!s) then
1111            (if h.hstrict then
1112              (debug("tac1 1\n");
1113              tac1:=(Tacticals.thens
1114                ~start:(PrimitiveTactics.apply_tac
1115                 ~term:_Rfourier_lt_lt)
1116                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1117                 (rational_to_fraction c)])
1118              )
1119            else
1120              (debug("tac1 2\n");
1121              Fourier.print_rational(c1);
1122              tac1:=(Tacticals.thens
1123               ~start:(
1124                 fun ~status ->
1125                 debug("INIZIO TAC 1 2\n");
1126                 let curi,metasenv,pbo,pty = proof in
1127                 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1128                  metasenv in
1129                 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1130                 debug ("ty = "^ CicPp.ppterm ty^"\n");
1131                 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1132               ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1133                 (rational_to_fraction c)])
1134              )
1135            )
1136          else
1137            (if h.hstrict then
1138              (debug("tac1 3\n");
1139              tac1:=(Tacticals.thens
1140                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1141                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1142                 (rational_to_fraction c)])
1143              )
1144            else
1145              (debug("tac1 4\n");
1146              tac1:=(Tacticals.thens
1147                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1148                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1149                 (rational_to_fraction c)])
1150              )
1151            )
1152          );
1153          s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1154
1155        let tac2 =
1156          if sres then
1157            tac_zero_inf_false goal (rational_to_fraction cres)
1158          else
1159            tac_zero_infeq_false goal (rational_to_fraction cres)
1160        in
1161        tac:=(Tacticals.thens
1162          ~start:(my_cut ~term:ineq)
1163          ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
1164            ~start:(fun ~status:(proof,goal as status) ->
1165              let curi,metasenv,pbo,pty = proof in
1166              let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1167               metasenv in
1168              PrimitiveTactics.change_tac ~what:ty
1169               ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1170            ~continuation:(Tacticals.then_
1171              ~start:(PrimitiveTactics.apply_tac ~term:
1172                (if sres then _Rnot_lt_lt else _Rnot_le_le))
1173              ~continuation:(Tacticals.thens
1174                ~start:(
1175                  fun ~status ->
1176                  debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1177                  let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1178                   ~status
1179                  in
1180                  (match r with (p,gl) ->
1181                    debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1182                  r)
1183                ~continuations:[(Tacticals.thens
1184                  ~start:(
1185                    fun ~status ->
1186                    let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1187                    (match r with (p,gl) ->
1188                      debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1189                    r)
1190                  ~continuations:
1191                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1192                  ;Tacticals.try_tactics
1193                    ~tactics:[ "ring", (fun ~status ->
1194                                         debug("begin RING\n");
1195                                         let r = Ring.ring_tac  ~status in
1196                                         debug ("end RING\n");
1197                                         r)
1198                         ; "id", Tacticals.id_tac]
1199                  ])
1200                ;(*Tacticals.id_tac*)
1201                 Tacticals.then_
1202                  ~start:
1203                   (
1204                   fun ~status:(proof,goal as status) ->
1205                    let curi,metasenv,pbo,pty = proof in
1206                    let metano,context,ty = List.find (function (m,_,_) -> m=
1207                     goal) metasenv in
1208                    (* check if ty is of type *)
1209                    let w1 =
1210                      debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1211                      (match ty with
1212                      Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1213                      |_ -> assert false)
1214                    in
1215                    let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1216                    debug("fine MY_CHNGE\n");
1217                    r
1218
1219                   )
1220                  ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1221          ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1222
1223     |_-> assert false)(*match (!lutil) *)
1224   |_-> assert false); (*match res*)
1225   debug ("finalmente applico tac\n");
1226   (
1227   let r = !tac ~status:(proof,goal) in
1228   debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1229
1230   )
1231 ;;
1232
1233 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
1234
1235