helm/ocaml/tactics/fourierR.ml

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