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   | _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
 487 ;;
 488
 489
 490 let int_to_real n =
 491    let x = int_to_real_aux (abs n) in
 492    if n < 0 then
 493         Cic.Appl [ _Ropp ; x ]
 494    else
 495         x
 496 ;;
 497
 498
 499 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 500 *)
 501
 502 let rational_to_real x =
 503    let (n,d)=rational_to_fraction x in
 504    Cic.Appl [ _Rmult ; int_to_real n ; Cic.Appl [ _Rinv ; int_to_real d ]  ]
 505 ;;
 506
 507 (* preuve que 0<n*1/d
 508 *)
 509
 510
 511 (*
 512 let tac_zero_inf_pos gl (n,d) =
 513    (*let cste = pf_parse_constr gl in*)
 514    let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 515    let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 516    for i=1 to n-1 do
 517        tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
 518    for i=1 to d-1 do
 519        tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
 520    (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
 521 ;;*)
 522 let tac_zero_inf_pos (n,d) ~status =
 523    (*let cste = pf_parse_constr gl in*)
 524    let pall str ~status:(proof,goal) t =
 525      debug ("tac "^str^" :\n" );
 526      let curi,metasenv,pbo,pty = proof in
 527      let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 528      debug ("th = "^ CicPp.ppterm t ^"\n");
 529      debug ("ty = "^ CicPp.ppterm ty^"\n");
 530    in
 531    let tacn=ref
 532      (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
 533    let tacd=ref
 534      (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
 535
 536
 537   for i=1 to n-1 do
 538        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;
 539    for i=1 to d-1 do
 540        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;
 541
 542
 543
 544 debug("TAC ZERO INF POS\n");
 545
 546 (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
 547   ~continuations:[
 548    !tacn ;
 549    !tacd ]
 550   ~status)
 551 ;;
 552
 553
 554
 555 (* preuve que 0<=n*1/d
 556 *)
 557
 558 let tac_zero_infeq_pos gl (n,d) =
 559    (*let cste = pf_parse_constr gl in*)
 560    let tacn = ref (if n=0 then
 561         (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
 562         else
 563         (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ))
 564    in
 565    let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
 566    for i=1 to n-1 do
 567        tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_zero_pos_plus1) ~continuation:!tacn); done;
 568    for i=1 to d-1 do
 569        tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
 570    (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd])
 571 ;;
 572
 573
 574
 575 (* preuve que 0<(-n)*(1/d) => False
 576 *)
 577
 578 let tac_zero_inf_false gl (n,d) =
 579     if n=0 then (PrimitiveTactics.apply_tac ~term:_Rnot_lt0)
 580     else
 581      (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rle_not_lt)
 582               ~continuation:(tac_zero_infeq_pos gl (-n,d)))
 583 ;;
 584
 585 (* preuve que 0<=(-n)*(1/d) => False
 586 *)
 587
 588 let tac_zero_infeq_false gl (n,d) =
 589      (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
 590               ~continuation:(tac_zero_inf_pos (-n,d)))
 591 ;;
 592
 593
 594 (* *********** ********** ******** ??????????????? *********** **************)
 595
 596 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
 597   let curi,metasenv,pbo,pty = proof in
 598   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 599   let fresh_meta = ProofEngineHelpers.new_meta proof in
 600   let irl =
 601    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 602   let metasenv' = (fresh_meta,context,t)::metasenv in
 603    let proof' = curi,metasenv',pbo,pty in
 604     let proof'',goals =
 605      PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) ~status:(proof',goal)
 606     in
 607      proof'',fresh_meta::goals
 608 ;;
 609
 610
 611
 612
 613
 614 let my_cut ~term:c ~status:(proof,goal)=
 615   let curi,metasenv,pbo,pty = proof in
 616   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 617
 618   let fresh_meta = ProofEngineHelpers.new_meta proof in
 619   let irl =
 620    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 621   let metasenv' = (fresh_meta,context,c)::metasenv in
 622    let proof' = curi,metasenv',pbo,pty in
 623     let proof'',goals =
 624      apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] ~status:(proof',goal)
 625     in
 626      (* We permute the generated goals to be consistent with Coq *)
 627      match goals with
 628         [] -> assert false
 629       | he::tl -> proof'',he::fresh_meta::tl
 630 ;;
 631
 632
 633 let exact = PrimitiveTactics.exact_tac;;
 634
 635 let tac_use h ~status:(proof,goal as status) =
 636 debug("Inizio TC_USE\n");
 637 let curi,metasenv,pbo,pty = proof in
 638 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 639 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
 640 debug ("ty = "^ CicPp.ppterm ty^"\n");
 641
 642 let res =
 643 match h.htype with
 644   "Rlt" -> exact ~term:h.hname ~status
 645   |"Rle" -> exact ~term:h.hname ~status
 646   |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
 647       ~continuation:(exact ~term:h.hname)) ~status
 648   |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
 649       ~continuation:(exact ~term:h.hname)) ~status
 650   |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
 651       ~continuation:(exact ~term:h.hname)) ~status
 652   |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
 653       ~continuation:(exact ~term:h.hname)) ~status
 654   |_->assert false
 655 in
 656 debug("Fine TAC_USE\n");
 657 res
 658 ;;
 659
 660
 661
 662 let is_ineq (h,t) =
 663     match t with
 664        Cic.Appl ( Cic.Const(u,boh)::next) ->
 665          (match (UriManager.string_of_uri u) with
 666                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
 667                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
 668                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
 669                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
 670                 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
 671                    (match (List.hd next) with
 672                        Cic.Const (uri,_) when
 673                         UriManager.string_of_uri uri =
 674                         "cic:/Coq/Reals/Rdefinitions/R.con" -> true
 675                      | _ -> false)
 676                 |_->false)
 677      |_->false
 678 ;;
 679
 680 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 681
 682 let mkAppL a =
 683    Cic.Appl(Array.to_list a)
 684 ;;
 685
 686 (* Résolution d'inéquations linéaires dans R *)
 687 let rec strip_outer_cast c = match c with
 688   | Cic.Cast (c,_) -> strip_outer_cast c
 689   | _ -> c
 690 ;;
 691
 692 let find_in_context id context =
 693   let rec find_in_context_aux c n =
 694         match c with
 695         [] -> failwith (id^" not found in context")
 696         | a::next -> (match a with
 697                         Some (Cic.Name(name),_) when name = id -> n
 698                               (*? magari al posto di _ qualcosaltro?*)
 699                         | _ -> find_in_context_aux next (n+1))
 700   in
 701   find_in_context_aux context 1
 702 ;;
 703
 704 (* mi sembra quadratico *)
 705 let rec filter_real_hyp context cont =
 706   match context with
 707   [] -> []
 708   | Some(Cic.Name(h),Cic.Decl(t))::next -> (
 709                                 let n = find_in_context h cont in
 710                         [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
 711   | a::next -> debug("  no\n"); filter_real_hyp next cont
 712 ;;
 713
 714 (* lifts everithing at the conclusion level *)
 715 let rec superlift c n=
 716   match c with
 717   [] -> []
 718   | Some(name,Cic.Decl(a))::next  -> [Some(name,Cic.Decl(CicSubstitution.lift n a))] @ superlift next (n+1)
 719   | Some(name,Cic.Def(a))::next   -> [Some(name,Cic.Def(CicSubstitution.lift n a))] @ superlift next (n+1)
 720   | _::next -> superlift next (n+1) (*??  ??*)
 721
 722 ;;
 723
 724 (* fix !!!!!!!!!!  this may not work *)
 725 let equality_replace a b ~status =
 726   let proof,goal = status in
 727   let curi,metasenv,pbo,pty = proof in
 728   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 729 prerr_endline ("<MY_CUT: " ^ CicPp.ppterm a ^ " <=> " ^ CicPp.ppterm b) ;
 730 prerr_endline ("### IN MY_CUT: ") ;
 731 prerr_endline ("@ " ^ CicPp.ppterm ty) ;
 732 List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ;
 733 prerr_endline ("##- IN MY_CUT ") ;
 734 let res =
 735         let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in
 736 (*CSC: codice ad-hoc per questo caso!!! Non funge in generale *)
 737         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
 738 in
 739 prerr_endline "EUREKA" ;
 740 res
 741 ;;
 742
 743 let tcl_fail a ~status:(proof,goal) =
 744         match a with
 745         1 -> raise (ProofEngineTypes.Fail "fail-tactical")
 746         |_-> (proof,[goal])
 747 ;;
 748
 749
 750 let assumption_tac ~status:(proof,goal)=
 751   let curi,metasenv,pbo,pty = proof in
 752   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 753   let num = ref 0 in
 754   let tac_list = List.map
 755         ( fun x -> num := !num + 1;
 756                    match x with
 757                         Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
 758                         | _ -> ("fake",tcl_fail 1)
 759         )
 760         context
 761   in
 762   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
 763 ;;
 764
 765 (* !!!!! fix !!!!!!!!!! *)
 766 let contradiction_tac ~status:(proof,goal)=
 767         Tacticals.then_
 768                 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
 769                 ~continuation:(Tacticals.then_
 770                         ~start:(Ring.elim_type_tac ~term:_False)
 771                         ~continuation:(assumption_tac))
 772         ~status:(proof,goal)
 773 ;;
 774
 775 (* ********************* TATTICA ******************************** *)
 776
 777 let rec fourier ~status:(s_proof,s_goal)=
 778   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
 779   let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) s_metasenv in
 780
 781   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
 782   debug_pcontext s_context;
 783
 784   let fhyp = String.copy "new_hyp_for_fourier" in
 785
 786    (* here we need to negate the thesis, but to do this we nned to apply the right theoreme,
 787       so let's parse our thesis *)
 788
 789   let th_to_appl = ref _Rfourier_not_le_gt in
 790   (match s_ty with
 791         Cic.Appl ( Cic.Const(u,boh)::args) ->
 792                 (match UriManager.string_of_uri u with
 793                          "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := _Rfourier_not_ge_lt
 794                         |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := _Rfourier_not_gt_le
 795                         |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := _Rfourier_not_le_gt
 796                         |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := _Rfourier_not_lt_ge
 797                         |_-> failwith "fourier can't be applyed")
 798         |_-> failwith "fourier can't be applyed"); (* fix maybe strip_outer_cast goes here?? *)
 799
 800    (* now let's change our thesis applying the th and put it with hp *)
 801
 802    let proof,gl = Tacticals.then_
 803         ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
 804         ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
 805                 ~status:(s_proof,s_goal) in
 806    let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in
 807
 808    debug ("port la tesi sopra e la nego. contesto :\n");
 809    debug_pcontext s_context;
 810
 811    (* now we have all the right environment *)
 812
 813    let curi,metasenv,pbo,pty = proof in
 814    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 815
 816
 817    (* now we want to convert hp to inequations, but first we must lift
 818       everyting to thesis level, so that a variable has the save Rel(n)
 819       in each hp ( needed by ineq1_of_term ) *)
 820
 821     (* ? fix if None  ?????*)
 822     (* fix change superlift with a real name *)
 823
 824   let l_context = superlift context 1 in
 825   let hyps = filter_real_hyp l_context l_context in
 826
 827   debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
 828
 829   let lineq =ref [] in
 830
 831   (* transform hyps into inequations *)
 832
 833   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
 834                         with _-> ())
 835               hyps;
 836
 837
 838   debug ("applico fourier a "^ string_of_int (List.length !lineq)^" disequazioni\n");
 839
 840   let res=fourier_lineq (!lineq) in
 841   let tac=ref Ring.id_tac in
 842   if res=[] then
 843         (print_string "Tactic Fourier fails.\n";flush stdout;failwith "fourier_tac fails")
 844   else
 845   (
 846   match res with (*match res*)
 847   [(cres,sres,lc)]->
 848
 849      (* in lc we have the coefficient to "reduce" the system *)
 850
 851      print_string "Fourier's method can prove the goal...\n";flush stdout;
 852
 853      debug "I coeff di moltiplicazione rit sono: ";
 854
 855      let lutil=ref [] in
 856      List.iter
 857         (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
 858                                      (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
 859                                      )
 860         (List.combine (!lineq) lc);
 861
 862      print_string (" quindi lutil e' lunga "^string_of_int (List.length (!lutil))^"\n");
 863
 864      (* on construit la combinaison linéaire des inéquation *)
 865
 866      (match (!lutil) with (*match (!lutil) *)
 867       (h1,c1)::lutil ->
 868
 869           debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
 870
 871           let s=ref (h1.hstrict) in
 872
 873           (*  let t1=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hleft|]) in
 874               let t2=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hright|]) in
 875           *)
 876
 877           let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
 878           let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
 879
 880           List.iter (fun (h,c) ->
 881                s:=(!s)||(h.hstrict);
 882                t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl [_Rmult;rational_to_real c;h.hleft ]  ]);
 883                t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl [_Rmult;rational_to_real c;h.hright]  ]))
 884                lutil;
 885
 886           let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
 887           let tc=rational_to_real cres in
 888
 889
 890           (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
 891
 892           debug "inizio a costruire tac1\n";
 893           Fourier.print_rational(c1);
 894
 895           let tac1=ref ( fun ~status ->
 896                         debug ("Sotto tattica t1 "^(if h1.hstrict then "strict" else "lasc")^"\n");
 897                         if h1.hstrict then
 898                             (Tacticals.thens ~start:(
 899                             fun ~status ->
 900                             debug ("inizio t1 strict\n");
 901                             let curi,metasenv,pbo,pty = proof in
 902                             let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 903                             debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
 904                             debug ("ty = "^ CicPp.ppterm ty^"\n");
 905
 906                             PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
 907                                              ~continuations:[tac_use h1;
 908
 909                                                 Ring.id_tac] ~status
 910
 911                                              (*tac_zero_inf_pos (rational_to_fraction c1)] ~status*)
 912
 913                                              )
 914                          else
 915                             (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
 916                                              ~continuations:[tac_use h1;tac_zero_inf_pos                                                 (rational_to_fraction c1)] ~status))
 917
 918           in
 919           s:=h1.hstrict;
 920
 921           List.iter (fun (h,c) ->
 922                (if (!s) then
 923                     (if h.hstrict then
 924                         (debug("tac1 1\n");
 925                         tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
 926                                                         ~term:_Rfourier_lt_lt)
 927                                                ~continuations:[!tac1;tac_use h;
 928                                                        tac_zero_inf_pos
 929                                                        (rational_to_fraction c)]))
 930                     else
 931                     (
 932                         debug("tac1 2\n");
 933                         Fourier.print_rational(c1);
 934                         tac1:=(Tacticals.thens ~start:(
 935                                         fun ~status ->
 936                                         debug("INIZIO TAC 1 2\n");
 937
 938                                         let curi,metasenv,pbo,pty = proof in
 939                                         let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 940                                         debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
 941                                         debug ("ty = "^ CicPp.ppterm ty^"\n");
 942
 943                                         PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status
 944
 945                                                        )
 946                                                ~continuations:[!tac1;tac_use h;
 947
 948                                                        Ring.id_tac
 949                                                        (*tac_zero_inf_pos
 950                                                        (rational_to_fraction c)*)
 951
 952                                                        ]))
 953                     )
 954                 else
 955                     (if h.hstrict then
 956                         (
 957
 958                         debug("tac1 3\n");
 959                         tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
 960                                                ~continuations:[!tac1;tac_use h;
 961                                                        tac_zero_inf_pos
 962                                                        (rational_to_fraction c)]))
 963                     else
 964                         (
 965                         debug("tac1 4\n");
 966                         tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
 967                                                ~continuations:[!tac1;tac_use h;
 968                                                        tac_zero_inf_pos
 969                                                        (rational_to_fraction c)]))
 970
 971                                                        )
 972                                                       );
 973               s:=(!s)||(h.hstrict))
 974               lutil;(*end List.iter*)
 975
 976            let tac2= if sres then
 977                           tac_zero_inf_false goal (rational_to_fraction cres)
 978                       else
 979                           tac_zero_infeq_false goal (rational_to_fraction cres)
 980            in
 981            tac:=(Tacticals.thens ~start:(my_cut ~term:ineq)
 982                      ~continuations:[Tacticals.then_  (* ?????????????????????????????? *)
 983                         ~start:(fun ~status:(proof,goal as status) ->
 984                                  let curi,metasenv,pbo,pty = proof in
 985                                  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 986                                   PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status)
 987                         ~continuation:(Tacticals.then_
 988                                 ~start:(PrimitiveTactics.apply_tac
 989                                                 ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
 990                                 ~continuation:Ring.id_tac
 991 (*CSC
 992                                 ~continuation:(Tacticals.thens
 993                                                 ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
 994                                                 ~continuations:[tac2;(Tacticals.thens
 995                                                         ~start:(equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
 996                                                         ~continuations:
 997 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...    *)
 998                                         [Tacticals.try_tactics
 999                                                 (* ???????????????????????????? *)
1000                                                 ~tactics:[ "ring", Ring.ring_tac  ; "id", Ring.id_tac]
1001                                         ;
1002                                         Tacticals.then_
1003                                                 ~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
1004                                                 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
1005                                         ]
1006
1007                                          )
1008                                                 ] (* end continuations before comment *)
1009                                         ) *)
1010                                 );
1011                        !tac1]
1012                 );(*end tac:=*)
1013            tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False)
1014                                  ~continuations:[Tacticals.then_
1015                                         (* ???????????????????????????????
1016                                            in coq era intro *)
1017                                         ~start:(PrimitiveTactics.intros_tac ~name:(String.copy "??"))
1018                                         (* ????????????????????????????? *)
1019
1020                                         ~continuation:contradiction_tac;!tac])
1021
1022
1023       |_-> assert false)(*match (!lutil) *)
1024   |_-> assert false); (*match res*)
1025
1026   debug ("finalmente applico tac\n");
1027   (!tac ~status:(proof,goal))
1028
1029 ;;
1030
1031 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
1032