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 propositions.
• Convenient support for automation: tactics followed with the symbol "~" or "*" will call automation on the generated subgoals. The 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