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