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