helm/ocaml/tactics/fourierR.ml

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