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