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