]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/ring.ml
Yet another localization error in eat_prods fixed.
[helm.git] / components / tactics / ring.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 open CicReduction
29 open PrimitiveTactics
30 open ProofEngineTypes
31 open UriManager
32
33 (** DEBUGGING *)
34
35   (** perform debugging output? *)
36 let debug = false
37 let debug_print = fun _ -> ()
38
39   (** debugging print *)
40 let warn s = debug_print (lazy ("RING WARNING: " ^ (Lazy.force s)))
41
42 (** CIC URIS *)
43
44 (**
45   Note: For constructors URIs aren't really URIs but rather triples of
46   the form (uri, typeno, consno).  This discrepancy is to preserver an
47   uniformity of invocation of "mkXXX" functions.
48 *)
49
50 let equality_is_a_congruence_A =
51  uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var"
52 let equality_is_a_congruence_x =
53  uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var"
54 let equality_is_a_congruence_y =
55  uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var"
56
57 let apolynomial_uri =
58   uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
59 let apvar_uri = (apolynomial_uri, 0, 1)
60 let ap0_uri = (apolynomial_uri, 0, 2)
61 let ap1_uri = (apolynomial_uri, 0, 3)
62 let applus_uri = (apolynomial_uri, 0, 4)
63 let apmult_uri = (apolynomial_uri, 0, 5)
64 let apopp_uri = (apolynomial_uri, 0, 6)
65
66 let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var"
67 let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind"
68 let empty_vm_uri = (varmap_uri, 0, 1)
69 let node_vm_uri = (varmap_uri, 0, 2)
70 let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con"
71 let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind"
72 let left_idx_uri = (index_uri, 0, 1)
73 let right_idx_uri = (index_uri, 0, 2)
74 let end_idx_uri = (index_uri, 0, 3)
75
76 let abstract_rings_A_uri =
77  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var"
78 let abstract_rings_Aplus_uri =
79  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var"
80 let abstract_rings_Amult_uri =
81  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var"
82 let abstract_rings_Aone_uri =
83  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var"
84 let abstract_rings_Azero_uri =
85  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var"
86 let abstract_rings_Aopp_uri =
87  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var"
88 let abstract_rings_Aeq_uri =
89  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var"
90 let abstract_rings_vm_uri =
91  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var"
92 let abstract_rings_T_uri =
93  uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var"
94 let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con"
95 let interp_sacs_uri =
96   uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con"
97 let apolynomial_normalize_uri =
98   uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con"
99 let apolynomial_normalize_ok_uri =
100   uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con"
101
102 (** CIC PREDICATES *)
103
104   (**
105     check whether a term is a constant or not, if argument "uri" is given and is
106     not "None" also check if the constant correspond to the given one or not
107   *)
108 let cic_is_const ?(uri: uri option = None) term =
109   match uri with
110   | None ->
111       (match term with
112         | Cic.Const _ -> true
113         | _ -> false)
114   | Some realuri ->
115       (match term with
116         | Cic.Const (u, _) when (eq u realuri) -> true
117         | _ -> false)
118
119 (** PROOF AND GOAL ACCESSORS *)
120
121   (**
122     @param proof a proof
123     @return the uri of a given proof
124   *)
125 let uri_of_proof ~proof:(uri, _, _, _) = uri
126
127   (**
128     @param status current proof engine status
129     @raise Failure if proof is None
130     @return current goal's metasenv
131   *)
132 let metasenv_of_status ((_,m,_,_), _) = m
133
134   (**
135     @param status a proof engine status
136     @raise Failure when proof or goal are None
137     @return context corresponding to current goal
138   *)
139 let context_of_status status =
140   let (proof, goal) = status in
141   let metasenv = metasenv_of_status status in
142   let _, context, _ = CicUtil.lookup_meta goal metasenv in
143    context
144
145 (** CIC TERM CONSTRUCTORS *)
146
147   (**
148     Create a Cic term consisting of a constant
149     @param uri URI of the constant
150     @proof current proof
151     @exp_named_subst explicit named substitution
152   *)
153 let mkConst ~uri ~exp_named_subst =
154   Cic.Const (uri, exp_named_subst)
155
156   (**
157     Create a Cic term consisting of a constructor
158     @param uri triple <uri, typeno, consno> where uri is the uri of an inductive
159     type, typeno is the type number in a mutind structure (0 based), consno is
160     the constructor number (1 based)
161     @exp_named_subst explicit named substitution
162   *)
163 let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst =
164  Cic.MutConstruct (uri, typeno, consno, exp_named_subst)
165
166   (**
167     Create a Cic term consisting of a type member of a mutual induction
168     @param uri pair <uri, typeno> where uri is the uri of a mutual inductive
169     type and typeno is the type number (0 based) in the mutual induction
170     @exp_named_subst explicit named substitution
171   *)
172 let mkMutInd ~uri:(uri, typeno) ~exp_named_subst =
173  Cic.MutInd (uri, typeno, exp_named_subst)
174
175 (** EXCEPTIONS *)
176
177   (**
178     raised when the current goal is not ringable; a goal is ringable when is an
179     equality on reals (@see r_uri)
180   *)
181 exception GoalUnringable
182
183 (** RING's FUNCTIONS LIBRARY *)
184
185   (**
186     Check whether the ring tactic can be applied on a given term (i.e. that is
187     an equality on reals)
188     @param term to be tested
189     @return true if the term is ringable, false otherwise
190   *)
191 let ringable =
192   let is_equality = function
193     | Cic.MutInd (uri, 0, []) when (eq uri HelmLibraryObjects.Logic.eq_URI) -> true
194     | _ -> false
195   in
196   let is_real = function
197     | Cic.Const (uri, _) when (eq uri HelmLibraryObjects.Reals.r_URI) -> true
198     | _ -> false
199   in
200   function
201     | Cic.Appl (app::set::_::_::[]) when (is_equality app && is_real set) ->
202         warn (lazy "Goal Ringable!");
203         true
204     | _ ->
205         warn (lazy "Goal Not Ringable :-((");
206         false
207
208   (**
209     split an equality goal of the form "t1 = t2" in its two subterms t1 and t2
210     after checking that the goal is ringable
211     @param goal the current goal
212     @return a pair (t1,t2) that are two sides of the equality goal
213     @raise GoalUnringable if the goal isn't ringable
214   *)
215 let split_eq = function
216   | (Cic.Appl (_::_::t1::t2::[])) as term when ringable term ->
217         warn (lazy ("<term1>" ^ (CicPp.ppterm t1) ^ "</term1>"));
218         warn (lazy ("<term2>" ^ (CicPp.ppterm t2) ^ "</term2>"));
219         (t1, t2)
220   | _ -> raise GoalUnringable
221
222   (**
223     @param i an integer index representing a 1 based number of node in a binary
224     search tree counted in a fbs manner (i.e.: 1 is the root, 2 is the left
225     child of the root (if any), 3 is the right child of the root (if any), 4 is
226     the left child of the left child of the root (if any), ....)
227     @param proof the current proof
228     @return an index representing the same node in a varmap (@see varmap_uri),
229     the returned index is as defined in index (@see index_uri)
230   *)
231 let path_of_int n =
232   let rec digits_of_int n =
233     if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1))
234   in
235   List.fold_right
236     (fun digit path ->
237       Cic.Appl [
238         mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) [];
239         path])
240     (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *)
241     (mkCtor end_idx_uri [])
242
243   (**
244     Build a variable map (@see varmap_uri) from a variables array.
245     A variable map is almost a binary tree so this function receiving a var list
246     like [v;w;x;y;z] will build a varmap of shape:       v
247                                                         / \
248                                                        w   x
249                                                       / \
250                                                      y   z
251     @param vars variables array
252     @return a cic term representing the variable map containing vars variables
253   *)
254 let btree_of_array ~vars =
255   let r = HelmLibraryObjects.Reals.r in
256   let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
257   let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
258   let size = Array.length vars in
259   let halfsize = size lsr 1 in
260   let rec aux n =   (* build the btree starting from position n *)
261       (*
262         n is the position in the vars array _1_based_ in order to access
263         left and right child using (n*2, n*2+1) trick
264       *)
265     if n > size then
266       empty_vm_r
267     else if n > halfsize then  (* no more children *)
268       Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r]
269     else  (* still children *)
270       Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)]
271   in
272   aux 1
273
274   (**
275     abstraction function:
276     concrete polynoms       ----->      (abstract polynoms, varmap)
277     @param terms list of conrete polynoms
278     @return a pair <aterms, varmap> where aterms is a list of abstract polynoms
279     and varmap is the variable map needed to interpret them
280   *)
281 let abstract_poly ~terms =
282   let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *)
283   let varlist = ref [] in  (* vars list in reverse order *)
284   let counter = ref 1 in  (* index of next new variable *)
285   let rec aux = function  (* TODO not tail recursive *)
286     (* "bop" -> binary operator | "uop" -> unary operator *)
287     | Cic.Appl (bop::t1::t2::[])
288       when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rplus_URI) bop) -> (* +. *)
289         Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
290     | Cic.Appl (bop::t1::t2::[])
291       when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.rmult_URI) bop) -> (* *. *)
292         Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
293     | Cic.Appl (uop::t::[])
294       when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.ropp_URI) uop) -> (* ~-. *)
295         Cic.Appl [mkCtor apopp_uri []; aux t]
296     | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r0_URI) t) -> (* 0. *)
297         mkCtor ap0_uri []
298     | t when (cic_is_const ~uri:(Some HelmLibraryObjects.Reals.r1_URI) t) -> (* 1. *)
299         mkCtor ap1_uri []
300     | t ->  (* variable *)
301       try
302         Hashtbl.find varhash t (* use an old var *)
303       with Not_found -> begin (* create a new var *)
304         let newvar =
305           Cic.Appl [mkCtor apvar_uri []; path_of_int !counter]
306         in
307         incr counter;
308         varlist := t :: !varlist;
309         Hashtbl.add varhash t newvar;
310         newvar
311       end
312   in
313   let aterms = List.map aux terms in  (* abstract vars *)
314   let varmap =  (* build varmap *)
315     btree_of_array ~vars:(Array.of_list (List.rev !varlist))
316   in
317   (aterms, varmap)
318
319   (**
320     given a list of abstract terms (i.e. apolynomials) build the ring "segments"
321     that is triples like (t', t'', t''') where
322           t'    = interp_ap(varmap, at)
323           t''   = interp_sacs(varmap, (apolynomial_normalize at))
324           t'''  = apolynomial_normalize_ok(varmap, at)
325     at is the abstract term built from t, t is a single member of aterms
326   *)
327 let build_segments ~terms =
328   let theory_args_subst varmap =
329    [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ;
330     abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ;
331     abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ;
332     abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ;
333     abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ;
334     abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ;
335     abstract_rings_vm_uri, varmap] in
336   let theory_args_subst' eq varmap t =
337    [abstract_rings_A_uri, HelmLibraryObjects.Reals.r ;
338     abstract_rings_Aplus_uri, HelmLibraryObjects.Reals.rplus ;
339     abstract_rings_Amult_uri, HelmLibraryObjects.Reals.rmult ;
340     abstract_rings_Aone_uri, HelmLibraryObjects.Reals.r1 ;
341     abstract_rings_Azero_uri, HelmLibraryObjects.Reals.r0 ;
342     abstract_rings_Aopp_uri, HelmLibraryObjects.Reals.ropp ;
343     abstract_rings_Aeq_uri, eq ;
344     abstract_rings_vm_uri, varmap ;
345     abstract_rings_T_uri, t] in
346   let interp_ap varmap =
347    mkConst interp_ap_uri (theory_args_subst varmap) in
348   let interp_sacs varmap =
349    mkConst interp_sacs_uri (theory_args_subst varmap) in
350   let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in
351   let apolynomial_normalize_ok eq varmap t =
352    mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
353   let lxy_false =   (** Cic funcion "fun (x,y):R -> false" *)
354     Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r,
355       Cic.Lambda (Cic.Anonymous, HelmLibraryObjects.Reals.r, HelmLibraryObjects.Datatypes.falseb))
356   in
357   let (aterms, varmap) = abstract_poly ~terms in  (* abstract polys *)
358   List.map    (* build ring segments *)
359    (fun t ->
360      Cic.Appl [interp_ap varmap ; t],
361      Cic.Appl (
362        [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
363      Cic.Appl [apolynomial_normalize_ok lxy_false varmap HelmLibraryObjects.Reals.rtheory ; t]
364    ) aterms
365
366
367 let status_of_single_goal_tactic_result =
368  function
369     proof,[goal] -> proof,goal
370   | _ ->
371     raise (Fail (lazy "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal"))
372
373 (* Galla: spostata in variousTactics.ml 
374   (**
375     auxiliary tactic "elim_type"
376     @param status current proof engine status
377     @param term term to cut
378   *)
379 let elim_type_tac ~term status =
380   warn (lazy "in Ring.elim_type_tac");
381   Tacticals.thens ~start:(cut_tac ~term)
382    ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status
383 *)
384
385   (**
386     auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
387     @param status current proof engine status
388     @param term term to cut
389     @param proof term used to prove second subgoal generated by elim_type
390   *)
391 (* FG: METTERE I NOMI ANCHE QUI? *)  
392 let elim_type2_tac ~term ~proof =
393  let elim_type2_tac ~term ~proof status =
394   let module E = EliminationTactics in
395   warn (lazy "in Ring.elim_type2");
396   ProofEngineTypes.apply_tactic 
397    (Tacticals.thens ~start:(E.elim_type_tac term)
398     ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof]) status
399  in
400   ProofEngineTypes.mk_tactic (elim_type2_tac ~term ~proof)
401
402 (* Galla: spostata in variousTactics.ml
403   (**
404     Reflexivity tactic, try to solve current goal using "refl_eqT"
405     Warning: this isn't equale to the coq's Reflexivity because this one tries
406     only refl_eqT, coq's one also try "refl_equal"
407     @param status current proof engine status
408   *)
409 let reflexivity_tac (proof, goal) =
410   warn (lazy "in Ring.reflexivity_tac");
411   let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
412   try
413     apply_tac (proof, goal) ~term:refl_eqt
414   with (Fail _) as e ->
415     let e_str = Printexc.to_string e in
416     raise (Fail ("Reflexivity failed with exception: " ^ e_str))
417 *)
418
419   (** lift an 8-uple of debrujins indexes of n *)
420 let lift ~n (a,b,c,d,e,f,g,h) =
421   match (List.map (CicSubstitution.lift n) [a;b;c;d;e;f;g;h]) with
422   | [a;b;c;d;e;f;g;h] -> (a,b,c,d,e,f,g,h)
423   | _ -> assert false
424
425   (**
426     remove hypothesis from a given status starting from the last one
427     @param count number of hypotheses to remove
428     @param status current proof engine status
429   *)
430 let purge_hyps_tac ~count =
431  let purge_hyps_tac ~count status =
432   let module S = ProofEngineStructuralRules in
433   let (proof, goal) = status in
434   let rec aux n context status =
435     assert(n>=0);
436     match (n, context) with
437     | (0, _) -> status
438     | (n, hd::tl) ->
439         let name_of_hyp =
440          match hd with
441             None
442           | Some (Cic.Anonymous,_) -> assert false
443           | Some (Cic.Name name,_) -> name
444         in
445          aux (n-1) tl
446           (status_of_single_goal_tactic_result 
447            (ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status))
448     | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
449   in
450    let (_, metasenv, _, _) = proof in
451     let (_, context, _) = CicUtil.lookup_meta goal metasenv in
452      let proof',goal' = aux count context status in
453       assert (goal = goal') ;
454       proof',[goal']
455  in
456   ProofEngineTypes.mk_tactic (purge_hyps_tac ~count)
457
458 (** THE TACTIC! *)
459
460   (**
461     Ring tactic, does associative and commutative rewritings in Reals ring
462     @param status current proof engine status
463   *)
464  
465 let ring_tac status =
466   let (proof, goal) = status in
467   warn (lazy "in Ring tactic");
468   let eqt = mkMutInd (HelmLibraryObjects.Logic.eq_URI, 0) [] in
469   let r = HelmLibraryObjects.Reals.r in
470   let metasenv = metasenv_of_status status in
471   let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
472   let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
473   match (build_segments ~terms:[t1; t2]) with
474   | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
475      if debug then
476       List.iter  (* debugging, feel free to remove *)
477         (fun (descr, term) ->
478           warn (lazy (descr ^ " " ^ (CicPp.ppterm term))))
479         (List.combine
480           ["t1"; "t1'"; "t1''"; "t1'_eq_t1''";
481            "t2"; "t2'"; "t2''"; "t2'_eq_t2''"]
482           [t1; t1'; t1''; t1'_eq_t1'';
483            t2; t2'; t2''; t2'_eq_t2'']);
484       try
485         let new_hyps = ref 0 in  (* number of new hypotheses created *)
486         ProofEngineTypes.apply_tactic 
487          (Tacticals.first
488           ~tactics:[
489             "reflexivity", EqualityTactics.reflexivity_tac ;
490             "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
491             "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
492             "exact sym_eqt su t1 ...", exact_tac
493             ~term:(
494               Cic.Appl
495                [mkConst HelmLibraryObjects.Logic.sym_eq_URI
496                  [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r;
497                   equality_is_a_congruence_x, t1'' ;
498                   equality_is_a_congruence_y, t1
499                  ] ;
500                 t1'_eq_t1''
501                ]) ;
502             "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
503               let status' = (* status after 1st elim_type use *)
504                 let context = context_of_status status in
505                 let b,_ = (*TASSI : FIXME*)
506                   are_convertible context t1'' t1 CicUniv.empty_ugraph in 
507                 if not b then begin
508                   warn (lazy "t1'' and t1 are NOT CONVERTIBLE");
509                   let newstatus =
510                     ProofEngineTypes.apply_tactic 
511                     (elim_type2_tac  (* 1st elim_type use *)
512                       ~proof:t1'_eq_t1''
513                       ~term:(Cic.Appl [eqt; r; t1''; t1]))
514                     status 
515                   in
516                    incr new_hyps; (* elim_type add an hyp *)
517                    match newstatus with
518                       (proof,[goal]) -> proof,goal
519                     | _ -> assert false
520                 end else begin
521                   warn (lazy "t1'' and t1 are CONVERTIBLE");
522                   status
523                 end
524               in
525               let (t1,t1',t1'',t1'_eq_t1'',t2,t2',t2'',t2'_eq_t2'') =
526                 lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
527               in
528               let status'' =
529                ProofEngineTypes.apply_tactic
530                 (Tacticals.first (* try to solve 1st subgoal *)
531                   ~tactics:[
532                     "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
533                     "exact sym_eqt su t2 ...",
534                       exact_tac
535                        ~term:(
536                          Cic.Appl
537                           [mkConst HelmLibraryObjects.Logic.sym_eq_URI
538                             [equality_is_a_congruence_A, HelmLibraryObjects.Reals.r;
539                              equality_is_a_congruence_x, t2'' ;
540                              equality_is_a_congruence_y, t2
541                             ] ;
542                            t2'_eq_t2''
543                           ]) ;
544                     "elim_type eqt su t2 ...", 
545                      ProofEngineTypes.mk_tactic (fun status ->
546                       let status' =
547                         let context = context_of_status status in
548                         let b,_ = (* TASSI:FIXME *)
549                           are_convertible context t2'' t2 CicUniv.empty_ugraph 
550                         in
551                           if not b then begin 
552                           warn (lazy "t2'' and t2 are NOT CONVERTIBLE");
553                           let newstatus =
554                             ProofEngineTypes.apply_tactic 
555                              (elim_type2_tac  (* 2nd elim_type use *)
556                               ~proof:t2'_eq_t2''
557                               ~term:(Cic.Appl [eqt; r; t2''; t2]))
558                              status
559                           in
560                           incr new_hyps; (* elim_type add an hyp *)
561                           match newstatus with
562                              (proof,[goal]) -> proof,goal
563                            | _ -> assert false
564                         end else begin
565                           warn (lazy "t2'' and t2 are CONVERTIBLE");
566                           status
567                         end
568                       in
569                       try (* try to solve main goal *)
570                         warn (lazy "trying reflexivity ....");
571                         ProofEngineTypes.apply_tactic 
572                          EqualityTactics.reflexivity_tac status'
573                       with (Fail _) ->  (* leave conclusion to the user *)
574                         warn (lazy "reflexivity failed, solution's left as an ex :-)");
575                         ProofEngineTypes.apply_tactic 
576                          (purge_hyps_tac ~count:!new_hyps) status')])
577                   status'       
578               in
579               status'')])
580          status      
581       with (Fail s) ->
582         raise (Fail (lazy ("Ring failure: " ^ Lazy.force s)))
583     end
584   | _ -> (* impossible: we are applying ring exacty to 2 terms *)
585     assert false
586
587   (* wrap ring_tac catching GoalUnringable and raising Fail *)
588
589 let ring_tac status =
590   try
591     ring_tac status
592   with GoalUnringable ->
593     raise (Fail (lazy "goal unringable"))
594
595 let ring_tac = ProofEngineTypes.mk_tactic ring_tac
596