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