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.
val is_quantified_hypothesis : Names.Id.t -> Proofview.Goal.t -> bool
val introduction : Names.Id.t -> unit Proofview.tactic
val convert_concl : cast:bool -> check:bool -> EConstr.types -> Constr.cast_kind -> unit Proofview.tactic
val convert_hyp : check:bool -> reorder:bool -> 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
val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t
val find_intro_names : Environ.env -> Evd.evar_map -> EConstr.rel_context -> 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 intros_move : (Names.Id.t * Names.Id.t Logic.move_location) list -> 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_using_then : Names.Id.t -> (Names.Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
val intro_mustbe_force : Names.Id.t -> unit Proofview.tactic
val intros_mustbe_force : Names.Id.t list -> 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_using_then : Names.Id.t list -> (Names.Id.t list -> unit Proofview.tactic) -> 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 intros_until : Tactypes.quantified_hypothesis -> unit Proofview.tactic
val intros_clearing : bool list -> unit Proofview.tactic
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 : (Names.Id.t -> unit Proofview.tactic) -> Tactypes.quantified_hypothesis -> unit Proofview.tactic
Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings
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 finish_evar_resolution : ?flags:Pretyping.inference_flags -> Environ.env -> Evd.evar_map -> (Evd.evar_map option * EConstr.constr) -> Evd.evar_map * EConstr.constr
Tell if a used hypothesis should be cleared by default or not
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 "**"
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
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 : cast:bool -> check:bool -> (tactic_reduction * Constr.cast_kind) -> unit Proofview.tactic
val e_reduct_in_concl : cast:bool -> 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 * Evaluable.t) list -> unit Proofview.tactic
val unfold_in_hyp : (Locus.occurrences * Evaluable.t) list -> Locus.hyp_location -> unit Proofview.tactic
val unfold_option : (Locus.occurrences * Evaluable.t) 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
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 -> Names.Id.t option -> 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 apply_type : typecheck:bool -> EConstr.constr -> EConstr.constr list -> unit Proofview.tactic
val apply : EConstr.constr -> unit Proofview.tactic
val eapply : ?with_classes:bool -> EConstr.constr -> unit Proofview.tactic
val apply_with_bindings_gen : ?with_classes:bool -> 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 * EConstr.constr Tactypes.with_bindings Proofview.tactic CAst.t) list -> unit Proofview.tactic
val apply_with_bindings : EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val eapply_with_bindings : ?with_classes:bool -> 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 * EConstr.constr Tactypes.with_bindings Proofview.tactic CAst.t) list -> Tactypes.intro_pattern option -> unit Proofview.tactic -> unit Proofview.tactic
val general_elim_clause : evars_flag -> Unification.unify_flags -> Names.Id.t option -> ((Constr.metavariable list * Unification.Meta.t) * EConstr.t * EConstr.types) -> Names.Constant.t -> 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 general_case_analysis : evars_flag -> clear_flag -> EConstr.constr Tactypes.with_bindings -> unit Proofview.tactic
val simplest_case : EConstr.constr -> unit Proofview.tactic
val exfalso : unit Proofview.tactic
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 split_with_delayed_bindings : evars_flag -> EConstr.constr Tactypes.bindings Tactypes.delayed_open list -> unit Proofview.tactic
val simplest_left : unit Proofview.tactic
val simplest_right : unit Proofview.tactic
val simplest_split : unit Proofview.tactic
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
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
Implements the tactics assert, enough and pose proof; note that "by" applies on the first goal for both assert and enough
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
Common entry point for user-level "assert", "enough" and "pose proof"
val forward : bool -> unit Proofview.tactic option option -> Tactypes.intro_pattern option -> EConstr.constr -> unit Proofview.tactic
Implements the tactic cut, actually a modus ponens rule
val cut : EConstr.types -> unit Proofview.tactic
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
Common entry point for user-level "set", "pose" and "remember"
val letin_pat_tac : evars_flag -> (bool * Tactypes.intro_pattern_naming) option -> Names.Name.t -> (Evd.evar_map option * EConstr.constr) -> Locus.clause -> unit Proofview.tactic
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 evarconv_unify : ?state:TransparentState.t -> ?with_ho:bool -> EConstr.constr -> EConstr.constr -> 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) -> (Rocqlib.rocq_eq_data * EConstr.types * (EConstr.types * EConstr.constr * EConstr.constr)) -> (EConstr.constr * EConstr.types) -> unit Proofview.tactic) -> unit
val with_set_strategy : (Conv_oracle.level * Names.GlobRef.t list) list -> 'a Proofview.tactic -> 'a Proofview.tactic
Tactic analogous to the Strategy
vernacular, but only applied locally to the tactic argument
module Simple : sig ... end
Simplified version of some of the above tactics
val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic
refine ~typecheck c
is Refine.refine ~typecheck c
followed by beta-iota-reduction of the conclusion.
val reduce_after_refine : unit Proofview.tactic
The reducing tactic called after refine
.
module Internal : sig ... end