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 (* $Id$ *)
  27
  28
  29 (******************** THE FOURIER TACTIC ***********************)
  30
  31 (* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
  32 des inéquations et équations sont entiers. En attendant la tactique Field.
  33 *)
  34
  35 open Fourier
  36 open ProofEngineTypes
  37
  38
  39 let debug x = print_string ("____ "^x) ; flush stdout;;
  40
  41 let debug_pcontext x =
  42  let str = ref "" in
  43  List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
  44   a ^ " " | _ ->()) x ;
  45  debug ("contesto : "^ (!str) ^ "\n")
  46 ;;
  47
  48 (******************************************************************************
  49 Operations on linear combinations.
  50
  51 Opérations sur les combinaisons linéaires affines.
  52 La partie homogène d'une combinaison linéaire est en fait une table de hash
  53 qui donne le coefficient d'un terme du calcul des constructions,
  54 qui est zéro si le terme n'y est pas.
  55 *)
  56
  57
  58
  59 (**
  60         The type for linear combinations
  61 *)
  62 type flin = {fhom:(Cic.term , rational)Hashtbl.t;fcste:rational}
  63 ;;
  64
  65 (**
  66         @return an empty flin
  67 *)
  68 let flin_zero () = {fhom = Hashtbl.create 50;fcste=r0}
  69 ;;
  70
  71 (**
  72         @param f a flin
  73         @param x a Cic.term
  74         @return the rational associated with x (coefficient)
  75 *)
  76 let flin_coef f x =
  77         try
  78                 (Hashtbl.find f.fhom x)
  79         with
  80                 _ -> r0
  81 ;;
  82
  83 (**
  84         Adds c to the coefficient of x
  85         @param f a flin
  86         @param x a Cic.term
  87         @param c a rational
  88         @return the new flin
  89 *)
  90 let flin_add f x c =
  91     match x with
  92     Cic.Rel(n) ->(
  93       let cx = flin_coef f x in
  94       Hashtbl.remove f.fhom x;
  95       Hashtbl.add f.fhom x (rplus cx c);
  96       f)
  97     |_->debug ("Internal error in Fourier! this is not a Rel "^CicPp.ppterm x^"\n");
  98       let cx = flin_coef f x in
  99       Hashtbl.remove f.fhom x;
 100       Hashtbl.add f.fhom x (rplus cx c);
 101       f
 102 ;;
 103 (**
 104         Adds c to f.fcste
 105         @param f a flin
 106         @param c a rational
 107         @return the new flin
 108 *)
 109 let flin_add_cste f c =
 110     {fhom=f.fhom;
 111      fcste=rplus f.fcste c}
 112 ;;
 113
 114 (**
 115         @return a empty flin with r1 in fcste
 116 *)
 117 let flin_one () = flin_add_cste (flin_zero()) r1;;
 118
 119 (**
 120         Adds two flin
 121 *)
 122 let flin_plus f1 f2 =
 123     let f3 = flin_zero() in
 124     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
 125     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
 126     flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
 127 ;;
 128
 129 (**
 130         Substracts two flin
 131 *)
 132 let flin_minus f1 f2 =
 133     let f3 = flin_zero() in
 134     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
 135     Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
 136     flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
 137 ;;
 138
 139 (**
 140         @return a times f
 141 *)
 142 let flin_emult a f =
 143     let f2 = flin_zero() in
 144     Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
 145     flin_add_cste f2 (rmult a f.fcste);
 146 ;;
 147
 148
 149 (*****************************************************************************)
 150
 151
 152 (**
 153         @param t a term
 154         @raise Failure if conversion is impossible
 155         @return rational proiection of t
 156 *)
 157 let rec rational_of_term t =
 158   (* fun to apply f to the first and second rational-term of l *)
 159   let rat_of_binop f l =
 160           let a = List.hd l and
 161             b = List.hd(List.tl l) in
 162         f (rational_of_term a) (rational_of_term b)
 163   in
 164   (* as before, but f is unary *)
 165   let rat_of_unop f l =
 166           f (rational_of_term (List.hd l))
 167   in
 168   match t with
 169   | Cic.Cast (t1,t2) -> (rational_of_term t1)
 170   | Cic.Appl (t1::next) ->
 171         (match t1 with
 172            Cic.Const (u,boh) ->
 173             if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then
 174                       rat_of_unop rop next
 175             else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then
 176                       rat_of_unop rinv next
 177             else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then
 178                       rat_of_binop rmult next
 179             else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then
 180                       rat_of_binop rdiv next
 181             else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then
 182                       rat_of_binop rplus next
 183             else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then
 184                       rat_of_binop rminus next
 185             else failwith "not a rational"
 186           | _ -> failwith "not a rational")
 187   | Cic.Const (u,boh) ->
 188         if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then r1
 189         else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then r0
 190         else failwith "not a rational"
 191   |  _ -> failwith "not a rational"
 192 ;;
 193
 194 (* coq wrapper
 195 let rational_of_const = rational_of_term;;
 196 *)
 197 let fails f a =
 198  try
 199    let tmp = (f a) in
 200    false
 201  with
 202    _-> true
 203  ;;
 204
 205 let rec flin_of_term t =
 206         let fl_of_binop f l =
 207                 let a = List.hd l and
 208                     b = List.hd(List.tl l) in
 209                 f (flin_of_term a)  (flin_of_term b)
 210         in
 211   try(
 212     match t with
 213   | Cic.Cast (t1,t2) -> (flin_of_term t1)
 214   | Cic.Appl (t1::next) ->
 215         begin
 216         match t1 with
 217         Cic.Const (u,boh) ->
 218             begin
 219              if UriManager.eq u HelmLibraryObjects.Reals.ropp_URI then
 220                   flin_emult (rop r1) (flin_of_term (List.hd next))
 221              else if UriManager.eq u HelmLibraryObjects.Reals.rplus_URI then
 222                   fl_of_binop flin_plus next
 223              else if UriManager.eq u HelmLibraryObjects.Reals.rminus_URI then
 224                   fl_of_binop flin_minus next
 225              else if UriManager.eq u HelmLibraryObjects.Reals.rmult_URI then
 226                      begin
 227                 let arg1 = (List.hd next) and
 228                     arg2 = (List.hd(List.tl next))
 229                 in
 230                 if fails rational_of_term arg1
 231                    then
 232                    if fails rational_of_term arg2
 233                       then
 234                       ( (* prodotto tra 2 incognite ????? impossibile*)
 235                       failwith "Sistemi lineari!!!!\n"
 236                       )
 237                       else
 238                       (
 239                       match arg1 with
 240                       Cic.Rel(n) -> (*trasformo al volo*)
 241                                     (flin_add (flin_zero()) arg1 (rational_of_term arg2))
 242                        |_-> (* test this *)
 243                            let tmp = flin_of_term arg1 in
 244                            flin_emult  (rational_of_term arg2) (tmp)
 245                       )
 246                    else
 247                    if fails rational_of_term arg2
 248                       then
 249                       (
 250                       match arg2 with
 251                       Cic.Rel(n) -> (*trasformo al volo*)
 252                                     (flin_add (flin_zero()) arg2 (rational_of_term arg1))
 253                        |_-> (* test this *)
 254                            let tmp = flin_of_term arg2 in
 255                            flin_emult (rational_of_term arg1) (tmp)
 256
 257                       )
 258                       else
 259                       (  (*prodotto tra razionali*)
 260                       (flin_add_cste (flin_zero()) (rmult (rational_of_term arg1) (rational_of_term arg2)))
 261                       )
 262                           (*try
 263                         begin
 264                         (*let a = rational_of_term arg1 in
 265                         debug("ho fatto rational of term di "^CicPp.ppterm arg1^
 266                          " e ho ottenuto "^string_of_int a.num^"/"^string_of_int a.den^"\n");*)
 267                         let a = flin_of_term arg1
 268                            try
 269                                 begin
 270                                 let b = (rational_of_term arg2) in
 271                                 debug("ho fatto rational of term di "^CicPp.ppterm arg2^
 272                                  " e ho ottenuto "^string_of_int b.num^"/"^string_of_int b.den^"\n");
 273                                     (flin_add_cste (flin_zero()) (rmult a b))
 274                                 end
 275                            with
 276                                 _ -> debug ("ho fallito2 su "^CicPp.ppterm arg2^"\n");
 277                                      (flin_add (flin_zero()) arg2 a)
 278                         end
 279                       with
 280                         _-> debug ("ho fallito1 su "^CicPp.ppterm arg1^"\n");
 281                             (flin_add(flin_zero()) arg1 (rational_of_term arg2))
 282                             *)
 283                 end
 284             else if UriManager.eq u HelmLibraryObjects.Reals.rinv_URI then
 285                let a=(rational_of_term (List.hd next)) in
 286                flin_add_cste (flin_zero()) (rinv a)
 287             else if UriManager.eq u HelmLibraryObjects.Reals.rdiv_URI then
 288                     begin
 289                       let b=(rational_of_term (List.hd(List.tl next))) in
 290                        try
 291                         begin
 292                         let a = (rational_of_term (List.hd next)) in
 293                         (flin_add_cste (flin_zero()) (rdiv a b))
 294                         end
 295                        with
 296                         _-> (flin_add (flin_zero()) (List.hd next) (rinv b))
 297                 end
 298             else assert false
 299             end
 300         |_ -> assert false
 301         end
 302   | Cic.Const (u,boh) ->
 303         begin
 304          if UriManager.eq u HelmLibraryObjects.Reals.r1_URI then flin_one ()
 305          else if UriManager.eq u HelmLibraryObjects.Reals.r0_URI then flin_zero ()
 306          else assert false
 307         end
 308   |_-> assert false)
 309   with _ -> debug("eccezione = "^CicPp.ppterm t^"\n");flin_add (flin_zero()) t r1
 310 ;;
 311
 312 (* coq wrapper
 313 let flin_of_constr = flin_of_term;;
 314 *)
 315
 316 (**
 317         Translates a flin to (c,x) list
 318         @param f a flin
 319         @return something like (c1,x1)::(c2,x2)::...::(cn,xn)
 320 *)
 321 let flin_to_alist f =
 322     let res=ref [] in
 323     Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
 324     !res
 325 ;;
 326
 327 (* Représentation des hypothèses qui sont des inéquations ou des équations.
 328 *)
 329
 330 (**
 331         The structure for ineq
 332 *)
 333 type hineq={hname:Cic.term; (* le nom de l'hypothèse *)
 334             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
 335             hleft:Cic.term;
 336             hright:Cic.term;
 337             hflin:flin;
 338             hstrict:bool}
 339 ;;
 340
 341 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 342 *)
 343
 344 let ineq1_of_term (h,t) =
 345     match t with (* match t *)
 346        Cic.Appl (t1::next) ->
 347          let arg1= List.hd next in
 348          let arg2= List.hd(List.tl next) in
 349          (match t1 with (* match t1 *)
 350            Cic.Const (u,boh) ->
 351              if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
 352                             [{hname=h;
 353                            htype="Rlt";
 354                            hleft=arg1;
 355                            hright=arg2;
 356                            hflin= flin_minus (flin_of_term arg1)
 357                                              (flin_of_term arg2);
 358                            hstrict=true}]
 359              else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
 360                            [{hname=h;
 361                            htype="Rgt";
 362                            hleft=arg2;
 363                            hright=arg1;
 364                            hflin= flin_minus (flin_of_term arg2)
 365                                              (flin_of_term arg1);
 366                            hstrict=true}]
 367              else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
 368                            [{hname=h;
 369                            htype="Rle";
 370                            hleft=arg1;
 371                            hright=arg2;
 372                            hflin= flin_minus (flin_of_term arg1)
 373                                              (flin_of_term arg2);
 374                            hstrict=false}]
 375              else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
 376                            [{hname=h;
 377                            htype="Rge";
 378                            hleft=arg2;
 379                            hright=arg1;
 380                            hflin= flin_minus (flin_of_term arg2)
 381                                              (flin_of_term arg1);
 382                            hstrict=false}]
 383              else assert false
 384           | Cic.MutInd (u,i,o) ->
 385              if UriManager.eq u HelmLibraryObjects.Logic.eq_URI then
 386                             let t0= arg1 in
 387                            let arg1= arg2 in
 388                            let arg2= List.hd(List.tl (List.tl next)) in
 389                     (match t0 with
 390                          Cic.Const (u,boh) ->
 391                            if UriManager.eq u HelmLibraryObjects.Reals.r_URI then
 392                          [{hname=h;
 393                            htype="eqTLR";
 394                            hleft=arg1;
 395                            hright=arg2;
 396                            hflin= flin_minus (flin_of_term arg1)
 397                                              (flin_of_term arg2);
 398                            hstrict=false};
 399                           {hname=h;
 400                            htype="eqTRL";
 401                            hleft=arg2;
 402                            hright=arg1;
 403                            hflin= flin_minus (flin_of_term arg2)
 404                                              (flin_of_term arg1);
 405                            hstrict=false}]
 406                           else assert false
 407                         |_-> assert false)
 408                   else assert false
 409           |_-> assert false)(* match t1 *)
 410         |_-> assert false (* match t *)
 411 ;;
 412 (* coq wrapper
 413 let ineq1_of_constr = ineq1_of_term;;
 414 *)
 415
 416 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 417 *)
 418
 419 let rec print_rl l =
 420  match l with
 421  []-> ()
 422  | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
 423 ;;
 424
 425 let rec print_sys l =
 426  match l with
 427  [] -> ()
 428  | (a,b)::next -> (print_rl a;
 429                  print_string (if b=true then "strict\n"else"\n");
 430                 print_sys next)
 431  ;;
 432
 433 (*let print_hash h =
 434         Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
 435 ;;*)
 436
 437 let fourier_lineq lineq1 =
 438    let nvar=ref (-1) in
 439    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
 440    List.iter (fun f ->
 441                Hashtbl.iter (fun x c ->
 442                                  try (Hashtbl.find hvar x;())
 443                                  with _-> nvar:=(!nvar)+1;
 444                                              Hashtbl.add hvar x (!nvar);
 445                                           debug("aggiungo una var "^
 446                                            string_of_int !nvar^" per "^
 447                                             CicPp.ppterm x^"\n"))
 448                             f.hflin.fhom)
 449              lineq1;
 450    (*print_hash hvar;*)
 451    debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
 452    let sys= List.map (fun h->
 453                let v=Array.create ((!nvar)+1) r0 in
 454                Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x) <- c)
 455                   h.hflin.fhom;
 456                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
 457              lineq1 in
 458    debug ("chiamo unsolvable sul sistema di "^
 459     string_of_int (List.length sys) ^"\n");
 460    print_sys sys;
 461    unsolvable sys
 462 ;;
 463
 464 (*****************************************************************************
 465 Construction de la preuve en cas de succès de la méthode de Fourier,
 466 i.e. on obtient une contradiction.
 467 *)
 468
 469
 470 let _eqT = Cic.MutInd(HelmLibraryObjects.Logic.eq_URI, 0, []) ;;
 471 let _False = Cic.MutInd (HelmLibraryObjects.Logic.false_URI, 0, []) ;;
 472 let _not = Cic.Const (HelmLibraryObjects.Logic.not_URI,[]);;
 473 let _R0 = Cic.Const (HelmLibraryObjects.Reals.r0_URI,[]);;
 474 let _R1 = Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);;
 475 let _R = Cic.Const (HelmLibraryObjects.Reals.r_URI,[]);;
 476 let _Rfourier_eqLR_to_le=Cic.Const ((UriManager.uri_of_string
 477  "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"), []) ;;
 478 let _Rfourier_eqRL_to_le=Cic.Const ((UriManager.uri_of_string
 479  "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"), []) ;;
 480 let _Rfourier_ge_to_le  =Cic.Const ((UriManager.uri_of_string
 481  "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con"), []) ;;
 482 let _Rfourier_gt_to_lt         =Cic.Const ((UriManager.uri_of_string
 483  "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con"), []) ;;
 484 let _Rfourier_le=Cic.Const ((UriManager.uri_of_string
 485  "cic:/Coq/fourier/Fourier_util/Rfourier_le.con"), []) ;;
 486 let _Rfourier_le_le =Cic.Const ((UriManager.uri_of_string
 487  "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con"), []) ;;
 488 let _Rfourier_le_lt =Cic.Const ((UriManager.uri_of_string
 489  "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con"), []) ;;
 490 let _Rfourier_lt=Cic.Const ((UriManager.uri_of_string
 491  "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con"), []) ;;
 492 let _Rfourier_lt_le =Cic.Const ((UriManager.uri_of_string
 493  "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con"), []) ;;
 494 let _Rfourier_lt_lt =Cic.Const ((UriManager.uri_of_string
 495  "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con"), []) ;;
 496 let _Rfourier_not_ge_lt = Cic.Const ((UriManager.uri_of_string
 497  "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con"), []) ;;
 498 let _Rfourier_not_gt_le = Cic.Const ((UriManager.uri_of_string
 499  "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con"), []) ;;
 500 let _Rfourier_not_le_gt = Cic.Const ((UriManager.uri_of_string
 501  "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con"), []) ;;
 502 let _Rfourier_not_lt_ge = Cic.Const ((UriManager.uri_of_string
 503  "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con"), []) ;;
 504 let _Rinv  = Cic.Const (HelmLibraryObjects.Reals.rinv_URI, []);;
 505 let _Rinv_R1 = Cic.Const(HelmLibraryObjects.Reals.rinv_r1_URI, []);;
 506 let _Rle = Cic.Const (HelmLibraryObjects.Reals.rle_URI, []);;
 507 let _Rle_mult_inv_pos =  Cic.Const ((UriManager.uri_of_string
 508  "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con"), []) ;;
 509 let _Rle_not_lt = Cic.Const ((UriManager.uri_of_string
 510  "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con"), []) ;;
 511 let _Rle_zero_1 = Cic.Const ((UriManager.uri_of_string
 512  "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"), []) ;;
 513 let _Rle_zero_pos_plus1 =  Cic.Const ((UriManager.uri_of_string
 514  "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con"), []) ;;
 515 let _Rlt = Cic.Const (HelmLibraryObjects.Reals.rlt_URI, []);;
 516 let _Rlt_mult_inv_pos = Cic.Const ((UriManager.uri_of_string
 517  "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con"), []) ;;
 518 let _Rlt_not_le =  Cic.Const ((UriManager.uri_of_string
 519  "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con"), []) ;;
 520 let _Rlt_zero_1 = Cic.Const ((UriManager.uri_of_string
 521  "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"), []) ;;
 522 let _Rlt_zero_pos_plus1 = Cic.Const ((UriManager.uri_of_string
 523  "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con"), []) ;;
 524 let _Rminus = Cic.Const (HelmLibraryObjects.Reals.rminus_URI, []);;
 525 let _Rmult = Cic.Const (HelmLibraryObjects.Reals.rmult_URI, []);;
 526 let _Rnot_le_le =Cic.Const ((UriManager.uri_of_string
 527  "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con"), []) ;;
 528 let _Rnot_lt0 = Cic.Const ((UriManager.uri_of_string
 529  "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con"), []) ;;
 530 let _Rnot_lt_lt =Cic.Const ((UriManager.uri_of_string
 531  "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con"), []) ;;
 532 let _Ropp = Cic.Const (HelmLibraryObjects.Reals.ropp_URI, []);;
 533 let _Rplus = Cic.Const (HelmLibraryObjects.Reals.rplus_URI, []);;
 534
 535 (******************************************************************************)
 536
 537 let is_int x = (x.den)=1
 538 ;;
 539
 540 (* fraction = couple (num,den) *)
 541 let rec rational_to_fraction x= (x.num,x.den)
 542 ;;
 543
 544 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 545 *)
 546
 547 let rec int_to_real_aux n =
 548   match n with
 549     0 -> _R0 (* o forse R0 + R0 ????? *)
 550   | 1 -> _R1
 551   | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
 552 ;;
 553
 554
 555 let int_to_real n =
 556    let x = int_to_real_aux (abs n) in
 557    if n < 0 then
 558            Cic.Appl [ _Ropp ; x ]
 559    else
 560            x
 561 ;;
 562
 563
 564 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 565 *)
 566
 567 let rational_to_real x =
 568    let (n,d)=rational_to_fraction x in
 569    Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ]  ]
 570 ;;
 571
 572 (* preuve que 0<n*1/d
 573 *)
 574
 575 let tac_zero_inf_pos (n,d) =
 576  let tac_zero_inf_pos (n,d) status =
 577    (*let cste = pf_parse_constr gl in*)
 578    let pall str (proof,goal) t =
 579      debug ("tac "^str^" :\n" );
 580      let curi,metasenv,pbo,pty = proof in
 581      let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 582      debug ("th = "^ CicPp.ppterm t ^"\n");
 583      debug ("ty = "^ CicPp.ppterm ty^"\n");
 584    in
 585    let tacn=ref (mk_tactic (fun status ->
 586         pall "n0" status _Rlt_zero_1 ;
 587         apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in
 588    let tacd=ref (mk_tactic (fun status ->
 589         pall "d0" status _Rlt_zero_1 ;
 590         apply_tactic (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1) status )) in
 591
 592
 593   for i=1 to n-1 do
 594        tacn:=(Tacticals.then_
 595         ~start:(mk_tactic (fun status ->
 596           pall ("n"^string_of_int i) status _Rlt_zero_pos_plus1;
 597           apply_tactic
 598            (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1)
 599            status))
 600         ~continuation:!tacn);
 601   done;
 602   for i=1 to d-1 do
 603        tacd:=(Tacticals.then_
 604         ~start:(mk_tactic (fun status ->
 605           pall "d" status _Rlt_zero_pos_plus1 ;
 606           apply_tactic
 607            (PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) status))
 608         ~continuation:!tacd);
 609   done;
 610
 611 debug("TAC ZERO INF POS\n");
 612   apply_tactic
 613   (Tacticals.thens
 614     ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
 615     ~continuations:[!tacn ;!tacd ] )
 616   status
 617  in
 618   mk_tactic (tac_zero_inf_pos (n,d))
 619 ;;
 620
 621
 622
 623 (* preuve que 0<=n*1/d
 624 *)
 625
 626 let tac_zero_infeq_pos gl (n,d) =
 627  let tac_zero_infeq_pos gl (n,d) status =
 628   (*let cste = pf_parse_constr gl in*)
 629   debug("inizio tac_zero_infeq_pos\n");
 630   let tacn = ref
 631    (*(if n=0 then
 632      (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
 633     else*)
 634      (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
 635   (* ) *)
 636    in
 637    let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 638    for i=1 to n-1 do
 639        tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 640         ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
 641    done;
 642    for i=1 to d-1 do
 643        tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 644         ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
 645    done;
 646    apply_tactic
 647     (Tacticals.thens
 648      ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos)
 649      ~continuations:[!tacn;!tacd]) status
 650  in
 651   mk_tactic (tac_zero_infeq_pos gl (n,d))
 652 ;;
 653
 654
 655
 656 (* preuve que 0<(-n)*(1/d) => False
 657 *)
 658
 659 let tac_zero_inf_false gl (n,d) =
 660  let tac_zero_inf_false gl (n,d) status =
 661    if n=0 then
 662     apply_tactic (PrimitiveTactics.apply_tac ~term:_Rnot_lt0) status
 663    else
 664     apply_tactic (Tacticals.then_
 665      ~start:( mk_tactic (fun status ->
 666        let (proof, goal) = status in
 667        let curi,metasenv,pbo,pty = proof in
 668        let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 669         apply_tactic (PrimitiveTactics.apply_tac ~term:_Rle_not_lt) status))
 670      ~continuation:(tac_zero_infeq_pos gl (-n,d)))
 671     status
 672  in
 673   mk_tactic (tac_zero_inf_false gl (n,d))
 674 ;;
 675
 676 (* preuve que 0<=n*(1/d) => False ; n est negatif
 677 *)
 678
 679 let tac_zero_infeq_false gl (n,d) =
 680  let tac_zero_infeq_false gl (n,d) status =
 681   let (proof, goal) = status in
 682   let curi,metasenv,pbo,pty = proof in
 683   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 684
 685   debug("faccio fold di " ^ CicPp.ppterm
 686          (Cic.Appl
 687            [_Rle ; _R0 ;
 688             Cic.Appl
 689              [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
 690            ]
 691          ) ^ "\n") ;
 692   debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
 693   (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
 694   apply_tactic
 695    (Tacticals.then_
 696     ~start:
 697       (ReductionTactics.fold_tac
 698         ~reduction:(const_lazy_reduction CicReduction.whd)
 699         ~pattern:(ProofEngineTypes.conclusion_pattern None)
 700         ~term:
 701           (const_lazy_term
 702             (Cic.Appl
 703             [_Rle ; _R0 ;
 704               Cic.Appl
 705                [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]])))
 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 (lazy "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.first ~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 (* here we need to negate the thesis, but to do this we need to apply the
 947    right theoreme,so let's parse our thesis *)
 948
 949   let th_to_appl = ref _Rfourier_not_le_gt in
 950   (match s_ty with
 951    Cic.Appl ( Cic.Const(u,boh)::args) ->
 952     th_to_appl :=
 953     (if UriManager.eq u HelmLibraryObjects.Reals.rlt_URI then
 954       _Rfourier_not_ge_lt
 955      else if UriManager.eq u HelmLibraryObjects.Reals.rle_URI then
 956                _Rfourier_not_gt_le
 957      else if UriManager.eq u HelmLibraryObjects.Reals.rgt_URI then
 958                _Rfourier_not_le_gt
 959      else if UriManager.eq u HelmLibraryObjects.Reals.rge_URI then
 960                _Rfourier_not_lt_ge
 961      else failwith "fourier can't be applyed")
 962    |_-> failwith "fourier can't be applyed");
 963    (* fix maybe strip_outer_cast goes here?? *)
 964
 965    (* now let's change our thesis applying the th and put it with hp *)
 966
 967    let proof,gl = apply_tactic
 968     (Tacticals.then_
 969       ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
 970       ~continuation:(PrimitiveTactics.intros_tac ()))
 971     (s_proof,s_goal)
 972    in
 973    let goal = if List.length gl = 1 then List.hd gl
 974                                     else failwith "a new goal" in
 975
 976    debug ("port la tesi sopra e la nego. contesto :\n");
 977    debug_pcontext s_context;
 978
 979    (* now we have all the right environment *)
 980
 981    let curi,metasenv,pbo,pty = proof in
 982    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 983
 984    (* now we want to convert hp to inequations, but first we must lift
 985       everyting to thesis level, so that a variable has the save Rel(n)
 986       in each hp ( needed by ineq1_of_term ) *)
 987
 988     (* ? fix if None  ?????*)
 989     (* fix change superlift with a real name *)
 990
 991   let l_context = superlift context 1 in
 992   let hyps = filter_real_hyp l_context l_context in
 993
 994   debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
 995
 996   let lineq =ref [] in
 997
 998   (* transform hyps into inequations *)
 999
1000   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1001                         with _-> ())
1002               hyps;
1003
1004   debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1005          " disequazioni\n");
1006
1007   let res=fourier_lineq (!lineq) in
1008   let tac=ref Tacticals.id_tac in
1009   if res=[] then
1010           (print_string "Tactic Fourier fails.\n";flush stdout;
1011          failwith "fourier_tac fails")
1012   else
1013   (
1014   match res with (*match res*)
1015   [(cres,sres,lc)]->
1016
1017      (* in lc we have the coefficient to "reduce" the system *)
1018
1019      print_string "Fourier's method can prove the goal...\n";flush stdout;
1020
1021      debug "I coeff di moltiplicazione rit sono: ";
1022
1023      let lutil=ref [] in
1024      List.iter
1025         (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1026            (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1027                                      )
1028         (List.combine (!lineq) lc);
1029
1030      print_string (" quindi lutil e' lunga "^
1031       string_of_int (List.length (!lutil))^"\n");
1032
1033      (* on construit la combinaison linéaire des inéquation *)
1034
1035      (match (!lutil) with (*match (!lutil) *)
1036        (h1,c1)::lutil ->
1037        debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1038
1039        let s=ref (h1.hstrict) in
1040
1041
1042        let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1043        let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1044
1045        List.iter (fun (h,c) ->
1046                s:=(!s)||(h.hstrict);
1047                t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1048                      [_Rmult;rational_to_real c;h.hleft ]  ]);
1049                t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1050                      [_Rmult;rational_to_real c;h.hright]  ]))
1051                lutil;
1052
1053        let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1054        let tc=rational_to_real cres in
1055
1056
1057 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1058
1059        debug "inizio a costruire tac1\n";
1060        Fourier.print_rational(c1);
1061
1062        let tac1=ref ( mk_tactic (fun status ->
1063          apply_tactic
1064           (if h1.hstrict then
1065            (Tacticals.thens
1066              ~start:(mk_tactic (fun status ->
1067               debug ("inizio t1 strict\n");
1068               let curi,metasenv,pbo,pty = proof in
1069               let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1070               debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1071               debug ("ty = "^ CicPp.ppterm ty^"\n");
1072               apply_tactic
1073                (PrimitiveTactics.apply_tac ~term:_Rfourier_lt) status))
1074             ~continuations:[tac_use h1;
1075               tac_zero_inf_pos (rational_to_fraction c1)])
1076           else
1077            (Tacticals.thens
1078              ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1079              ~continuations:[tac_use h1;tac_zero_inf_pos
1080               (rational_to_fraction c1)]))
1081           status))
1082
1083        in
1084        s:=h1.hstrict;
1085        List.iter (fun (h,c) ->
1086          (if (!s) then
1087            (if h.hstrict then
1088              (debug("tac1 1\n");
1089              tac1:=(Tacticals.thens
1090                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt_lt)
1091                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1092                 (rational_to_fraction c)]))
1093             else
1094              (debug("tac1 2\n");
1095              Fourier.print_rational(c1);
1096              tac1:=(Tacticals.thens
1097               ~start:(mk_tactic (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                 apply_tactic
1104                  (PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le)
1105                  status))
1106               ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1107                 (rational_to_fraction c)])))
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             else
1116              (debug("tac1 4\n");
1117              tac1:=(Tacticals.thens
1118                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1119                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1120                 (rational_to_fraction c)]))));
1121          s:=(!s)||(h.hstrict)) (* end fun -> *)
1122          lutil;(*end List.iter*)
1123
1124        let tac2 =
1125          if sres then
1126            tac_zero_inf_false goal (rational_to_fraction cres)
1127          else
1128            tac_zero_infeq_false goal (rational_to_fraction cres)
1129        in
1130        tac:=(Tacticals.thens
1131          ~start:(my_cut ~term:ineq)
1132          ~continuations:[Tacticals.then_
1133            ~start:( mk_tactic (fun status ->
1134              let (proof, goal) = status in
1135              let curi,metasenv,pbo,pty = proof in
1136              let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1137              apply_tactic
1138               (ReductionTactics.change_tac
1139                 ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
1140                 (const_lazy_term (Cic.Appl [ _not; ineq])))
1141               status))
1142            ~continuation:(Tacticals.then_
1143              ~start:(PrimitiveTactics.apply_tac ~term:
1144                (if sres then _Rnot_lt_lt else _Rnot_le_le))
1145              ~continuation:(Tacticals.thens
1146                ~start:(mk_tactic (fun status ->
1147                  debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^
1148                   CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1149                  let r = apply_tactic
1150                   (equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
1151                   status
1152                  in
1153                  (match r with (p,gl) ->
1154                    debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1155                  r))
1156                ~continuations:[(Tacticals.thens
1157                  ~start:(mk_tactic (fun status ->
1158                    let r = apply_tactic
1159                     (equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
1160                     status
1161                    in
1162                    (match r with (p,gl) ->
1163                      debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1164                    r))
1165                  ~continuations:
1166                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1;
1167                     Tacticals.first
1168                      ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac]
1169                    ])
1170                ;(*Tacticals.id_tac*)
1171                 Tacticals.then_
1172                  ~start:(mk_tactic (fun status ->
1173                    let (proof, goal) = status in
1174                    let curi,metasenv,pbo,pty = proof in
1175                    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
1176                    (* check if ty is of type *)
1177                    let w1 =
1178                      debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1179                      (match ty with
1180                      Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1181                      |_ -> assert false)
1182                    in
1183                    let r = apply_tactic
1184                     (ReductionTactics.change_tac
1185                       ~pattern:(ProofEngineTypes.conclusion_pattern (Some ty))
1186                       (const_lazy_term w1)) status
1187                    in
1188                    debug("fine MY_CHNGE\n");
1189                    r))
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 = apply_tactic !tac (proof,goal) in
1198   debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1199
1200   )
1201 ;;
1202
1203 let fourier_tac = mk_tactic fourier
1204
1205