diff options
Diffstat (limited to 'tactics/tactics.mli')
-rw-r--r-- | tactics/tactics.mli | 194 |
1 files changed, 101 insertions, 93 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index fb5c0efd..0e552bd4 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactics.mli 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Util @@ -27,20 +27,14 @@ open Genarg open Tacexpr open Nametab open Rawterm +open Pattern open Termops (*i*) -val inj_open : constr -> open_constr -val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen -val inj_ebindings : constr bindings -> open_constr bindings - (* Main tactics. *) (*s General functions. *) -val type_clenv_binding : goal sigma -> - constr * constr -> open_constr bindings -> constr - val string_of_inductive : constr -> string val head_constr : constr -> constr * constr list val head_constr_bound : constr -> constr * constr list @@ -56,19 +50,19 @@ val convert_concl : constr -> cast_kind -> tactic val convert_hyp : named_declaration -> tactic val thin : identifier list -> tactic val mutual_fix : - identifier -> int -> (identifier * int * constr) list -> tactic + identifier -> int -> (identifier * int * constr) list -> int -> tactic val fix : identifier option -> int -> tactic -val mutual_cofix : identifier -> (identifier * constr) list -> tactic +val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic val cofix : identifier option -> tactic (*s Introduction tactics. *) +val fresh_id_in_env : identifier list -> identifier -> env -> identifier val fresh_id : identifier list -> identifier -> goal sigma -> identifier val find_intro_names : rel_context -> goal sigma -> identifier list val intro : tactic val introf : tactic -val intro_force : bool -> tactic val intro_move : identifier option -> identifier move_location -> tactic (* [intro_avoiding idl] acts as intro but prevents the new identifier @@ -106,9 +100,9 @@ val try_intros_until : (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) -val onInductionArg : - (constr with_ebindings -> tactic) -> - constr with_ebindings induction_arg -> tactic +val onInductionArg : + (constr with_bindings -> tactic) -> + constr with_bindings induction_arg -> tactic (*s Introduction tactics with eliminations. *) @@ -130,35 +124,35 @@ val exact_proof : Topconstr.constr_expr -> tactic type tactic_reduction = env -> evar_map -> constr -> constr val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic -val reduct_option : tactic_reduction * cast_kind -> simple_clause -> tactic +val reduct_option : tactic_reduction * cast_kind -> goal_location -> tactic val reduct_in_concl : tactic_reduction * cast_kind -> tactic -val change_in_concl : (occurrences * constr) option -> constr -> tactic -val change_in_hyp : (occurrences * constr) option -> constr -> +val change_in_concl : (occurrences * constr_pattern) option -> constr -> + tactic +val change_in_hyp : (occurrences * constr_pattern) option -> constr -> hyp_location -> tactic val red_in_concl : tactic -val red_in_hyp : hyp_location -> tactic -val red_option : simple_clause -> tactic +val red_in_hyp : hyp_location -> tactic +val red_option : goal_location -> tactic val hnf_in_concl : tactic -val hnf_in_hyp : hyp_location -> tactic -val hnf_option : simple_clause -> tactic +val hnf_in_hyp : hyp_location -> tactic +val hnf_option : goal_location -> tactic val simpl_in_concl : tactic -val simpl_in_hyp : hyp_location -> tactic -val simpl_option : simple_clause -> tactic +val simpl_in_hyp : hyp_location -> tactic +val simpl_option : goal_location -> tactic val normalise_in_concl : tactic -val normalise_in_hyp : hyp_location -> tactic -val normalise_option : simple_clause -> tactic +val normalise_in_hyp : hyp_location -> tactic +val normalise_option : goal_location -> tactic val normalise_vm_in_concl : tactic val unfold_in_concl : (occurrences * evaluable_global_reference) list -> tactic -val unfold_in_hyp : +val unfold_in_hyp : (occurrences * evaluable_global_reference) list -> hyp_location -> tactic -val unfold_option : - (occurrences * evaluable_global_reference) list -> simple_clause - -> tactic +val unfold_option : + (occurrences * evaluable_global_reference) list -> goal_location -> tactic val change : - (occurrences * constr) option -> constr -> clause -> tactic -val pattern_option : - (occurrences * constr) list -> simple_clause -> tactic + constr_pattern option -> constr -> clause -> tactic +val pattern_option : + (occurrences * constr) list -> goal_location -> tactic val reduce : red_expr -> clause -> tactic val unfold_constr : global_reference -> tactic @@ -168,7 +162,7 @@ val clear : identifier list -> tactic val clear_body : identifier list -> tactic val keep : identifier list -> tactic -val specialize : int option -> constr with_ebindings -> tactic +val specialize : int option -> constr with_bindings -> tactic val move_hyp : bool -> identifier -> identifier move_location -> tactic val rename_hyp : (identifier * identifier) list -> tactic @@ -181,32 +175,30 @@ val apply_type : constr -> constr list -> tactic val apply_term : constr -> constr list -> tactic val bring_hyps : named_context -> tactic -val apply : constr -> tactic -val apply_without_reduce : constr -> tactic -val apply_list : constr list -> tactic - -val apply_with_ebindings_gen : - advanced_flag -> evars_flag -> open_constr with_ebindings list -> tactic +val apply : constr -> tactic +val eapply : constr -> tactic + +val apply_with_bindings_gen : + advanced_flag -> evars_flag -> constr with_bindings located list -> tactic val apply_with_bindings : constr with_bindings -> tactic val eapply_with_bindings : constr with_bindings -> tactic -val apply_with_ebindings : open_constr with_ebindings -> tactic -val eapply_with_ebindings : open_constr with_ebindings -> tactic - val cut_and_apply : constr -> tactic -val apply_in : +val apply_in : advanced_flag -> evars_flag -> identifier -> - open_constr with_ebindings list -> - intro_pattern_expr located option -> tactic + constr with_bindings located list -> + intro_pattern_expr located option -> tactic + +val simple_apply_in : identifier -> constr -> tactic (*s Elimination tactics. *) (* The general form of an induction principle is the following: - + forall prm1 prm2 ... prmp, (induction parameters) forall Q1...,(Qi:Ti_1 -> Ti_2 ->...-> Ti_ni),...Qq, (predicates) branch1, branch2, ... , branchr, (branches of the principle) @@ -229,66 +221,82 @@ val apply_in : (* [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) -type elim_scheme = { - elimc: constr with_ebindings option; +type elim_scheme = { + elimc: constr with_bindings option; elimt: types; indref: global_reference option; + index: int; (* index of the elimination type in the scheme *) params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (* number of parameters *) predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) npredicates: int; (* Number of predicates *) branches: rel_context; (* branchr,...,branch1 *) - nbranches: int; (* Number of branches *) + nbranches: int; (* Number of branches *) args: rel_context; (* (xni, Ti_ni) ... (x1, Ti_1) *) nargs: int; (* number of arguments *) - indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) + indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise *) - concl: types; (* Qi x1...xni HI (f...), HI and (f...) + concl: types; (* Qi x1...xni HI (f...), HI and (f...) are optional and mutually exclusive *) indarg_in_concl: bool; (* true if HI appears at the end of conclusion *) farg_in_concl: bool; (* true if (f...) appears at the end of conclusion *) } -val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme +val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme val rebuild_elimtype_from_scheme: elim_scheme -> types +(* elim principle with the index of its inductive arg *) +type eliminator = { + elimindex : int option; (* None = find it automatically *) + elimbody : constr with_bindings +} + +val elimination_clause_scheme : evars_flag -> + bool -> int -> clausenv -> clausenv -> tactic + +val elimination_in_clause_scheme : evars_flag -> identifier -> int -> + clausenv -> clausenv -> tactic + +val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) -> + 'a -> eliminator -> tactic + val general_elim : evars_flag -> - constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic -val general_elim_in : evars_flag -> - identifier -> constr with_ebindings -> constr with_ebindings -> tactic + constr with_bindings -> eliminator -> ?allow_K:bool -> tactic +val general_elim_in : evars_flag -> + identifier -> constr with_bindings -> eliminator -> tactic -val default_elim : evars_flag -> constr with_ebindings -> tactic +val default_elim : evars_flag -> constr with_bindings -> tactic val simplest_elim : constr -> tactic -val elim : - evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic +val elim : + evars_flag -> constr with_bindings -> constr with_bindings option -> tactic val simple_induct : quantified_hypothesis -> tactic -val new_induct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> - intro_pattern_expr located option * intro_pattern_expr located option -> - clause option -> tactic +val new_induct : evars_flag -> constr with_bindings induction_arg list -> + constr with_bindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + clause option -> tactic (*s Case analysis tactics. *) -val general_case_analysis : evars_flag -> constr with_ebindings -> tactic +val general_case_analysis : evars_flag -> constr with_bindings -> tactic val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic -val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> - intro_pattern_expr located option * intro_pattern_expr located option -> - clause option -> tactic +val new_destruct : evars_flag -> constr with_bindings induction_arg list -> + constr with_bindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + clause option -> tactic (*s Generic case analysis / induction tactics. *) -val induction_destruct : evars_flag -> rec_flag -> - (constr with_ebindings induction_arg list * - constr with_ebindings option * - (intro_pattern_expr located option * intro_pattern_expr located option) * - clause option) list -> - tactic +val induction_destruct : rec_flag -> evars_flag -> + (constr with_bindings induction_arg list * + constr with_bindings option * + (intro_pattern_expr located option * intro_pattern_expr located option)) + list * + clause option -> tactic (*s Eliminations giving the type instead of the proof. *) @@ -307,18 +315,18 @@ val dorE : bool -> clause ->tactic (*s Introduction tactics. *) -val constructor_tac : evars_flag -> int option -> int -> - open_constr bindings -> tactic +val constructor_tac : evars_flag -> int option -> int -> + constr bindings -> tactic val any_constructor : evars_flag -> tactic option -> tactic -val one_constructor : int -> open_constr bindings -> tactic +val one_constructor : int -> constr bindings -> tactic val left : constr bindings -> tactic val right : constr bindings -> tactic val split : constr bindings -> tactic -val left_with_ebindings : evars_flag -> open_constr bindings -> tactic -val right_with_ebindings : evars_flag -> open_constr bindings -> tactic -val split_with_ebindings : evars_flag -> open_constr bindings -> tactic +val left_with_bindings : evars_flag -> constr bindings -> tactic +val right_with_bindings : evars_flag -> constr bindings -> tactic +val split_with_bindings : evars_flag -> constr bindings list -> tactic val simplest_left : tactic val simplest_right : tactic @@ -327,31 +335,32 @@ val simplest_split : tactic (*s Logical connective tactics. *) val register_setoid_reflexivity : tactic -> unit -val reflexivity_red : bool -> goal sigma -> tactic option +val reflexivity_red : bool -> tactic val reflexivity : tactic val intros_reflexivity : tactic val register_setoid_symmetry : tactic -> unit -val symmetry_red : bool -> goal sigma -> tactic option +val symmetry_red : bool -> tactic val symmetry : tactic val register_setoid_symmetry_in : (identifier -> tactic) -> unit val symmetry_in : identifier -> tactic val intros_symmetry : clause -> tactic -val register_setoid_transitivity : (constr -> tactic) -> unit -val transitivity_red : bool -> constr -> goal sigma -> tactic option +val register_setoid_transitivity : (constr option -> tactic) -> unit +val transitivity_red : bool -> constr option -> tactic val transitivity : constr -> tactic -val intros_transitivity : constr -> tactic +val etransitivity : tactic +val intros_transitivity : constr option -> tactic val cut : constr -> tactic val cut_intro : constr -> tactic -val cut_replacing : - identifier -> constr -> (tactic -> tactic) -> tactic +val assert_replacing : identifier -> types -> tactic -> tactic +val cut_replacing : identifier -> types -> tactic -> tactic val cut_in_parallel : constr list -> 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 -> +val letin_tac : (bool * intro_pattern_expr located) option -> name -> constr -> types option -> clause -> tactic val assert_tac : name -> types -> tactic val assert_by : name -> types -> tactic -> tactic @@ -359,7 +368,7 @@ val pose_proof : name -> constr -> tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * name) list -> tactic -val generalize_dep : constr -> tactic +val generalize_dep : ?with_let:bool (* Don't lose let bindings *) -> constr -> tactic val unify : ?state:Names.transparent_state -> constr -> constr -> tactic val resolve_classes : tactic @@ -368,9 +377,8 @@ val tclABSTRACT : identifier option -> tactic -> tactic val admit_as_an_axiom : tactic -val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic - -val dependent_pattern : constr -> tactic +val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic +val specialize_eqs : identifier -> tactic -val register_general_multi_rewrite : - (bool -> evars_flag -> open_constr with_bindings -> clause -> tactic) -> unit +val register_general_multi_rewrite : + (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit |