diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 439 |
1 files changed, 246 insertions, 193 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index e82ee021..6025883f 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -1,133 +1,139 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util +open Loc open Names open Term +open Context open Environ -open Sign -open Tacmach open Proof_type -open Reduction open Evd -open Evar_refiner open Clenv open Redexpr -open Tacticals -open Libnames -open Genarg +open Globnames open Tacexpr -open Nametab -open Glob_term open Pattern -open Termops open Unification +open Misctypes +open Locus (** Main tactics. *) (** {6 General functions. } *) -val string_of_inductive : constr -> string -val head_constr : constr -> constr * constr list -val head_constr_bound : constr -> constr * constr list -val is_quantified_hypothesis : identifier -> goal sigma -> bool - -exception Bound +val is_quantified_hypothesis : Id.t -> goal sigma -> bool (** {6 Primitive tactics. } *) -val introduction : identifier -> tactic +val introduction : ?check:bool -> Id.t -> unit Proofview.tactic val refine : constr -> tactic -val convert_concl : constr -> cast_kind -> tactic -val convert_hyp : named_declaration -> tactic -val thin : identifier list -> tactic +val convert_concl : ?check:bool -> types -> cast_kind -> unit Proofview.tactic +val convert_hyp : ?check:bool -> named_declaration -> unit Proofview.tactic +val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic +val convert_hyp_no_check : named_declaration -> unit Proofview.tactic +val thin : Id.t list -> tactic val mutual_fix : - identifier -> int -> (identifier * int * constr) list -> int -> tactic -val fix : identifier option -> int -> tactic -val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic -val cofix : identifier option -> tactic + Id.t -> int -> (Id.t * int * constr) list -> int -> tactic +val fix : Id.t option -> int -> tactic +val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic +val cofix : Id.t option -> tactic + +val convert : constr -> constr -> unit Proofview.tactic +val convert_leq : constr -> constr -> unit Proofview.tactic (** {6 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 fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t +val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t +val find_intro_names : rel_context -> goal sigma -> Id.t list -val intro : tactic -val introf : tactic -val intro_move : identifier option -> identifier move_location -> tactic +val intro : unit Proofview.tactic +val introf : unit Proofview.tactic +val intro_move : Id.t option -> Id.t move_location -> unit Proofview.tactic +val intro_move_avoid : Id.t option -> Id.t list -> Id.t move_location -> unit Proofview.tactic - (** [intro_avoiding idl] acts as intro but prevents the new identifier + (** [intro_avoiding idl] acts as intro but prevents the new Id.t to belong to [idl] *) -val intro_avoiding : identifier list -> tactic +val intro_avoiding : Id.t list -> unit Proofview.tactic -val intro_replacing : identifier -> tactic -val intro_using : identifier -> tactic -val intro_mustbe_force : identifier -> tactic -val intro_then : (identifier -> tactic) -> tactic -val intros_using : identifier list -> tactic -val intro_erasing : identifier -> tactic -val intros_replacing : identifier list -> tactic +val intro_replacing : Id.t -> unit Proofview.tactic +val intro_using : Id.t -> unit Proofview.tactic +val intro_mustbe_force : Id.t -> unit Proofview.tactic +val intro_then : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic +val intros_using : Id.t list -> unit Proofview.tactic +val intros_replacing : Id.t list -> unit Proofview.tactic +val intros_possibly_replacing : Id.t list -> unit Proofview.tactic -val intros : tactic +val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : bool -> quantified_hypothesis -> goal sigma -> int -val intros_until_n_wored : int -> tactic -val intros_until : quantified_hypothesis -> tactic +val intros_until : quantified_hypothesis -> unit Proofview.tactic -val intros_clearing : bool list -> tactic +val intros_clearing : bool list -> unit Proofview.tactic -(** Assuming a tactic [tac] depending on an hypothesis identifier, +(** Assuming a tactic [tac] depending on an hypothesis Id.t, [try_intros_until tac arg] first assumes that arg denotes a quantified hypothesis (denoted by name or by index) and try to introduce it in context before to apply [tac], otherwise assume the hypothesis is already in context and directly apply [tac] *) val try_intros_until : - (identifier -> tactic) -> quantified_hypothesis -> tactic + (Id.t -> unit Proofview.tactic) -> quantified_hypothesis -> unit Proofview.tactic (** Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) val onInductionArg : - (constr with_bindings -> tactic) -> - constr with_bindings induction_arg -> tactic + (clear_flag -> constr with_bindings -> unit Proofview.tactic) -> + constr with_bindings induction_arg -> unit Proofview.tactic + +(** Tell if a used hypothesis should be cleared by default or not *) + +val use_clear_hyp_by_default : unit -> bool (** {6 Introduction tactics with eliminations. } *) -val intro_pattern : identifier move_location -> intro_pattern_expr -> tactic -val intro_patterns : intro_pattern_expr located list -> tactic -val intros_pattern : - identifier move_location -> intro_pattern_expr located list -> tactic +val intro_patterns : intro_patterns -> unit Proofview.tactic +val intro_patterns_to : Id.t move_location -> intro_patterns -> + unit Proofview.tactic +val intro_patterns_bound_to : int -> Id.t move_location -> intro_patterns -> + unit Proofview.tactic +val intro_pattern_to : Id.t move_location -> delayed_open_constr intro_pattern_expr -> + unit Proofview.tactic + +(** Implements user-level "intros", with [] standing for "**" *) +val intros_patterns : intro_patterns -> unit Proofview.tactic (** {6 Exact tactics. } *) -val assumption : tactic +val assumption : unit Proofview.tactic val exact_no_check : constr -> tactic val vm_cast_no_check : constr -> tactic -val exact_check : constr -> tactic -val exact_proof : Topconstr.constr_expr -> tactic +val exact_check : constr -> unit Proofview.tactic +val exact_proof : Constrexpr.constr_expr -> tactic (** {6 Reduction tactics. } *) type tactic_reduction = env -> evar_map -> constr -> constr -val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic -val reduct_option : tactic_reduction * cast_kind -> goal_location -> tactic +type change_arg = evar_map -> evar_map * constr + +val reduct_in_hyp : ?check:bool -> tactic_reduction -> hyp_location -> tactic +val reduct_option : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic val reduct_in_concl : tactic_reduction * cast_kind -> tactic -val change_in_concl : (occurrences * constr_pattern) option -> constr -> - tactic -val change_in_hyp : (occurrences * constr_pattern) option -> constr -> - hyp_location -> tactic +val change_in_concl : (occurrences * constr_pattern) option -> change_arg -> unit Proofview.tactic +val change_concl : constr -> unit Proofview.tactic +val change_in_hyp : (occurrences * constr_pattern) option -> change_arg -> + hyp_location -> unit Proofview.tactic val red_in_concl : tactic val red_in_hyp : hyp_location -> tactic val red_option : goal_location -> tactic @@ -148,7 +154,7 @@ val unfold_in_hyp : val unfold_option : (occurrences * evaluable_global_reference) list -> goal_location -> tactic val change : - constr_pattern option -> constr -> clause -> tactic + constr_pattern option -> change_arg -> clause -> tactic val pattern_option : (occurrences * constr) list -> goal_location -> tactic val reduce : red_expr -> clause -> tactic @@ -156,44 +162,50 @@ val unfold_constr : global_reference -> tactic (** {6 Modification of the local context. } *) -val clear : identifier list -> tactic -val clear_body : identifier list -> tactic -val keep : identifier list -> tactic +val clear : Id.t list -> tactic +val clear_body : Id.t list -> unit Proofview.tactic +val unfold_body : Id.t -> tactic +val keep : Id.t list -> unit Proofview.tactic +val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic -val specialize : int option -> constr with_bindings -> tactic +val specialize : constr with_bindings -> tactic -val move_hyp : bool -> identifier -> identifier move_location -> tactic -val rename_hyp : (identifier * identifier) list -> tactic +val move_hyp : Id.t -> Id.t move_location -> tactic +val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic -val revert : identifier list -> tactic +val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) val apply_type : constr -> constr list -> tactic -val apply_term : constr -> constr list -> tactic -val bring_hyps : named_context -> tactic +val bring_hyps : named_context -> unit Proofview.tactic -val apply : constr -> tactic -val eapply : constr -> tactic +val apply : constr -> unit Proofview.tactic +val eapply : constr -> unit Proofview.tactic val apply_with_bindings_gen : - advanced_flag -> evars_flag -> constr with_bindings located list -> tactic + advanced_flag -> evars_flag -> (clear_flag * constr with_bindings located) list -> unit Proofview.tactic -val apply_with_bindings : constr with_bindings -> tactic -val eapply_with_bindings : constr with_bindings -> tactic +val apply_with_delayed_bindings_gen : + advanced_flag -> evars_flag -> (clear_flag * delayed_open_constr_with_bindings located) list -> unit Proofview.tactic -val cut_and_apply : constr -> tactic +val apply_with_bindings : constr with_bindings -> unit Proofview.tactic +val eapply_with_bindings : constr with_bindings -> unit Proofview.tactic + +val cut_and_apply : constr -> unit Proofview.tactic val apply_in : - advanced_flag -> evars_flag -> identifier -> - constr with_bindings located list -> - intro_pattern_expr located option -> tactic + advanced_flag -> evars_flag -> clear_flag -> Id.t -> + (clear_flag * constr with_bindings located) list -> + intro_pattern option -> unit Proofview.tactic -val simple_apply_in : identifier -> constr -> tactic +val apply_delayed_in : + advanced_flag -> evars_flag -> clear_flag -> Id.t -> + (clear_flag * delayed_open_constr_with_bindings located) list -> + intro_pattern option -> unit Proofview.tactic (** {6 Elimination tactics. } *) - (* The general form of an induction principle is the following: @@ -223,7 +235,6 @@ 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,...) *) @@ -240,150 +251,192 @@ type elim_scheme = { farg_in_concl: bool; (** true if (f...) appears at the end of conclusion *) } - 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 *) + elimrename : (bool * int array) option; (** None = don't rename Prop hyps with H-names *) elimbody : constr with_bindings } -val elimination_clause_scheme : evars_flag -> ?flags:unify_flags -> - int -> clausenv -> clausenv -> tactic +val general_elim : evars_flag -> clear_flag -> + constr with_bindings -> eliminator -> unit Proofview.tactic -val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags -> - identifier -> int -> clausenv -> clausenv -> tactic +val general_elim_clause : evars_flag -> unify_flags -> identifier option -> + clausenv -> eliminator -> unit Proofview.tactic -val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) -> - 'a -> eliminator -> tactic - -val general_elim : evars_flag -> - constr with_bindings -> eliminator -> tactic -val general_elim_in : evars_flag -> identifier -> - constr with_bindings -> eliminator -> tactic - -val default_elim : evars_flag -> constr with_bindings -> tactic -val simplest_elim : constr -> tactic +val default_elim : evars_flag -> clear_flag -> constr with_bindings -> + unit Proofview.tactic +val simplest_elim : constr -> unit Proofview.tactic val elim : - evars_flag -> constr with_bindings -> constr with_bindings option -> tactic + evars_flag -> clear_flag -> constr with_bindings -> constr with_bindings option -> unit Proofview.tactic -val simple_induct : quantified_hypothesis -> tactic +val simple_induct : quantified_hypothesis -> unit Proofview.tactic -val new_induct : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> - intro_pattern_expr located option * intro_pattern_expr located option -> - clause option -> tactic +val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option -> + constr with_bindings option -> unit Proofview.tactic (** {6 Case analysis tactics. } *) -val general_case_analysis : evars_flag -> constr with_bindings -> tactic -val simplest_case : constr -> tactic +val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings -> unit Proofview.tactic +val simplest_case : constr -> unit Proofview.tactic -val simple_destruct : quantified_hypothesis -> tactic -val new_destruct : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> - intro_pattern_expr located option * intro_pattern_expr located option -> - clause option -> tactic +val simple_destruct : quantified_hypothesis -> unit Proofview.tactic +val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option -> + constr with_bindings option -> unit Proofview.tactic (** {6 Generic case analysis / induction tactics. } *) +(** Implements user-level "destruct" and "induction" *) + val induction_destruct : rec_flag -> evars_flag -> - ((evar_map * constr with_bindings) induction_arg * - (intro_pattern_expr located option * intro_pattern_expr located option)) - list * - constr with_bindings option * - clause option -> tactic + (delayed_open_constr_with_bindings induction_arg + * (intro_pattern_naming option * or_and_intro_pattern option) + * clause option) list * + constr with_bindings option -> unit Proofview.tactic (** {6 Eliminations giving the type instead of the proof. } *) -val case_type : constr -> tactic -val elim_type : constr -> tactic +val case_type : types -> unit Proofview.tactic +val elim_type : types -> unit Proofview.tactic -(** {6 Some eliminations which are frequently used. } *) +(** {6 Constructor tactics. } *) -val impE : identifier -> tactic -val andE : identifier -> tactic -val orE : identifier -> tactic -val dImp : clause -> tactic -val dAnd : clause -> tactic -val dorE : bool -> clause ->tactic +val constructor_tac : evars_flag -> int option -> int -> + constr bindings -> unit Proofview.tactic +val any_constructor : evars_flag -> unit Proofview.tactic option -> unit Proofview.tactic +val one_constructor : int -> constr bindings -> unit Proofview.tactic +val left : constr bindings -> unit Proofview.tactic +val right : constr bindings -> unit Proofview.tactic +val split : constr bindings -> unit Proofview.tactic -(** {6 Introduction tactics. } *) +val left_with_bindings : evars_flag -> constr bindings -> unit Proofview.tactic +val right_with_bindings : evars_flag -> constr bindings -> unit Proofview.tactic +val split_with_bindings : evars_flag -> constr bindings list -> unit Proofview.tactic -val constructor_tac : evars_flag -> int option -> int -> - constr bindings -> tactic -val any_constructor : evars_flag -> tactic option -> 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_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 -val simplest_split : tactic - -(** {6 Logical connective tactics. } *) - -val register_setoid_reflexivity : tactic -> unit -val reflexivity_red : bool -> tactic -val reflexivity : tactic -val intros_reflexivity : tactic - -val register_setoid_symmetry : tactic -> unit -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 option -> tactic) -> unit -val transitivity_red : bool -> constr option -> tactic -val transitivity : constr -> tactic -val etransitivity : tactic -val intros_transitivity : constr option -> tactic - -val cut : constr -> tactic -val cut_intro : constr -> 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 -> - constr -> types option -> clause -> tactic -val letin_pat_tac : (bool * intro_pattern_expr located) option -> name -> - evar_map * constr -> types option -> clause -> tactic -val assert_tac : name -> types -> tactic -val assert_by : name -> types -> tactic -> tactic -val pose_proof : name -> constr -> tactic +val simplest_left : unit Proofview.tactic +val simplest_right : unit Proofview.tactic +val simplest_split : unit Proofview.tactic + +(** {6 Equality tactics. } *) + +val setoid_reflexivity : unit Proofview.tactic Hook.t +val reflexivity_red : bool -> unit Proofview.tactic +val reflexivity : unit Proofview.tactic +val intros_reflexivity : unit Proofview.tactic + +val setoid_symmetry : unit Proofview.tactic Hook.t +val symmetry_red : bool -> unit Proofview.tactic +val symmetry : unit Proofview.tactic +val setoid_symmetry_in : (Id.t -> unit Proofview.tactic) Hook.t +val intros_symmetry : clause -> unit Proofview.tactic + +val setoid_transitivity : (constr option -> unit Proofview.tactic) Hook.t +val transitivity_red : bool -> constr option -> unit Proofview.tactic +val transitivity : constr -> unit Proofview.tactic +val etransitivity : unit Proofview.tactic +val intros_transitivity : constr option -> unit Proofview.tactic + +(** {6 Cut tactics. } *) + +val assert_before_replacing: Id.t -> types -> unit Proofview.tactic +val assert_after_replacing : Id.t -> types -> unit Proofview.tactic +val assert_before : Name.t -> types -> unit Proofview.tactic +val assert_after : Name.t -> types -> unit Proofview.tactic + +val assert_as : (* true = before *) bool -> + intro_pattern option -> constr -> unit Proofview.tactic + +(** Implements the tactics assert, enough and pose proof; note that "by" + applies on the first goal for both assert and enough *) + +val assert_by : Name.t -> types -> unit Proofview.tactic -> + unit Proofview.tactic +val enough_by : Name.t -> types -> unit Proofview.tactic -> + unit Proofview.tactic +val pose_proof : Name.t -> constr -> + unit Proofview.tactic + +(** Common entry point for user-level "assert", "enough" and "pose proof" *) + +val forward : bool -> unit Proofview.tactic option -> + intro_pattern option -> constr -> unit Proofview.tactic + +(** Implements the tactic cut, actually a modus ponens rule *) + +val cut : types -> unit Proofview.tactic + +(** {6 Tactics for adding local definitions. } *) + +val letin_tac : (bool * intro_pattern_naming) option -> + Name.t -> constr -> types option -> clause -> unit Proofview.tactic + +(** Common entry point for user-level "set", "pose" and "remember" *) + +val letin_pat_tac : (bool * intro_pattern_naming) option -> + Name.t -> pending_constr -> clause -> unit Proofview.tactic + +(** {6 Generalize tactics. } *) val generalize : constr list -> tactic -val generalize_gen : ((occurrences * constr) * name) list -> tactic +val generalize_gen : ((occurrences * constr) * Name.t) list -> tactic +val new_generalize : constr list -> unit Proofview.tactic +val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.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 +(** {6 Other tactics. } *) + +val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic + +val tclABSTRACT : Id.t option -> unit Proofview.tactic -> unit Proofview.tactic + +val admit_as_an_axiom : unit Proofview.tactic + +val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic +val specialize_eqs : Id.t -> tactic + +val general_rewrite_clause : + (bool -> evars_flag -> constr with_bindings -> clause -> unit Proofview.tactic) Hook.t + +val subst_one : + (bool -> Id.t -> Id.t * constr * bool -> unit Proofview.tactic) Hook.t + +val declare_intro_decomp_eq : + ((int -> unit Proofview.tactic) -> Coqlib.coq_eq_data * types * + (types * constr * constr) -> + constr * types -> unit Proofview.tactic) -> unit + +(** {6 Simple form of basic tactics. } *) + +module Simple : sig + (** Simplified version of some of the above tactics *) + + val intro : Id.t -> unit Proofview.tactic + val generalize : constr list -> tactic + val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic + + val apply : constr -> unit Proofview.tactic + val eapply : constr -> unit Proofview.tactic + val elim : constr -> unit Proofview.tactic + val case : constr -> unit Proofview.tactic + val apply_in : identifier -> constr -> unit Proofview.tactic + +end -val tclABSTRACT : identifier option -> tactic -> tactic +(** {6 Tacticals defined directly in term of Proofview} *) -val admit_as_an_axiom : tactic +module New : sig -val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic -val specialize_eqs : identifier -> tactic + val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*constr) -> unit Proofview.tactic + (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c] + followed by beta-iota-reduction of the conclusion. *) -val register_general_multi_rewrite : - (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit + val reduce_after_refine : unit Proofview.tactic + (** The reducing tactic called after {!refine}. *) -val register_subst_one : - (bool -> identifier -> identifier * constr * bool -> tactic) -> unit + open Proofview + val exact_proof : Constrexpr.constr_expr -> unit tactic +end |