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
 752       (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
 753       ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
 754        ~status:(proof',goal)
 755     in
 756      proof'',fresh_meta::goals
 757 ;;
 758
 759
 760
 761
 762
 763 let my_cut ~term:c ~status:(proof,goal)=
 764   let curi,metasenv,pbo,pty = proof in
 765   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 766
 767 debug("my_cut di "^CicPp.ppterm c^"\n");
 768
 769
 770   let fresh_meta = ProofEngineHelpers.new_meta proof in
 771   let irl =
 772    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 773   let metasenv' = (fresh_meta,context,c)::metasenv in
 774    let proof' = curi,metasenv',pbo,pty in
 775     let proof'',goals =
 776      apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
 777       CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
 778        ~status:(proof',goal)
 779     in
 780      (* We permute the generated goals to be consistent with Coq *)
 781      match goals with
 782         [] -> assert false
 783       | he::tl -> proof'',he::fresh_meta::tl
 784 ;;
 785
 786
 787 let exact = PrimitiveTactics.exact_tac;;
 788
 789 let tac_use h ~status:(proof,goal as status) =
 790 debug("Inizio TC_USE\n");
 791 let curi,metasenv,pbo,pty = proof in
 792 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 793 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
 794 debug ("ty = "^ CicPp.ppterm ty^"\n");
 795
 796 let res =
 797 match h.htype with
 798   "Rlt" -> exact ~term:h.hname ~status
 799   |"Rle" -> exact ~term:h.hname ~status
 800   |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 801              ~term:_Rfourier_gt_to_lt)
 802               ~continuation:(exact ~term:h.hname)) ~status
 803   |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 804              ~term:_Rfourier_ge_to_le)
 805               ~continuation:(exact ~term:h.hname)) ~status
 806   |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 807                ~term:_Rfourier_eqLR_to_le)
 808                 ~continuation:(exact ~term:h.hname)) ~status
 809   |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 810                ~term:_Rfourier_eqRL_to_le)
 811                 ~continuation:(exact ~term:h.hname)) ~status
 812   |_->assert false
 813 in
 814 debug("Fine TAC_USE\n");
 815 res
 816 ;;
 817
 818
 819
 820 let is_ineq (h,t) =
 821     match t with
 822        Cic.Appl ( Cic.Const(u,boh)::next) ->
 823          (match (UriManager.string_of_uri u) with
 824                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
 825                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
 826                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
 827                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
 828                 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
 829                    (match (List.hd next) with
 830                        Cic.Const (uri,_) when
 831                         UriManager.string_of_uri uri =
 832                         "cic:/Coq/Reals/Rdefinitions/R.con" -> true
 833                      | _ -> false)
 834                 |_->false)
 835      |_->false
 836 ;;
 837
 838 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 839
 840 let mkAppL a =
 841    Cic.Appl(Array.to_list a)
 842 ;;
 843
 844 (* Résolution d'inéquations linéaires dans R *)
 845 let rec strip_outer_cast c = match c with
 846   | Cic.Cast (c,_) -> strip_outer_cast c
 847   | _ -> c
 848 ;;
 849
 850 let find_in_context id context =
 851   let rec find_in_context_aux c n =
 852         match c with
 853         [] -> failwith (id^" not found in context")
 854         | a::next -> (match a with
 855                         Some (Cic.Name(name),_) when name = id -> n
 856                               (*? magari al posto di _ qualcosaltro?*)
 857                         | _ -> find_in_context_aux next (n+1))
 858   in
 859   find_in_context_aux context 1
 860 ;;
 861
 862 (* mi sembra quadratico *)
 863 let rec filter_real_hyp context cont =
 864   match context with
 865   [] -> []
 866   | Some(Cic.Name(h),Cic.Decl(t))::next -> (
 867                                 let n = find_in_context h cont in
 868                         [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
 869   | a::next -> debug("  no\n"); filter_real_hyp next cont
 870 ;;
 871
 872 (* lifts everithing at the conclusion level *)
 873 let rec superlift c n=
 874   match c with
 875   [] -> []
 876   | Some(name,Cic.Decl(a))::next  -> [Some(name,Cic.Decl(
 877                   CicSubstitution.lift n a))] @ superlift next (n+1)
 878   | Some(name,Cic.Def(a))::next   -> [Some(name,Cic.Def(
 879                   CicSubstitution.lift n a))] @ superlift next (n+1)
 880   | _::next -> superlift next (n+1) (*??  ??*)
 881
 882 ;;
 883
 884 let equality_replace a b ~status =
 885 debug("inizio EQ\n");
 886  let module C = Cic in
 887   let proof,goal = status in
 888   let curi,metasenv,pbo,pty = proof in
 889   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 890    let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
 891    let fresh_meta = ProofEngineHelpers.new_meta proof in
 892    let irl =
 893     ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 894    let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
 895 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
 896    let (proof,goals) =
 897     rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
 898      ~status:((curi,metasenv',pbo,pty),goal)
 899    in
 900    let new_goals = fresh_meta::goals in
 901 debug("fine EQ -> goals : "^string_of_int( List.length new_goals)  ^" = "
 902   ^string_of_int( List.length goals)^"+ meta\n");
 903     (proof,new_goals)
 904 ;;
 905
 906 let tcl_fail a ~status:(proof,goal) =
 907         match a with
 908         1 -> raise (ProofEngineTypes.Fail "fail-tactical")
 909         |_-> (proof,[goal])
 910 ;;
 911
 912
 913 let assumption_tac ~status:(proof,goal)=
 914   let curi,metasenv,pbo,pty = proof in
 915   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 916   let num = ref 0 in
 917   let tac_list = List.map
 918         ( fun x -> num := !num + 1;
 919                 match x with
 920                   Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
 921                   | _ -> ("fake",tcl_fail 1)
 922         )
 923         context
 924   in
 925   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
 926 ;;
 927
 928 (* !!!!! fix !!!!!!!!!! *)
 929 let contradiction_tac ~status:(proof,goal)=
 930         Tacticals.then_
 931                 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
 932                 ~continuation:(Tacticals.then_
 933                         ~start:(Ring.elim_type_tac ~term:_False)
 934                         ~continuation:(assumption_tac))
 935         ~status:(proof,goal)
 936 ;;
 937
 938 (* ********************* TATTICA ******************************** *)
 939
 940 let rec fourier ~status:(s_proof,s_goal)=
 941   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
 942   let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
 943    s_metasenv in
 944
 945   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
 946   debug_pcontext s_context;
 947
 948   let fhyp = String.copy "new_hyp_for_fourier" in
 949
 950 (* here we need to negate the thesis, but to do this we need to apply the right
 951 theoreme,so let's parse our thesis *)
 952
 953   let th_to_appl = ref _Rfourier_not_le_gt in
 954   (match s_ty with
 955    Cic.Appl ( Cic.Const(u,boh)::args) ->
 956     (match UriManager.string_of_uri u with
 957        "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
 958                _Rfourier_not_ge_lt
 959        |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
 960                _Rfourier_not_gt_le
 961        |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
 962                _Rfourier_not_le_gt
 963        |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
 964                _Rfourier_not_lt_ge
 965        |_-> failwith "fourier can't be applyed")
 966    |_-> failwith "fourier can't be applyed");
 967    (* fix maybe strip_outer_cast goes here?? *)
 968
 969    (* now let's change our thesis applying the th and put it with hp *)
 970
 971    let proof,gl = Tacticals.then_
 972         ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
 973         ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
 974                 ~status:(s_proof,s_goal) in
 975    let goal = if List.length gl = 1 then List.hd gl
 976                                     else failwith "a new goal" in
 977
 978    debug ("port la tesi sopra e la nego. contesto :\n");
 979    debug_pcontext s_context;
 980
 981    (* now we have all the right environment *)
 982
 983    let curi,metasenv,pbo,pty = proof in
 984    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 985
 986
 987    (* now we want to convert hp to inequations, but first we must lift
 988       everyting to thesis level, so that a variable has the save Rel(n)
 989       in each hp ( needed by ineq1_of_term ) *)
 990
 991     (* ? fix if None  ?????*)
 992     (* fix change superlift with a real name *)
 993
 994   let l_context = superlift context 1 in
 995   let hyps = filter_real_hyp l_context l_context in
 996
 997   debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
 998
 999   let lineq =ref [] in
1000
1001   (* transform hyps into inequations *)
1002
1003   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1004                         with _-> ())
1005               hyps;
1006
1007
1008   debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1009          " disequazioni\n");
1010
1011   let res=fourier_lineq (!lineq) in
1012   let tac=ref Tacticals.id_tac in
1013   if res=[] then
1014         (print_string "Tactic Fourier fails.\n";flush stdout;
1015          failwith "fourier_tac fails")
1016   else
1017   (
1018   match res with (*match res*)
1019   [(cres,sres,lc)]->
1020
1021      (* in lc we have the coefficient to "reduce" the system *)
1022
1023      print_string "Fourier's method can prove the goal...\n";flush stdout;
1024
1025      debug "I coeff di moltiplicazione rit sono: ";
1026
1027      let lutil=ref [] in
1028      List.iter
1029         (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1030            (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1031                                      )
1032         (List.combine (!lineq) lc);
1033
1034      print_string (" quindi lutil e' lunga "^
1035       string_of_int (List.length (!lutil))^"\n");
1036
1037      (* on construit la combinaison linéaire des inéquation *)
1038
1039      (match (!lutil) with (*match (!lutil) *)
1040        (h1,c1)::lutil ->
1041        debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1042
1043        let s=ref (h1.hstrict) in
1044
1045
1046        let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1047        let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1048
1049        List.iter (fun (h,c) ->
1050                s:=(!s)||(h.hstrict);
1051                t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1052                      [_Rmult;rational_to_real c;h.hleft ]  ]);
1053                t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1054                      [_Rmult;rational_to_real c;h.hright]  ]))
1055                lutil;
1056
1057        let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1058        let tc=rational_to_real cres in
1059
1060
1061 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1062
1063        debug "inizio a costruire tac1\n";
1064        Fourier.print_rational(c1);
1065
1066        let tac1=ref ( fun ~status ->
1067          if h1.hstrict then
1068            (Tacticals.thens
1069              ~start:(
1070               fun ~status ->
1071               debug ("inizio t1 strict\n");
1072               let curi,metasenv,pbo,pty = proof in
1073               let metano,context,ty = List.find
1074                (function (m,_,_) -> m=goal) metasenv in
1075               debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1076               debug ("ty = "^ CicPp.ppterm ty^"\n");
1077               PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1078             ~continuations:[tac_use h1;tac_zero_inf_pos
1079              (rational_to_fraction c1)]
1080             ~status
1081            )
1082            else
1083            (Tacticals.thens
1084              ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1085              ~continuations:[tac_use h1;tac_zero_inf_pos
1086               (rational_to_fraction c1)] ~status
1087            )
1088          )
1089
1090        in
1091        s:=h1.hstrict;
1092        List.iter (fun (h,c) ->
1093          (if (!s) then
1094            (if h.hstrict then
1095              (debug("tac1 1\n");
1096              tac1:=(Tacticals.thens
1097                ~start:(PrimitiveTactics.apply_tac
1098                 ~term:_Rfourier_lt_lt)
1099                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1100                 (rational_to_fraction c)])
1101              )
1102            else
1103              (debug("tac1 2\n");
1104              Fourier.print_rational(c1);
1105              tac1:=(Tacticals.thens
1106               ~start:(
1107                 fun ~status ->
1108                 debug("INIZIO TAC 1 2\n");
1109                 let curi,metasenv,pbo,pty = proof in
1110                 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1111                  metasenv in
1112                 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1113                 debug ("ty = "^ CicPp.ppterm ty^"\n");
1114                 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1115               ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1116                 (rational_to_fraction c)])
1117              )
1118            )
1119          else
1120            (if h.hstrict then
1121              (debug("tac1 3\n");
1122              tac1:=(Tacticals.thens
1123                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1124                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1125                 (rational_to_fraction c)])
1126              )
1127            else
1128              (debug("tac1 4\n");
1129              tac1:=(Tacticals.thens
1130                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1131                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1132                 (rational_to_fraction c)])
1133              )
1134            )
1135          );
1136          s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1137
1138        let tac2 =
1139          if sres then
1140            tac_zero_inf_false goal (rational_to_fraction cres)
1141          else
1142            tac_zero_infeq_false goal (rational_to_fraction cres)
1143        in
1144        tac:=(Tacticals.thens
1145          ~start:(my_cut ~term:ineq)
1146          ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
1147            ~start:(fun ~status:(proof,goal as status) ->
1148              let curi,metasenv,pbo,pty = proof in
1149              let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1150               metasenv in
1151              PrimitiveTactics.change_tac ~what:ty
1152               ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1153            ~continuation:(Tacticals.then_
1154              ~start:(PrimitiveTactics.apply_tac ~term:
1155                (if sres then _Rnot_lt_lt else _Rnot_le_le))
1156              ~continuation:(Tacticals.thens
1157                ~start:(
1158                  fun ~status ->
1159                  debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1160                  let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1161                   ~status
1162                  in
1163                  (match r with (p,gl) ->
1164                    debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1165                  r)
1166                ~continuations:[(Tacticals.thens
1167                  ~start:(
1168                    fun ~status ->
1169                    let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1170                    (match r with (p,gl) ->
1171                      debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1172                    r)
1173                  ~continuations:
1174                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1175                  ;Tacticals.try_tactics
1176                    ~tactics:[ "ring", (fun ~status ->
1177                                         debug("begin RING\n");
1178                                         let r = Ring.ring_tac  ~status in
1179                                         debug ("end RING\n");
1180                                         r)
1181                         ; "id", Tacticals.id_tac]
1182                  ])
1183                ;(*Tacticals.id_tac*)
1184                 Tacticals.then_
1185                  ~start:
1186                   (
1187                   fun ~status:(proof,goal as status) ->
1188                    let curi,metasenv,pbo,pty = proof in
1189                    let metano,context,ty = List.find (function (m,_,_) -> m=
1190                     goal) metasenv in
1191                    (* check if ty is of type *)
1192                    let w1 =
1193                      debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1194                      (match ty with
1195                      (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*)
1196                      Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1197                      |_ -> assert false)
1198                    in
1199                    let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1200                    debug("fine MY_CHNGE\n");
1201                    r
1202
1203                   )
1204                  ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1205          ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1206        (*tac:=(Tacticals.thens
1207          ~start:(PrimitiveTactics.cut_tac ~term:_False)
1208          ~continuations:[Tacticals.then_
1209            ~start:(PrimitiveTactics.intros_tac ~name:"??")
1210            ~continuation:contradiction_tac
1211          ;!tac]) FIXED - this was useless*)
1212         (* tac:=!tac*)
1213
1214
1215     |_-> assert false)(*match (!lutil) *)
1216   |_-> assert false); (*match res*)
1217   debug ("finalmente applico tac\n");
1218   (
1219   let r = !tac ~status:(proof,goal) in
1220   debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1221
1222   )
1223 ;;
1224
1225 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
1226
1227