diff options
32 files changed, 296 insertions, 193 deletions
@@ -285,14 +285,14 @@ Tactics - New syntax "rename a into b, c into d" for "rename a into b; rename c into d" - New tactics "dependent induction/destruction H [ generalizing id_1 .. id_n ]" to do induction-inversion on instantiated inductive families à la BasicElim. -- Tactic "apply" now able to reason modulo unfolding of constants - (possible source of incompatibility in situations where apply may fail, - e.g. as argument of a try or a repeat and in a ltac function); - version of apply that does not unfold is renamed into "simple apply" - (usable for compatibility or for automation). -- Tactic "apply" now able to traverse conjunctions and to select the first - matching lemma among the components of the conjunction; tactic apply also - able to apply lemmas of conclusion an empty type. +- Tactics "apply" and "apply in" now able to reason modulo unfolding of + constants (possible source of incompatibility in situations where apply + may fail, e.g. as argument of a try or a repeat and in a ltac function); + versions that do not unfold are renamed into "simple apply" and + "simple apply in" (usable for compatibility or for automation). +- Tactics "apply" and "apply in" now able to traverse conjunctions and to + select the first matching lemma among the components of the conjunction; + tactic "apply" also able to apply lemmas of conclusion an empty type. - Tactic "apply" now supports application of several lemmas in a row. - Tactics "set" and "pose" can set functions using notation "(f x1..xn := c)". - New tactic "instantiate" (without argument). diff --git a/contrib/cc/cctac.ml b/contrib/cc/cctac.ml index d2df855ee..dcd0ea469 100644 --- a/contrib/cc/cctac.ml +++ b/contrib/cc/cctac.ml @@ -317,7 +317,7 @@ let refute_tac c t1 t2 p gls = [|intype;tt1;tt2|]) in let hid=pf_get_new_id (id_of_string "Heq") gls in let false_t=mkApp (c,[|mkVar hid|]) in - tclTHENS (true_cut (Name hid) neweq) + tclTHENS (assert_tac (Name hid) neweq) [proof_tac p; simplest_elim false_t] gls let convert_to_goal_tac c t1 t2 p gls = @@ -329,14 +329,14 @@ let convert_to_goal_tac c t1 t2 p gls = let identity=mkLambda (Name x,sort,mkRel 1) in let endt=mkApp (Lazy.force _eq_rect, [|sort;tt1;identity;c;tt2;mkVar e|]) in - tclTHENS (true_cut (Name e) neweq) + tclTHENS (assert_tac (Name e) neweq) [proof_tac p;exact_check endt] gls let convert_to_hyp_tac c1 t1 c2 t2 p gls = let tt2=constr_of_term t2 in let h=pf_get_new_id (id_of_string "H") gls in let false_t=mkApp (c2,[|mkVar h|]) in - tclTHENS (true_cut (Name h) tt2) + tclTHENS (assert_tac (Name h) tt2) [convert_to_goal_tac c1 t1 t2 p; simplest_elim false_t] gls @@ -358,7 +358,7 @@ let discriminate_tac cstr p gls = let endt=mkApp (Lazy.force _eq_rect, [|outtype;trivial;pred;identity;concl;injt|]) in let neweq=mkApp(Lazy.force _eq,[|intype;t1;t2|]) in - tclTHENS (true_cut (Name hid) neweq) + tclTHENS (assert_tac (Name hid) neweq) [proof_tac p;exact_check endt] gls (* wrap everything *) diff --git a/contrib/fourier/fourier.ml b/contrib/fourier/fourier.ml index afd85de0a..dd54aea29 100644 --- a/contrib/fourier/fourier.ml +++ b/contrib/fourier/fourier.ml @@ -202,4 +202,4 @@ let test2=[ deduce test2;; unsolvable test2;; -*)
\ No newline at end of file +*) diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 903136ca2..52543cea1 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -153,7 +153,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic = fun g -> let prov_id = pf_get_new_id hyp_id g in tclTHENS - ((* observe_tac msg *) (forward (Some (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t)) + ((* observe_tac msg *) (assert_by (Name prov_id) t (tclCOMPLETE tac))) [tclTHENLIST [ (* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]); @@ -429,7 +429,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma = in (* observe_tac "rec hyp " *) (tclTHENS - (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x) + (assert_tac (Name rec_pte_id) t_x) [ (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps); (* observe_tac "prove rec hyp" *) @@ -618,7 +618,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id fun g -> let prov_hid = pf_get_new_id hid g in tclTHENLIST[ - forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args)); + pose_proof (Name prov_hid) (mkApp(mkVar hid,args)); thin [hid]; h_rename [prov_hid,hid] ] g @@ -1546,10 +1546,9 @@ let prove_principle_for_gen ((* observe_tac "prove_rec_arg_acc" *) (tclCOMPLETE (tclTHEN - (forward - (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))) - (dummy_loc,Genarg.IntroIdentifier wf_thm_id) - (mkApp (delayed_force well_founded,[|input_type;relation|]))) + (assert_by (Name wf_thm_id) + (mkApp (delayed_force well_founded,[|input_type;relation|])) + (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)) ( (* observe_tac *) (* "apply wf_thm" *) @@ -1610,10 +1609,10 @@ let prove_principle_for_gen (List.rev_map (fun (na,_,_) -> Nameops.out_name na) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); - (* observe_tac "" *) (forward - (Some (prove_rec_arg_acc)) - (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id) + (* observe_tac "" *) (assert_by + (Name acc_rec_arg_id) (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])) + (prove_rec_arg_acc) ); (* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids))); (* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *) diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4 index 654474b32..a79b46d96 100644 --- a/contrib/funind/g_indfun.ml4 +++ b/contrib/funind/g_indfun.ml4 @@ -358,7 +358,7 @@ let poseq_unsafe idunsafe cstr gl = tclTHEN (Tactics.letin_tac None (Name idunsafe) cstr None allClauses) (tclTHENFIRST - (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) + (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr)) Tactics.reflexivity) gl diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index f62d70ab9..5c8f08715 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -445,10 +445,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem in tclTHENSEQ [ observe_tac "intro args_names" (tclMAP h_intro args_names); - observe_tac "principle" (forward - (Some (h_exact f_principle)) - (dummy_loc,Genarg.IntroIdentifier principle_id) - princ_type); + observe_tac "principle" (assert_by + (Name principle_id) + princ_type + (h_exact f_principle)); tclTHEN_i (observe_tac "functional_induction" ( fun g -> diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml index 528c276c0..100868a0e 100644 --- a/contrib/funind/recdef.ml +++ b/contrib/funind/recdef.ml @@ -740,7 +740,6 @@ let termination_proof_header is_mes input_type ids args_id relation (observe_tac "first assert" (assert_tac - true (* the assert thm is in first subgoal *) (Name wf_rec_arg) (mkApp (delayed_force acc_rel, [|input_type;relation;mkVar rec_arg_id|]) @@ -753,7 +752,6 @@ let termination_proof_header is_mes input_type ids args_id relation (observe_tac "second assert" (assert_tac - true (Name wf_thm) (mkApp (delayed_force well_founded,[|input_type;relation|])) ) @@ -1155,7 +1153,7 @@ let rec introduce_all_values_eq cont_tac functional termine [] -> let heq2 = next_global_ident_away true heq_id ids in tclTHENLIST - [forward None (dummy_loc,IntroIdentifier heq2) + [pose_proof (Name heq2) (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|])); simpl_iter (onHyp heq2); unfold_in_hyp [((true,[1]), evaluable_of_global_reference diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml index 203bc9e3d..e59de34a4 100644 --- a/contrib/interface/depends.ml +++ b/contrib/interface/depends.ml @@ -67,6 +67,7 @@ let explore_tree pfs = | Move (bool, identifier, identifier') -> "Move" | Rename (identifier, identifier') -> "Rename" | Change_evars -> "Change_evars" + | Order _ -> "Order" in let pt = proof_of_pftreestate pfs in (* We expect 0 *) @@ -280,8 +281,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of | TacExact c | TacExactNoCheck c | TacVmCastNoCheck c -> depends_of_'constr c acc - | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc - | TacApply (_, _, _) -> failwith "TODO" + | TacApply (_, _, [cb], None) -> depends_of_'constr_with_bindings cb acc + | TacApply (_, _, _, _) -> failwith "TODO" | TacElim (_, cwb, cwbo) -> depends_of_'constr_with_bindings cwb (Option.fold_right depends_of_'constr_with_bindings cwbo acc) @@ -420,6 +421,7 @@ and depends_of_prim_rule pr acc = match pr with | Move _ -> acc | Rename _ -> acc | Change_evars -> acc + | Order _ -> acc let rec depends_of_pftree pt acc = match pt.ref with diff --git a/contrib/interface/paths.ml b/contrib/interface/paths.ml index b1244d158..a157ca925 100644 --- a/contrib/interface/paths.ml +++ b/contrib/interface/paths.ml @@ -23,4 +23,4 @@ let rec lex_smaller p1 p2 = match p1,p2 with [], _ -> true | a::tl1, b::tl2 when a < b -> true | a::tl1, b::tl2 when a = b -> lex_smaller tl1 tl2 -| _ -> false;;
\ No newline at end of file +| _ -> false;; diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index 65eadf13d..01747aa58 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function | PbpRight -> TacAtom (zz, TacRight (false,NoBindings)) | PbpIntros l -> TacAtom (zz, TacIntroPattern l) | PbpLApply h -> TacAtom (zz, TacLApply (make_var h)) - | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings])) + | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings],None)) | PbpElim (hyp_name, names) -> let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in TacAtom diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 4b9c1332a..cf861642d 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1202,7 +1202,8 @@ let rec natural_ntree ig ntree = | TacExtend (_,"InductionIntro",[a]) -> let id=(out_gen wit_ident a) in natural_induction ig lh g gs ge id ltree true - | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree + | TacApply (_,false,[c,_],None) -> + natural_apply ig lh g gs (snd c) ltree | TacExact c -> natural_exact ig lh g gs (snd c) ltree | TacCut c -> natural_cut ig lh g gs (snd c) ltree | TacExtend (_,"CutIntro",[a]) -> diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 8ec6cfb2f..b404478ff 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1163,12 +1163,12 @@ and xlate_tac = xlate_error "TODO: trivial using" | TacReduce (red, l) -> CT_reduce (xlate_red_tactic red, xlate_clause l) - | TacApply (true,false,[c,bindl]) -> + | TacApply (true,false,[c,bindl],None) -> CT_apply (xlate_formula c, xlate_bindings bindl) - | TacApply (true,true,[c,bindl]) -> + | TacApply (true,true,[c,bindl],None) -> CT_eapply (xlate_formula c, xlate_bindings bindl) - | TacApply (_,_,_) -> - xlate_error "TODO: simple (e)apply and iterated apply" + | TacApply (_,_,_,_) -> + xlate_error "TODO: simple (e)apply and iterated apply and apply in" | TacConstructor (false,n_or_meta, bindl) -> let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error "" in CT_constructor (CT_int n, xlate_bindings bindl) @@ -1256,13 +1256,13 @@ and xlate_tac = but the structures are different *) xlate_clause cl) | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember" - | TacAssert (None, (_,IntroIdentifier id), c) -> + | TacAssert (None, Some (_,IntroIdentifier id), c) -> CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c) - | TacAssert (None, (_,IntroAnonymous), c) -> + | TacAssert (None, None, c) -> CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c) - | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) -> + | TacAssert (Some (TacId []), Some (_,IntroIdentifier id), c) -> CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c) - | TacAssert (Some (TacId []), (_,IntroAnonymous), c) -> + | TacAssert (Some (TacId []), None, c) -> CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c) | TacAssert _ -> xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'" diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 920b33b7a..4079b0f20 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -232,7 +232,7 @@ let build_dependent_sum l = trace (spc () ++ str ("treating evar " ^ string_of_id n)); (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype) with _ -> ()); - let tac = assert_tac true (Name n) hyptype in + let tac = assert_tac (Name n) hyptype in let conttac = (fun cont -> conttac diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index b7545e09c..9488f1dea 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -16,6 +16,8 @@ Eauto: e_resolve_constr, vernac_e_resolve_constr -> simplest_eapply Tactics: apply_with_bindings -> apply_with_bindings_wo_evars Eauto.simplest_apply -> Hiddentac.h_simplest_apply Evarutil.define_evar_as_arrow -> define_evar_as_product +Old version of Tactics.assert_tac disappears +Tactics.true_cut renamed into Tactics.assert_tac ** Universe names (univ.mli) diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index ba106e240..07d9df9c5 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -376,7 +376,7 @@ well-formed in the local context. The tactic {\tt apply} tries to match the current goal against the conclusion of the type of {\term}. If it succeeds, then the tactic returns as many subgoals as the number of non dependent premises of the type of {\term}. If the conclusion of -the type of {\term} does not match the goal {\tt and} the conclusion +the type of {\term} does not match the goal {\em and} the conclusion is an inductive type isomorphic to a tuple type, then each component of the tuple is recursively matched to the goal in the left-to-right order. @@ -656,19 +656,27 @@ in the list of subgoals remaining to prove. \end{Variants} \subsection{{\tt apply {\term} in {\ident}} -\tacindex{apply {\ldots} in}} +\tacindex{apply \ldots\ in}} This tactic applies to any goal. The argument {\term} is a term well-formed in the local context and the argument {\ident} is an hypothesis of the context. The tactic {\tt apply {\term} in {\ident}} tries to match the conclusion of the type of {\ident} against a non -dependent premises of the type of {\term}, trying them from right to +dependent premise of the type of {\term}, trying them from right to left. If it succeeds, the statement of hypothesis {\ident} is replaced by the conclusion of the type of {\term}. The tactic also returns as many subgoals as the number of other non dependent premises in the type of {\term} and of the non dependent premises of the type -of {\ident}. The tactic {\tt apply} relies on first-order -pattern-matching with dependent types. +of {\ident}. If the conclusion of the type of {\term} does not match +the goal {\em and} the conclusion is an inductive type isomorphic to a +tuple type, then the tuple is (recursively) decomposed and the first +component of the tuple of which a non dependent premise matches the +conclusion of the type of {\ident}. Tuples are decomposed in a +width-first left-to-right order (for instance if the type of {\tt H1} +is a \verb=A <-> B= statement, and the type of {\tt H2} is \verb=B= +then {\tt apply H1 in H2} transforms the type of {\tt H2} into {\tt + B}). The tactic {\tt apply} relies on first-order pattern-matching +with dependent types. \begin{ErrMsgs} \item \errindex{Statement without assumptions} @@ -693,6 +701,7 @@ instantiate the parameters of the corresponding type of {\term} (see syntax of bindings in Section~\ref{Binding-list}). \item {\tt eapply \nelist{{\term} {\bindinglist}}{,} in {\ident}} +\tacindex{eapply {\ldots} in} This works as {\tt apply \nelist{{\term} {\bindinglist}}{,} in {\ident}} but turns unresolved bindings into existential variables, if @@ -709,6 +718,24 @@ This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in This works as {\tt apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}. +\item {\tt simple apply {\term} in {\ident}} +\tacindex{simple apply {\ldots} in} +\tacindex{simple eapply {\ldots} in} + +This behaves like {\tt apply {\term} in {\ident}} but it reasons +modulo conversion only on subterms that contain no variables to +instantiate. For instance, if {\tt id := fun x:nat => x} and {\tt H : + forall y, id y = y -> True} and {\tt H0 : O = O} then {\tt simple + apply H in H0} does not succeed because it would require the +conversion of {\tt f ?y} and {\tt O} where {\tt ?y} is a variable to +instantiate. Tactic {\tt simple apply {\term} in {\ident}} does not +either traverse tuples as {\tt apply {\term} in {\ident}} does. + +\item {\tt simple apply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}\\ +{\tt simple eapply \nelist{{\term}{,} {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} + +This are the general forms of {\tt simple apply {\term} in {\ident}} and +{\tt simple eapply {\term} in {\ident}}. \end{Variants} \subsection{\tt generalize \term diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 809e5bec3..1f4aa8b24 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -364,10 +364,14 @@ GEXTEND Gram [ [ "*"; occs = occs -> occs | -> no_occurrences_expr ] ] ; - simple_clause: + in_hyp_list: [ [ "in"; idl = LIST1 id_or_meta -> idl | -> [] ] ] ; + in_hyp_as: + [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat) + | -> None ] ] + ; orient: [ [ "->" -> true | "<-" -> false @@ -406,9 +410,9 @@ GEXTEND Gram eliminator: [ [ "using"; el = constr_with_bindings -> el ] ] ; - with_names: - [ [ "as"; ipat = simple_intropattern -> ipat - | -> dummy_loc,IntroAnonymous ] ] + as_ipat: + [ [ "as"; ipat = simple_intropattern -> Some ipat + | -> None ] ] ; with_inversion_names: [ [ "as"; ipat = disjunctive_intropattern -> Some ipat @@ -473,13 +477,14 @@ GEXTEND Gram | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c - | IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," -> - TacApply (true,false,cl) - | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," -> - TacApply (true,true,cl) - | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP "," - -> TacApply (false,false,cl) - | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP "," -> TacApply (false,true,cl) + | IDENT "apply"; cl = LIST1 constr_with_bindings SEP ","; + inhyp = in_hyp_as -> TacApply (true,false,cl,inhyp) + | IDENT "eapply"; cl = LIST1 constr_with_bindings SEP ","; + inhyp = in_hyp_as -> TacApply (true,true,cl,inhyp) + | IDENT "simple"; IDENT "apply"; cl = LIST1 constr_with_bindings SEP ","; + inhyp = in_hyp_as -> TacApply (false,false,cl,inhyp) + | IDENT "simple"; IDENT "eapply"; cl = LIST1 constr_with_bindings SEP","; + inhyp = in_hyp_as -> TacApply (false,true,cl,inhyp) | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (false,cl,el) | IDENT "eelim"; cl = constr_with_bindings; el = OPT eliminator -> @@ -511,15 +516,15 @@ GEXTEND Gram (* Begin compatibility *) | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; c = lconstr; ")" -> - TacAssert (None,(loc,IntroIdentifier id),c) + TacAssert (None,Some (loc,IntroIdentifier id),c) | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAssert (Some tac,(loc,IntroIdentifier id),c) + TacAssert (Some tac,Some (loc,IntroIdentifier id),c) (* End compatibility *) - | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic -> + | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> TacAssert (Some tac,ipat,c) - | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = with_names -> + | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> TacAssert (None,ipat,c) | IDENT "cut"; c = constr -> TacCut c @@ -620,18 +625,18 @@ GEXTEND Gram TacInversion (DepInversion (k,co,ids),hyp) | IDENT "simple"; IDENT "inversion"; hyp = quantified_hypothesis; ids = with_inversion_names; - cl = simple_clause -> + cl = in_hyp_list -> TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp) | IDENT "inversion"; hyp = quantified_hypothesis; ids = with_inversion_names; - cl = simple_clause -> + cl = in_hyp_list -> TacInversion (NonDepInversion (FullInversion, cl, ids), hyp) | IDENT "inversion_clear"; hyp = quantified_hypothesis; ids = with_inversion_names; - cl = simple_clause -> + cl = in_hyp_list -> TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp) | IDENT "inversion"; hyp = quantified_hypothesis; - "using"; c = constr; cl = simple_clause -> + "using"; c = constr; cl = in_hyp_list -> TacInversion (InversionUsing (c,cl), hyp) (* Conversion *) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 77eec5e60..78d5cc926 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -123,10 +123,6 @@ let pr_with_constr prc = function | None -> mt () | Some c -> spc () ++ hov 1 (str "with" ++ spc () ++ prc c) -let pr_with_names = function - | None -> mt () - | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat) - let rec pr_message_token prid = function | MsgString s -> qs s | MsgInt n -> int n @@ -379,9 +375,9 @@ let pr_with_inversion_names = function | None -> mt () | Some ipat -> pr_as_intro_pattern ipat -let pr_with_names = function - | _,IntroAnonymous -> mt () - | ipat -> pr_as_intro_pattern ipat +let pr_as_ipat = function + | None -> mt () + | Some ipat -> pr_as_intro_pattern ipat let pr_as_name = function | Anonymous -> mt () @@ -400,7 +396,7 @@ let pr_assertion _prlc prc ipat c = match ipat with spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c) *) | ipat -> - spc() ++ prc c ++ pr_with_names ipat + spc() ++ prc c ++ pr_as_ipat ipat let pr_assumption prlc prc ipat c = match ipat with (* Use this "optimisation" or use only the general case ? @@ -408,7 +404,7 @@ let pr_assumption prlc prc ipat c = match ipat with spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c) *) | ipat -> - spc() ++ prc c ++ pr_with_names ipat + spc() ++ prc c ++ pr_as_ipat ipat let pr_by_tactic prt = function | TacId [] -> mt () @@ -429,6 +425,10 @@ let pr_simple_clause pr_id = function | [] -> mt () | l -> pr_in (spc () ++ prlist_with_sep spc pr_id l) +let pr_in_hyp_as pr_id = function + | None -> mt () + | Some (id,ipat) -> pr_simple_clause pr_id [id] ++ pr_as_ipat ipat + let pr_clauses pr_id = function | { onhyps=None; concl_occs=occs } -> if occs = no_occurrences_expr then pr_in (str " * |-") @@ -702,10 +702,11 @@ and pr_atom1 = function | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) - | TacApply (a,ev,cb) -> + | TacApply (a,ev,cb,inhyp) -> hov 1 ((if a then mt() else str "simple ") ++ str (with_evars ev "apply") ++ spc () ++ - prlist_with_sep pr_coma pr_with_bindings cb) + prlist_with_sep pr_coma pr_with_bindings cb ++ + pr_in_hyp_as pr_ident inhyp) | TacElim (ev,cb,cbo) -> hov 1 (str (with_evars ev "elim") ++ pr_arg pr_with_bindings cb ++ pr_opt pr_eliminator cbo) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 9c1a10b0e..fc5df1a6c 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -308,8 +308,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacVmCastNoCheck c -> <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> - | Tacexpr.TacApply (b,false,cb) -> - <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ >> + | Tacexpr.TacApply (b,false,cb,None) -> + <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >> | Tacexpr.TacElim (false,cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in @@ -345,7 +345,7 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacCut c -> <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >> | Tacexpr.TacAssert (t,ipat,c) -> - let ipat = mlexpr_of_located mlexpr_of_intro_pattern ipat in + let ipat = mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern) ipat in <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ $mlexpr_of_constr c$ >> | Tacexpr.TacGeneralize cl -> diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b6be71ea0..3f66ddcbc 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -98,7 +98,6 @@ type 'id message_token = | MsgInt of int | MsgIdent of 'id - type 'id gsimple_clause = ('id raw_hyp_location) option (* onhyps: [None] means *on every hypothesis* @@ -154,7 +153,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacExact of 'constr | TacExactNoCheck of 'constr | TacVmCastNoCheck of 'constr - | TacApply of advanced_flag * evars_flag * 'constr with_bindings list + | TacApply of advanced_flag * evars_flag * 'constr with_bindings list * + ('id * intro_pattern_expr located option) option | TacElim of evars_flag * 'constr with_bindings * 'constr with_bindings option | TacElimType of 'constr @@ -166,7 +166,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacCofix of identifier option | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list | TacCut of 'constr - | TacAssert of 'tac option * intro_pattern_expr located * 'constr + | TacAssert of 'tac option * intro_pattern_expr located option * 'constr | TacGeneralize of ('constr with_occurrences * name) list | TacGeneralizeDep of 'constr | TacLetTac of name * 'constr * 'id gclause * letin_flag diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 299e3fd17..741874cb3 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -107,7 +107,7 @@ let clean_tmp gls = clean_all (tmp_ids gls) gls let assert_postpone id t = - assert_as true (dummy_loc, Genarg.IntroIdentifier id) t + assert_tac (Name id) t (* start a proof *) @@ -780,7 +780,7 @@ let consider_tac c hyps gls = | _ -> let id = pf_get_new_id (id_of_string "_tmp") gls in tclTHEN - (forward None (dummy_loc, Genarg.IntroIdentifier id) c) + (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c) (consider_match false [] [id] hyps) gls diff --git a/tactics/equality.ml b/tactics/equality.ml index e3914b8c5..eba3a119f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -272,7 +272,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = let e = build_coq_eq () in let sym = build_coq_sym_eq () in let eq = applist (e, [t1;c1;c2]) in - tclTHENS (assert_tac false Anonymous eq) + tclTHENS (assert_as false None eq) [onLastHyp (fun id -> tclTHEN (tclTRY (general_multi_rewrite false false (inj_open (mkVar id),NoBindings) clause)) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 845483436..62ac0d4d7 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -486,23 +486,6 @@ END -TACTIC EXTEND apply_in -| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] -> - [ apply_in false id cl None ] -| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) - "as" simple_intropattern(ipat) ] -> - [ apply_in false id cl (Some ipat) ] -END - - -TACTIC EXTEND eapply_in -| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] -> - [ apply_in true id cl None ] -| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) - "as" simple_intropattern(ipat) ] -> - [ apply_in true id cl (Some ipat) ] -END - (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) TACTIC EXTEND generalize_eqs diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 6498c3542..c9992c36f 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -39,9 +39,12 @@ let h_exact_no_check c = abstract_tactic (TacExactNoCheck (inj_open c)) (exact_no_check c) let h_vm_cast_no_check c = abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c) -let h_apply simple ev cb = - abstract_tactic (TacApply (simple,ev,cb)) +let h_apply simple ev cb = + abstract_tactic (TacApply (simple,ev,cb,None)) (apply_with_ebindings_gen simple ev cb) +let h_apply_in simple ev cb (id,ipat as inhyp) = + abstract_tactic (TacApply (simple,ev,cb,Some inhyp)) + (apply_in simple ev id cb ipat) let h_elim ev cb cbo = abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) (elim ev cb cbo) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 851c33e7a..faa8c4150 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -39,6 +39,9 @@ val h_vm_cast_no_check : constr -> tactic val h_apply : advanced_flag -> evars_flag -> open_constr with_bindings list -> tactic +val h_apply_in : advanced_flag -> evars_flag -> + open_constr with_bindings list -> + identifier * intro_pattern_expr located option -> tactic val h_elim : evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic diff --git a/tactics/inv.ml b/tactics/inv.ml index e0ed2d1ef..b6923bb83 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -469,7 +469,7 @@ let raw_inversion inv_kind id status names gl = case_nodep_then_using in (tclTHENS - (true_cut Anonymous cut_concl) + (assert_tac Anonymous cut_concl) [case_tac names (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) (Some elim_predicate) ([],[]) ind indclause; diff --git a/tactics/refine.ml b/tactics/refine.ml index 9225fd9d7..88038a88e 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -314,7 +314,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = because of evars limitation, use non dependent assert instead *) | LetIn (Name id,c1,t1,c2), _ -> tclTHENS - (assert_tac true (Name id) t1) + (assert_tac (Name id) t1) [(match List.hd sgp with | None -> tclIDTAC | Some th -> onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)); diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 644a68666..f74d6dfdf 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -1917,7 +1917,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_ let eq_left_to_right = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c1 ; c2 ])) in let eq_right_to_left = mkApp (relation.rel_aeq, Array.of_list (List.append args [ c2 ; c1 ])) in let replace dir eq = - tclTHENS (assert_tac false Anonymous eq) + tclTHENS (assert_as false None eq) [onLastHyp (fun id -> tclTHEN (rewrite_tac dir all_occurrences (mkVar id) ~new_goals) @@ -1929,7 +1929,7 @@ let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_ with Optimize -> (* (!replace tac_opt c1 c2) gl *) let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in - tclTHENS (assert_tac false Anonymous eq) + tclTHENS (assert_as false None eq) [onLastHyp (fun id -> tclTHEN (rewrite_tac false all_occurrences (mkVar id) ~new_goals) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index e89672e51..bf0534167 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -596,20 +596,24 @@ let intern_red_expr ist = function | Simpl o -> Simpl (Option.map (intern_constr_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r +let intern_in_hyp_as ist lf (id,ipat) = + (intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat) + +let intern_hyp_list ist = List.map (intern_hyp_or_metaid ist) let intern_inversion_strength lf ist = function | NonDepInversion (k,idl,ids) -> - NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl, + NonDepInversion (k,intern_hyp_list ist idl, Option.map (intern_intro_pattern lf ist) ids) | DepInversion (k,copt,ids) -> DepInversion (k, Option.map (intern_constr ist) copt, Option.map (intern_intro_pattern lf ist) ids) | InversionUsing (c,idl) -> - InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl) + InversionUsing (intern_constr ist c, intern_hyp_list ist idl) (* Interprets an hypothesis name *) let intern_hyp_location ist (((b,occs),id),hl) = - (((b,List.map (intern_or_var ist) occs),intern_hyp ist (skip_metaid id)), hl) + (((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl) let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c = let c = intern_gen as_type ~allow_patvar:true ~ltacvars:(ltacvar,[]) @@ -704,8 +708,9 @@ let rec intern_atomic lf ist x = | TacExact c -> TacExact (intern_constr ist c) | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c) - | TacApply (a,ev,cb) -> - TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb) + | TacApply (a,ev,cb,inhyp) -> + TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb, + Option.map (intern_in_hyp_as ist lf) inhyp) | TacElim (ev,cb,cbo) -> TacElim (ev,intern_constr_with_bindings ist cb, Option.map (intern_constr_with_bindings ist) cbo) @@ -723,7 +728,7 @@ let rec intern_atomic lf ist x = | TacCut c -> TacCut (intern_type ist c) | TacAssert (otac,ipat,c) -> TacAssert (Option.map (intern_tactic ist) otac, - intern_intro_pattern lf ist ipat, + Option.map (intern_intro_pattern lf ist) ipat, intern_constr_gen (otac<>None) ist c) | TacGeneralize cl -> TacGeneralize (List.map (fun (c,na) -> @@ -1659,6 +1664,9 @@ let rec interp_intro_pattern ist gl = function and interp_or_and_intro_pattern ist gl = List.map (List.map (interp_intro_pattern ist gl)) +let interp_in_hyp_as ist gl (id,ipat) = + (interp_hyp ist gl id,Option.map (interp_intro_pattern ist gl) ipat) + (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) let coerce_to_quantified_hypothesis = function @@ -2186,8 +2194,11 @@ and interp_atomic ist gl = function | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c) - | TacApply (a,ev,cb) -> + | TacApply (a,ev,cb,None) -> h_apply a ev (List.map (interp_open_constr_with_bindings ist gl) cb) + | TacApply (a,ev,cb,Some cl) -> + h_apply_in a ev (List.map (interp_open_constr_with_bindings ist gl) cb) + (interp_in_hyp_as ist gl cl) | TacElim (ev,cb,cbo) -> h_elim ev (interp_constr_with_bindings ist gl cb) (Option.map (interp_constr_with_bindings ist gl) cbo) @@ -2207,7 +2218,7 @@ and interp_atomic ist gl = function let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in abstract_tactic (TacAssert (t,ipat,inj_open c)) (Tactics.forward (Option.map (interp_tactic ist) t) - (interp_intro_pattern ist gl ipat) c) + (Option.map (interp_intro_pattern ist gl) ipat) c) | TacGeneralize cl -> h_generalize_gen (pf_interp_constr_with_occurrences_and_name_as_list ist gl cl) @@ -2523,8 +2534,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacExact c -> TacExact (subst_rawconstr subst c) | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c) | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c) - | TacApply (a,ev,cb) -> - TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb) + | TacApply (a,ev,cb,cl) -> + TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb,cl) | TacElim (ev,cb,cbo) -> TacElim (ev,subst_raw_with_bindings subst cb, Option.map (subst_raw_with_bindings subst) cbo) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b4371ac23..3511585d5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -566,17 +566,11 @@ let cut c gl = let cut_intro t = tclTHENFIRST (cut t) intro -(* let cut_replacing id t tac = - tclTHENS (cut t) - [tclORELSE - (intro_replacing id) - (tclORELSE (intro_erasing id) (intro_using id)); - tac (refine_no_check (mkVar id)) ] *) - (* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le but, ou dans une autre hypothèse *) let cut_replacing id t tac = - tclTHENS (cut t) [ intro_replacing id; tac (refine_no_check (mkVar id)) ] + tclTHENLAST (internal_cut_rev_replace id t) + (tac (refine_no_check (mkVar id))) let cut_in_parallel l = let rec prec = function @@ -729,32 +723,54 @@ let general_case_analysis with_evars (c,lbindc as cx) = let simplest_case c = general_case_analysis false (c,NoBindings) +(* Apply a tactic below the products of the conclusion of a lemma *) + +let descend_in_conjunctions tac exit c gl = + try + let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + match match_with_conjunction (snd (decompose_prod t)) with + | Some _ -> + let n = (mis_constr_nargs mind).(0) in + let sort = elimination_sort_of_goal gl in + let elim = pf_apply make_case_gen gl mind sort in + tclTHENLAST + (general_elim true (c,NoBindings) (elim,NoBindings)) + (tclTHENLIST [ + tclDO n intro; + tclLAST_NHYPS n (fun l -> + tclFIRST + (List.map (fun id -> tclTHEN (tac (mkVar id)) (thin l)) l))]) + gl + | None -> + raise Exit + with RefinerError _|UserError _|Exit -> exit () + (****************************************************) (* Resolution tactics *) (****************************************************) (* Resolution with missing arguments *) -let general_apply with_delta with_destruct with_evars (c,lbind) gl = +let check_evars sigma evm gl = + let origsigma = gl.sigma in + let rest = + Evd.fold (fun ev evi acc -> + if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev) + then Evd.add acc ev evi else acc) + evm Evd.empty + in + if rest <> Evd.empty then + errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ + fnl () ++ pr_evar_map rest) + +let general_apply with_delta with_destruct with_evars (c,lbind) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in (* The actual type of the theorem. It will be matched against the goal. If this fails, then the head constant will be unfolded step by step. *) - let concl_nprod = nb_prod (pf_concl gl) in + let concl_nprod = nb_prod (pf_concl gl0) in let evm, c = c in - let origsigm = gl.sigma in - let check_evars sigm = - let rest = - Evd.fold (fun ev evi acc -> - if Evd.mem sigm ev && not (Evd.mem origsigm ev) && not (Evd.is_defined sigm ev) then - Evd.add acc ev evi - else acc) evm Evd.empty - in - if not (rest = Evd.empty) then - errorlabstrm "apply" (str"Uninstantiated existential variables: " ++ fnl () ++ - pr_evar_map rest) - in let rec try_main_apply c gl = let thm_ty0 = nf_betaiota (pf_type_of gl c) in let try_apply thm_ty nprod = @@ -762,7 +778,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl = if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in let res = Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in - if not with_evars then check_evars (fst res).sigma; + if not with_evars then check_evars (fst res).sigma evm gl0; res in try try_apply thm_ty0 concl_nprod @@ -780,32 +796,15 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl = try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit with PretypeError _|RefinerError _|UserError _|Failure _|Exit -> if with_destruct then - try - let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in - match match_with_conjunction (snd (decompose_prod t)) with - | Some _ -> - let n = (mis_constr_nargs mind).(0) in - let sort = elimination_sort_of_goal gl in - let elim = pf_apply make_case_gen gl mind sort in - tclTHENLAST - (general_elim with_evars (c,NoBindings) (elim,NoBindings)) - (tclTHENLIST [ - tclDO n intro; - tclLAST_NHYPS n (fun l -> - tclFIRST - (List.map (fun id -> - tclTHEN (try_main_apply (mkVar id)) (thin l)) l)) - ]) gl - | None -> - raise Exit - with RefinerError _|UserError _|Exit -> raise exn + descend_in_conjunctions + try_main_apply (fun _ -> raise exn) c gl else raise exn in try_red_apply thm_ty0 in - if evm = Evd.empty then try_main_apply c gl + if evm = Evd.empty then try_main_apply c gl0 else - tclTHEN (tclEVARS (Evd.merge gl.sigma evm)) (try_main_apply c) gl + tclTHEN (tclEVARS (Evd.merge gl0.sigma evm)) (try_main_apply c) gl0 let rec apply_with_ebindings_gen b e = function | [] -> @@ -855,21 +854,43 @@ let find_matching_clause unifier clause = with NotExtensibleClause -> failwith "Cannot apply" in find clause -let progress_with_clause innerclause clause = +let progress_with_clause flags innerclause clause = let ordered_metas = List.rev (clenv_independent clause) in if ordered_metas = [] then error "Statement without assumptions."; - let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in + let f mv = + find_matching_clause (clenv_fchain mv ~flags clause) innerclause in try list_try_find f ordered_metas with Failure _ -> error "Unable to unify." -let apply_in_once gl innerclause (d,lbind) = +let apply_in_once_main flags innerclause (d,lbind) gl = let thm = nf_betaiota (pf_type_of gl d) in let rec aux clause = - try progress_with_clause innerclause clause + try progress_with_clause flags innerclause clause with err -> try aux (clenv_push_prod clause) - with NotExtensibleClause -> raise err - in aux (make_clenv_binding gl (d,thm) lbind) + with NotExtensibleClause -> raise err in + aux (make_clenv_binding gl (d,thm) lbind) + +let apply_in_once with_delta with_destruct with_evars id ((sigma,d),lbind) gl0 = + let flags = + if with_delta then default_unify_flags else default_no_delta_unify_flags in + let t' = pf_get_hyp_typ gl0 id in + let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in + let rec aux c gl = + try + let clause = apply_in_once_main flags innerclause (c,lbind) gl in + let res = clenv_refine_in with_evars id clause gl in + if not with_evars then check_evars (fst res).sigma sigma gl0; + res + with exn when with_destruct -> + descend_in_conjunctions aux (fun _ -> raise exn) c gl + in + if sigma = Evd.empty then aux d gl0 + else + tclTHEN (tclEVARS (Evd.merge gl0.sigma sigma)) (aux d) gl0 + + + (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1200,7 +1221,9 @@ let intro_patterns = function let make_id s = fresh_id [] (default_id_of_sort s) -let prepare_intros s (loc,ipat) gl = match ipat with +let prepare_intros s ipat gl = match ipat with + | None -> make_id s gl, tclIDTAC + | Some (loc,ipat) -> match ipat with | IntroIdentifier id -> id, tclIDTAC | IntroAnonymous -> make_id s gl, tclIDTAC | IntroFresh id -> fresh_id [] id gl, tclIDTAC @@ -1212,11 +1235,11 @@ let prepare_intros s (loc,ipat) gl = match ipat with intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) let ipat_of_name = function - | Anonymous -> IntroAnonymous - | Name id -> IntroIdentifier id + | Anonymous -> None + | Name id -> Some (dloc, IntroIdentifier id) let allow_replace c gl = function (* A rather arbitrary condition... *) - | _, IntroIdentifier id -> + | Some (_, IntroIdentifier id) -> fst (decompose_app (snd (decompose_lam_assum c))) = mkVar id | _ -> false @@ -1231,8 +1254,7 @@ let assert_as first ipat c gl = (if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl | _ -> error "Not a proposition or a type." -let assert_tac first na = assert_as first (dloc,ipat_of_name na) -let true_cut = assert_tac true +let assert_tac na = assert_as true (ipat_of_name na) (* apply in as *) @@ -1246,12 +1268,13 @@ let as_tac id ipat = match ipat with user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected") | None -> tclIDTAC -let apply_in with_evars id lemmas ipat gl = - let t' = pf_get_hyp_typ gl id in - let innermostclause = mk_clenv_from_n gl (Some 0) (mkVar id,t') in - let clause = List.fold_left (apply_in_once gl) innermostclause lemmas in - tclTHEN (clenv_refine_in with_evars id clause) (as_tac id ipat) - gl +let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl = + tclTHEN + (tclMAP (apply_in_once with_delta with_destruct with_evars id) lemmas) + (as_tac id ipat) + gl + +let apply_in simple with_evars = general_apply_in simple simple with_evars (**************************) (* Generalize tactics *) @@ -1499,6 +1522,9 @@ let forward usetac ipat c gl = | Some tac -> tclTHENFIRST (assert_as true ipat c) tac gl +let pose_proof na c = forward None (ipat_of_name na) c +let assert_by na t tac = forward (Some tac) (ipat_of_name na) t + (*****************************) (* Ad hoc unfold *) (*****************************) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f18860af4..050473bfe 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -193,7 +193,9 @@ val eapply_with_ebindings : open_constr with_ebindings -> tactic val cut_and_apply : constr -> tactic -val apply_in : evars_flag -> identifier -> constr with_ebindings list -> +val apply_in : + advanced_flag -> evars_flag -> identifier -> + open_constr with_ebindings list -> intro_pattern_expr located option -> tactic (*s Elimination tactics. *) @@ -344,12 +346,14 @@ val cut_replacing : identifier -> constr -> (tactic -> tactic) -> tactic val cut_in_parallel : constr list -> tactic -val assert_as : bool -> intro_pattern_expr located -> constr -> tactic -val forward : tactic option -> intro_pattern_expr located -> constr -> tactic +val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic +val forward : tactic option -> intro_pattern_expr located option -> constr -> tactic val letin_tac : (bool * intro_pattern_expr located) option -> name -> constr -> types option -> clause -> tactic -val true_cut : name -> constr -> tactic -val assert_tac : bool -> name -> constr -> tactic +val assert_tac : name -> types -> tactic +val assert_by : name -> types -> tactic -> tactic +val pose_proof : name -> constr -> tactic + val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * name) list -> tactic val generalize_dep : constr -> tactic diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 319ed6880..4f47702c6 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -12,6 +12,44 @@ intros; apply Znot_le_gt, Zgt_lt in H. apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto. Qed. +(* Test application under tuples *) + +Goal (forall x, x=0 <-> 0=x) -> 1=0 -> 0=1. +intros H H'. +apply H in H'. +exact H'. +Qed. + +(* Test as clause *) + +Goal (forall x, x=0 <-> (0=x /\ True)) -> 1=0 -> True. +intros H H'. +apply H in H' as (_,H'). +exact H'. +Qed. + +(* Test application modulo conversion *) + +Goal (forall x, id x = 0 -> 0 = x) -> 1 = id 0 -> 0 = 1. +intros H H'. +apply H in H'. +exact H'. +Qed. + +(* Check apply/eapply distinction in presence of open terms *) + +Parameter h : forall x y z : nat, x = z -> x = y. +Implicit Arguments h [[x] [y]]. +Goal 1 = 0 -> True. +intro H. +apply h in H || exact I. +Qed. + +Goal False -> 1 = 0. +intro H. +apply h || contradiction. +Qed. + (* Check if it unfolds when there are not enough premises *) Goal forall n, n = S n -> False. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index e798d8755..a17ea69fe 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -536,7 +536,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) tclREPEAT ( tclTHENSEQ [ - apply_in false freshz [(andb_prop()),Rawterm.NoBindings] None; + apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None; fun gl -> let fresht = fresh_id (!avoid) (id_of_string "Z") gsig in @@ -748,8 +748,8 @@ let compute_dec_tact ind lnamesparrec nparrec = Pfedit.by ( tclTHENSEQ [ intros_using fresh_first_intros; intros_using [freshn;freshm]; - assert_as true (dl,Genarg.IntroIdentifier freshH) ( - mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) + assert_tac (Name freshH) ( + mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) ) ]); (*we do this so we don't have to prove the same goal twice *) Pfedit.by ( tclTHEN @@ -795,7 +795,7 @@ let compute_dec_tact ind lnamesparrec nparrec = unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all; - assert_as true (dl,Genarg.IntroIdentifier freshH3) + assert_tac (Name freshH3) (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])) ]); Pfedit.by |