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