helm/gTopLevel/fourierR.ml

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