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