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:
 697           (ProofEngineTypes.conclusion_pattern
 698             (Some
 699               (Cic.Appl
 700                 [_Rle ; _R0 ;
 701                  Cic.Appl
 702                   [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
 703                 ]
 704               )))
 705       )
 706     ~continuation:
 707       (Tacticals.then_
 708         ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
 709         ~continuation:(tac_zero_inf_pos (-n,d))))
 710    status
 711  in
 712   mk_tactic (tac_zero_infeq_false gl (n,d))
 713 ;;
 714
 715
 716 (* *********** ********** ******** ??????????????? *********** **************)
 717
 718 let apply_type_tac ~cast:t ~applist:al =
 719  let apply_type_tac ~cast:t ~applist:al (proof,goal) =
 720   let curi,metasenv,pbo,pty = proof in
 721   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 722   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
 723   let irl =
 724    CicMkImplicit.identity_relocation_list_for_metavariable context in
 725   let metasenv' = (fresh_meta,context,t)::metasenv in
 726    let proof' = curi,metasenv',pbo,pty in
 727     let proof'',goals =
 728      apply_tactic
 729       (PrimitiveTactics.apply_tac
 730        (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) *)
 731        ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al))) (* ??? *)
 732       (proof',goal)
 733     in
 734      proof'',fresh_meta::goals
 735  in
 736   mk_tactic (apply_type_tac ~cast:t ~applist:al)
 737 ;;
 738
 739 let my_cut ~term:c =
 740  let my_cut ~term:c (proof,goal) =
 741   let curi,metasenv,pbo,pty = proof in
 742   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 743   let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
 744   let irl =
 745    CicMkImplicit.identity_relocation_list_for_metavariable context in
 746   let metasenv' = (fresh_meta,context,c)::metasenv in
 747    let proof' = curi,metasenv',pbo,pty in
 748     let proof'',goals =
 749      apply_tactic
 750       (apply_type_tac
 751        ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty))
 752        ~applist:[Cic.Meta(fresh_meta,irl)])
 753       (proof',goal)
 754     in
 755      (* We permute the generated goals to be consistent with Coq *)
 756      match goals with
 757         [] -> assert false
 758       | he::tl -> proof'',he::fresh_meta::tl
 759  in
 760   mk_tactic (my_cut ~term:c)
 761 ;;
 762
 763 let exact = PrimitiveTactics.exact_tac;;
 764
 765 let tac_use h =
 766  let tac_use h status =
 767   let (proof, goal) = status in
 768   debug("Inizio TC_USE\n");
 769   let curi,metasenv,pbo,pty = proof in
 770   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 771   debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
 772   debug ("ty = "^ CicPp.ppterm ty^"\n");
 773   apply_tactic
 774    (match h.htype with
 775       "Rlt" -> exact ~term:h.hname
 776     | "Rle" -> exact ~term:h.hname
 777     | "Rgt" -> (Tacticals.then_
 778                  ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
 779                  ~continuation:(exact ~term:h.hname))
 780     | "Rge" -> (Tacticals.then_
 781                  ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
 782                  ~continuation:(exact ~term:h.hname))
 783     | "eqTLR" -> (Tacticals.then_
 784                    ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
 785                    ~continuation:(exact ~term:h.hname))
 786     | "eqTRL" -> (Tacticals.then_
 787                    ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
 788                    ~continuation:(exact ~term:h.hname))
 789     | _->assert false)
 790    status
 791  in
 792   mk_tactic (tac_use h)
 793 ;;
 794
 795 let is_ineq (h,t) =
 796     match t with
 797        Cic.Appl ( Cic.Const(u,boh)::next) ->
 798          (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI or
 799              UriManager.eq u HelmLibraryObjects.Reals.rgt_URI or
 800              UriManager.eq u HelmLibraryObjects.Reals.rle_URI or
 801              UriManager.eq u HelmLibraryObjects.Reals.rge_URI then true
 802           else if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then
 803                    (match (List.hd next) with
 804                        Cic.Const (uri,_) when
 805                         UriManager.eq uri HelmLibraryObjects.Reals.r_URI
 806                          -> true
 807                      | _ -> false)
 808            else false)
 809      |_->false
 810 ;;
 811
 812 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 813
 814 let mkAppL a =
 815    Cic.Appl(Array.to_list a)
 816 ;;
 817
 818 (* Résolution d'inéquations linéaires dans R *)
 819 let rec strip_outer_cast c = match c with
 820   | Cic.Cast (c,_) -> strip_outer_cast c
 821   | _ -> c
 822 ;;
 823
 824 (*let find_in_context id context =
 825   let rec find_in_context_aux c n =
 826           match c with
 827         [] -> failwith (id^" not found in context")
 828         | a::next -> (match a with
 829                         Some (Cic.Name(name),_) when name = id -> n
 830                               (*? magari al posto di _ qualcosaltro?*)
 831                         | _ -> find_in_context_aux next (n+1))
 832   in
 833   find_in_context_aux context 1
 834 ;;
 835
 836 (* mi sembra quadratico *)
 837 let rec filter_real_hyp context cont =
 838   match context with
 839   [] -> []
 840   | Some(Cic.Name(h),Cic.Decl(t))::next -> (
 841                                   let n = find_in_context h cont in
 842                                 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
 843                           [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
 844   | a::next -> debug("  no\n"); filter_real_hyp next cont
 845 ;;*)
 846
 847 let filter_real_hyp context _ =
 848   let rec filter_aux context num =
 849    match context with
 850      [] -> []
 851    | Some(Cic.Name(h),Cic.Decl(t))::next ->
 852        [(Cic.Rel(num),t)] @ filter_aux next (num+1)
 853    | a::next -> filter_aux next (num+1)
 854   in
 855    filter_aux context 1
 856 ;;
 857
 858
 859 (* lifts everithing at the conclusion level *)
 860 let rec superlift c n=
 861   match c with
 862     [] -> []
 863   | Some(name,Cic.Decl(a))::next  ->
 864      [Some(name,Cic.Decl(CicSubstitution.lift n a))]@ superlift next (n+1)
 865   | Some(name,Cic.Def(a,None))::next ->
 866      [Some(name,Cic.Def((CicSubstitution.lift n a),None))]@ superlift next (n+1)
 867   | Some(name,Cic.Def(a,Some ty))::next   ->
 868      [Some(name,
 869       Cic.Def((CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))
 870       ] @ superlift next (n+1)
 871   | _::next -> superlift next (n+1) (*??  ??*)
 872
 873 ;;
 874
 875 let equality_replace a b =
 876  let equality_replace a b status =
 877  debug("inizio EQ\n");
 878   let module C = Cic in
 879    let proof,goal = status in
 880    let curi,metasenv,pbo,pty = proof in
 881    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 882     let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
 883     let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
 884     let irl =
 885      CicMkImplicit.identity_relocation_list_for_metavariable context in
 886     let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
 887  debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
 888     let (proof,goals) = apply_tactic
 889      (EqualityTactics.rewrite_simpl_tac
 890        ~direction:`LeftToRight
 891        ~pattern:(ProofEngineTypes.conclusion_pattern None)
 892        (C.Meta (fresh_meta,irl)))
 893      ((curi,metasenv',pbo,pty),goal)
 894     in
 895     let new_goals = fresh_meta::goals in
 896  debug("fine EQ -> goals : "^string_of_int( List.length new_goals)  ^" = "
 897    ^string_of_int( List.length goals)^"+ meta\n");
 898      (proof,new_goals)
 899  in
 900   mk_tactic (equality_replace a b)
 901 ;;
 902
 903 let tcl_fail a (proof,goal) =
 904   match a with
 905     1 -> raise (ProofEngineTypes.Fail "fail-tactical")
 906   | _ -> (proof,[goal])
 907 ;;
 908
 909 (* Galla: moved in variousTactics.ml
 910 let assumption_tac (proof,goal)=
 911   let curi,metasenv,pbo,pty = proof in
 912   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 913   let num = ref 0 in
 914   let tac_list = List.map
 915           ( fun x -> num := !num + 1;
 916                 match x with
 917                   Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
 918                   | _ -> ("fake",tcl_fail 1)
 919         )
 920           context
 921   in
 922   Tacticals.try_tactics ~tactics:tac_list (proof,goal)
 923 ;;
 924 *)
 925 (* Galla: moved in negationTactics.ml
 926 (* !!!!! fix !!!!!!!!!! *)
 927 let contradiction_tac (proof,goal)=
 928         Tacticals.then_
 929                 (*inutile sia questo che quello prima  della chiamata*)
 930                 ~start:PrimitiveTactics.intros_tac
 931                 ~continuation:(Tacticals.then_
 932                         ~start:(VariousTactics.elim_type_tac ~term:_False)
 933                         ~continuation:(assumption_tac))
 934         (proof,goal)
 935 ;;
 936 *)
 937
 938 (* ********************* TATTICA ******************************** *)
 939
 940 let rec fourier (s_proof,s_goal)=
 941   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
 942   let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
 943   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
 944   debug_pcontext s_context;
 945
 946   let fhyp = String.copy "new_hyp_for_fourier" in
 947
 948 (* here we need to negate the thesis, but to do this we need to apply the
 949    right theoreme,so let's parse our thesis *)
 950
 951   let th_to_appl = ref _Rfourier_not_le_gt in
 952   (match s_ty with
 953    Cic.Appl ( Cic.Const(u,boh)::args) ->
 954     th_to_appl :=
 955     (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
 956       _Rfourier_not_ge_lt
 957      else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
 958                _Rfourier_not_gt_le
 959      else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
 960                _Rfourier_not_le_gt
 961      else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
 962                _Rfourier_not_lt_ge
 963      else failwith "fourier can't be applyed")
 964    |_-> failwith "fourier can't be applyed");
 965    (* fix maybe strip_outer_cast goes here?? *)
 966
 967    (* now let's change our thesis applying the th and put it with hp *)
 968
 969    let proof,gl = apply_tactic
 970     (Tacticals.then_
 971       ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
 972       ~continuation:(PrimitiveTactics.intros_tac ()))
 973     (s_proof,s_goal)
 974    in
 975    let goal = if List.length gl = 1 then List.hd gl
 976                                     else failwith "a new goal" in
 977
 978    debug ("port la tesi sopra e la nego. contesto :\n");
 979    debug_pcontext s_context;
 980
 981    (* now we have all the right environment *)
 982
 983    let curi,metasenv,pbo,pty = proof in
 984    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 985
 986    (* now we want to convert hp to inequations, but first we must lift
 987       everyting to thesis level, so that a variable has the save Rel(n)
 988       in each hp ( needed by ineq1_of_term ) *)
 989
 990     (* ? fix if None  ?????*)
 991     (* fix change superlift with a real name *)
 992
 993   let l_context = superlift context 1 in
 994   let hyps = filter_real_hyp l_context l_context in
 995
 996   debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
 997
 998   let lineq =ref [] in
 999
1000   (* transform hyps into inequations *)
1001
1002   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1003                         with _-> ())
1004               hyps;
1005
1006   debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1007          " disequazioni\n");
1008
1009   let res=fourier_lineq (!lineq) in
1010   let tac=ref Tacticals.id_tac in
1011   if res=[] then
1012           (print_string "Tactic Fourier fails.\n";flush stdout;
1013          failwith "fourier_tac fails")
1014   else
1015   (
1016   match res with (*match res*)
1017   [(cres,sres,lc)]->
1018
1019      (* in lc we have the coefficient to "reduce" the system *)
1020
1021      print_string "Fourier's method can prove the goal...\n";flush stdout;
1022
1023      debug "I coeff di moltiplicazione rit sono: ";
1024
1025      let lutil=ref [] in
1026      List.iter
1027         (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1028            (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1029                                      )
1030         (List.combine (!lineq) lc);
1031
1032      print_string (" quindi lutil e' lunga "^
1033       string_of_int (List.length (!lutil))^"\n");
1034
1035      (* on construit la combinaison linéaire des inéquation *)
1036
1037      (match (!lutil) with (*match (!lutil) *)
1038        (h1,c1)::lutil ->
1039        debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1040
1041        let s=ref (h1.hstrict) in
1042
1043
1044        let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1045        let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1046
1047        List.iter (fun (h,c) ->
1048                s:=(!s)||(h.hstrict);
1049                t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1050                      [_Rmult;rational_to_real c;h.hleft ]  ]);
1051                t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1052                      [_Rmult;rational_to_real c;h.hright]  ]))
1053                lutil;
1054
1055        let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1056        let tc=rational_to_real cres in
1057
1058
1059 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1060
1061        debug "inizio a costruire tac1\n";
1062        Fourier.print_rational(c1);
1063
1064        let tac1=ref ( mk_tactic (fun status ->
1065          apply_tactic
1066           (if h1.hstrict then
1067            (Tacticals.thens
1068              ~start:(mk_tactic (fun status ->
1069               debug ("inizio t1 strict\n");
1070               let curi,metasenv,pbo,pty = proof in
1071               let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1072               debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1073               debug ("ty = "^ CicPp.ppterm ty^"\n");
1074               apply_tactic
1075                (PrimitiveTactics.apply_tac ~term:_Rfourier_lt) status))
1076             ~continuations:[tac_use h1;
1077               tac_zero_inf_pos (rational_to_fraction c1)])
1078           else
1079            (Tacticals.thens
1080              ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1081              ~continuations:[tac_use h1;tac_zero_inf_pos
1082               (rational_to_fraction c1)]))
1083           status))
1084
1085        in
1086        s:=h1.hstrict;
1087        List.iter (fun (h,c) ->
1088          (if (!s) then
1089            (if h.hstrict then
1090              (debug("tac1 1\n");
1091              tac1:=(Tacticals.thens
1092                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt_lt)
1093                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1094                 (rational_to_fraction c)]))
1095             else
1096              (debug("tac1 2\n");
1097              Fourier.print_rational(c1);
1098              tac1:=(Tacticals.thens
1099               ~start:(mk_tactic (fun status ->
1100                 debug("INIZIO TAC 1 2\n");
1101                 let curi,metasenv,pbo,pty = proof in
1102                 let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1103                 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1104                 debug ("ty = "^ CicPp.ppterm ty^"\n");
1105                 apply_tactic
1106                  (PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le)
1107                  status))
1108               ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1109                 (rational_to_fraction c)])))
1110           else
1111            (if h.hstrict then
1112              (debug("tac1 3\n");
1113              tac1:=(Tacticals.thens
1114                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1115                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1116                 (rational_to_fraction c)]))
1117             else
1118              (debug("tac1 4\n");
1119              tac1:=(Tacticals.thens
1120                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1121                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1122                 (rational_to_fraction c)]))));
1123          s:=(!s)||(h.hstrict)) (* end fun -> *)
1124          lutil;(*end List.iter*)
1125
1126        let tac2 =
1127          if sres then
1128            tac_zero_inf_false goal (rational_to_fraction cres)
1129          else
1130            tac_zero_infeq_false goal (rational_to_fraction cres)
1131        in
1132        tac:=(Tacticals.thens
1133          ~start:(my_cut ~term:ineq)
1134          ~continuations:[Tacticals.then_
1135            ~start:( mk_tactic (fun status ->
1136              let (proof, goal) = status in
1137              let curi,metasenv,pbo,pty = proof in
1138              let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1139              apply_tactic
1140               (PrimitiveTactics.change_tac
1141                 ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
1142                 (Cic.Appl [ _not; ineq]))
1143               status))
1144            ~continuation:(Tacticals.then_
1145              ~start:(PrimitiveTactics.apply_tac ~term:
1146                (if sres then _Rnot_lt_lt else _Rnot_le_le))
1147              ~continuation:(Tacticals.thens
1148                ~start:(mk_tactic (fun status ->
1149                  debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^
1150                   CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1151                  let r = apply_tactic
1152                   (equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
1153                   status
1154                  in
1155                  (match r with (p,gl) ->
1156                    debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1157                  r))
1158                ~continuations:[(Tacticals.thens
1159                  ~start:(mk_tactic (fun status ->
1160                    let r = apply_tactic
1161                     (equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
1162                     status
1163                    in
1164                    (match r with (p,gl) ->
1165                      debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1166                    r))
1167                  ~continuations:
1168                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
1169                     Tacticals.try_tactics
1170                      ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac]
1171                    ])
1172                ;(*Tacticals.id_tac*)
1173                 Tacticals.then_
1174                  ~start:(mk_tactic (fun status ->
1175                    let (proof, goal) = status in
1176                    let curi,metasenv,pbo,pty = proof in
1177                    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1178                    (* check if ty is of type *)
1179                    let w1 =
1180                      debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1181                      (match ty with
1182                      Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1183                      |_ -> assert false)
1184                    in
1185                    let r = apply_tactic
1186                     (PrimitiveTactics.change_tac
1187                       ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
1188                       w1) status
1189                    in
1190                    debug("fine MY_CHNGE\n");
1191                    r))
1192                  ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1193          ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1194
1195     |_-> assert false)(*match (!lutil) *)
1196   |_-> assert false); (*match res*)
1197   debug ("finalmente applico tac\n");
1198   (
1199   let r = apply_tactic !tac (proof,goal) in
1200   debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1201
1202   )
1203 ;;
1204
1205 let fourier_tac = mk_tactic fourier
1206
1207