An improved set of tactics for CoqBack to Main

This library provides a set of tactics that extends the set of builtin tactics provided with the standard distribution of Coq. It overcomes a number of limitations of the standard set of tactics, and thereby helps users to write shorter and more robust scripts. Implemented in Ltac, the tactic programming language of Coq, the library is fully compatible with the standard distribution of Coq and should not break existing scripts. The library consists of a single file named LibTactics.v. To use the library, all you need to do is to compile it, and then import it in your developments.

An overview of the features appears further on this page. The easiest way to learn how to use the new tactics is to run the commented demo file, included in the distribution. You can also browse directly through the documented syntax-highlighted source script of the library. Note that the tactics are distributed under the GNU-LGPL license.

Overview of the extended set of tactics

Arthur Charguéraud

Notation

E: stands for an expression
H: stands for an existing hypothesis
X: stands for a fresh identifier
I: stands for an introduction pattern 
R: stands for a definition (a "reference") 
__: is a special notation for "wildcard"

Manipulation of hypotheses

introv I1 I2 .. IN   (introduction that inputs only the name of hypotheses, not variables)
intros_all           (introduces all arguments, unfolding all definitions on the way)
gen H1 H2 .. HN      (generalizes and clears hypotheses and their dependencies)
clears H1 ... HN     (clears hypotheses and their dependencies)
sets X: E            (defines X as a local definition for E, and replaces occurences of E with X)
sets_eq X: E         (introduces a name X and an equality X = E, and replaces occurences of E with X)

Proof structure

false             (replaces the goal by "False", and try to solve it with contradiction and discriminate)
false E           (proves any goal by contradiction, using an absurd term E)
tryfalse          (proves a goal by contradiction or discriminate, or do nothing)
asserts I: E      (asserts statement E as first subgoal, destruct E as I in the second goal)
cuts I: E         (asserts statement E as second subgoal, destruct E as I in the first goal)
put X: E          (define X to be a name for E, synonymous of pose)
lets I: E         (adds an hypothesis I whose type is the type of E)
lets I1 .. IN: E  (a shortand for "lets [I1[..IN]]: E", useful to decompose conjunctions)

N-ary constructions

splits           (splits an N-ary conjunction into N goals)
splits N         (same as above, but unfolds if necessary to obtain N branches)
destructs E      (destructs an N-ary conjunction E into N hypotheses)
branch N         (selects the N-th branch of a M-ary disjunction)
branch N of M    (same as above, but unfolds if necessary to obtain M branches)
branches E       (case analysis on an N-ary disjunction E)
exists E1 .. EN  (to provide witnesses to an N-ary existential goal, wildcards are supported)

Inversion and induction

inverts H             (inversion followed with substitution of freshly introduced variables)
inverts keep H        (same as above, but H is not cleared)
invert H as I1..IN    (same as inverts H, but allows to name produced hypotheses)
inversions H          (faster implementation of inverts H, but might substitute too many variables)
inductions_wf X: E H  (applies the well-founded induction principle for a particular well-founded relation)

Working with equalities

substs            (improved implementation of subst – does not fail on circular equalities)
fequals           (improved implementation of f_equal – calls congruence, and better on tuples)
decides_equality  (improved implementation of decide equality – ability to unfold definitions)
rewrite_all E     (rewrites E as many time as possible)
asserts_rewrite E (rewrites with E and generates E as first subgoal)
cuts_rewrite E    (rewrites with E and generates E as second subgoal)

Simplification and unfolding

simpls        (simpl everywhere in hypotheses and conclusion)
unsimpl E     (replace the simplification of E with E)
unfolds R     (unfolds the definition of R in hypotheses and conclusion)
unfolds       (unfolds the head definition of the goal)
unfolds in H  (unfolds the head definition of the hypothesis H)
folds R       (folds R in hypotheses and conclusion)
renames H1 to H1', .., HN to HN'  (multiple renaming)

Development

skip             (admits the current goal - works even if it contains existential variables)
skip I: E        (adds an hypothesis I of type E to the context, and assume it is true)
skip_cuts E      (replaces the current goal with an arbitrary new goal E)
skip_rewrite E   (rewrites with the equality E, admitting the statement E)
sort             (reorders hypotheses to get all the propositions at the bottom of the goal)

Automation

- any tactic name followed with the symbol "~" will call [auto] on all subgoals
- any tactic name followed with the symbol "*" will call [induction eauto] on all subgoals
- these default bindings may be customized locally in a development

Advanced instantiation mode

To instantiate a lemma on particular hypotheses, four instantiation modes are available:

  • Mode "Args": provide a list of the arguments on which to apply the lemma,
  • Mode "Vars": provide only variables, hypotheses are turned into subgoals,
  • Mode "Hyps": provide only hypotheses, variables are introduced as existentials,
  • Mode "Hnts": provide a list of arguments to be used on a first-match basis.

The default mode is the automatic mode, "Hnts", which is used when no mode is specified explicitly.
Below, H stands for the lemma to be instantiated, and the names Ei correspond to the arguments.
Note that wildcards, written "__", can be provided in place of any argument. 

lets I: H E1 ... EN                    (instantiates a lemma and names it)
lets I: (>>> H E1 ... EN)     
lets I: (>>>Mode H E1 ... EN)

applys H E1 ... EN                     (instantiates a lemma and applies it)
applys (>>> H E1 ... EN)     
applys (>>>Mode H E1 ... EN)     

specializes H E1 ... EN                (instantiates an hypothesis H in-place)
specializes H (>>> E1 ... EN)
specializes H (>>>Mode E1 ... EN)

forwards I: H                          (instantiates a lemma, then "forwards" it)
forwards I: (>>> H E1 ... EN) 
forwards I: (>>>Mode H E1 ... HN)

Note: "forwards I: H" is equivalent to "lets I: (>>> H __ __ .. __)",
which can also be abbreviated as "lets I: (>>> H ___)", with a triple-underscore.

Arthur Charguéraud