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