helm/gTopLevel/fourierR.ml

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