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