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