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