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