Coq comes with a set of builtin tactics, such as reflexivity, intros, inversion and so on. While it is possible to conduct proofs using only those tactics, you can significantly increase your productivity by working with a set of more powerful tactics. This chapter describes a number of such useful tactics, which, for various reasons, are not yet available by default in Coq. These tactics are defined in the LibTactics.v file.
Remark: SSReflect is another package providing powerful tactics.
The library LibTactics
differs from SSReflect
in two respects:
SSReflectwas primarily developed for proving mathematical theorems, whereas
LibTacticswas primarily developed for proving theorems on programming languages. In particular,
LibTacticsprovides a number of useful tactics that have no counterpart in the
SSReflectpackage.
SSReflectentirely rethinks the presentation of tactics, whereas
LibTacticsmostly stick to the traditional presentation of Coq tactics, simply providing a number of additional tactics. For this reason,
LibTacticsis probably easier to get started with than
SSReflect.
This chapter is a tutorial focusing on the most useful features
from the LibTactics
library. It does not aim at presenting all
the features of LibTactics
. The detailed specification of tactics
can be found in the source file LibTactics.v. Further documentation
as well as demos can be found at http://www.chargueraud.org/softs/tlc/.
In this tutorial, tactics are presented using examples taken from
the core chapters of the Software Foundations
course. To illustrate
the various ways in which a given tactic can be used, we use a
tactic that duplicates a given goal. More precisely, dup produces
two copies of the current goal, and dup n produces n copies of it.
This section presents the following tactics:
The tactic introv allows to automatically introduce the variables of a theorem and explicitly name the hypotheses involved. In the example shown next, the variables c, st, st1 and st2 involved in the statement of determinism need not be named explicitly, because their name where already given in the statement of the lemma. On the contrary, it is useful to provide names for the two hypotheses, which we name E1 and E2, respectively.
When there is no hypothesis to be named, one can call introv without any argument.
The tactic introv also applies to statements in which forall and -> are interleaved.
Like the arguments of intros, the arguments of introv can be structured patterns.
Remark: the tactic introv works even when definitions need to be unfolded in order to reveal hypotheses.
The inversion tactic of Coq is not very satisfying for three reasons. First, it produces a bunch of equalities which one typically wants to substitute away, using subst. Second, it introduces meaningless names for hypotheses. Third, a call to inversion H does not remove H from the context, even though in most cases an hypothesis is no longer needed after being inverted. The tactic inverts address all of these three issues. It is intented to be used in place of the tactic inversion.
The following example illustrates how the tactic inverts H behaves mostly like inversion H except that it performs some substitutions in order to eliminate the trivial equalities that are being produced by inversion.
A slightly more interesting example appears next.
The tactic inverts H as. is like inverts H except that the variables and hypotheses being produced are placed in the goal rather than in the context. This strategy allows naming those new variables and hypotheses explicitly, using either intros or introv.
In the particular case where a call to inversion produces a single subgoal, one can use the syntax inverts H as H1 H2 H3 for calling inverts and naming the new hypotheses H1, H2 and H3. In other words, the tactic inverts H as H1 H2 H3 is equivalent to inverts H as; introv H1 H2 H3. An example follows.
A more involved example appears next. In particular, this example shows that the name of the hypothesis being inverted can be reused.
Note: in the rare cases where one needs to perform an inversion on an hypothesis H without clearing H from the context, one can use the tactic inverts keep H, where the keyword keep indicates that the hypothesis should be kept in the context.
Because Coq encodes conjunctions and disjunctions using binary
constructors /\ and \/, working with a conjunction or a
disjunction of N facts can sometimes be quite cumbursome.
For this reason, LibTactics
provides tactics offering direct
support for n-ary conjunctions and disjunctions. It also provides
direct support for n-ary existententials.
This section presents the following tactics:
The tactic splits applies to a goal made of a conjunction of n propositions and it produces n subgoals. For example, it decomposes the goal G1 /\ G2 /\ G3 into the three subgoals G1, G2 and G3.
The tactic branch k can be used to prove a n-ary disjunction. For example, if the goal takes the form G1 \/ G2 \/ G3, the tactic branch 2 leaves only G2 as subgoal. The following example illustrates the behavior of the branch tactic.
One of the major weakness of Coq compared with other interactive proof assistants is its relatively poor support for reasoning with equalities. The tactics described next aims at simplifying pieces of proof scripts manipulating equalities.
This section presents the following tactics:
The tactic asserts_rewrite (E1 = E2) replaces E1 with E2 in the goal, and produces the goal E1 = E2.
The tactic cuts_rewrite (E1 = E2) is like asserts_rewrite (E1 = E2), except that the equality E1 = E2 appears as first subgoal.
More generally, the tactics asserts_rewrite and cuts_rewrite can be provided a lemma as argument. For example, one can write asserts_rewrite (forall a b, a*(S b) = a*b+a). This formulation is useful when a and b are big terms, since there is no need to repeat their statements.
The tactic substs is similar to subst except that it
does not fail when the goal contains circular equalities
,
such as x = f x.
The tactic fequals is similar to f_equal except that it directly discharges all the trivial subgoals produced. Moreover, the tactic fequals features an enhanced treatment of equalities between tuples.
The tactic applys_eq is a variant of eapply that introduces equalities for subterms that do not unify. For example, assume the goal is the proposition P x y and assume we have the assumption H asserting that P x z holds. We know that we can prove y to be equal to z. So, we could call the tactic assert_rewrite (y = z) and change the goal to P x z, but this would require copy-pasting the values of y and z. With the tactic applys_eq, we can call applys_eq H 1, which proves the goal and leaves only the subgoal y = z. The value 1 given as argument to applys_eq indicates that we want an equality to be introduced for the first argument of P x y counting from the right. The three following examples illustrate the behavior of a call to applys_eq H 1, a call to applys_eq H 2, and a call to applys_eq H 1 2.
If the mismatch was on the first argument of P instead of the second, we would have written applys_eq H 2. Recall that the occurences are counted from the right.
When we have a mismatch on two arguments, we want to produce two equalities. To achieve this, we may call applys_eq H 1 2. More generally, the tactic applys_eq expects a lemma and a sequence of natural numbers as arguments.
This section of the tutorial introduces a few tactics that help make proof scripts shorter and more readable:
The tactic unfolds (without any argument) unfolds the head constant of the goal. This tactic saves the need to name the constant explicitly.
Remark: contrary to the tactic hnf, which may unfold several constants, unfolds performs only a single step of unfolding.
Remark: the tactic unfolds in H can be used to unfold the head definition of the hypothesis H.
The tactic false can be used to replace any goal with False. In short, it is a shorthand for exfalso. Moreover, false proves the goal if it contains an absurd assumption, such as False or 0 = S n, or if it contains contradictory assumptions, such as x = true and x = false.
The tactic false can be given an argument: false H replace the goals with False and then applies H.
The tactic tryfalse is a shorthand for try solve [false]: it tries to find a contradiction in the goal. The tactic tryfalse is generally called after a case analysis.
The tactic gen is a shortand for generalize dependent that accepts several arguments at once. An invokation of this tactic takes the form gen x y z.
Temporarily admitting a given subgoal is very useful when constructing proofs. Several tactics are provided as useful wrappers around the builtin admit tactic.
The tactic admits H: P adds the hypothesis H: P to the context, without checking whether the proposition P is true. It is useful for exploiting a fact and postponing its proof. Note: admits H: P is simply a shorthand for assert (H:P). admit.
The tactic admit_rewrite (E1 = E2) replaces E1 with E2 in the goal, without checking that E1 is actually equal to E2.
The tactic admit_goal adds the current goal as hypothesis. This cheat is useful to set up the structure of a proof by induction without having to worry about the induction hypothesis being applied only to smaller arguments. Using skip_goal, one can construct a proof in two steps: first, check that the main arguments go through without waisting time on fixing the details of the induction hypotheses; then, focus on fixing the invokations of the induction hypothesis.
The tactic sort reorganizes the proof context by placing all the variables at the top and all the hypotheses at the bottom, thereby making the proof context more readable.
This last section describes a mechanism for instantiating a lemma by providing some of its arguments and leaving other implicit. Variables whose instantiation is not provided are turned into existentential variables, and facts whose instantiation is not provided are turned into subgoals.
Remark: this instantion mechanism goes far beyond the abilities of
the Implicit Arguments
mechanism. The point of the instantiation
mechanism described in this section is that you will no longer need
to spend time figuring out how many underscore symbols you need to
write.
In this section, we'll use a useful feature of Coq for decomposing conjunctions and existentials. In short, a tactic like intros or destruct can be provided with a pattern (H1 & H2 & H3 & H4 & H5), which is a shorthand for [H1 [H2 [H3 [H4 H5]]]]]. For example, destruct (H _ _ _ Htypt) as [T [Hctx Hsub]]. can be rewritten in the form destruct (H _ _ _ Htypt) as (T & Hctx & Hsub).
When we have a lemma (or an assumption) that we want to exploit,
we often need to explicitly provide arguments to this lemma,
writing something like:
destruct (typing_inversion_var _ _ _ Htypt) as (T & Hctx & Hsub).
The need to write several times the underscore
symbol is tedious.
Not only we need to figure out how many of them to write down, but
it also makes the proof scripts look prettly ugly. With the tactic
lets, one can simply write:
lets (T & Hctx & Hsub): typing_inversion_var Htypt.
In short, this tactic lets allows to specialize a lemma on a bunch of variables and hypotheses. The syntax is lets I: E0 E1 .. EN, for building an hypothesis named I by applying the fact E0 to the arguments E1 to EN. Not all the arguments need to be provided, however the arguments that are provided need to be provided in the correct order. The tactic relies on a first-match algorithm based on types in order to figure out how the to instantiate the lemma with the arguments provided.
First, assume we have an assumption H with the type of the form has_type G (var x) T. We can obtain the conclusion of the lemma typing_inversion_var by invoking the tactics lets K: typing_inversion_var H, as shown next.
Assume now that we know the values of G, x and T and we want to obtain S, and have has_type G (var x) T be produced as a subgoal. To indicate that we want all the remaining arguments of typing_inversion_var to be produced as subgoals, we use a triple-underscore symbol ___. (We'll later introduce a shorthand tactic called forwards to avoid writing triple underscores.)
Usually, there is only one context G and one type T that are going to be suitable for proving has_type G (var x) T, so we don't really need to bother giving G and T explicitly. It suffices to call lets (S & Eq & Sub): typing_inversion_var x. The variables G and T are then instantiated using existential variables.
We may go even further by not giving any argument to instantiate typing_inversion_var. In this case, three unification variables are introduced.
Note: if we provide lets with only the name of the lemma as argument, it simply adds this lemma in the proof context, without trying to instantiate any of its arguments.
A last useful feature of lets is the double-underscore symbol, which allows skipping an argument when several arguments have the same type. In the following example, our assumption quantifies over two variables n and m, both of type nat. We would like m to be instantiated as the value 3, but without specifying a value for n. This can be achieved by writting lets K: H __ 3.
Note: one can write lets: E0 E1 E2 in place of lets H: E0 E1 E2. In this case, the name H is chosen arbitrarily.
Note: the tactics lets accepts up to five arguments. Another syntax is available for providing more than five arguments. It consists in using a list introduced with the special symbol >>, for example lets H: (>> E0 E1 E2 E3 E4 E5 E6 E7 E8 E9 10).
The tactics applys, forwards and specializes are shorthand that may be used in place of lets to perform specific tasks.
Examples of use of applys appear further on. Several examples of use of forwards can be found in the tutorial chapter UseAuto.
The following proof shows several examples where lets is used instead of destruct, as well as examples where applys is used instead of apply. The proof also contains some holes that you need to fill in as an exercise.
In this chapter we have presented a number of tactics that help make proof script more concise and more robust on change.
If you are interested in using LibTactics.v in your own developments, make sure you get the lastest version from: http://www.chargueraud.org/softs/tlc/.