helm/ocaml/tactics/fourierR.ml

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