Tealeaves.Util.LibTactics
(* Chapter maintained by Arthur Chargueraud *)
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:
External credits:
- 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.
- thanks to Xavier Leroy for providing the idea of tactic forward
- thanks to Georges Gonthier for the implementation trick in rapply
Set Implicit Arguments.
Require Import Coq.Lists.List.
Declare Scope ltac_scope.
(* 2021-05-25 14:19 *)