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