helm/gTopLevel/fourierR.ml

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