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