helm/gTopLevel/fourierR.ml

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