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