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