Module Tactics

General functions.
val is_quantified_hypothesis : Names.Id.t -> Proofview.Goal.t -> bool
Primitive tactics.
val introduction : Names.Id.t -> unit Proofview.tactic
val convert_concl : check:bool -> EConstr.types -> Constr.cast_kind -> unit Proofview.tactic
val convert_hyp : check:bool -> reorder:bool -> EConstr.named_declaration -> unit Proofview.tactic
val convert_concl_no_check : EConstr.types -> Constr.cast_kind -> unit Proofview.tactic
val convert_hyp_no_check : EConstr.named_declaration -> unit Proofview.tactic
val mutual_fix : Names.Id.t -> int -> (Names.Id.t * int * EConstr.constr) list -> int -> unit Proofview.tactic
val fix : Names.Id.t -> int -> unit Proofview.tactic
val mutual_cofix : Names.Id.t -> (Names.Id.t * EConstr.constr) list -> int -> unit Proofview.tactic
val cofix : Names.Id.t -> unit Proofview.tactic
val convert : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val convert_leq : EConstr.constr -> EConstr.constr -> unit Proofview.tactic
Introduction tactics.
val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t
val fresh_id : Names.Id.Set.t -> Names.Id.t -> Goal.goal Evd.sigma -> Names.Id.t
val find_intro_names : EConstr.rel_context -> Goal.goal Evd.sigma -> Names.Id.t list
val intro : unit Proofview.tactic
val introf : unit Proofview.tactic
val intro_move : Names.Id.t option -> Names.Id.t Logic.move_location -> unit Proofview.tactic
val intro_move_avoid : Names.Id.t option -> Names.Id.Set.t -> Names.Id.t Logic.move_location -> unit Proofview.tactic
val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic

intro_avoiding idl acts as intro but prevents the new Id.t to belong to idl

val intro_replacing : Names.Id.t -> unit Proofview.tactic
val intro_using : Names.Id.t -> unit Proofview.tactic
val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic
val intro_then : (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val intros_using : Names.Id.t list -> unit Proofview.tactic
val intros_replacing : Names.Id.t list -> unit Proofview.tactic
val intros_possibly_replacing : Names.Id.t list -> unit Proofview.tactic
val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic

auto_intros_tac names handles Automatic Introduction of binders

val intros : unit Proofview.tactic
val depth_of_quantified_hypothesis : bool -> Tactypes.quantified_hypothesis -> Proofview.Goal.t -> int

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 intros_until : Tactypes.quantified_hypothesis -> unit Proofview.tactic
val intros_clearing : bool list -> unit Proofview.tactic
val try_intros_until : (Names.Id.t -> unit Proofview.tactic) -> Tactypes.quantified_hypothesis -> unit Proofview.tactic
type evars_flag = bool
type rec_flag = bool
type advanced_flag = bool
type clear_flag = bool option
type 'a core_destruction_arg =
| ElimOnConstr of 'a
| ElimOnIdent of Names.lident
| ElimOnAnonHyp of int
type 'a destruction_arg = clear_flag * 'a core_destruction_arg
val onInductionArg : (clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic) -> EConstr.constr Tactypes.with_bindings destruction_arg -> unit Proofview.tactic
val force_destruction_arg : evars_flag -> Environ.env -> Evd.evar_map -> Tactypes.delayed_open_constr_with_bindings destruction_arg -> Evd.evar_map * EConstr.constr Tactypes.with_bindings destruction_arg
val use_clear_hyp_by_default : unit -> bool
Introduction tactics with eliminations.
val intro_patterns : evars_flag -> Tactypes.intro_patterns -> unit Proofview.tactic
val intro_patterns_to : evars_flag -> Names.Id.t Logic.move_location -> Tactypes.intro_patterns -> unit Proofview.tactic
val intro_patterns_bound_to : evars_flag -> int -> Names.Id.t Logic.move_location -> Tactypes.intro_patterns -> unit Proofview.tactic
val intro_pattern_to : evars_flag -> Names.Id.t Logic.move_location -> Tactypes.delayed_open_constr Tactypes.intro_pattern_expr -> unit Proofview.tactic
val intros_patterns : evars_flag -> Tactypes.intro_patterns -> unit Proofview.tactic

Implements user-level "intros", with standing for "**"

Exact tactics.
val assumption : unit Proofview.tactic
val exact_no_check : EConstr.constr -> unit Proofview.tactic
val vm_cast_no_check : EConstr.constr -> unit Proofview.tactic
val native_cast_no_check : EConstr.constr -> unit Proofview.tactic
val exact_check : EConstr.constr -> unit Proofview.tactic
val exact_proof : Constrexpr.constr_expr -> unit Proofview.tactic
Reduction tactics.
type tactic_reduction = Reductionops.reduction_function
type e_tactic_reduction = Reductionops.e_reduction_function
type change_arg = Ltac_pretype.patvar_map -> Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.constr
val make_change_arg : EConstr.constr -> change_arg
val reduct_in_hyp : check:bool -> reorder:bool -> tactic_reduction -> Locus.hyp_location -> unit Proofview.tactic
val reduct_option : check:bool -> (tactic_reduction * Constr.cast_kind) -> Locus.goal_location -> unit Proofview.tactic
val reduct_in_concl : check:bool -> (tactic_reduction * Constr.cast_kind) -> unit Proofview.tactic
val e_reduct_in_concl : check:bool -> (e_tactic_reduction * Constr.cast_kind) -> unit Proofview.tactic
val change_in_concl : check:bool -> (Locus.occurrences * Pattern.constr_pattern) option -> change_arg -> unit Proofview.tactic
val change_concl : EConstr.constr -> unit Proofview.tactic
val change_in_hyp : check:bool -> (Locus.occurrences * Pattern.constr_pattern) option -> change_arg -> Locus.hyp_location -> unit Proofview.tactic
val red_in_concl : unit Proofview.tactic
val red_in_hyp : Locus.hyp_location -> unit Proofview.tactic
val red_option : Locus.goal_location -> unit Proofview.tactic
val hnf_in_concl : unit Proofview.tactic
val hnf_in_hyp : Locus.hyp_location -> unit Proofview.tactic
val hnf_option : Locus.goal_location -> unit Proofview.tactic
val simpl_in_concl : unit Proofview.tactic
val simpl_in_hyp : Locus.hyp_location -> unit Proofview.tactic
val simpl_option : Locus.goal_location -> unit Proofview.tactic
val normalise_in_concl : unit Proofview.tactic
val normalise_in_hyp : Locus.hyp_location -> unit Proofview.tactic
val normalise_option : Locus.goal_location -> unit Proofview.tactic
val normalise_vm_in_concl : unit Proofview.tactic
val unfold_in_concl : (Locus.occurrences * Names.evaluable_global_reference) list -> unit Proofview.tactic
val unfold_in_hyp : (Locus.occurrences * Names.evaluable_global_reference) list -> Locus.hyp_location -> unit Proofview.tactic
val unfold_option : (Locus.occurrences * Names.evaluable_global_reference) list -> Locus.goal_location -> unit Proofview.tactic
val change : check:bool -> Pattern.constr_pattern option -> change_arg -> Locus.clause -> unit Proofview.tactic
val pattern_option : (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic
val reduce : Redexpr.red_expr -> Locus.clause -> unit Proofview.tactic
val unfold_constr : Names.GlobRef.t -> unit Proofview.tactic
Modification of the local context.
val clear : Names.Id.t list -> unit Proofview.tactic
val clear_body : Names.Id.t list -> unit Proofview.tactic
val unfold_body : Names.Id.t -> unit Proofview.tactic
val keep : Names.Id.t list -> unit Proofview.tactic
val apply_clear_request : clear_flag -> bool -> EConstr.constr -> unit Proofview.tactic
val specialize : EConstr.constr Tactypes.with_bindings -> Tactypes.intro_pattern option -> unit Proofview.tactic
val move_hyp : Names.Id.t -> Names.Id.t Logic.move_location -> unit Proofview.tactic
val rename_hyp : (Names.Id.t * Names.Id.t) list -> unit Proofview.tactic
val revert : Names.Id.t list -> unit Proofview.tactic
Resolution tactics.
val apply_type : typecheck:bool -> EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
val bring_hyps : EConstr.named_context -> unit Proofview.tactic
val apply : EConstr.constr -> unit Proofview.tactic
val eapply : EConstr.constr -> unit Proofview.tactic
val apply_with_bindings_gen : advanced_flag -> evars_flag -> (clear_flag * EConstr.constr Tactypes.with_bindings CAst.t) list -> unit Proofview.tactic
val apply_with_delayed_bindings_gen : advanced_flag -> evars_flag -> (clear_flag * Tactypes.delayed_open_constr_with_bindings CAst.t) list -> unit Proofview.tactic
val apply_with_bindings : EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val eapply_with_bindings : EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val cut_and_apply : EConstr.constr -> unit Proofview.tactic
val apply_in : advanced_flag -> evars_flag -> Names.Id.t -> (clear_flag * EConstr.constr Tactypes.with_bindings CAst.t) list -> Tactypes.intro_pattern option -> unit Proofview.tactic
val apply_delayed_in : advanced_flag -> evars_flag -> Names.Id.t -> (clear_flag * Tactypes.delayed_open_constr_with_bindings CAst.t) list -> Tactypes.intro_pattern option -> unit Proofview.tactic
Elimination tactics.
type elim_scheme = {
elimc : EConstr.constr Tactypes.with_bindings option;
elimt : EConstr.types;
indref : Names.GlobRef.t option;
params : EConstr.rel_context;

(prm1,tprm1);(prm2,tprm2)...(prmp,tprmp)

nparams : int;

number of parameters

predicates : EConstr.rel_context;

(Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...)

npredicates : int;

Number of predicates

branches : EConstr.rel_context;

branchr,...,branch1

nbranches : int;

Number of branches

args : EConstr.rel_context;

(xni, Ti_ni) ... (x1, Ti_1)

nargs : int;

number of arguments

indarg : EConstr.rel_declaration option;

Some (H,I prm1..prmp x1...xni) if HI is in premisses, None otherwise

concl : EConstr.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

}

rel_contexts and rel_declaration actually contain triples, and lists are actually in reverse order to fit compose_prod.

val compute_elim_sig : Evd.evar_map -> ?⁠elimc:EConstr.constr Tactypes.with_bindings -> EConstr.types -> elim_scheme
type eliminator = {
elimindex : int option;

None = find it automatically

elimbody : EConstr.constr Tactypes.with_bindings;
}

elim principle with the index of its inductive arg

val general_elim : evars_flag -> clear_flag -> EConstr.constr Tactypes.with_bindings -> eliminator -> unit Proofview.tactic
val general_elim_clause : evars_flag -> Unification.unify_flags -> Names.Id.t option -> Clenv.clausenv -> eliminator -> unit Proofview.tactic
val default_elim : evars_flag -> clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val simplest_elim : EConstr.constr -> unit Proofview.tactic
val elim : evars_flag -> clear_flag -> EConstr.constr Tactypes.with_bindings -> EConstr.constr Tactypes.with_bindings option -> unit Proofview.tactic
val induction : evars_flag -> clear_flag -> EConstr.constr -> Tactypes.or_and_intro_pattern option -> EConstr.constr Tactypes.with_bindings option -> unit Proofview.tactic
Case analysis tactics.
val general_case_analysis : evars_flag -> clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val simplest_case : EConstr.constr -> unit Proofview.tactic
val destruct : evars_flag -> clear_flag -> EConstr.constr -> Tactypes.or_and_intro_pattern option -> EConstr.constr Tactypes.with_bindings option -> unit Proofview.tactic
Generic case analysis / induction tactics.
val induction_destruct : rec_flag -> evars_flag -> ((Tactypes.delayed_open_constr_with_bindings destruction_arg * (Tactypes.intro_pattern_naming option * Tactypes.or_and_intro_pattern option) * Locus.clause option) list * EConstr.constr Tactypes.with_bindings option) -> unit Proofview.tactic
Eliminations giving the type instead of the proof.
val case_type : EConstr.types -> unit Proofview.tactic
val elim_type : EConstr.types -> unit Proofview.tactic
Constructor tactics.
val constructor_tac : evars_flag -> int option -> int -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val any_constructor : evars_flag -> unit Proofview.tactic option -> unit Proofview.tactic
val one_constructor : int -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val left : EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val right : EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val split : EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val left_with_bindings : evars_flag -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val right_with_bindings : evars_flag -> EConstr.constr Tactypes.bindings -> unit Proofview.tactic
val split_with_bindings : evars_flag -> EConstr.constr Tactypes.bindings list -> unit Proofview.tactic
val simplest_left : unit Proofview.tactic
val simplest_right : unit Proofview.tactic
val simplest_split : unit Proofview.tactic
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 : (Names.Id.t -> unit Proofview.tactic) Hook.t
val intros_symmetry : Locus.clause -> unit Proofview.tactic
val setoid_transitivity : (EConstr.constr option -> unit Proofview.tactic) Hook.t
val transitivity_red : bool -> EConstr.constr option -> unit Proofview.tactic
val transitivity : EConstr.constr -> unit Proofview.tactic
val etransitivity : unit Proofview.tactic
val intros_transitivity : EConstr.constr option -> unit Proofview.tactic
Cut tactics.
val assert_before_replacing : Names.Id.t -> EConstr.types -> unit Proofview.tactic
val assert_after_replacing : Names.Id.t -> EConstr.types -> unit Proofview.tactic
val assert_before : Names.Name.t -> EConstr.types -> unit Proofview.tactic
val assert_after : Names.Name.t -> EConstr.types -> unit Proofview.tactic
val assert_as : bool -> Names.Id.t option -> Tactypes.intro_pattern option -> EConstr.constr -> unit Proofview.tactic
val assert_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic
val enough_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic
val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic
val forward : bool -> unit Proofview.tactic option option -> Tactypes.intro_pattern option -> EConstr.constr -> unit Proofview.tactic
val cut : EConstr.types -> unit Proofview.tactic
Tactics for adding local definitions.
val pose_tac : Names.Name.t -> EConstr.constr -> unit Proofview.tactic
val letin_tac : (bool * Tactypes.intro_pattern_naming) option -> Names.Name.t -> EConstr.constr -> EConstr.types option -> Locus.clause -> unit Proofview.tactic
val letin_pat_tac : evars_flag -> (bool * Tactypes.intro_pattern_naming) option -> Names.Name.t -> (Evd.evar_map * EConstr.constr) -> Locus.clause -> unit Proofview.tactic
Generalize tactics.
val generalize : EConstr.constr list -> unit Proofview.tactic
val generalize_gen : (EConstr.constr Locus.with_occurrences * Names.Name.t) list -> unit Proofview.tactic
val new_generalize_gen : ((Locus.occurrences * EConstr.constr) * Names.Name.t) list -> unit Proofview.tactic
val generalize_dep : ?⁠with_let:bool -> EConstr.constr -> unit Proofview.tactic
Other tactics.
val constr_eq : strict:bool -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic

Syntactic equality up to universes. With strict the universe constraints must be already true to succeed, without strict they are added to the evar map.

val unify : ?⁠state:TransparentState.t -> EConstr.constr -> EConstr.constr -> unit Proofview.tactic
val abstract_generalize : ?⁠generalize_vars:bool -> ?⁠force_dep:bool -> Names.Id.t -> unit Proofview.tactic
val specialize_eqs : Names.Id.t -> unit Proofview.tactic
val general_rewrite_clause : (bool -> evars_flag -> EConstr.constr Tactypes.with_bindings -> Locus.clause -> unit Proofview.tactic) Hook.t
val subst_one : (bool -> Names.Id.t -> (Names.Id.t * EConstr.constr * bool) -> unit Proofview.tactic) Hook.t
val declare_intro_decomp_eq : ((int -> unit Proofview.tactic) -> (Coqlib.coq_eq_data * EConstr.types * (EConstr.types * EConstr.constr * EConstr.constr)) -> (EConstr.constr * EConstr.types) -> unit Proofview.tactic) -> unit
Simple form of basic tactics.
module Simple : sig ... end
Tacticals defined directly in term of Proofview
module New : sig ... end