Module Tactics

Main tactics defined in ML. This file is huge and should probably be split in more reasonable units at some point. Because of its size and age, the implementation features various styles and stages of the proof engine. This has to be uniformized someday.

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