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