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