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("\nTAC 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 =
 636 debug("Inizio TC_USE\n");
 637 let res =
 638 match h.htype with
 639   "Rlt" -> exact ~term:h.hname ~status
 640   |"Rle" -> exact ~term:h.hname ~status
 641   |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
 642       ~continuation:(exact ~term:h.hname)) ~status
 643   |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
 644       ~continuation:(exact ~term:h.hname)) ~status
 645   |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
 646       ~continuation:(exact ~term:h.hname)) ~status
 647   |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
 648       ~continuation:(exact ~term:h.hname)) ~status
 649   |_->assert false
 650 in
 651 debug("Fine TAC_USE");
 652 res
 653 ;;
 654
 655
 656
 657 let is_ineq (h,t) =
 658     match t with
 659        Cic.Appl ( Cic.Const(u,boh)::next) ->
 660          (match (UriManager.string_of_uri u) with
 661                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
 662                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
 663                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
 664                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
 665                 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
 666                    (match (List.hd next) with
 667                        Cic.Const (uri,_) when
 668                         UriManager.string_of_uri uri =
 669                         "cic:/Coq/Reals/Rdefinitions/R.con" -> true
 670                      | _ -> false)
 671                 |_->false)
 672      |_->false
 673 ;;
 674
 675 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 676
 677 let mkAppL a =
 678    Cic.Appl(Array.to_list a)
 679 ;;
 680
 681 (* Résolution d'inéquations linéaires dans R *)
 682 let rec strip_outer_cast c = match c with
 683   | Cic.Cast (c,_) -> strip_outer_cast c
 684   | _ -> c
 685 ;;
 686
 687 let find_in_context id context =
 688   let rec find_in_context_aux c n =
 689         match c with
 690         [] -> failwith (id^" not found in context")
 691         | a::next -> (match a with
 692                         Some (Cic.Name(name),_) when name = id -> n
 693                               (*? magari al posto di _ qualcosaltro?*)
 694                         | _ -> find_in_context_aux next (n+1))
 695   in
 696   find_in_context_aux context 1
 697 ;;
 698
 699 (* mi sembra quadratico *)
 700 let rec filter_real_hyp context cont =
 701   match context with
 702   [] -> []
 703   | Some(Cic.Name(h),Cic.Decl(t))::next -> (
 704                                 let n = find_in_context h cont in
 705                         [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
 706   | a::next -> debug("  no\n"); filter_real_hyp next cont
 707 ;;
 708
 709 (* lifts everithing at the conclusion level *)
 710 let rec superlift c n=
 711   match c with
 712   [] -> []
 713   | Some(name,Cic.Decl(a))::next  -> [Some(name,Cic.Decl(CicSubstitution.lift n a))] @ superlift next (n+1)
 714   | Some(name,Cic.Def(a))::next   -> [Some(name,Cic.Def(CicSubstitution.lift n a))] @ superlift next (n+1)
 715   | _::next -> superlift next (n+1) (*??  ??*)
 716
 717 ;;
 718
 719 (* fix !!!!!!!!!!  this may not work *)
 720 let equality_replace a b ~status =
 721   let proof,goal = status in
 722   let curi,metasenv,pbo,pty = proof in
 723   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 724 prerr_endline ("<MY_CUT: " ^ CicPp.ppterm a ^ " <=> " ^ CicPp.ppterm b) ;
 725 prerr_endline ("### IN MY_CUT: ") ;
 726 prerr_endline ("@ " ^ CicPp.ppterm ty) ;
 727 List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ;
 728 prerr_endline ("##- IN MY_CUT ") ;
 729 let res =
 730         let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in
 731 (*CSC: codice ad-hoc per questo caso!!! Non funge in generale *)
 732         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
 733 in
 734 prerr_endline "EUREKA" ;
 735 res
 736 ;;
 737
 738 let tcl_fail a ~status:(proof,goal) =
 739         match a with
 740         1 -> raise (ProofEngineTypes.Fail "fail-tactical")
 741         |_-> (proof,[goal])
 742 ;;
 743
 744
 745 let assumption_tac ~status:(proof,goal)=
 746   let curi,metasenv,pbo,pty = proof in
 747   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 748   let num = ref 0 in
 749   let tac_list = List.map
 750         ( fun x -> num := !num + 1;
 751                    match x with
 752                         Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
 753                         | _ -> ("fake",tcl_fail 1)
 754         )
 755         context
 756   in
 757   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
 758 ;;
 759
 760 (* !!!!! fix !!!!!!!!!! *)
 761 let contradiction_tac ~status:(proof,goal)=
 762         Tacticals.then_
 763                 ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
 764                 ~continuation:(Tacticals.then_
 765                         ~start:(Ring.elim_type_tac ~term:_False)
 766                         ~continuation:(assumption_tac))
 767         ~status:(proof,goal)
 768 ;;
 769
 770 (* ********************* TATTICA ******************************** *)
 771
 772 let rec fourier ~status:(s_proof,s_goal)=
 773   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
 774   let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) s_metasenv in
 775
 776   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
 777   debug_pcontext s_context;
 778
 779   let fhyp = String.copy "new_hyp_for_fourier" in
 780
 781    (* here we need to negate the thesis, but to do this we nned to apply the right theoreme,
 782       so let's parse our thesis *)
 783
 784   let th_to_appl = ref _Rfourier_not_le_gt in
 785   (match s_ty with
 786         Cic.Appl ( Cic.Const(u,boh)::args) ->
 787                 (match UriManager.string_of_uri u with
 788                          "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := _Rfourier_not_ge_lt
 789                         |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := _Rfourier_not_gt_le
 790                         |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := _Rfourier_not_le_gt
 791                         |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := _Rfourier_not_lt_ge
 792                         |_-> failwith "fourier can't be applyed")
 793         |_-> failwith "fourier can't be applyed"); (* fix maybe strip_outer_cast goes here?? *)
 794
 795    (* now let's change our thesis applying the th and put it with hp *)
 796
 797    let proof,gl = Tacticals.then_
 798         ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
 799         ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
 800                 ~status:(s_proof,s_goal) in
 801    let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in
 802
 803    debug ("port la tesi sopra e la nego. contesto :\n");
 804    debug_pcontext s_context;
 805
 806    (* now we have all the right environment *)
 807
 808    let curi,metasenv,pbo,pty = proof in
 809    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 810
 811
 812    (* now we want to convert hp to inequations, but first we must lift
 813       everyting to thesis level, so that a variable has the save Rel(n)
 814       in each hp ( needed by ineq1_of_term ) *)
 815
 816     (* ? fix if None  ?????*)
 817     (* fix change superlift with a real name *)
 818
 819   let l_context = superlift context 1 in
 820   let hyps = filter_real_hyp l_context l_context in
 821
 822   debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
 823
 824   let lineq =ref [] in
 825
 826   (* transform hyps into inequations *)
 827
 828   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
 829                         with _-> ())
 830               hyps;
 831
 832
 833   debug ("applico fourier a "^ string_of_int (List.length !lineq)^" disequazioni\n");
 834
 835   let res=fourier_lineq (!lineq) in
 836   let tac=ref Ring.id_tac in
 837   if res=[] then
 838         (print_string "Tactic Fourier fails.\n";flush stdout;failwith "fourier_tac fails")
 839   else
 840   (
 841   match res with (*match res*)
 842   [(cres,sres,lc)]->
 843
 844      (* in lc we have the coefficient to "reduce" the system *)
 845
 846      print_string "Fourier's method can prove the goal...\n";flush stdout;
 847
 848      debug "I coeff di moltiplicazione rit sono: ";
 849
 850      let lutil=ref [] in
 851      List.iter
 852         (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
 853                                      (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
 854                                      )
 855         (List.combine (!lineq) lc);
 856
 857      print_string (" quindi lutil e' lunga "^string_of_int (List.length (!lutil))^"\n");
 858
 859      (* on construit la combinaison linéaire des inéquation *)
 860
 861      (match (!lutil) with (*match (!lutil) *)
 862       (h1,c1)::lutil ->
 863
 864           debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
 865
 866           let s=ref (h1.hstrict) in
 867
 868           (*  let t1=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hleft|]) in
 869               let t2=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hright|]) in
 870           *)
 871
 872           let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
 873           let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
 874
 875           List.iter (fun (h,c) ->
 876                s:=(!s)||(h.hstrict);
 877                t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl [_Rmult;rational_to_real c;h.hleft ]  ]);
 878                t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl [_Rmult;rational_to_real c;h.hright]  ]))
 879                lutil;
 880
 881           let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
 882           let tc=rational_to_real cres in
 883
 884
 885           (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
 886
 887           debug "inizio a costruire tac1\n";
 888
 889           let tac1=ref ( fun ~status ->
 890                         debug "Sotto tattica t1\n";
 891                         if h1.hstrict then
 892                             (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt)
 893                                              ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status)
 894                          else
 895                             (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
 896                                              ~continuations:[tac_use h1;tac_zero_inf_pos                                                 (rational_to_fraction c1)] ~status))
 897
 898           in
 899           s:=h1.hstrict;
 900
 901           List.iter (fun (h,c) ->
 902                (if (!s) then
 903                     (if h.hstrict then
 904                         (debug("tac1 1\n");
 905                         tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
 906                                                        ~term:_Rfourier_lt_lt)
 907                                                ~continuations:[!tac1;tac_use h;
 908                                                        tac_zero_inf_pos
 909                                                        (rational_to_fraction c)]))
 910                     else
 911                     (
 912                         debug("tac1 2\n");
 913                         tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
 914                                                        ~term:_Rfourier_lt_le)
 915                                                ~continuations:[!tac1;tac_use h;
 916                                                        tac_zero_inf_pos
 917                                                        (rational_to_fraction c)]))
 918                     )
 919                 else
 920                     (if h.hstrict then
 921                         (
 922
 923                         debug("tac1 3\n");
 924                         tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
 925                                                ~continuations:[!tac1;tac_use h;
 926                                                        tac_zero_inf_pos
 927                                                        (rational_to_fraction c)]))
 928                     else
 929                         (
 930                         debug("tac1 4\n");
 931                         tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
 932                                                ~continuations:[!tac1;tac_use h;
 933                                                        tac_zero_inf_pos
 934                                                        (rational_to_fraction c)]))
 935
 936                                                        )
 937                                                       );
 938               s:=(!s)||(h.hstrict))
 939               lutil;(*end List.iter*)
 940
 941            let tac2= if sres then
 942                           tac_zero_inf_false goal (rational_to_fraction cres)
 943                       else
 944                           tac_zero_infeq_false goal (rational_to_fraction cres)
 945            in
 946            tac:=(Tacticals.thens ~start:(my_cut ~term:ineq)
 947                      ~continuations:[Tacticals.then_  (* ?????????????????????????????? *)
 948                         ~start:(fun ~status:(proof,goal as status) ->
 949                                  let curi,metasenv,pbo,pty = proof in
 950                                  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 951                                   PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status)
 952                         ~continuation:(Tacticals.then_
 953                                 ~start:(PrimitiveTactics.apply_tac
 954                                                 ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
 955                                 ~continuation:Ring.id_tac
 956 (*CSC
 957                                 ~continuation:(Tacticals.thens
 958                                                 ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
 959                                                 ~continuations:[tac2;(Tacticals.thens
 960                                                         ~start:(equality_replace (Cic.Appl[_Rinv;_R1]) _R1)
 961                                                         ~continuations:
 962 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ...    *)
 963                                         [Tacticals.try_tactics
 964                                                 (* ???????????????????????????? *)
 965                                                 ~tactics:[ "ring", Ring.ring_tac  ; "id", Ring.id_tac]
 966                                         ;
 967                                         Tacticals.then_
 968                                                 ~start:(PrimitiveTactics.apply_tac ~term:_sym_eqT)
 969                                                 ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
 970                                         ]
 971
 972                                          )
 973                                                 ] (* end continuations before comment *)
 974                                         ) *)
 975                                 );
 976                        !tac1]
 977                 );(*end tac:=*)
 978            tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False)
 979                                  ~continuations:[Tacticals.then_
 980                                         (* ???????????????????????????????
 981                                            in coq era intro *)
 982                                         ~start:(PrimitiveTactics.intros_tac ~name:(String.copy "??"))
 983                                         (* ????????????????????????????? *)
 984
 985                                         ~continuation:contradiction_tac;!tac])
 986
 987
 988       |_-> assert false)(*match (!lutil) *)
 989   |_-> assert false); (*match res*)
 990
 991   debug ("finalmente applico tac\n");
 992   (!tac ~status:(proof,goal))
 993
 994 ;;
 995
 996 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
 997