helm/ocaml/tactics/fourierR.ml

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