X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fring.ml;h=399d2c2892334297ed970f25b47fe363ede544e8;hb=347d3c4262af67b378f4a65f735f48797ffc37a3;hp=080e280b5f25325f1faf2daaa141ad8b2e3f5414;hpb=76cb30ecd0159512548aee0ba7085ab17c6fd5bd;p=helm.git diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index 080e280b5..399d2c289 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -48,8 +48,13 @@ let warn s = let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind" let refl_eqt_uri = (eqt_uri, 0, 1) -let sym_eqt_uri = - uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con" +let equality_is_a_congruence_A = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var" +let equality_is_a_congruence_x = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var" +let equality_is_a_congruence_y = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var" +let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con" let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind" let true_uri = (bool_uri, 0, 1) let false_uri = (bool_uri, 0, 2) @@ -63,8 +68,7 @@ let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con" let apolynomial_uri = - uri_of_string - "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind" + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind" let apvar_uri = (apolynomial_uri, 0, 1) let ap0_uri = (apolynomial_uri, 0, 2) let ap1_uri = (apolynomial_uri, 0, 3) @@ -72,36 +76,41 @@ let applus_uri = (apolynomial_uri, 0, 4) let apmult_uri = (apolynomial_uri, 0, 5) let apopp_uri = (apolynomial_uri, 0, 6) -let varmap_uri = - uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap.ind" +let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var" +let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind" let empty_vm_uri = (varmap_uri, 0, 1) let node_vm_uri = (varmap_uri, 0, 2) -let varmap_find_uri = - uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap_find.con" -let index_uri = - uri_of_string "cic:/Coq/ring/Quote/variables_map/index.ind" +let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con" +let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind" let left_idx_uri = (index_uri, 0, 1) let right_idx_uri = (index_uri, 0, 2) let end_idx_uri = (index_uri, 0, 3) -let interp_ap_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con" +let abstract_rings_A_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var" +let abstract_rings_Aplus_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var" +let abstract_rings_Amult_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var" +let abstract_rings_Aone_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var" +let abstract_rings_Azero_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var" +let abstract_rings_Aopp_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var" +let abstract_rings_Aeq_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var" +let abstract_rings_vm_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var" +let abstract_rings_T_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var" +let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con" let interp_sacs_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con" + uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con" let apolynomial_normalize_uri = - uri_of_string - "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con" + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con" let apolynomial_normalize_ok_uri = - uri_of_string - "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con" - -(** HELPERS *) - - (** - "Some" constructor's inverse - @raise Failure "unsome" if None is passed - *) -let unsome = function None -> failwith "unsome" | Some item -> item + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con" (** CIC PREDICATES *) @@ -147,24 +156,17 @@ let conj_of_metano metano = @raise Failure if proof is None @return current goal's metasenv *) -let metasenv_of_status ~status:(proof, goal) = - match proof with - | None -> failwith "Ring.metasenv_of_status invoked on None goal" - | Some (_, m, _, _) -> m +let metasenv_of_status ~status:((_,m,_,_), _) = m (** @param status a proof engine status @raise Failure when proof or goal are None @return context corresponding to current goal *) -let context_of_status ~status:(proof, goal) = - let metasenv = metasenv_of_status ~status:(proof, goal) in - let _, context, _ = - match goal with - | None -> failwith "Ring.context_of_status invoked on None goal" - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - context +let context_of_status ~status:(proof, goal as status) = + let metasenv = metasenv_of_status ~status:status in + let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in + context (** CIC TERM CONSTRUCTORS *) @@ -172,30 +174,29 @@ let context_of_status ~status:(proof, goal) = Create a Cic term consisting of a constant @param uri URI of the constant @proof current proof + @exp_named_subst explicit named substitution *) -let mkConst ~uri ~proof = - let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in - Cic.Const (uri, cookingsno) +let mkConst ~uri ~exp_named_subst = + Cic.Const (uri, exp_named_subst) (** Create a Cic term consisting of a constructor @param uri triple where uri is the uri of an inductive type, typeno is the type number in a mutind structure (0 based), consno is the constructor number (1 based) - @param proof current proof + @exp_named_subst explicit named substitution *) -let mkCtor ~uri:(uri, typeno, consno) ~proof = - let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in - Cic.MutConstruct (uri, cookingsno, typeno, consno) +let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst = + Cic.MutConstruct (uri, typeno, consno, exp_named_subst) (** Create a Cic term consisting of a type member of a mutual induction @param uri pair where uri is the uri of a mutual inductive type and typeno is the type number (0 based) in the mutual induction + @exp_named_subst explicit named substitution *) -let mkMutInd ~uri:(uri, typeno) ~proof = - let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in - Cic.MutInd (uri, cookingsno, typeno) +let mkMutInd ~uri:(uri, typeno) ~exp_named_subst = + Cic.MutInd (uri, typeno, exp_named_subst) (** EXCEPTIONS *) @@ -210,12 +211,12 @@ exception GoalUnringable (** Check whether the ring tactic can be applied on a given term (i.e. that is an equality on reals) - @param term term to be tested + @param term to be tested @return true if the term is ringable, false otherwise *) let ringable = let is_equality = function - | Cic.MutInd uri _ 0 when (eq uri eqt_uri) -> true + | Cic.MutInd uri 0 [] when (eq uri eqt_uri) -> true | _ -> false in let is_real = function @@ -253,17 +254,17 @@ let split_eq = function @return an index representing the same node in a varmap (@see varmap_uri), the returned index is as defined in index (@see index_uri) *) -let path_of_int n proof = +let path_of_int n = let rec digits_of_int n = if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1)) in List.fold_right (fun digit path -> Cic.Appl [ - mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) proof; + mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) []; path]) (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *) - (mkCtor end_idx_uri proof) + (mkCtor end_idx_uri []) (** Build a variable map (@see varmap_uri) from a variables array. @@ -274,15 +275,12 @@ let path_of_int n proof = / \ y z @param vars variables array - @param proof current proof @return a cic term representing the variable map containing vars variables *) -let btree_of_array ~vars ~proof = - let r = mkConst r_uri proof in (* cic objects *) - let empty_vm = mkCtor empty_vm_uri proof in - let empty_vm_r = Cic.Appl [empty_vm; r] in - let node_vm = mkCtor node_vm_uri proof in - let node_vm_r = Cic.Appl [node_vm; r] in +let btree_of_array ~vars = + let r = mkConst r_uri [] in (* cic objects *) + let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in + let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in let size = Array.length vars in let halfsize = size lsr 1 in let rec aux n = (* build the btree starting from position n *) @@ -293,9 +291,9 @@ let btree_of_array ~vars ~proof = if n > size then empty_vm_r else if n > halfsize then (* no more children *) - Cic.Appl [node_vm; r; vars.(n-1); empty_vm_r; empty_vm_r] + Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r] else (* still children *) - Cic.Appl [node_vm; r; vars.(n-1); aux (n*2); aux (n*2+1)] + Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)] in aux 1 @@ -303,11 +301,10 @@ let btree_of_array ~vars ~proof = abstraction function: concrete polynoms -----> (abstract polynoms, varmap) @param terms list of conrete polynoms - @param proof current proof @return a pair where aterms is a list of abstract polynoms and varmap is the variable map needed to interpret them *) -let abstract_poly ~terms ~proof = +let abstract_poly ~terms = let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *) let varlist = ref [] in (* vars list in reverse order *) let counter = ref 1 in (* index of next new variable *) @@ -315,23 +312,23 @@ let abstract_poly ~terms ~proof = (* "bop" -> binary operator | "uop" -> unary operator *) | Cic.Appl (bop::t1::t2::[]) when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *) - Cic.Appl [mkCtor applus_uri proof; aux t1; aux t2] + Cic.Appl [mkCtor applus_uri []; aux t1; aux t2] | Cic.Appl (bop::t1::t2::[]) when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *) - Cic.Appl [mkCtor apmult_uri proof; aux t1; aux t2] + Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2] | Cic.Appl (uop::t::[]) when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *) - Cic.Appl [mkCtor apopp_uri proof; aux t] + Cic.Appl [mkCtor apopp_uri []; aux t] | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *) - mkCtor ap0_uri proof + mkCtor ap0_uri [] | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *) - mkCtor ap1_uri proof + mkCtor ap1_uri [] | t -> (* variable *) try Hashtbl.find varhash t (* use an old var *) with Not_found -> begin (* create a new var *) let newvar = - Cic.Appl [mkCtor apvar_uri proof; path_of_int !counter proof] + Cic.Appl [mkCtor apvar_uri []; path_of_int !counter] in incr counter; varlist := t :: !varlist; @@ -339,8 +336,11 @@ let abstract_poly ~terms ~proof = newvar end in - (List.map aux terms, - btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof) + let aterms = List.map aux terms in (* abstract vars *) + let varmap = (* build varmap *) + btree_of_array ~vars:(Array.of_list (List.rev !varlist)) + in + (aterms, varmap) (** given a list of abstract terms (i.e. apolynomials) build the ring "segments" @@ -350,99 +350,69 @@ let abstract_poly ~terms ~proof = t''' = apolynomial_normalize_ok(varmap, at) at is the abstract term built from t, t is a single member of aterms *) -let build_segments ~terms ~proof = - let r = mkConst r_uri proof in (* cic objects *) - let rplus = mkConst rplus_uri proof in - let rmult = mkConst rmult_uri proof in - let ropp = mkConst ropp_uri proof in - let r0 = mkConst r0_uri proof in - let r1 = mkConst r1_uri proof in - let interp_ap = mkConst interp_ap_uri proof in - let interp_sacs = mkConst interp_sacs_uri proof in - let apolynomial_normalize = mkConst apolynomial_normalize_uri proof in - let apolynomial_normalize_ok = mkConst apolynomial_normalize_ok_uri proof in - let rtheory = mkConst rtheory_uri proof in +let build_segments ~terms = + let r = mkConst r_uri [] in (* cic objects *) + let rplus = mkConst rplus_uri [] in + let rmult = mkConst rmult_uri [] in + let ropp = mkConst ropp_uri [] in + let r1 = mkConst r1_uri [] in + let r0 = mkConst r0_uri [] in + let theory_args_subst varmap = + [abstract_rings_A_uri, r ; + abstract_rings_Aplus_uri, rplus ; + abstract_rings_Amult_uri, rmult ; + abstract_rings_Aone_uri, r1 ; + abstract_rings_Azero_uri, r0 ; + abstract_rings_Aopp_uri, ropp ; + abstract_rings_vm_uri, varmap] in + let theory_args_subst' eq varmap t = + [abstract_rings_A_uri, r ; + abstract_rings_Aplus_uri, rplus ; + abstract_rings_Amult_uri, rmult ; + abstract_rings_Aone_uri, r1 ; + abstract_rings_Azero_uri, r0 ; + abstract_rings_Aopp_uri, ropp ; + abstract_rings_Aeq_uri, eq ; + abstract_rings_vm_uri, varmap ; + abstract_rings_T_uri, t] in + let interp_ap varmap = + mkConst interp_ap_uri (theory_args_subst varmap) in + let interp_sacs varmap = + mkConst interp_sacs_uri (theory_args_subst varmap) in + let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in + let apolynomial_normalize_ok eq varmap t = + mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in + let rtheory = mkConst rtheory_uri [] in let lxy_false = (** Cic funcion "fun (x,y):R -> false" *) - Cic.Lambda (Cic.Anonimous, r, - Cic.Lambda (Cic.Anonimous, r, - mkCtor false_uri proof)) + Cic.Lambda (Cic.Anonymous, r, + Cic.Lambda (Cic.Anonymous, r, + mkCtor false_uri [])) in - let theory_args = [r; rplus; rmult; r1; r0; ropp] in - let (aterms, varmap) = abstract_poly ~terms ~proof in (* abstract polys *) + let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *) List.map (* build ring segments *) - (fun t -> - Cic.Appl ((interp_ap :: theory_args) @ [varmap; t]), - Cic.Appl ( - interp_sacs :: - (theory_args @ - [varmap; Cic.Appl [apolynomial_normalize; t]])), - Cic.Appl ( - (apolynomial_normalize_ok :: theory_args) @ - [lxy_false; varmap; rtheory; t])) - aterms - -(** AUX TACTIC{,AL}S *) + (fun t -> + Cic.Appl [interp_ap varmap ; t], + Cic.Appl ( + [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]), + Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t] + ) aterms - (** - naive implementation of ORELSE tactical, try a sequence of tactics in turn: - if one fails pass to the next one and so on, eventually raises (failure "no - tactics left") - TODO warning: not tail recursive due to "try .. with" boxing - *) -let rec try_tactics ~(tactics: (string * tactic) list) ~status = - warn "in Ring.try_tactics"; - match tactics with - | (descr, tac)::tactics -> - warn ("Ring.try_tactics IS TRYING " ^ descr); - (try - let res = tac ~status in - warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!"); - res - with - | (Fail _) as e -> begin (* TODO: codice replicato perche' non funge il - binding multiplo con "as" *) - warn ( - "Ring.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics ~status - end - | (CicTypeChecker.NotWellTyped _) as e -> begin (* TODO: si puo' togliere? *) - warn ( - "Ring.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics ~status - end - | (CicUnification.UnificationFailed) as e -> begin - warn ( - "Ring.try_tactics failed with exn: " ^ - Printexc.to_string e); - try_tactics ~tactics ~status - end - ) - | [] -> raise (Fail "try_tactics: no tactics left") + +let status_of_single_goal_tactic_result = + function + proof,[goal] -> proof,goal + | _ -> + raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal") (** auxiliary tactic "elim_type" @param status current proof engine status @param term term to cut *) -let elim_type_tac ~status ~term = +let elim_type_tac ~term ~status = warn "in Ring.elim_type_tac"; - let status' = cut_tac ~term ~status in - elim_intros_simpl_tac ~term:(Cic.Rel 1) ~status:status' - - (** - move to next goal - @param status current proof engine status - *) -let next_goal ~status = - warn "in Ring.next_goal"; - (match status with - | ((Some (_, metasenv, _, _)) as proof, goal) -> - (match metasenv with - | _::(n, _, _)::_ -> (proof, Some n) - | _ -> raise (Fail "No other goal available")) - | _ -> assert false) + Tacticals.thens ~start:(cut_tac ~term) + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status (** auxiliary tactic, use elim_type and try to close 2nd subgoal using proof @@ -450,9 +420,12 @@ let next_goal ~status = @param term term to cut @param proof term used to prove second subgoal generated by elim_type *) -let elim_type2_tac ~status ~term ~proof = - exact_tac ~term:proof ~status:(next_goal (elim_type_tac ~term ~status)) +let elim_type2_tac ~term ~proof ~status = + warn "in Ring.elim_type2"; + Tacticals.thens ~start:(elim_type_tac ~term) + ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status +(* spostata in variousTactics.ml (** Reflexivity tactic, try to solve current goal using "refl_eqT" Warning: this isn't equale to the coq's Reflexivity because this one tries @@ -461,12 +434,13 @@ let elim_type2_tac ~status ~term ~proof = *) let reflexivity_tac ~status:(proof, goal) = warn "in Ring.reflexivity_tac"; - let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:(unsome proof) in + let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in try apply_tac ~status:(proof, goal) ~term:refl_eqt with (Fail _) as e -> let e_str = Printexc.to_string e in raise (Fail ("Reflexivity failed with exception: " ^ e_str)) +*) (** lift an 8-uple of debrujins indexes of n *) let lift ~n (a,b,c,d,e,f,g,h) = @@ -479,25 +453,22 @@ let lift ~n (a,b,c,d,e,f,g,h) = @param count number of hypotheses to remove @param status current proof engine status *) -let purge_hyps ~count ~status:(proof, goal) = +let purge_hyps_tac ~count ~status:(proof, goal as status) = let module S = ProofEngineStructuralRules in let rec aux n context status = assert(n>=0); match (n, context) with | (0, _) -> status - | (n, hd::tl) -> aux (n-1) tl (S.clear ~status ~hyp:hd) - | (_, []) -> failwith "Ring.purge_hyps: no hypotheses left" - in - let metano = - match goal with - | None -> failwith "Ring.purge_hyps invoked on None goal" - | Some n -> n + | (n, hd::tl) -> + aux (n-1) tl + (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status)) + | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left" in - match proof with - | None -> failwith "Ring.purge_hyps invoked on None proof" - | Some (_, metasenv, _, _) -> - let (_, context, _) = conj_of_metano metano metasenv in - aux count context (proof, goal) + let (_, metasenv, _, _) = proof in + let (_, context, _) = conj_of_metano goal metasenv in + let proof',goal' = aux count context status in + assert (goal = goal') ; + proof',[goal'] (** THE TACTIC! *) @@ -505,16 +476,14 @@ let purge_hyps ~count ~status:(proof, goal) = Ring tactic, does associative and commutative rewritings in Reals ring @param status current proof engine status *) -let ring_tac ~status:(proof, goal) = +let ring_tac ~status:((proof, goal) as status) = warn "in Ring tactic"; - let status = (proof, goal) in - let (proof, goal) = (unsome proof), (unsome goal) in - let eqt = mkMutInd (eqt_uri, 0) proof in - let r = mkConst r_uri proof in + let eqt = mkMutInd (eqt_uri, 0) [] in + let r = mkConst r_uri [] in let metasenv = metasenv_of_status ~status in let (metano, context, ty) = conj_of_metano goal metasenv in let (t1, t2) = split_eq ty in (* goal like t1 = t2 *) - match (build_segments ~terms:[t1; t2] ~proof) with + match (build_segments ~terms:[t1; t2]) with | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin List.iter (* debugging, feel free to remove *) (fun (descr, term) -> @@ -526,16 +495,22 @@ let ring_tac ~status:(proof, goal) = t2; t2'; t2''; t2'_eq_t2'']); try let new_hyps = ref 0 in (* number of new hypotheses created *) - try_tactics + Tacticals.try_tactics ~status ~tactics:[ - "reflexivity", reflexivity_tac; - "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1''; - "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; - "exact sym_eqt su t1 ...", exact_tac ~term:( - Cic.Appl [ - mkConst sym_eqt_uri proof; mkConst r_uri proof; - t1''; t1; t1'_eq_t1'']); + "reflexivity", VariousTactics.reflexivity_tac ; + "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; + "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ; + "exact sym_eqt su t1 ...", exact_tac + ~term:( + Cic.Appl + [mkConst sym_eqt_uri + [equality_is_a_congruence_A, mkConst r_uri [] ; + equality_is_a_congruence_x, t1'' ; + equality_is_a_congruence_y, t1 + ] ; + t1'_eq_t1'' + ]) ; "elim_type eqt su t1 ...", (fun ~status -> let status' = (* status after 1st elim_type use *) let context = context_of_status ~status in @@ -546,8 +521,10 @@ let ring_tac ~status:(proof, goal) = ~status ~proof:t1'_eq_t1'' ~term:(Cic.Appl [eqt; r; t1''; t1]) in - incr new_hyps; (* elim_type add an hyp *) - newstatus + incr new_hyps; (* elim_type add an hyp *) + match newstatus with + (proof,[goal]) -> proof,goal + | _ -> assert false end else begin warn "t1'' and t1 are CONVERTIBLE"; status @@ -557,16 +534,21 @@ let ring_tac ~status:(proof, goal) = lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'') in let status'' = - try_tactics (* try to solve 1st subgoal *) + Tacticals.try_tactics (* try to solve 1st subgoal *) ~status:status' ~tactics:[ "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; "exact sym_eqt su t2 ...", - exact_tac ~term:( - Cic.Appl [ - mkConst sym_eqt_uri proof; - mkConst r_uri proof; - t2''; t2; t2'_eq_t2'']); + exact_tac + ~term:( + Cic.Appl + [mkConst sym_eqt_uri + [equality_is_a_congruence_A, mkConst r_uri [] ; + equality_is_a_congruence_x, t2'' ; + equality_is_a_congruence_y, t2 + ] ; + t2'_eq_t2'' + ]) ; "elim_type eqt su t2 ...", (fun ~status -> let status' = let context = context_of_status ~status in @@ -578,7 +560,9 @@ let ring_tac ~status:(proof, goal) = ~term:(Cic.Appl [eqt; r; t2''; t2]) in incr new_hyps; (* elim_type add an hyp *) - newstatus + match newstatus with + (proof,[goal]) -> proof,goal + | _ -> assert false end else begin warn "t2'' and t2 are CONVERTIBLE"; status @@ -586,14 +570,14 @@ let ring_tac ~status:(proof, goal) = in try (* try to solve main goal *) warn "trying reflexivity ...."; - reflexivity_tac ~status:status' + VariousTactics.reflexivity_tac ~status:status' with (Fail _) -> (* leave conclusion to the user *) warn "reflexivity failed, solution's left as an ex :-)"; - purge_hyps ~count:!new_hyps ~status:status')] + purge_hyps_tac ~count:!new_hyps ~status:status')] in status'')] - with (Fail _) -> - raise (Fail "Ring failure") + with (Fail s) -> + raise (Fail ("Ring failure: " ^ s)) end | _ -> (* impossible: we are applying ring exacty to 2 terms *) assert false