This file contains a set of tactics that extends the set of builtin tactics provided with the standard distribution of Coq. It intends to overcome a number of limitations of the standard set of tactics, and thereby to help user to write shorter and more robust scripts.
Hopefully, Coq tactics will be improved as time goes by, and this file should ultimately be useless. In the meanwhile, serious Coq users will probably find it very useful.
The present file contains the implementation and the detailed documentation of those tactics. The SF reader need not read this file; instead, he/she is encouraged to read the chapter named UseTactics.v, which is gentle introduction to the most useful tactics from the LibTactic library.
The main features offered are:
~or
*will call automation on the generated subgoals. The symbol
~stands for auto and
*for intuition eauto. These bindings can be customized.
External credits:
Any Coq value can be boxed into the type Boxer. This is useful to use Coq computations for implementing tactics.
ltac_no_arg is a constant that can be used to simulate optional arguments in tactic definitions. Use mytactic ltac_no_arg on the tactic invokation, and use match arg with ltac_no_arg => .. or match type of arg with ltac_No_arg => .. to test whether an argument was provided.
ltac_wild is a constant that can be used to simulate wildcard arguments in tactic definitions. Notation is __.
ltac_wilds is another constant that is typically used to simulate a sequence of N wildcards, with N chosen appropriately depending on the context. Notation is ___.
ltac_Mark and ltac_mark are dummy definitions used as sentinel by tactics, to mark a certain position in the context or in the goal.
gen_until_mark repeats generalize on hypotheses from the context, starting from the bottom and stopping as soon as reaching an hypothesis of type Mark. If fails if Mark does not appear in the context.
gen_until_mark_with_processing F is similar to gen_until_mark except that it calls F on each hypothesis immediately before generalizing it. This is useful for processing the hypotheses.
intro_until_mark repeats intro until reaching an hypothesis of type Mark. It throws away the hypothesis Mark. It fails if Mark does not appear as an hypothesis in the goal.
A datatype of type list Boxer is used to manipulate list of Coq values in ltac. Notation is >> v1 v2 ... vN for building a list containing the values v1 through vN.
The tactic list_boxer_of inputs a term E and returns a term
of type list boxer
, according to the following rules:
list Boxer, then it returns E;
Use the hint facility to implement a database mapping terms to terms. To declare a new database, use a definition: Definition mydatabase := True.
Then, to map mykey to myvalue, write the hint: Hint Extern 1 (Register mydatabase mykey) => Provide myvalue.
Finally, to query the value associated with a key, run the tactic ltac_database_get mydatabase mykey. This will leave at the head of the goal the term myvalue. It can then be named and exploited using intro.
In a list of arguments >> H1 H2 .. HN passed to a tactic such as lets or applys or forwards or specializes, the term rm, an identity function, can be placed in front of the name of an hypothesis to be deleted.
rm_term E removes one hypothesis that admits the same type as E.
rm_inside E calls rm_term Ei for any subterm of the form rm Ei found in E
For faster performance, one may deactivate rm_inside by replacing the body of this definition with idtac.
When tactic takes a natural number as argument, it may be parsed either as a natural number or as a relative number. In order for tactics to convert their arguments into natural numbers, we provide a conversion tactic.
ltac_pattern E at K is the same as pattern E at K except that K is a Coq number (nat or Z) rather than a Ltac integer. Syntax ltac_pattern E as K in H is also available.
ltac_set (x := E) at K is the same as set (x := E) at K except that K is a Coq number (nat or Z) rather than a Ltac integer.
show tac executes a tactic tac that produces a result, and then display its result.
dup N produces N copies of the current goal. It is useful for building examples on which to illustrate behaviour of tactics. dup is short for dup 2.
is_not_evar E succeeds only if E is not an evar; it fails otherwise. It thus implements the negation of is_evar
is_evar_as_bool E evaluates to true if E is an evar and to false otherwise.
with_evar T (fun M => tac) creates a new evar that can be used in the tactic tac under the name M.
get_last_hyp tt is a function that returns the last hypothesis at the bottom of the context. It is useful to obtain the default name associated with the hypothesis, e.g. intro; let H := get_last_hyp tt in let H' := fresh "P" H in ...
ltac_tag_subst is a specific marker for hypotheses which is used to tag hypotheses that are equalities to be substituted.
ltac_to_generalize is a specific marker for hypotheses to be generalized.
get_head E is a tactic that returns the head constant of the term E, ie, when applied to a term of the form P x1 ... xN it returns P. If E is not an application, it returns E. Warning: the tactic seems to loop in some cases when the goal is a product and one uses the result of this function.
get_fun_arg E is a tactic that decomposes an application term E, ie, when applied to a term of the form X1 ... XN it returns a pair made of X1 .. X(N-1) and XN.
ltac_action_at K of E do Tac isolates the K-th occurence of E in the goal, setting it in the form P E for some named pattern P, then calls tactic Tac, and finally unfolds P. Syntax ltac_action_at K of E in H do Tac is also available.
protects E do Tac temporarily assigns a name to the expression E so that the execution of tactic Tac will not modify E. This is useful for instance to restrict the action of simpl.
eq' is an alias for eq to be used for equalities in inductive definitions, so that they don't get mixed with equalities generated by inversion.
rapply is a tactic similar to eapply except that it is based on the refine tactics, and thus is strictly more powerful (at least in theory :). In short, it is able to perform on-the-fly conversions when required for arguments to match, and it is able to instantiate existentials when required.
The tactics applys_N T, where N is a natural number, provides a more efficient way of using applys T. It avoids trying out all possible arities, by specifying explicitely the arity of function T.
lets_base H E adds an hypothesis H : T to the context, where T is the type of term E. If H is an introduction pattern, it will destruct H according to the pattern.
applys_to H E transform the type of hypothesis H by replacing it by the result of the application of the term E to H. Intuitively, it is equivalent to lets H: (E H).
applys_to H1,...,HN E applys E to several hypotheses
constructors calls constructor or econstructor.
asserts H: T is another syntax for assert (H : T), which also works with introduction patterns. For instance, one can write: asserts \[x P\] (exists n, n = 3), or asserts \[H|H\] (n = 0 \/ n = 1).
asserts H1 .. HN: T is a shorthand for asserts \[H1 \[H2 \[.. HN\]\]\]\: T].
asserts: T is asserts H: T with H being chosen automatically.
cuts H: T is the same as asserts H: T except that the two subgoals generated are swapped: the subgoal T comes second. Note that contrary to cut, it introduces the hypothesis.
cuts: T is cuts H: T with H being chosen automatically.
cuts H1 .. HN: T is a shorthand for cuts \[H1 \[H2 \[.. HN\]\]\]\: T].
The instantiation tactics are used to instantiate a lemma E (whose type is a product) on some arguments. The type of E is made of implications and universal quantifications, e.g. forall x, P x -> forall y z, Q x y z -> R z.
The first possibility is to provide arguments in order: first x,
then a proof of P x, then y etc... In this mode, called Args
,
all the arguments are to be provided. If a wildcard is provided
(written __), then an existential variable will be introduced in
place of the argument.
It is very convenient to give some arguments the lemma should be instantiated on, and let the tactic find out automatically where underscores should be insterted. Underscore arguments __ are interpret as follows: an underscore means that we want to skip the argument that has the same type as the next real argument provided (real means not an underscore). If there is no real argument after underscore, then the underscore is used for the first possible argument.
The general syntax is tactic (>> E1 .. EN) where tactic is the name of the tactic (possibly with some arguments) and Ei are the arguments. Moreover, some tactics accept the syntax tactic E1 .. EN as short for tactic (>> E1 .. EN) for values of N up to 5.
Finally, if the argument EN given is a triple-underscore ___, then it is equivalent to providing a list of wildcards, with the appropriate number of wildcards. This means that all the remaining arguments of the lemma will be instantiated. Definitions in the conclusion are not unfolded in this case.
newer version : support for typeclasses
lets H: (>> E0 E1 .. EN) will instantiate lemma E0 on the arguments Ei (which may be wildcards __), and name H the resulting term. H may be an introduction pattern, or a sequence of introduction patterns I1 I2 IN, or empty. Syntax lets H: E0 E1 .. EN is also available. If the last argument EN is ___ (triple-underscore), then all arguments of H will be instantiated.
forwards H: (>> E0 E1 .. EN) is short for forwards H: (>> E0 E1 .. EN ___). The arguments Ei can be wildcards __ (except E0). H may be an introduction pattern, or a sequence of introduction pattern, or empty. Syntax forwards H: E0 E1 .. EN is also available.
forwards_nounfold I: E is like forwards I: E but does not unfold the head constant of E if there is no visible quantification or hypothesis in E. It is meant to be used mainly by tactics.
forwards_nounfold_then E ltac:(fun K => ..) is like forwards: E but it provides the resulting term to a continuation, under the name K.
applys (>> E0 E1 .. EN) instantiates lemma E0 on the arguments Ei (which may be wildcards __), and apply the resulting term to the current goal, using the tactic applys defined earlier on. applys E0 E1 E2 .. EN is also available.
fapplys (>> E0 E1 .. EN) instantiates lemma E0 on the arguments Ei and on the argument ___ meaning that all evars should be explicitly instantiated, and apply the resulting term to the current goal. fapplys E0 E1 E2 .. EN is also available.
specializes H (>> E1 E2 .. EN) will instantiate hypothesis H on the arguments Ei (which may be wildcards __). If the last argument EN is ___ (triple-underscore), then all arguments of H get instantiated.
specializes_vars H is equivalent to specializes H __ .. __ with as many double underscore as the number of dependent arguments visible from the type of H. Note that no unfolding is currently being performed (this behavior might change in the future). The current implementation is restricted to the case where H is an existing hypothesis -- TODO: generalize.
fapply is a version of apply based on forwards.
sapply stands for super apply
. It tries
apply, eapply, applys and fapply,
and also tries to head-normalize the goal first.
lets_simpl H: E is the same as lets H: E excepts that it calls simpl on the hypothesis H. lets_simpl: E is also provided.
lets_hnf H: E is the same as lets H: E excepts that it calls hnf to set the definition in head normal form. lets_hnf: E is also provided.
puts X: E is a synonymous for pose (X := E). Alternative syntax is puts: E.
logic E, where E is a fact, is equivalent to assert H:E; [tauto | eapply H; clear H]. It is useful for instance to prove a conjunction [A /\ B] by showing first [A] and then [A -> B], through the command [logic (foral A B, A -> (A -> B) -> A /\ B)]
The tactic equates replaces a goal of the form P x y z with a goal of the form P x ?a z and a subgoal ?a = y. The introduction of the evar ?a makes it possible to apply lemmas that would not apply to the original goal, for example a lemma of the form forall n m, P n n m, because x and y might be equal but not convertible.
Usage is equates i1 ... ik, where the indices are the positions of the arguments to be replaced by evars, counting from the right-hand side. If 0 is given as argument, then the entire goal is replaced by an evar.
applys_eq H i1 .. iK is the same as equates i1 .. iK followed by apply H on the first subgoal.
false_goal replaces any goal by the goal False. Contrary to the tactic false (below), it does not try to do anything else
false_post is the underlying tactic used to prove goals of the form False. In the default implementation, it proves the goal if the context contains False or an hypothesis of the form C x1 .. xN = D y1 .. yM, or if the congruence tactic finds a proof of x <> x for some x.
false replaces any goal by the goal False, and calls false_post
tryfalse tries to solve a goal by contradiction, and leaves the goal unchanged if it cannot solve it. It is equivalent to try solve \[ false \].
false E tries to exploit lemma E to prove the goal false. false E1 .. EN is equivalent to false (>> E1 .. EN), which tries to apply applys (>> E1 .. EN) and if it does not work then tries forwards H: (>> E1 .. EN) followed with false
false_invert H proves a goal if it absurd after calling inversion H and false
false_invert proves any goal provided there is at least one hypothesis H in the context (or as a universally quantified hypothesis visible at the head of the goal) that can be proved absurd by calling inversion H.
tryfalse_invert H and tryfalse_invert are like the above but leave the goal unchanged if they don't solve it.
false_neq_self_hyp proves any goal if the context contains an hypothesis of the form E <> E. It is a restricted and optimized version of false. It is intended to be used by other tactics only.
introv is used to name only non-dependent hypothesis.
intros_all repeats intro as long as possible. Contrary to intros, it unfolds any definition on the way. Remark that it also unfolds the definition of negation, so applying intros_all to a goal of the form forall x, P x -> ~Q will introduce x and P x and Q, and will leave False in the goal.
intros_hnf introduces an hypothesis and sets in head normal form
gen X1 .. XN is a shorthand for calling generalize dependent successively on variables XN...X1. Note that the variables are generalized in reverse order, following the convention of the generalize tactic: it means that X1 will be the first quantified variable in the resulting goal.
generalizes X is a shorthand for calling generalize X; clear X. It is weaker than tactic gen X since it does not support dependencies. It is mainly intended for writing tactics.
sets X: E is the same as set (X := E) in *, that is, it replaces all occurences of E by a fresh meta-variable X whose definition is E.
def_to_eq E X H applies when X := E is a local definition. It adds an assumption H: X = E and then clears the definition of X. def_to_eq_sym is similar except that it generates the equality H: E = X.
set_eq X H: E generates the equality H: X = E, for a fresh name X, and replaces E by X in the current goal. Syntaxes set_eq X: E and set_eq: E are also available. Similarly, set_eq <- X H: E generates the equality H: E = X.
sets_eq X HX: E does the same but replaces E by X everywhere in the goal. sets_eq X HX: E in H replaces in H. set_eq X HX: E in |- performs no substitution at all.
gen_eq X: E is a tactic whose purpose is to introduce equalities so as to work around the limitation of the induction tactic which typically loses information. gen_eq E as X replaces all occurences of term E with a fresh variable X and the equality X = E as extra hypothesis to the current conclusion. In other words a conclusion C will be turned into (X = E) -> C. gen_eq: E and gen_eq: E as X are also accepted.
sets_let X finds the first let-expression in the goal and names its body X. sets_eq_let X is similar, except that it generates an explicit equality. Tactics sets_let X in H and sets_eq_let X in H allow specifying a particular hypothesis (by default, the first one that contains a let is considered).
Known limitation: it does not seem possible to support naming of multiple let-in constructs inside a term, from ltac.
rewrites E is similar to rewrite except that it supports the rm directives to clear hypotheses on the fly, and that it supports a list of arguments in the form rewrites (>> E1 E2 E3) to indicate that forwards should be invoked first before rewrites is called.
rewrite_all E iterates version of rewrite E as long as possible. Warning: this tactic can easily get into an infinite loop. Syntax for rewriting from right to left and/or into an hypothese is similar to the one of rewrite.
asserts_rewrite E asserts that an equality E holds (generating a corresponding subgoal) and rewrite it straight away in the current goal. It avoids giving a name to the equality and later clearing it. Syntax for rewriting from right to left and/or into an hypothese is similar to the one of rewrite. Note: the tactic replaces plays a similar role.
cuts_rewrite E is the same as asserts_rewrite E except that subgoals are permuted.
rewrite_except H EQ rewrites equality EQ everywhere but in hypothesis H. Mainly useful for other tactics.
rewrites E at K applies when E is of the form T1 = T2 rewrites the equality E at the K-th occurence of T1 in the current goal. Syntaxes rewrites <- E at K and rewrites E at K in H are also available.
replaces E with F is the same as replace E with F except that the equality E = F is generated as first subgoal. Syntax replaces E with F in H is also available. Note that contrary to replace, replaces does not try to solve the equality by assumption. Note: replaces E with F is similar to asserts_rewrite (E = F).
replaces E at K with F replaces the K-th occurence of E with F in the current goal. Syntax replaces E at K with F in H is also available.
changes is like change except that it does not silently fail to perform its task. (Note that, changes is implemented using rewrite, meaning that it might perform additional beta-reductions compared with the original change tactic.
renames X1 to Y1, ..., XN to YN is a shorthand for a sequence of renaming operations rename Xi into Yi.
unfolds unfolds the head definition in the goal, i.e. if the goal has form P x1 ... xN then it calls unfold P. If the goal is an equality, it tries to unfold the head constant on the left-hand side, and otherwise tries on the right-hand side. If the goal is a product, it calls intros first. warning: this tactic is overriden in LibReflect.
unfolds in H unfolds the head definition of hypothesis H, i.e. if H has type P x1 ... xN then it calls unfold P in H.
unfolds in H1,H2,..,HN allows unfolding the head constant in several hypotheses at once.
unfolds P1,..,PN is a shortcut for unfold P1,..,PN in *.
folds P1,..,PN is a shortcut for fold P1 in *; ..; fold PN in *.
simpls is a shortcut for simpl in *.
simpls P1,..,PN is a shortcut for simpl P1 in *; ..; simpl PN in *.
unsimpl E replaces all occurence of X by E, where X is the result which the tactic simpl would give when applied to E. It is useful to undo what simpl has simplified too far.
unsimpl E in H is similar to unsimpl E but it applies inside a particular hypothesis H.
unsimpl E in * applies unsimpl E everywhere possible. unsimpls E is a synonymous.
nosimpl t protects the Coq termt against some forms of simplification. See Gonthier's work for details on this trick.
substs does the same as subst, except that it does not fail when there are circular equalities in the context.
Implementation of substs below, which allows to call subst on all the hypotheses that lie beyond a given position in the proof context.
substs below body E applies subst on all equalities that appear in the context below the first hypothesis whose body is E. If there is no such hypothesis in the context, it is equivalent to subst. For instance, if H is an hypothesis, then substs below H will substitute equalities below hypothesis H.
substs below H applies subst on all equalities that appear in the context below the hypothesis named H. Note that the current implementation is technically incorrect since it will confuse different hypotheses with the same body.
subst_hyp H substitutes the equality contained in the first hypothesis from the context.
subst_hyp H substitutes the equality contained in H.
intro_subst is a shorthand for intro H; subst_hyp H: it introduces and substitutes the equality at the head of the current goal.
subst_local substitutes all local definition from the context
subst_eq E takes an equality x = t and replace x with t everywhere in the goal
pi_rewrite E replaces E of type Prop with a fresh unification variable, and is thus a practical way to exploit proof irrelevance, without writing explicitly rewrite (proof_irrelevance E E'). Particularly useful when E' is a big expression.
Note: current implementation only supports up to arity 5
fequal is a variation on f_equal which has a better behaviour on equalities between n-ary tuples.
fequals is the same as fequal except that it tries and solve all trivial subgoals, using reflexivity and congruence (as well as the proof-irrelevance principle). fequals applies to goals of the form f x1 .. xN = f y1 .. yN and produces some subgoals of the form xi = yi).
fequals_rec calls fequals recursively. It is equivalent to repeat (progress fequals).
invert keep H is same to inversion H except that it puts all the facts obtained in the goal. The keyword keep means that the hypothesis H should not be removed.
invert keep H as X1 .. XN is the same as inversion H as ... except that only hypotheses which are not variable need to be named explicitely, in a similar fashion as introv is used to name only hypotheses.
invert H is same to inversion H except that it puts all the facts obtained in the goal and clears hypothesis H. In other words, it is equivalent to invert keep H; clear H.
invert H as X1 .. XN is the same as invert keep H as X1 .. XN but it also clears hypothesis H.
Our inversion tactics is able to get rid of dependent equalities generated by inversion, using proof irrelevance.
inverts keep H is same to invert keep H except that it applies subst to all the equalities generated by the inversion.
inverts keep H as X1 .. XN is the same as invert keep H as X1 .. XN except that it applies subst to all the equalities generated by the inversion
inverts H is same to inverts keep H except that it clears hypothesis H.
inverts H as X1 .. XN is the same as inverts keep H as X1 .. XN but it also clears the hypothesis H.
inverts H as performs an inversion on hypothesis H, substitutes generated equalities, and put in the goal the other freshly-created hypotheses, for the user to name explicitly. inverts keep H as is the same except that it does not clear H. TODO: reimplement inverts above using this one
lets_inverts E as I1 .. IN is intuitively equivalent to inverts E, with the difference that it applies to any expression and not just to the name of an hypothesis.
Underlying implementation of injects
injects keep H takes an hypothesis H of the form C a1 .. aN = C b1 .. bN and substitute all equalities ai = bi that have been generated.
injects H is similar to injects keep H but clears the hypothesis H.
inject H as X1 .. XN is the same as injection followed by intros X1 .. XN
The tactics inversions and injections provided in this section are similar to inverts and injects except that they perform substitution on all equalities from the context and not only the ones freshly generated. The counterpart is that they have simpler implementations.
DEPRECATED: these tactics should no longer be used.
inversions keep H is the same as inversions H but it does not clear hypothesis H.
inversions H is a shortcut for inversion H followed by subst and clear H. It is a rough implementation of inverts keep H which behave badly when the proof context already contains equalities. It is provided in case the better implementation turns out to be too slow.
injections keep H is the same as injection H followed by intros and subst. It is a rough implementation of injects keep H which behave badly when the proof context already contains equalities, or when the goal starts with a forall or an implication.
injections H is the same as injection H followed by clear H and intros and subst. It is a rough implementation of injects keep H which behave badly when the proof context already contains equalities, or when the goal starts with a forall or an implication.
cases is similar to case_eq E except that it generates the equality in the context and not in the goal, and generates the equality the other way round. The syntax cases E as H allows specifying the name H of that hypothesis.
case_if_post H is to be defined later as a tactic to clean up hypothesis H and the goal. By defaults, it looks for obvious contradictions. Currently, this tactic is extended in LibReflect to clean up boolean propositions.
case_if looks for a pattern of the form if ?B then ?E1 else ?E2 in the goal, and perform a case analysis on B by calling destruct B. Subgoals containing a contradiction are discarded. case_if looks in the goal first, and otherwise in the first hypothesis that contains an if statement. case_if in H can be used to specify which hypothesis to consider. Syntaxes case_if as Eq and case_if in H as Eq allows to name the hypothesis coming from the case analysis.
cases_if is similar to case_if with two main differences: if it creates an equality of the form x = y and then substitutes it in the goal
case_ifs is like repeat case_if
destruct_if looks for a pattern of the form if ?B then ?E1 else ?E2 in the goal, and perform a case analysis on B by calling destruct B. It looks in the goal first, and otherwise in the first hypothesis that contains an if statement.
BROKEN since v8.5beta2. TODO: cleanup.
destruct_head_match performs a case analysis on the argument of the head pattern matching when the goal has the form match ?E with ... or match ?E with ... = _ or _ = match ?E with .... Due to the limits of Ltac, this tactic will not fail if a match does not occur. Instead, it might perform a case analysis on an unspecified subterm from the goal. Warning: experimental.
cases' E is similar to case_eq E except that it generates the equality in the context and not in the goal. The syntax cases' E as H allows specifying the name H of that hypothesis.
cases_if' is similar to cases_if except that it generates the symmetric equality.
inductions E is a shorthand for dependent induction E. inductions E gen X1 .. XN is a shorthand for dependent induction E generalizing X1 .. XN.
induction_wf IH: E X is used to apply the well-founded induction principle, for a given well-founded relation. It applies to a goal PX where PX is a proposition on X. First, it sets up the goal in the form (fun a => P a) X, using pattern X, and then it applies the well-founded induction principle instantiated on E.
Here E may be either:
Syntaxes induction_wf: E X and induction_wf E X.
Induction on the height of a derivation: the helper tactic induct_height helps proving the equivalence of the auxiliary judgment that includes a counter for the maximal height (see LibTacticsDemos for an example)
Tactic cofixs IH is like cofix IH except that the coinduction hypothesis is tagged in the form IH: COIND P instead of being just IH: P. This helps other tactics clearing the coinduction hypothesis using clear_coind
Tactic clear_coind clears all the coinduction hypotheses, assuming that they have been tagged
Tactic abstracts tac is like abstract tac except that it clears the coinduction hypotheses so that the productivity check will be happy. For example, one can use abstracts omega to obtain the same behavior as omega but with an auxiliary lemma being generated.
decides_equality is the same as decide equality excepts that it is able to unfold definitions at head of the current goal.
iff H can be used to prove an equivalence P <-> Q and name H the hypothesis obtained in each case. The syntaxes iff and iff H1 H2 are also available to specify zero or two names. The tactic iff <- H swaps the two subgoals, i.e. produces (Q -> P) as first subgoal.
N-ary Conjunctions Splitting in Goals
Underlying implementation of splits.
splits applies to a goal of the form (T1 /\ .. /\ TN) and destruct it into N subgoals T1 .. TN. If the goal is not a conjunction, then it unfolds the head definition.
splits N is similar to splits, except that it will unfold as many definitions as necessary to obtain an N-ary conjunction.
N-ary Conjunctions Deconstruction
Underlying implementation of destructs.
destructs T allows destructing a term T which is a N-ary conjunction. It is equivalent to destruct T as (H1 .. HN), except that it does not require to manually specify N different names.
destructs N T is equivalent to destruct T as (H1 .. HN), except that it does not require to manually specify N different names. Remark that it is not restricted to N-ary conjunctions.
Proving goals which are N-ary disjunctions
Underlying implementation of branch.
branch N applies to a goal of the form P1 \/ ... \/ PK \/ ... \/ PN and leaves the goal PK. It only able to unfold the head definition (if there is one), but for more complex unfolding one should use the tactic branch K of N.
branch K of N is similar to branch K except that the arity of the disjunction N is given manually, and so this version of the tactic is able to unfold definitions. In other words, applies to a goal of the form P1 \/ ... \/ PK \/ ... \/ PN and leaves the goal PK.
N-ary Disjunction Deconstruction
Underlying implementation of branches.
branches T allows destructing a term T which is a N-ary disjunction. It is equivalent to destruct T as [ H1 | .. | HN ] , and produces N subgoals corresponding to the N possible cases.
branches N T is the same as branches T except that the arity is forced to N. This version is useful to unfold definitions on the fly.
branches automatically finds a hypothesis h that is a disjunction and destructs it.
exists T1 ... TN is a shorthand for exists T1; ...; exists TN. It is intended to prove goals of the form exist X1 .. XN, P. If an argument provided is __ (double underscore), then an evar is introduced. exists T1 .. TN ___ is equivalent to exists T1 .. TN __ __ __ with as many __ as possible.
For compatibility with Coq syntax, exists T1, .., TN is also provided.
Existentials and conjunctions in hypotheses
unpack or unpack H destructs conjunctions and existentials in all or one hypothesis.
typeclass is an automation tactic specialized for finding typeclass instances.
solve_typeclass is a simpler version of typeclass, to use in hint tactics for resolving instances
hint E adds E as an hypothesis so that automation can use it. Syntax hint E1,..,EN is available
jauto is better at intuition eauto because it can open existentials from the context. In the same time, jauto can be faster than intuition eauto because it does not destruct disjunctions from the context. The strategy of jauto can be summarized as follows:
iauto is a shorthand for intuition eauto
The two following tactics defined the default behaviour of
light automation
and strong automation
. These tactics
may be redefined at any time using the syntax Ltac .. ::= ...
auto_tilde is the tactic which will be called each time a symbol ~ is used after a tactic.
auto_star is the tactic which will be called each time a symbol * is used after a tactic.
autos~ is a notation for tactic auto_tilde. It may be followed by lemmas (or proofs terms) which auto will be able to use for solving the goal.
autos is an alias for autos~
autos* is a notation for tactic auto_star. It may be followed by lemmas (or proofs terms) which auto will be able to use for solving the goal.
auto_false is a version of auto able to spot some contradictions. There is an ad-hoc support for goals in <->: split is called first. auto_false~ and auto_false* are also available.
Any tactic followed by the symbol ~ will have auto_tilde called on all of its subgoals. Three exceptions:
Some builtin tactics are not defined using tactic notations and thus cannot be extended, e.g., simpl and unfold. For these, notation such as simpl~ will not be available.
Any tactic followed by the symbol * will have auto* called on all of its subgoals. The exceptions to these rules are the same as for light automation.
Exception: use subs* instead of subst* if you import the library Coq.Classes.Equivalence.
hide_def x and show_def x can be used to hide/show the body of the definition x.
show_def unfolds Something in the goal
hide_defs and show_defs applies to all definitions
hide_hyp H replaces the type of H with the notation Something and show_hyp H reveals the type of the hypothesis. Note that the hidden type of H remains convertible the real type of H.
hide_hyps and show_hyps can be used to hide/show all hypotheses of type Prop.
hide H and show H automatically select between hide_hyp or hide_def, and show_hyp or show_def. Similarly hide_all and show_all apply to all.
hide_term E can be used to hide a term from the goal. show_term or show_term E can be used to reveal it. hide_term E in H can be used to specify an hypothesis.
show_unfold R unfolds the definition of R and reveals the hidden definition of R. --todo:test, and implement using unfold simply
sort sorts out hypotheses from the context by moving all the propositions (hypotheses of type Prop) to the bottom of the context.
clears X1 ... XN is a variation on clear which clears the variables X1..XN as well as all the hypotheses which depend on them. Contrary to clear, it never fails.
clears (without any argument) clears all the unused variables from the context. In other words, it removes any variable which is not a proposition (i.e. not of type Prop) and which does not appear in another hypothesis nor in the goal.
clears_all clears all the hypotheses from the context that can be cleared. It leaves only the hypotheses that are mentioned in the goal.
clears_but H1 H2 .. HN clears all hypotheses except the one that are mentioned and those that cannot be cleared.
clears_last clears the last hypothesis in the context. clears_last N clears the last N hypotheses in the context.
demo is like admit but it documents the fact that admit is intended
admits H: T adds an assumption named H of type T to the current context, blindly assuming that it is true. admit: T is another possible syntax. Note that H may be an intro pattern.
admit_cuts T simply replaces the current goal with T.
admit_goal H applies to any goal. It simply assumes
the current goal to be true. The assumption is named H
.
It is useful to set up proof by induction or coinduction.
Syntax admit_goal is also accepted.
admit_rewrite T can be applied when T is an equality. It blindly assumes this equality to be true, and rewrite it in the goal.
admit_rewrite T in H is similar as admit_rewrite, except that it rewrites in hypothesis H.
admit_rewrites_all T is similar as admit_rewrite, except that it rewrites everywhere (goal and all hypotheses).
forwards_nounfold_admit_sides_then E ltac:(fun K => ..) is like forwards: E but it provides the resulting term to a continuation, under the name K, and it admits any side-condition produced by the instantiation of E, using the skip tactic.
The module Program contains definitions that conflict with the current module. If you import Program, either directly or indirectly (e.g., through Setoid or ZArith), you will need to import the compability definitions through the top-level command: Import LibTacticsCompatibility.