Module Tactics

vm_cast_no_check new_concl changes the conclusion to new_concl by inserting a VMcast. It does not check that the new conclusion is indeed convertible to the old conclusion.

Same as vm_cast_no_check but uses a NATIVEcast.

convert_concl ~cast ~check new_concl kind changes the conclusion to new_concl, which should be convertible to the old conclusion.

• cast: if true insert a cast in the proof term using kind as the cast kind.
• check: if true we check for convertibility.

convert_hyp ~check ~reorder decl changes the declaration of x to decl, where x is the variable bound by decl.

• check: if true we check that x is in the context, that the new and old declarations of x are convertible (both the types and bodies need to be convertible), and that the new declaration of x has a body if and only if the old declaration of x has a body.

convert x y checks that x and y are convertible (using all conversion rules), and fails otherwise.

convert_leq x y checks that x is smaller than y for cumulativity (using all conversion rules), and fails otherwise.

introduction id is a low-level tactic which introduces a single variable with name id.

• Fails if the goal is not a product or a let-in.
• Fails if id is already declared in the context.

fresh_id_in_env avoid id env generates a fresh identifier built from id. The returned identifier is guaranteed to be distinct from:

• The identifiers in avoid.
• The global constants in env.
• The local variables in env.

find_intro_names env sigma ctx returns the names that would be created by intros, without actually doing intros.

intro introduces a single variable with an automatically-generated name. Fails if the goal is not a product or a let-in.

introf is a more aggressive version of intro:

• If the goal is an evar it will instantiate it with a product.
• It will attempt to head normalize the goal until it is a product, a let-in, or an evar.

intro_move id_opt loc introduces a single variable and moves it to location loc.

• If id_opt is Some id the introduced variable is named id.
• If id_opt is None we use an automatically generated name.
• It will instantiate evars and head-normalize the goal in the same way as introf.

intro_move_avoid id_opt avoid loc is the same as intro_move except that the automatically generated name is guaranteed to not be in the set avoid.

Generalization of intro_move to a list of variables and locations (processed from left to right).

intro_avoiding avoid introduces a single variable with an automatically-generated name which is guaranteed to not be the set avoid.

intro_replacing id introduces a single variable named id, replacing the previous declaration of id.

Fails if id is not already in the context.

Deprecated version of intro_using_then kept for backwards compatibility.

intro_using_then id tac introduces a single variable named id. It refreshes the name id if needed, and applies tac to the resulting identifier.

intro_mustbe_force id is the same as introf but the name id is used instead of an automatically-generated name.

Generalization of intro_mustbe_force to a list of variables (processed from left to right).

intro_then tac introduces a single variable with an automatically-generated name, and applies tac to the resulting identifier.

Deprecated variant of intros_using_then kept for backwards compatibility.

Generalization of intro_using_then to a list of variables (processed from left to right).

Generalization of intro_replacing to a list of variables (processed from left to right).

Variant of intros_replacing which does not assume that the variables are already declared in the context.

auto_intros_tac names introduces the variables in names.

• The variables are introduced from right to left (contrary to the conventional order).
• Names are chosen as follow: Anonymous indicates to generate a fresh name and Name id indicates to use the name id.
• It will instantiate evars and head-normalize the goal in the same way as introf.

intros keeps introducing variables while the goal is a product or a let-in.

intros_until hyp is a variant of intros which stops when hypothesis hyp is introduced.

intros_clearing bs introduces as many variables as booleans in bs. Each boolean indicates whether to clear the introduced variable (if true) or to keep it (if false).

Assuming a tactic tac depending on a hypothesis, try_intros_until tac arg first assumes that arg denotes a quantified hypothesis (denoted by name or by index) and tries to introduce it in context before applying tac, otherwise assumes the hypothesis is already in context and directly applies tac.

intro_patterns with_evars patt introduces variables and processes them according to the introduction patterns patt.

Variant of intro_patterns which moves introduced variables to location loc.

Variant of intro_patterns_to which introduces a single variable.

intros_patterns with_evars patt implements the user-level "intros" tactic:

• If patt is empty it will introduces as many variables as possible (using intros).
• Otherwise it will behave as intro_patterns with_evars patt.

assumption solves the goal if it is convertible to the type of a hypothesis. Fails if there is no such hypothesis.

exact_no_check x solves the goal with term x. It does not check that the type of x is convertible to the conclusion.

exact_check x solves the goal with term x. Fails if the type of x does not match the conclusion.

exact_proof x internalizes the constr_expr x using the conclusion, and solves the goal using the internalized term. Fails if x could not be internalized.

reduct_in_hyp ~check ~reorder red_fun hyp applies the reduction function red_fun in hypothesis hyp.

• check: if true we check that the new hypothesis is convertible to the old hypothesis.

reduct_in_concl ~cast ~check (red_fun, kind) applies the reduction function red_fun to the conclusion.

• cast: if true we insert a cast in the proof term using kind as the cast kind.
• check: if true we check that the new conclusion is convertible to the old conclusion.

reduct_option combines the behaviour of reduct_in_hyp and reduct_in_concl. If reducing in the conclusion it will insert a cast.

Same as reduct_in_concl but the reduction function can update the evar map.

change_in_concl ~check where change_fun changes the conclusion (or subterms of the conclusion) using the change function change_fun.

• check: if true we check that the new conclusion is convertible to the old conclusion.
• where: if None then the whole conclusion is changed. If Some (occs, patt) then only the subterms of the conclusion which match occurences occs and pattern patt are changed.

change_concl new_concl replaces the conclusion with new_concl. Fails if the new conclusion and old conclusion are not convertible.

change_in_hyp ~check where change_fun hyp is analogous to change_in_concl but works on the hypothesis hyp instead of the conclusion.

change ~check where change_fun clause applies the change function change_fun.

• check: if true we check that the changed terms are convertible to the old terms.
• clause: specifies where to apply the change function: to the conclusion and/or to a (subset of) hypotheses.
• where: if None we change the complete conclusion/hypothesis. If Some patt we change subterms matching pattern patt.

red_in_concl reduces the conclusion using the red reduction strategy.

red_in_hyp hyp reduces hypothesis hyp using the red reduction strategy.

red_option loc reduces the hypothesis or conclusion loc using the red reduction strategy.

hnf_in_concl reduces the conclusion to head normal form.

hnf_in_hyp hyp reduces hypothesis hyp to head normal form.

hnf_option loc reduces the hypothesis or conclusion loc to head normal form.

simpl_in_concl reduces the conclusion using the simpl reduction strategy.

simpl_in_hyp hyp reduces hypothesis hyp using the red reduction strategy.

simpl_option loc reduces the hypothesis or conclusion loc using the simpl reduction strategy.

normalise_in_concl reduces the conclusion to normal form.

normalise_in_hyp hyp reduces hypothesis hyp to normal form.

normalise_option loc reduces the hypothesis or conclusion loc to normal form.

normalise_in_concl reduces the conclusion to normal form using VM compute.

unfold_in_concl cs unfolds a list of constants cs in the conclusion. One can specify which occurences of each constant to unfold.

unfold_in_hyp cs hyp unfolds a list of constants cs in hypothesis hyp. One can specify which occurences of each constant to unfold.

unfold_option cs loc unfolds a list of constants cs in the hypothesis or conclusion loc. One can specify which occurences of each constant to unfold.

pattern_option [(occs1, t1); (occs2, t2); ...] loc implements the pattern user tactic. It performs beta-expansion for the terms ti at occurences occsi, in the goal location loc (i.e. either in the goal or in a hypothesis).

unfold_constr x unfolds all occurences of x in the conclusion.

clear ids removes hypotheses ids from the context.

clear_body ids removes the definitions (but not the declarations) of hypotheses ids from the context.

unfold_body id unfolds the definition of the local variable id in the conclusion and in all hypotheses. Fails if id does not have a body.

keep ids clears every hypothesis except:

• The hypotheses in ids.
• The hypotheses which occur in the conclusion.
• The hypotheses which occur in the type or body of a kept hypothesis.

move_hyp id loc moves hypothesis id to location loc.

rename_hyp [(x1, y1); (x2; y2); ...] renames hypotheses xi into yi.

• The names x1, x2, ... are expected to be distinct.
• The names y1, y2, ... are expected to be distinct.

use_clear_hyp_by_default () returns the default clear flag used by apply and related tactics.

• true means that hypotheses are cleared after being applied.
• false means that hypotheses are kept after being applied.

apply_clear_request c1 c2 id implements the clear behaviour of apply and friends.

• c1 is the primary clear flag. If None we use the secondary clear flag.
• c2 is the secondary clear flag, usually use_clear_hyp_by_default ().
• id is the identifier of the hypothesis to clear. If None we do nothing.

apply t applies the lemma t to the conclusion.

Variant of apply which allows creating new evars.

Variant of apply which takes a term with bindings (e.g. apply foo with (x := 42)).

Variant of eapply which takes a term with bindings (e.g. eapply foo with (x := 42)).

• with_classes specifies whether to attempt to solve remaining evars using typeclass resolution.

apply_with_bindings_gen ?with_classes advanced with_evars [(c1, t1); (c2, t2); ...] is the most general version of apply. It applies lemmas t1, t2, ... in order.

• with_evars: if true allow the creation of (non-goal) evars (i.e. setting with_evars to true gives the behaviour of eapply).
• with_classes: if true attempt to solve remaining evars using typeclass resolution.
• advanced: if true use delta reduction (constant unfolding) in unification, and descend under conjunctions in the conclusion.
• ci: if ti is a hypothesis, ci tells whether to clear ti after applying it. If ci is None we use the default clear flag.

Variant of apply_with_bindings_gen in which the terms are produced by tactics.

Variant of apply_with_bindings_gen which works on a hypothesis instead of the goal.

Variant of apply_in in which the terms are produced by tactics.

cut_and_apply t (where t has type A -> B) transforms a goal |- C into two goals |- B -> C and |- A .

simplest_elim t eliminates t using the default eliminator associated to t. It does not allow unresolved evars, and uses the default clear flag.

elim with_evars clear t eliminator eliminates t.

• with_evars: if true we allow unresolved evars (this is the behaviour of eelim).
• clear: if Some _, clear tells whether to remove t from the context. If None we use the default clear flag.
• eliminator: if Some _ we use this as the eliminator for t. If None we use the default eliminator associated to t.

Variant of elim which uses the default eliminator.

general_case_analysis with_evars clear (t, bindings) performs case analysis on t. If t is a variable which is not in the context, we attempt to perform introductions until t is in the context.

• with_evars: if true allow unsolved evars (this is the behaviour of ecase).
• clear: if Some _, clear tells whether to remove t from the context. If None we use the default clear flag.

simplest_case t performs case analysis on t. It does not allow unresolved evars, and uses the default clear flag.

exfalso changes the conclusion to False.

constructor_tac with_evars expected_num_ctors i bindings checks that the goal is an inductive ind and applies the i-th constructor of ind.

• with_evars: if true applying the constructor can leave evars (this gives the behaviour of econstructor).
• expected_num_ctors: if Some nctors we check that the number of constructors of ind is equal to nctors.
• i: index of the constructor to apply, starting at 1.
• bindings: bindings to use when applying the constructor.

one_constructor i bindings is a specialization of constructor_tac with:

• with_evars set to false.
• expected_num_ctors set to None.

any_constructor with_evars tac checks that the goal is an inductive ind and tries to apply the constructors of ind one by one (from first to last).

• with_evars: if true applying the constructor can leave evars (this gives the behaviour of econstructor).
• tac: we run tac after applying each constructor, and backtrack to the next constructor if tac fails.

simplest_left checks the goal is an inductive with two constructors and applies the first constructor.

Variant of simplest_left which takes bindings.

Variant of simplest_left which takes an evar flag and bindings.

simplest_right checks the goal is an inductive with two constructors and applies the second constructor.

Variant of simplest_right which takes bindings.

Variant of simplest_right which takes an evar flag and bindings.

simplest_left checks the goal is an inductive with one constructor and applies the (unique) constructor.

Variant of simplest_split which takes bindings.

Variant of simplest_split which takes an evar flag and bindings.

Variant of simplest_split which takes an evar flag and delayed bindings.

Hook to the setoid_reflexivity tactic, set at runtime.

reflexivity_red reduce solves a goal of the form x = y.

• reduce: if true we weak-head normalize the goal before checking it is indeed an equality.

Variant of reflexivity_red which does not perform reduction, and falls back to setoid_reflexivity in case of failure.

intros_reflexivity performs intros followed by reflexivity.

Hook to the setoid_symmetry tactic, set at runtime.

symmetry_red reduce checks the goal is of the form x = y and changes it to y = x.

• reduce: if true we weak-head normalize the goal before checking it is indeed an equality.

Variant of symmetry_red which does not perform reduction, and falls back to setoid_symmetry in case of failure.

Hook to the setoid_symmetry_in tactic, set at runtime.

intros_symmetry clause performs intros followed by symmetry on all the locations indicated by clause (i.e. the conclusion and/or a (subset of) hypotheses). Actual occurences contained in clause are not used: only the hypotheses names are relevant.

Hook to the setoid_transitivity tactic, set at runtime.

transitivity_red reduce t checks the goal is of the form x = y and changes it to x = t and t = y.

• reduce: if true we weak-head normalize the goal before checking it is indeed an equality.
• t: if Some then we use apply eq_trans with t to perform transitivity. If None we use eapply eq_trans instead.

Variant of transitivity_red which does not perform reduction, uses apply eq_trans with t, and falls back to setoid_transitivity in case of failure.

Variant of transitivity_red which does not perform reduction, uses eapply eq_trans, and falls back to setoid_transitivity in case of failure.

intros_transitivity t performs intros followed by transitivity t or etransivity t (depending on whether t is Some or None).

assert_before x T first asks to prove T, then to prove the original goal augmented with a new hypothesis of type x : T.

• x: if None the name of the hypothesis is generated automatically. If Some then it is the name of the hypothesis (which should not be already defined in the context).

Variant of assert_before which allows replacing hypotheses.

assert_after x T first asks the original goal augmented with a new hypothesis of type x : T, then to prove T.

• x: if None the name of the hypothesis is generated automatically. If Some then it is the name of the hypothesis (which should not be already defined in the context).

Variant of assert_after which allows replacing hypotheses.

forward before by_tac ipat t performs a forward reasoning step.

• If by_tac is None it adds a new hypothesis with _body_ equal to t.
• If by_tac is Some tac it asks to prove t and to prove the original goal augmented with a new hypothesis of type t. If tac is Some _ then tac is used to prove t (and tac is required to succeed).
• before: if true then t must be proved first. If false then t must be proved last.

assert_by x T tac adds a new hypothesis x : T. The tactic tac is used to prove T. If x is None a fresh name is automatically generated.

enough_by x T tac changes the goal to T. The tactic tac is used to prove the orignal goal augmented with a hypothesis x : T. If x is None a fresh name is automatically generated.

pose_proof x t adds a new hypothesis x := t. If x is None a fresh name is automatically generated.

Implements the tactic cut, actually a modus ponens rule.

pose_tac x t adds a new hypothesis x := t. If x is None a fresh name is automatically generated. Fails if there is alreay a hypothesis named x.

Common entry point for user-level "set", "pose", and "remember".

constr_eq ~strict x y checks that x and y are syntactically equal (i.e. alpha-equivalent), up to universes.

• strict: if true the universe constraints must be already true. If false any necessary universe constraints are added to the evar map.

Legacy unification. Use evarconv_unify instead.

evarconv_unify ?state ?with_ho x y unifies x and y, instantiating evars and adding universe constraints as needed. Fails if x and y are not unifiable.

• state: transparency state to use (defaults to TransparentState.full).
• with_ho: whether to use higher order unification (defaults to true).

Tactic analogous to the Strategy vernacular, but only applied locally to the tactic argument.

Simplified version of some of the above tactics

refine ~typecheck c is Refine.refine ~typecheck c followed by beta-iota-reduction of the conclusion.

The reducing tactic called after refine.

Deprecated since 9.2, use TacticErrors.not_convertible () instead.