LibTactics: A Collection of Handy General-Purpose Tactics

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:

• More convenient syntax for naming hypotheses, with tactics for introduction and inversion that take as input only the name of hypotheses of type Prop, rather than the name of all variables.
• Tactics providing true support for manipulating N-ary conjunctions, disjunctions and existentials, hidding the fact that the underlying implementation is based on binary predicates.
• Convenient support for automation: tactic followed with the symbol "~" or "*" will call automation on the generated subgoals. Symbol "~" stands for auto and "*" for intuition eauto. These bindings can be customized.
• Forward-chaining tactics are provided to instantiate lemmas either with variable or hypotheses or a mix of both.
• A more powerful implementation of apply is provided (it is based on refine and thus behaves better with respect to conversion).
• An improved inversion tactic which substitutes equalities on variables generated by the standard inversion mecanism. Moreover, it supports the elimination of dependently-typed equalities (requires axiom K, which is a weak form of Proof Irrelevance).
• Tactics for saving time when writing proofs, with tactics to asserts hypotheses or sub-goals, and improved tactics for clearing, renaming, and sorting hypotheses.

External credits:

• thanks to Xavier Leroy for providing the idea of tactic forward,
• thanks to Georges Gonthier for the implementation trick in rapply,

Additional notations for Coq

N-ary Existentials

∃ T1 ... TN, P is a shorthand for ∃ T1, ..., ∃ TN, P. Note that Coq.Program.Syntax already defines exists for arity up to 4.

Tools for programming with Ltac

Identity continuation

Untyped arguments for tactics

Any Coq value can be boxed into the type Boxer. This is useful to use Coq computations for implementing tactics.

Optional arguments for 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.

Wildcard arguments for tactics

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 ___.

Position markers

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.

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.

List of arguments for tactics

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:

• if E is already of type "list Boxer", then it returns E;
• otherwise, it returns the list (boxer E)::nil.

Databases of lemmas

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.

On-the-fly removal of hypotheses

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.

Numbers as arguments

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 natural rather than a Ltac integer. Syntax ltac_pattern E as K in H is also available.

Testing tactics

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.

Check no evar in goal

Tagging of hypotheses

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 ...

Tagging of hypotheses

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.

Deconstructing terms

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.

Action at occurence and action not at occurence

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.

An alias for eq

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.

Backward and forward chaining

Application

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).

constructors calls constructor or econstructor.

Assertions

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 \].

tryfalse by tac / is that same as tryfalse except that it tries to solve the goal using tactic tac if assumption and discriminate do not apply. It is equivalent to try solve \[ false; tac \]. Example: tryfalse by congruence/

false T tries false; apply T, or otherwise adds T as an assumption and calls false.

false_invert proves any goal provided there is at least one hypothesis H in the context that can be proved absurd by calling inversion H.

tryfalse_invert tries to prove the goal using false or false_invert, and leaves the goal unchanged if it does not succeed.

asserts H: T is another syntax for assert (H : T), which also works with introduction patterns. For instance, one can write: asserts \[x P\] (∃ 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].

Instantiation and forward-chaining

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. ∀ x, P x → ∀ 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 often saves a lot of time to give only the dependent variables, (here x, y and z), and have the hypotheses generated as subgoals. In this "Vars" mode, only variables are to be provided. For instance, lemma E applied to 3 and 4 is a term of type ∀ z, Q 3 4 z → R z, and P 3 is a new subgoal. It is possible to use wildcards to introduce existential variables. However, there are situations where some of the hypotheses already exists, and it saves time to instantiate the lemma E using the hypotheses. For instance, suppose F is a term of type P 2. Then the application of E to F in this "Hyps" mode is a term of type ∀ y z, Q 2 y z → R z. Each wildcard use will generate an assertion instead, for instance if G has type Q 2 3 4, then the application of E to a wildcard and to G in mode-h is a term of type R 4, and P 2 is a new subgoal. 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 (>>Hnts 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.

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.

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.

Experimental tactics for application

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.

Adding assumptions

lets_simpl H: E is the same as lets H: E excepts that it calls simpl on the hypothesis H.

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_simpl: E is the same as lets_simpl H: E with the name H being choosed automatically.

lets_hnf: E is the same as lets_hnf H: E with the name H being choosed automatically.

put X: E is a synonymous for pose (X := E). Other syntaxes are put: E.

Application of tautologies

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)]

Application modulo equalities

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 ∀ 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.