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