helm/gTopLevel/fourierR.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26
  27 (******************** OTHER USEFUL TACTICS **********************)
  28 (* 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 ~also_in_hypotheses:false
 779           ~term:
 780             (Cic.Appl
 781               [_Rle ; _R0 ;
 782                Cic.Appl
 783                 [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
 784               ]
 785             )
 786         )
 787       ~continuation:
 788         (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
 789           ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
 790  debug("end tac_zero_infeq_false\n");
 791  r
 792 (*PORTING
 793  Tacticals.id_tac ~status
 794 *)
 795 ;;
 796
 797
 798 (* *********** ********** ******** ??????????????? *********** **************)
 799
 800 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
 801   let curi,metasenv,pbo,pty = proof in
 802   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 803   let fresh_meta = ProofEngineHelpers.new_meta proof in
 804   let irl =
 805    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 806   let metasenv' = (fresh_meta,context,t)::metasenv in
 807    let proof' = curi,metasenv',pbo,pty in
 808     let proof'',goals =
 809      PrimitiveTactics.apply_tac
 810       (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*)
 811       ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *)
 812        ~status:(proof',goal)
 813     in
 814      proof'',fresh_meta::goals
 815 ;;
 816
 817
 818
 819
 820
 821 let my_cut ~term:c ~status:(proof,goal)=
 822   let curi,metasenv,pbo,pty = proof in
 823   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 824
 825 debug("my_cut di "^CicPp.ppterm c^"\n");
 826
 827
 828   let fresh_meta = ProofEngineHelpers.new_meta proof in
 829   let irl =
 830    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 831   let metasenv' = (fresh_meta,context,c)::metasenv in
 832    let proof' = curi,metasenv',pbo,pty in
 833     let proof'',goals =
 834      apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,
 835       CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)]
 836        ~status:(proof',goal)
 837     in
 838      (* We permute the generated goals to be consistent with Coq *)
 839      match goals with
 840         [] -> assert false
 841       | he::tl -> proof'',he::fresh_meta::tl
 842 ;;
 843
 844
 845 let exact = PrimitiveTactics.exact_tac;;
 846
 847 let tac_use h ~status:(proof,goal as status) =
 848 debug("Inizio TC_USE\n");
 849 let curi,metasenv,pbo,pty = proof in
 850 let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 851 debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
 852 debug ("ty = "^ CicPp.ppterm ty^"\n");
 853
 854 let res =
 855 match h.htype with
 856   "Rlt" -> exact ~term:h.hname ~status
 857   |"Rle" -> exact ~term:h.hname ~status
 858   |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 859              ~term:_Rfourier_gt_to_lt)
 860               ~continuation:(exact ~term:h.hname)) ~status
 861   |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 862              ~term:_Rfourier_ge_to_le)
 863               ~continuation:(exact ~term:h.hname)) ~status
 864   |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 865                ~term:_Rfourier_eqLR_to_le)
 866                 ~continuation:(exact ~term:h.hname)) ~status
 867   |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
 868                ~term:_Rfourier_eqRL_to_le)
 869                 ~continuation:(exact ~term:h.hname)) ~status
 870   |_->assert false
 871 in
 872 debug("Fine TAC_USE\n");
 873 res
 874 ;;
 875
 876
 877
 878 let is_ineq (h,t) =
 879     match t with
 880        Cic.Appl ( Cic.Const(u,boh)::next) ->
 881          (match (UriManager.string_of_uri u) with
 882                  "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
 883                 |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
 884                 |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
 885                 |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
 886                 |"cic:/Coq/Init/Logic_Type/eqT.con" ->
 887                    (match (List.hd next) with
 888                        Cic.Const (uri,_) when
 889                         UriManager.string_of_uri uri =
 890                         "cic:/Coq/Reals/Rdefinitions/R.con" -> true
 891                      | _ -> false)
 892                 |_->false)
 893      |_->false
 894 ;;
 895
 896 let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
 897
 898 let mkAppL a =
 899    Cic.Appl(Array.to_list a)
 900 ;;
 901
 902 (* Résolution d'inéquations linéaires dans R *)
 903 let rec strip_outer_cast c = match c with
 904   | Cic.Cast (c,_) -> strip_outer_cast c
 905   | _ -> c
 906 ;;
 907
 908 (*let find_in_context id context =
 909   let rec find_in_context_aux c n =
 910         match c with
 911         [] -> failwith (id^" not found in context")
 912         | a::next -> (match a with
 913                         Some (Cic.Name(name),_) when name = id -> n
 914                               (*? magari al posto di _ qualcosaltro?*)
 915                         | _ -> find_in_context_aux next (n+1))
 916   in
 917   find_in_context_aux context 1
 918 ;;
 919
 920 (* mi sembra quadratico *)
 921 let rec filter_real_hyp context cont =
 922   match context with
 923   [] -> []
 924   | Some(Cic.Name(h),Cic.Decl(t))::next -> (
 925                                 let n = find_in_context h cont in
 926                                 debug("assegno "^string_of_int n^" a "^CicPp.ppterm t^"\n");
 927                         [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
 928   | a::next -> debug("  no\n"); filter_real_hyp next cont
 929 ;;*)
 930 let filter_real_hyp context _ =
 931   let rec filter_aux context num =
 932    match context with
 933   [] -> []
 934   | Some(Cic.Name(h),Cic.Decl(t))::next ->
 935                 (
 936                 (*let n = find_in_context h cont in*)
 937                 debug("assegno "^string_of_int num^" a "^h^":"^CicPp.ppterm t^"\n");
 938                 [(Cic.Rel(num),t)] @ filter_aux next (num+1)
 939                 )
 940   | a::next -> filter_aux next (num+1)
 941   in
 942   filter_aux context 1
 943 ;;
 944
 945
 946 (* lifts everithing at the conclusion level *)
 947 let rec superlift c n=
 948   match c with
 949   [] -> []
 950   | Some(name,Cic.Decl(a))::next  -> [Some(name,Cic.Decl(
 951                   CicSubstitution.lift n a))] @ superlift next (n+1)
 952   | Some(name,Cic.Def(a))::next   -> [Some(name,Cic.Def(
 953                   CicSubstitution.lift n a))] @ superlift next (n+1)
 954   | _::next -> superlift next (n+1) (*??  ??*)
 955
 956 ;;
 957
 958 let equality_replace a b ~status =
 959 debug("inizio EQ\n");
 960  let module C = Cic in
 961   let proof,goal = status in
 962   let curi,metasenv,pbo,pty = proof in
 963   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 964    let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
 965    let fresh_meta = ProofEngineHelpers.new_meta proof in
 966    let irl =
 967     ProofEngineHelpers.identity_relocation_list_for_metavariable context in
 968    let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
 969 debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
 970    let (proof,goals) =
 971     VariousTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
 972      ~status:((curi,metasenv',pbo,pty),goal)
 973    in
 974    let new_goals = fresh_meta::goals in
 975 debug("fine EQ -> goals : "^string_of_int( List.length new_goals)  ^" = "
 976   ^string_of_int( List.length goals)^"+ meta\n");
 977     (proof,new_goals)
 978 ;;
 979
 980 let tcl_fail a ~status:(proof,goal) =
 981         match a with
 982         1 -> raise (ProofEngineTypes.Fail "fail-tactical")
 983         |_-> (proof,[goal])
 984 ;;
 985
 986
 987 let assumption_tac ~status:(proof,goal)=
 988   let curi,metasenv,pbo,pty = proof in
 989   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 990   let num = ref 0 in
 991   let tac_list = List.map
 992         ( fun x -> num := !num + 1;
 993                 match x with
 994                   Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
 995                   | _ -> ("fake",tcl_fail 1)
 996         )
 997         context
 998   in
 999   Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
1000 ;;
1001
1002 (* !!!!! fix !!!!!!!!!! *)
1003 let contradiction_tac ~status:(proof,goal)=
1004         Tacticals.then_
1005                 (*inutile sia questo che quello prima  della chiamata*)
1006                 ~start:
1007                   (PrimitiveTactics.intros_tac ~mknames:(function () -> "boh"))
1008                 ~continuation:(Tacticals.then_
1009                         ~start:(VariousTactics.elim_type_tac ~term:_False)
1010                         ~continuation:(assumption_tac))
1011         ~status:(proof,goal)
1012 ;;
1013
1014 (* ********************* TATTICA ******************************** *)
1015
1016 let rec fourier ~status:(s_proof,s_goal)=
1017   let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
1018   let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal)
1019    s_metasenv in
1020
1021   debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
1022   debug_pcontext s_context;
1023
1024   let fhyp = String.copy "new_hyp_for_fourier" in
1025
1026 (* here we need to negate the thesis, but to do this we need to apply the right
1027 theoreme,so let's parse our thesis *)
1028
1029   let th_to_appl = ref _Rfourier_not_le_gt in
1030   (match s_ty with
1031    Cic.Appl ( Cic.Const(u,boh)::args) ->
1032     (match UriManager.string_of_uri u with
1033        "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl :=
1034                _Rfourier_not_ge_lt
1035        |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl :=
1036                _Rfourier_not_gt_le
1037        |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl :=
1038                _Rfourier_not_le_gt
1039        |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl :=
1040                _Rfourier_not_lt_ge
1041        |_-> failwith "fourier can't be applyed")
1042    |_-> failwith "fourier can't be applyed");
1043    (* fix maybe strip_outer_cast goes here?? *)
1044
1045    (* now let's change our thesis applying the th and put it with hp *)
1046
1047    let proof,gl = Tacticals.then_
1048         ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
1049         ~continuation:
1050           (PrimitiveTactics.intros_tac ~mknames:(function () -> fhyp))
1051                 ~status:(s_proof,s_goal) in
1052    let goal = if List.length gl = 1 then List.hd gl
1053                                     else failwith "a new goal" in
1054
1055    debug ("port la tesi sopra e la nego. contesto :\n");
1056    debug_pcontext s_context;
1057
1058    (* now we have all the right environment *)
1059
1060    let curi,metasenv,pbo,pty = proof in
1061    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
1062
1063
1064    (* now we want to convert hp to inequations, but first we must lift
1065       everyting to thesis level, so that a variable has the save Rel(n)
1066       in each hp ( needed by ineq1_of_term ) *)
1067
1068     (* ? fix if None  ?????*)
1069     (* fix change superlift with a real name *)
1070
1071   let l_context = superlift context 1 in
1072   let hyps = filter_real_hyp l_context l_context in
1073
1074   debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
1075
1076   let lineq =ref [] in
1077
1078   (* transform hyps into inequations *)
1079
1080   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
1081                         with _-> ())
1082               hyps;
1083
1084
1085   debug ("applico fourier a "^ string_of_int (List.length !lineq)^
1086          " disequazioni\n");
1087
1088   let res=fourier_lineq (!lineq) in
1089   let tac=ref Tacticals.id_tac in
1090   if res=[] then
1091         (print_string "Tactic Fourier fails.\n";flush stdout;
1092          failwith "fourier_tac fails")
1093   else
1094   (
1095   match res with (*match res*)
1096   [(cres,sres,lc)]->
1097
1098      (* in lc we have the coefficient to "reduce" the system *)
1099
1100      print_string "Fourier's method can prove the goal...\n";flush stdout;
1101
1102      debug "I coeff di moltiplicazione rit sono: ";
1103
1104      let lutil=ref [] in
1105      List.iter
1106         (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
1107            (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
1108                                      )
1109         (List.combine (!lineq) lc);
1110
1111      print_string (" quindi lutil e' lunga "^
1112       string_of_int (List.length (!lutil))^"\n");
1113
1114      (* on construit la combinaison linéaire des inéquation *)
1115
1116      (match (!lutil) with (*match (!lutil) *)
1117        (h1,c1)::lutil ->
1118        debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
1119
1120        let s=ref (h1.hstrict) in
1121
1122
1123        let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
1124        let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
1125
1126        List.iter (fun (h,c) ->
1127                s:=(!s)||(h.hstrict);
1128                t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
1129                      [_Rmult;rational_to_real c;h.hleft ]  ]);
1130                t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
1131                      [_Rmult;rational_to_real c;h.hright]  ]))
1132                lutil;
1133
1134        let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
1135        let tc=rational_to_real cres in
1136
1137
1138 (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
1139
1140        debug "inizio a costruire tac1\n";
1141        Fourier.print_rational(c1);
1142
1143        let tac1=ref ( fun ~status ->
1144          if h1.hstrict then
1145            (Tacticals.thens
1146              ~start:(
1147               fun ~status ->
1148               debug ("inizio t1 strict\n");
1149               let curi,metasenv,pbo,pty = proof in
1150               let metano,context,ty = List.find
1151                (function (m,_,_) -> m=goal) metasenv in
1152               debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
1153               debug ("ty = "^ CicPp.ppterm ty^"\n");
1154               PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
1155             ~continuations:[tac_use h1;tac_zero_inf_pos
1156              (rational_to_fraction c1)]
1157             ~status
1158            )
1159            else
1160            (Tacticals.thens
1161              ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
1162              ~continuations:[tac_use h1;tac_zero_inf_pos
1163               (rational_to_fraction c1)] ~status
1164            )
1165          )
1166
1167        in
1168        s:=h1.hstrict;
1169        List.iter (fun (h,c) ->
1170          (if (!s) then
1171            (if h.hstrict then
1172              (debug("tac1 1\n");
1173              tac1:=(Tacticals.thens
1174                ~start:(PrimitiveTactics.apply_tac
1175                 ~term:_Rfourier_lt_lt)
1176                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1177                 (rational_to_fraction c)])
1178              )
1179            else
1180              (debug("tac1 2\n");
1181              Fourier.print_rational(c1);
1182              tac1:=(Tacticals.thens
1183               ~start:(
1184                 fun ~status ->
1185                 debug("INIZIO TAC 1 2\n");
1186                 let curi,metasenv,pbo,pty = proof in
1187                 let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1188                  metasenv in
1189                 debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
1190                 debug ("ty = "^ CicPp.ppterm ty^"\n");
1191                 PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status)
1192               ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1193                 (rational_to_fraction c)])
1194              )
1195            )
1196          else
1197            (if h.hstrict then
1198              (debug("tac1 3\n");
1199              tac1:=(Tacticals.thens
1200                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
1201                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1202                 (rational_to_fraction c)])
1203              )
1204            else
1205              (debug("tac1 4\n");
1206              tac1:=(Tacticals.thens
1207                ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
1208                ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
1209                 (rational_to_fraction c)])
1210              )
1211            )
1212          );
1213          s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
1214
1215        let tac2 =
1216          if sres then
1217            tac_zero_inf_false goal (rational_to_fraction cres)
1218          else
1219            tac_zero_infeq_false goal (rational_to_fraction cres)
1220        in
1221        tac:=(Tacticals.thens
1222          ~start:(my_cut ~term:ineq)
1223          ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_
1224            ~start:(fun ~status:(proof,goal as status) ->
1225              let curi,metasenv,pbo,pty = proof in
1226              let metano,context,ty = List.find (function (m,_,_) -> m=goal)
1227               metasenv in
1228              PrimitiveTactics.change_tac ~what:ty
1229               ~with_what:(Cic.Appl [ _not; ineq]) ~status)
1230            ~continuation:(Tacticals.then_
1231              ~start:(PrimitiveTactics.apply_tac ~term:
1232                (if sres then _Rnot_lt_lt else _Rnot_le_le))
1233              ~continuation:(Tacticals.thens
1234                ~start:(
1235                  fun ~status ->
1236                  debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
1237                  let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
1238                   ~status
1239                  in
1240                  (match r with (p,gl) ->
1241                    debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
1242                  r)
1243                ~continuations:[(Tacticals.thens
1244                  ~start:(
1245                    fun ~status ->
1246                    let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
1247                    (match r with (p,gl) ->
1248                      debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
1249                    r)
1250                  ~continuations:
1251                    [PrimitiveTactics.apply_tac ~term:_Rinv_R1
1252                  ;Tacticals.try_tactics
1253                    ~tactics:[ "ring", (fun ~status ->
1254                                         debug("begin RING\n");
1255                                         let r = Ring.ring_tac  ~status in
1256                                         debug ("end RING\n");
1257                                         r)
1258                         ; "id", Tacticals.id_tac]
1259                  ])
1260                ;(*Tacticals.id_tac*)
1261                 Tacticals.then_
1262                  ~start:
1263                   (
1264                   fun ~status:(proof,goal as status) ->
1265                    let curi,metasenv,pbo,pty = proof in
1266                    let metano,context,ty = List.find (function (m,_,_) -> m=
1267                     goal) metasenv in
1268                    (* check if ty is of type *)
1269                    let w1 =
1270                      debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
1271                      (match ty with
1272                      Cic.Prod (Cic.Anonymous,a,b) -> (Cic.Appl [_not;a])
1273                      |_ -> assert false)
1274                    in
1275                    let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in
1276                    debug("fine MY_CHNGE\n");
1277                    r
1278
1279                   )
1280                  ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
1281          ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
1282
1283     |_-> assert false)(*match (!lutil) *)
1284   |_-> assert false); (*match res*)
1285   debug ("finalmente applico tac\n");
1286   (
1287   let r = !tac ~status:(proof,goal) in
1288   debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r
1289
1290   )
1291 ;;
1292
1293 let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
1294
1295