diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 283 |
1 files changed, 191 insertions, 92 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index d6de2666..885138e4 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 9430 2006-12-12 08:25:19Z herbelin $ *) +(* $Id: extratactics.ml4 11166 2008-06-22 13:23:35Z herbelin $ *) open Pp open Pcoq @@ -16,6 +16,8 @@ open Genarg open Extraargs open Mod_subst open Names +open Tacexpr +open Rawterm (* Equality *) open Equality @@ -23,7 +25,7 @@ open Equality TACTIC EXTEND replace ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Util.option_map Tacinterp.eval_tactic tac) ] +-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Option.map Tacinterp.eval_tactic tac) ] END TACTIC EXTEND replace_term_left @@ -41,25 +43,93 @@ TACTIC EXTEND replace_term -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ] END +let induction_arg_of_quantified_hyp = function + | AnonHyp n -> ElimOnAnonHyp n + | NamedHyp id -> ElimOnIdent (Util.dummy_loc,id) + +(* Versions *_main must come first!! so that "1" is interpreted as a + ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a + ElimOnIdent and not as "constr" *) + +TACTIC EXTEND simplify_eq_main +| [ "simplify_eq" constr_with_bindings(c) ] -> + [ dEq false (Some (ElimOnConstr c)) ] +END TACTIC EXTEND simplify_eq - [ "simplify_eq" quantified_hypothesis_opt(h) ] -> [ dEq h ] + [ "simplify_eq" ] -> [ dEq false None ] +| [ "simplify_eq" quantified_hypothesis(h) ] -> + [ dEq false (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND esimplify_eq_main +| [ "esimplify_eq" constr_with_bindings(c) ] -> + [ dEq true (Some (ElimOnConstr c)) ] +END +TACTIC EXTEND esimplify_eq +| [ "esimplify_eq" ] -> [ dEq true None ] +| [ "esimplify_eq" quantified_hypothesis(h) ] -> + [ dEq true (Some (induction_arg_of_quantified_hyp h)) ] END +TACTIC EXTEND discriminate_main +| [ "discriminate" constr_with_bindings(c) ] -> + [ discr_tac false (Some (ElimOnConstr c)) ] +END TACTIC EXTEND discriminate - [ "discriminate" quantified_hypothesis_opt(h) ] -> [ discr_tac h ] +| [ "discriminate" ] -> [ discr_tac false None ] +| [ "discriminate" quantified_hypothesis(h) ] -> + [ discr_tac false (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND ediscriminate_main +| [ "ediscriminate" constr_with_bindings(c) ] -> + [ discr_tac true (Some (ElimOnConstr c)) ] +END +TACTIC EXTEND ediscriminate +| [ "ediscriminate" ] -> [ discr_tac true None ] +| [ "ediscriminate" quantified_hypothesis(h) ] -> + [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_discrHyp id = h_discriminate (Some id) +let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings) +TACTIC EXTEND injection_main +| [ "injection" constr_with_bindings(c) ] -> + [ injClause [] false (Some (ElimOnConstr c)) ] +END TACTIC EXTEND injection - [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause [] h ] +| [ "injection" ] -> [ injClause [] false None ] +| [ "injection" quantified_hypothesis(h) ] -> + [ injClause [] false (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND einjection_main +| [ "einjection" constr_with_bindings(c) ] -> + [ injClause [] true (Some (ElimOnConstr c)) ] +END +TACTIC EXTEND einjection +| [ "einjection" ] -> [ injClause [] true None ] +| [ "einjection" quantified_hypothesis(h) ] -> [ injClause [] true (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND injection_as_main +| [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> + [ injClause ipat false (Some (ElimOnConstr c)) ] END TACTIC EXTEND injection_as - [ "injection" quantified_hypothesis_opt(h) - "as" simple_intropattern_list(ipat)] -> [ injClause ipat h ] +| [ "injection" "as" simple_intropattern_list(ipat)] -> + [ injClause ipat false None ] +| [ "injection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> + [ injClause ipat false (Some (induction_arg_of_quantified_hyp h)) ] +END +TACTIC EXTEND einjection_as_main +| [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> + [ injClause ipat true (Some (ElimOnConstr c)) ] +END +TACTIC EXTEND einjection_as +| [ "einjection" "as" simple_intropattern_list(ipat)] -> + [ injClause ipat true None ] +| [ "einjection" quantified_hypothesis(h) "as" simple_intropattern_list(ipat) ] -> + [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_injHyp id = h_injection (Some id) +let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings) TACTIC EXTEND conditional_rewrite | [ "conditional" tactic(tac) "rewrite" orient(b) constr_with_bindings(c) ] @@ -150,82 +220,82 @@ let refine_tac = h_refine open Setoid_replace -TACTIC EXTEND setoid_replace - [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] -END - -TACTIC EXTEND setoid_rewrite - [ "setoid_rewrite" orient(b) constr(c) ] - -> [ general_s_rewrite b c ~new_goals:[] ] - | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ] - -> [ general_s_rewrite b c ~new_goals:l ] - | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] -> - [ general_s_rewrite_in h b c ~new_goals:[] ] - | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> - [ general_s_rewrite_in h b c ~new_goals:l ] -END - -VERNAC COMMAND EXTEND AddSetoid1 - [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ add_setoid n a aeq t ] -| [ "Add" "Morphism" constr(m) ":" ident(n) ] -> - [ new_named_morphism n m None ] -| [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> - [ new_named_morphism n m (Some s)] -END - -VERNAC COMMAND EXTEND AddRelation1 - [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> - [ add_relation n a aeq (Some t) (Some t') None ] -| [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "as" ident(n) ] -> - [ add_relation n a aeq (Some t) None None ] -| [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> - [ add_relation n a aeq None None None ] -END - -VERNAC COMMAND EXTEND AddRelation2 - [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> - [ add_relation n a aeq None (Some t') None ] -| [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> - [ add_relation n a aeq None (Some t') (Some t'') ] -END - -VERNAC COMMAND EXTEND AddRelation3 - [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] -> - [ add_relation n a aeq (Some t) None (Some t') ] -| [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> - [ add_relation n a aeq (Some t) (Some t') (Some t'') ] -| [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] -> - [ add_relation n a aeq None None (Some t) ] -END - -TACTIC EXTEND setoid_symmetry - [ "setoid_symmetry" ] -> [ setoid_symmetry ] - | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] -END - -TACTIC EXTEND setoid_reflexivity - [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] -END - -TACTIC EXTEND setoid_transitivity - [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] -END +(* TACTIC EXTEND setoid_replace *) +(* [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> *) +(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> *) +(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *) +(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> *) +(* [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> *) +(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> *) +(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *) +(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] *) +(* | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> *) +(* [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] *) +(* END *) + +(* TACTIC EXTEND setoid_rewrite *) +(* [ "setoid_rewrite" orient(b) constr(c) ] *) +(* -> [ general_s_rewrite b c ~new_goals:[] ] *) +(* | [ "setoid_rewrite" orient(b) constr(c) "generate" "side" "conditions" constr_list(l) ] *) +(* -> [ general_s_rewrite b c ~new_goals:l ] *) +(* | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) ] -> *) +(* [ general_s_rewrite_in h b c ~new_goals:[] ] *) +(* | [ "setoid_rewrite" orient(b) constr(c) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> *) +(* [ general_s_rewrite_in h b c ~new_goals:l ] *) +(* END *) + +(* VERNAC COMMAND EXTEND AddSetoid1 *) +(* [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> *) +(* [ add_setoid n a aeq t ] *) +(* | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> *) +(* [ new_named_morphism n m None ] *) +(* | [ "Add" "Morphism" constr(m) "with" "signature" morphism_signature(s) "as" ident(n) ] -> *) +(* [ new_named_morphism n m (Some s)] *) +(* END *) + +(* VERNAC COMMAND EXTEND AddRelation1 *) +(* [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *) +(* [ add_relation n a aeq (Some t) (Some t') None ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "as" ident(n) ] -> *) +(* [ add_relation n a aeq (Some t) None None ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> *) +(* [ add_relation n a aeq None None None ] *) +(* END *) + +(* VERNAC COMMAND EXTEND AddRelation2 *) +(* [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "as" ident(n) ] -> *) +(* [ add_relation n a aeq None (Some t') None ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *) +(* [ add_relation n a aeq None (Some t') (Some t'') ] *) +(* END *) + +(* VERNAC COMMAND EXTEND AddRelation3 *) +(* [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "transitivity" "proved" "by" constr(t') "as" ident(n) ] -> *) +(* [ add_relation n a aeq (Some t) None (Some t') ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(t) "symmetry" "proved" "by" constr(t') "transitivity" "proved" "by" constr(t'') "as" ident(n) ] -> *) +(* [ add_relation n a aeq (Some t) (Some t') (Some t'') ] *) +(* | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(t) "as" ident(n) ] -> *) +(* [ add_relation n a aeq None None (Some t) ] *) +(* END *) + +(* TACTIC EXTEND setoid_symmetry *) +(* [ "setoid_symmetry" ] -> [ setoid_symmetry ] *) +(* | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] *) +(* END *) + +(* TACTIC EXTEND setoid_reflexivity *) +(* [ "setoid_reflexivity" ] -> [ setoid_reflexivity ] *) +(* END *) + +(* TACTIC EXTEND setoid_transitivity *) +(* [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity t ] *) +(* END *) (* Inversion lemmas (Leminv) *) @@ -234,10 +304,10 @@ open Leminv VERNAC COMMAND EXTEND DeriveInversionClear [ "Derive" "Inversion_clear" ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_clear_tac ] + -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_clear_tac ] | [ "Derive" "Inversion_clear" natural(n) ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_clear_tac ] + -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_clear_tac ] | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort(s) ] -> [ add_inversion_lemma_exn na c s false inv_clear_tac ] @@ -257,10 +327,10 @@ VERNAC COMMAND EXTEND DeriveInversion -> [ add_inversion_lemma_exn na c (RProp Null) false inv_tac ] | [ "Derive" "Inversion" ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_tac ] + -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ] | [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ] - -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_tac ] + -> [ inversion_lemma_from_goal n na id Term.prop_sort false inv_tac ] END VERNAC COMMAND EXTEND DeriveDependentInversion @@ -290,16 +360,17 @@ TACTIC EXTEND evar END open Tacexpr +open Tacticals TACTIC EXTEND instantiate [ "instantiate" "(" integer(i) ":=" raw(c) ")" hloc(hl) ] -> [instantiate i c hl ] +| [ "instantiate" ] -> [ tclNORMEVAR ] END (** Nijmegen "step" tactic for setoid rewriting *) -open Tacticals open Tactics open Tactics open Libnames @@ -400,8 +471,36 @@ VERNAC COMMAND EXTEND ImplicitTactic [ Tacinterp.declare_implicit_tactic (Tacinterp.interp tac) ] END + + + +(*spiwack : Vernac commands for retroknowledge *) + +VERNAC COMMAND EXTEND RetroknowledgeRegister + | [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] -> + [ let tc = Constrintern.interp_constr Evd.empty (Global.env ()) c in + let tb = Constrintern.interp_constr Evd.empty (Global.env ()) b in + Global.register f tc tb ] +END + + + TACTIC EXTEND apply_in -| ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in id [c] ] +| ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in false id [c] ] | ["apply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") - "in" hyp(id) ] -> [ apply_in id (c::cl) ] + "in" hyp(id) ] -> [ apply_in false id (c::cl) ] END + + +TACTIC EXTEND eapply_in +| ["eapply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in true id [c] ] +| ["epply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") + "in" hyp(id) ] -> [ apply_in true id (c::cl) ] +END + +(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as + defined by Conor McBride *) +TACTIC EXTEND generalize_eqs +| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ] +END + |