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