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