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 Term
  33 open Tactics
  34 open Clenv
  35 open Names
  36 open Tacmach*)
  37 open Fourier
  38
  39 (******************************************************************************
  40 Opérations sur les combinaisons linéaires affines.
  41 La partie homogène d'une combinaison linéaire est en fait une table de hash
  42 qui donne le coefficient d'un terme du calcul des constructions,
  43 qui est zéro si le terme n'y est pas.
  44 *)
  45
  46 (*type flin = {fhom:(constr , rational)Hashtbl.t;
  47              fcste:rational};;
  48
  49 let flin_zero () = {fhom=Hashtbl.create 50;fcste=r0};;
  50
  51 let flin_coef f x = try (Hashtbl.find f.fhom x) with _-> r0;;
  52
  53 let flin_add f x c =
  54     let cx = flin_coef f x in
  55     Hashtbl.remove f.fhom x;
  56     Hashtbl.add f.fhom x (rplus cx c);
  57     f
  58 ;;
  59 let flin_add_cste f c =
  60     {fhom=f.fhom;
  61      fcste=rplus f.fcste c}
  62 ;;
  63
  64 let flin_one () = flin_add_cste (flin_zero()) r1;;
  65
  66 let flin_plus f1 f2 =
  67     let f3 = flin_zero() in
  68     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
  69     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f2.fhom;
  70     flin_add_cste (flin_add_cste f3 f1.fcste) f2.fcste;
  71 ;;
  72
  73 let flin_minus f1 f2 =
  74     let f3 = flin_zero() in
  75     Hashtbl.iter (fun x c -> let _=flin_add f3 x c in ()) f1.fhom;
  76     Hashtbl.iter (fun x c -> let _=flin_add f3 x (rop c) in ()) f2.fhom;
  77     flin_add_cste (flin_add_cste f3 f1.fcste) (rop f2.fcste);
  78 ;;
  79 let flin_emult a f =
  80     let f2 = flin_zero() in
  81     Hashtbl.iter (fun x c -> let _=flin_add f2 x (rmult a c) in ()) f.fhom;
  82     flin_add_cste f2 (rmult a f.fcste);
  83 ;;*)
  84
  85 (*****************************************************************************)
  86 (*let parse_ast   = Pcoq.parse_string Pcoq.Constr.constr;;
  87 let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);;
  88 let pf_parse_constr gl s =
  89    Astterm.interp_constr Evd.empty (pf_env gl) (parse_ast s);;
  90
  91 let rec string_of_constr c =
  92  match kind_of_term c with
  93    Cast (c,t) -> string_of_constr c
  94   |Const c -> string_of_path c
  95   |Var(c) -> string_of_id c
  96   | _ -> "not_of_constant"
  97 ;;
  98
  99 let rec rational_of_constr c =
 100   match kind_of_term c with
 101   | Cast (c,t) -> (rational_of_constr c)
 102   | App (c,args) ->
 103         (match kind_of_term c with
 104            Const c ->
 105                (match (string_of_path c) with
 106                  "Coq.Reals.Rdefinitions.Ropp" ->
 107                       rop (rational_of_constr args.(0))
 108                 |"Coq.Reals.Rdefinitions.Rinv" ->
 109                       rinv (rational_of_constr args.(0))
 110                 |"Coq.Reals.Rdefinitions.Rmult" ->
 111                       rmult (rational_of_constr args.(0))
 112                             (rational_of_constr args.(1))
 113                 |"Coq.Reals.Rdefinitions.Rdiv" ->
 114                       rdiv (rational_of_constr args.(0))
 115                             (rational_of_constr args.(1))
 116                 |"Coq.Reals.Rdefinitions.Rplus" ->
 117                       rplus (rational_of_constr args.(0))
 118                             (rational_of_constr args.(1))
 119                 |"Coq.Reals.Rdefinitions.Rminus" ->
 120                       rminus (rational_of_constr args.(0))
 121                              (rational_of_constr args.(1))
 122                 | _ -> failwith "not a rational")
 123           | _ -> failwith "not a rational")
 124   | Const c ->
 125         (match (string_of_path c) with
 126                "Coq.Reals.Rdefinitions.R1" -> r1
 127               |"Coq.Reals.Rdefinitions.R0" -> r0
 128               |  _ -> failwith "not a rational")
 129   |  _ -> failwith "not a rational"
 130 ;;
 131
 132 let rec flin_of_constr c =
 133   try(
 134     match kind_of_term c with
 135   | Cast (c,t) -> (flin_of_constr c)
 136   | App (c,args) ->
 137         (match kind_of_term c with
 138            Const c ->
 139             (match (string_of_path c) with
 140              "Coq.Reals.Rdefinitions.Ropp" ->
 141                   flin_emult (rop r1) (flin_of_constr args.(0))
 142             |"Coq.Reals.Rdefinitions.Rplus"->
 143                   flin_plus (flin_of_constr args.(0))
 144                             (flin_of_constr args.(1))
 145             |"Coq.Reals.Rdefinitions.Rminus"->
 146                   flin_minus (flin_of_constr args.(0))
 147                              (flin_of_constr args.(1))
 148             |"Coq.Reals.Rdefinitions.Rmult"->
 149              (try (let a=(rational_of_constr args.(0)) in
 150                    try (let b = (rational_of_constr args.(1)) in
 151                             (flin_add_cste (flin_zero()) (rmult a b)))
 152                    with _-> (flin_add (flin_zero())
 153                              args.(1)
 154                              a))
 155               with _-> (flin_add (flin_zero())
 156                                  args.(0)
 157                                  (rational_of_constr args.(1))))
 158             |"Coq.Reals.Rdefinitions.Rinv"->
 159                let a=(rational_of_constr args.(0)) in
 160                flin_add_cste (flin_zero()) (rinv a)
 161             |"Coq.Reals.Rdefinitions.Rdiv"->
 162               (let b=(rational_of_constr args.(1)) in
 163                try (let a = (rational_of_constr args.(0)) in
 164                        (flin_add_cste (flin_zero()) (rdiv a b)))
 165                with _-> (flin_add (flin_zero())
 166                              args.(0)
 167                              (rinv b)))
 168             |_->assert false)
 169            |_ -> assert false)
 170   | Const c ->
 171         (match (string_of_path c) with
 172                "Coq.Reals.Rdefinitions.R1" -> flin_one ()
 173               |"Coq.Reals.Rdefinitions.R0" -> flin_zero ()
 174               |_-> assert false)
 175   |_-> assert false)
 176   with _ -> flin_add (flin_zero())
 177                      c
 178                      r1
 179 ;;
 180
 181 let flin_to_alist f =
 182     let res=ref [] in
 183     Hashtbl.iter (fun x c -> res:=(c,x)::(!res)) f;
 184     !res
 185 ;;*)
 186
 187 (* Représentation des hypothèses qui sont des inéquations ou des équations.
 188 *)
 189 (*type hineq={hname:constr; (* le nom de l'hypothèse *)
 190             htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
 191             hleft:constr;
 192             hright:constr;
 193             hflin:flin;
 194             hstrict:bool}
 195 ;;*)
 196
 197 (* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
 198 *)
 199 (*let ineq1_of_constr (h,t) =
 200     match (kind_of_term t) with
 201        App (f,args) ->
 202          let t1= args.(0) in
 203          let t2= args.(1) in
 204          (match kind_of_term f with
 205            Const c ->
 206             (match (string_of_path c) with
 207                  "Coq.Reals.Rdefinitions.Rlt" -> [{hname=h;
 208                            htype="Rlt";
 209                            hleft=t1;
 210                            hright=t2;
 211                            hflin= flin_minus (flin_of_constr t1)
 212                                              (flin_of_constr t2);
 213                            hstrict=true}]
 214                 |"Coq.Reals.Rdefinitions.Rgt" -> [{hname=h;
 215                            htype="Rgt";
 216                            hleft=t2;
 217                            hright=t1;
 218                            hflin= flin_minus (flin_of_constr t2)
 219                                              (flin_of_constr t1);
 220                            hstrict=true}]
 221                 |"Coq.Reals.Rdefinitions.Rle" -> [{hname=h;
 222                            htype="Rle";
 223                            hleft=t1;
 224                            hright=t2;
 225                            hflin= flin_minus (flin_of_constr t1)
 226                                              (flin_of_constr t2);
 227                            hstrict=false}]
 228                 |"Coq.Reals.Rdefinitions.Rge" -> [{hname=h;
 229                            htype="Rge";
 230                            hleft=t2;
 231                            hright=t1;
 232                            hflin= flin_minus (flin_of_constr t2)
 233                                              (flin_of_constr t1);
 234                            hstrict=false}]
 235                 |_->assert false)
 236           | Ind (sp,i) ->
 237               (match (string_of_path sp) with
 238                  "Coq.Init.Logic_Type.eqT" ->  let t0= args.(0) in
 239                            let t1= args.(1) in
 240                            let t2= args.(2) in
 241                     (match (kind_of_term t0) with
 242                          Const c ->
 243                            (match (string_of_path c) with
 244                               "Coq.Reals.Rdefinitions.R"->
 245                          [{hname=h;
 246                            htype="eqTLR";
 247                            hleft=t1;
 248                            hright=t2;
 249                            hflin= flin_minus (flin_of_constr t1)
 250                                              (flin_of_constr t2);
 251                            hstrict=false};
 252                           {hname=h;
 253                            htype="eqTRL";
 254                            hleft=t2;
 255                            hright=t1;
 256                            hflin= flin_minus (flin_of_constr t2)
 257                                              (flin_of_constr t1);
 258                            hstrict=false}]
 259                            |_-> assert false)
 260                          |_-> assert false)
 261                    |_-> assert false)
 262           |_-> assert false)
 263         |_-> assert false
 264 ;;*)
 265
 266 (* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
 267 *)
 268
 269 (*let fourier_lineq lineq1 =
 270    let nvar=ref (-1) in
 271    let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
 272    List.iter (fun f ->
 273                Hashtbl.iter (fun x c ->
 274                                  try (Hashtbl.find hvar x;())
 275                                  with _-> nvar:=(!nvar)+1;
 276                                           Hashtbl.add hvar x (!nvar))
 277                             f.hflin.fhom)
 278              lineq1;
 279    let sys= List.map (fun h->
 280                let v=Array.create ((!nvar)+1) r0 in
 281                Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
 282                   h.hflin.fhom;
 283                ((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
 284              lineq1 in
 285    unsolvable sys
 286 ;;*)
 287
 288 (******************************************************************************
 289 Construction de la preuve en cas de succès de la méthode de Fourier,
 290 i.e. on obtient une contradiction.
 291 *)
 292
 293 (*let is_int x = (x.den)=1
 294 ;;*)
 295
 296 (* fraction = couple (num,den) *)
 297 (*let rec rational_to_fraction x= (x.num,x.den)
 298 ;;*)
 299
 300 (* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
 301 *)
 302 (*let int_to_real n =
 303    let nn=abs n in
 304    let s=ref "" in
 305    if nn=0
 306    then s:="R0"
 307    else (s:="R1";
 308         for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
 309    if n<0 then s:="(Ropp "^(!s)^")";
 310    !s
 311 ;;*)
 312 (* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
 313 *)
 314 (*let rational_to_real x =
 315    let (n,d)=rational_to_fraction x in
 316    ("(Rmult "^(int_to_real n)^" (Rinv "^(int_to_real d)^"))")
 317 ;;*)
 318
 319 (* preuve que 0<n*1/d
 320 *)
 321 (*let tac_zero_inf_pos gl (n,d) =
 322    let cste = pf_parse_constr gl in
 323    let tacn=ref (apply (cste "Rlt_zero_1")) in
 324    let tacd=ref (apply (cste "Rlt_zero_1")) in
 325    for i=1 to n-1 do
 326        tacn:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacn); done;
 327    for i=1 to d-1 do
 328        tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
 329    (tclTHENS (apply (cste "Rlt_mult_inv_pos")) [!tacn;!tacd])
 330 ;;*)
 331
 332 (* preuve que 0<=n*1/d
 333 *)
 334 (*let tac_zero_infeq_pos gl (n,d)=
 335    let cste = pf_parse_constr gl in
 336    let tacn=ref (if n=0
 337                  then (apply (cste "Rle_zero_zero"))
 338                  else (apply (cste "Rle_zero_1"))) in
 339    let tacd=ref (apply (cste "Rlt_zero_1")) in
 340    for i=1 to n-1 do
 341        tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
 342    for i=1 to d-1 do
 343        tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
 344    (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
 345 ;;*)
 346
 347 (* preuve que 0<(-n)*(1/d) => False
 348 *)
 349 (*let tac_zero_inf_false gl (n,d) =
 350    let cste = pf_parse_constr gl in
 351     if n=0 then (apply (cste "Rnot_lt0"))
 352     else
 353      (tclTHEN (apply (cste "Rle_not_lt"))
 354               (tac_zero_infeq_pos gl (-n,d)))
 355 ;;*)
 356
 357 (* preuve que 0<=(-n)*(1/d) => False
 358 *)
 359 (*let tac_zero_infeq_false gl (n,d) =
 360    let cste = pf_parse_constr gl in
 361      (tclTHEN (apply (cste "Rlt_not_le"))
 362               (tac_zero_inf_pos gl (-n,d)))
 363 ;;
 364
 365 let create_meta () = mkMeta(new_meta());;
 366
 367 let my_cut c gl=
 368      let concl = pf_concl gl in
 369        apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
 370 ;;
 371 let exact = exact_check;;
 372
 373 let tac_use h = match h.htype with
 374                "Rlt" -> exact h.hname
 375               |"Rle" -> exact h.hname
 376               |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
 377                                 (exact h.hname))
 378               |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
 379                                 (exact h.hname))
 380               |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
 381                                 (exact h.hname))
 382               |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
 383                                 (exact h.hname))
 384               |_->assert false
 385 ;;
 386
 387 let is_ineq (h,t) =
 388     match (kind_of_term t) with
 389        App (f,args) ->
 390          (match (string_of_constr f) with
 391                  "Coq.Reals.Rdefinitions.Rlt" -> true
 392                 |"Coq.Reals.Rdefinitions.Rgt" -> true
 393                 |"Coq.Reals.Rdefinitions.Rle" -> true
 394                 |"Coq.Reals.Rdefinitions.Rge" -> true
 395                 |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
 396                             "Coq.Reals.Rdefinitions.R"->true
 397                             |_->false)
 398                 |_->false)
 399      |_->false
 400 ;;
 401
 402 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 403
 404 let mkAppL a =
 405    let l = Array.to_list a in
 406    mkApp(List.hd l, Array.of_list (List.tl l))
 407 ;;*)
 408
 409 (* Résolution d'inéquations linéaires dans R *)
 410
 411 (*
 412 let rec fourier gl=
 413     let parse = pf_parse_constr gl in
 414     let goal = strip_outer_cast (pf_concl gl) in
 415     let fhyp=id_of_string "new_hyp_for_fourier" in
 416     (* si le but est une inéquation, on introduit son contraire,
 417        et le but à prouver devient False *)
 418     try (let tac =
 419      match (kind_of_term goal) with
 420       App (f,args) ->
 421       (match (string_of_constr f) with
 422              "Coq.Reals.Rdefinitions.Rlt" ->
 423                (tclTHEN
 424                  (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
 425                           (intro_using  fhyp))
 426                  fourier)
 427             |"Coq.Reals.Rdefinitions.Rle" ->
 428              (tclTHEN
 429               (tclTHEN (apply (parse "Rfourier_not_gt_le"))
 430                        (intro_using  fhyp))
 431                         fourier)
 432             |"Coq.Reals.Rdefinitions.Rgt" ->
 433              (tclTHEN
 434               (tclTHEN (apply (parse "Rfourier_not_le_gt"))
 435                        (intro_using  fhyp))
 436               fourier)
 437             |"Coq.Reals.Rdefinitions.Rge" ->
 438              (tclTHEN
 439               (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
 440                        (intro_using  fhyp))
 441               fourier)
 442             |_->assert false)
 443         |_->assert false
 444       in tac gl)
 445      with _ ->
 446 *)
 447     (* les hypothèses *)
 448
 449 (*
 450     let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
 451                         (list_of_sign (pf_hyps gl)) in
 452     let lineq =ref [] in
 453     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
 454                         with _-> ())
 455               hyps;
 456 *)
 457
 458     (* lineq = les inéquations découlant des hypothèses *)
 459
 460
 461 (*
 462     let res=fourier_lineq (!lineq) in
 463     let tac=ref tclIDTAC in
 464     if res=[]
 465     then (print_string "Tactic Fourier fails.\n";
 466                        flush stdout)
 467
 468 *)
 469     (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
 470
 471 (*
 472     else (match res with
 473         [(cres,sres,lc)]->
 474 *)
 475     (* lc=coefficients multiplicateurs des inéquations
 476        qui donnent 0<cres ou 0<=cres selon sres *)
 477         (*print_string "Fourier's method can prove the goal...";flush stdout;*)
 478
 479
 480 (*
 481           let lutil=ref [] in
 482           List.iter
 483             (fun (h,c) ->
 484                           if c<>r0
 485                           then (lutil:=(h,c)::(!lutil)(*;
 486                                 print_rational(c);print_string " "*)))
 487                     (List.combine (!lineq) lc);
 488
 489 *)
 490        (* on construit la combinaison linéaire des inéquation *)
 491
 492 (*
 493              (match (!lutil) with
 494           (h1,c1)::lutil ->
 495           let s=ref (h1.hstrict) in
 496           let t1=ref (mkAppL [|parse "Rmult";
 497                           parse (rational_to_real c1);
 498                           h1.hleft|]) in
 499           let t2=ref (mkAppL [|parse "Rmult";
 500                           parse (rational_to_real c1);
 501                           h1.hright|]) in
 502           List.iter (fun (h,c) ->
 503                s:=(!s)||(h.hstrict);
 504                t1:=(mkAppL [|parse "Rplus";
 505                              !t1;
 506                              mkAppL [|parse "Rmult";
 507                                       parse (rational_to_real c);
 508                                       h.hleft|] |]);
 509                t2:=(mkAppL [|parse "Rplus";
 510                              !t2;
 511                              mkAppL [|parse "Rmult";
 512                                       parse (rational_to_real c);
 513                                       h.hright|] |]))
 514                lutil;
 515           let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
 516                               !t1;
 517                               !t2 |] in
 518            let tc=parse (rational_to_real cres) in
 519 *)
 520        (* puis sa preuve *)
 521 (*
 522            let tac1=ref (if h1.hstrict
 523                          then (tclTHENS (apply (parse "Rfourier_lt"))
 524                                  [tac_use h1;
 525                                   tac_zero_inf_pos  gl
 526                                       (rational_to_fraction c1)])
 527                          else (tclTHENS (apply (parse "Rfourier_le"))
 528                                  [tac_use h1;
 529                                   tac_zero_inf_pos  gl
 530                                       (rational_to_fraction c1)])) in
 531            s:=h1.hstrict;
 532            List.iter (fun (h,c)->
 533              (if (!s)
 534               then (if h.hstrict
 535                     then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
 536                                [!tac1;tac_use h;
 537                                 tac_zero_inf_pos  gl
 538                                       (rational_to_fraction c)])
 539                     else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
 540                                [!tac1;tac_use h;
 541                                 tac_zero_inf_pos  gl
 542                                       (rational_to_fraction c)]))
 543               else (if h.hstrict
 544                     then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
 545                                [!tac1;tac_use h;
 546                                 tac_zero_inf_pos  gl
 547                                       (rational_to_fraction c)])
 548                     else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
 549                                [!tac1;tac_use h;
 550                                 tac_zero_inf_pos  gl
 551                                       (rational_to_fraction c)])));
 552              s:=(!s)||(h.hstrict))
 553               lutil;
 554            let tac2= if sres
 555                       then tac_zero_inf_false gl (rational_to_fraction cres)
 556                       else tac_zero_infeq_false gl (rational_to_fraction cres)
 557            in
 558            tac:=(tclTHENS (my_cut ineq)
 559                      [tclTHEN (change_in_concl
 560                                (mkAppL [| parse "not"; ineq|]
 561                                        ))
 562                       (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
 563                                                else parse "Rnot_le_le"))
 564                             (tclTHENS (Equality.replace
 565                                        (mkAppL [|parse "Rminus";!t2;!t1|]
 566                                                )
 567                                        tc)
 568                                [tac2;
 569                                 (tclTHENS (Equality.replace (parse "(Rinv R1)")
 570                                                            (parse "R1"))
 571 *)
 572 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...    *)
 573 (*
 574                                 [tclORELSE
 575                                    (Ring.polynom [])
 576                                    tclIDTAC;
 577                                           (tclTHEN (apply (parse "sym_eqT"))
 578                                                 (apply (parse "Rinv_R1")))]
 579
 580                                          )
 581                                 ]));
 582                        !tac1]);
 583            tac:=(tclTHENS (cut (parse "False"))
 584                                   [tclTHEN intro contradiction;
 585                                    !tac])
 586       |_-> assert false) |_-> assert false
 587           );
 588     ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
 589       (!tac gl)
 590       ((tclABSTRACT None !tac) gl)
 591
 592 ;;
 593
 594 let fourier_tac x gl =
 595      fourier gl
 596 ;;
 597
 598 let v_fourier = add_tactic "Fourier" fourier_tac
 599 *)
 600
 601 (*open CicReduction*)
 602 (*open PrimitiveTactics*)
 603 (*open ProofEngineTypes*)
 604 let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;
 605