CoqDSC.LibTactics
- Tools for programming with Ltac
- Identity continuation
- Untyped arguments for tactics
- Optional arguments for tactics
- Wildcard arguments for tactics
- Position markers
- List of arguments for tactics
- Databases of lemmas
- On-the-fly removal of hypotheses
- Numbers as arguments
- Testing tactics
- Testing non-evars
- Check no evar in goal
- Helper function for introducing evars
- Tagging of hypotheses
- Tagging of hypotheses
- Deconstructing terms
- Action at occurence and action not at occurence
- An alias for eq
- Common tactics for simplifying goals like intuition
- Backward and forward chaining
- Introduction and generalization
- Rewriting
- Inversion
- Induction
- Coinduction
- Decidable equality
- Equivalence
- N-ary Conjunctions and Disjunctions
- Tactics to prove typeclass instances
- Tactics to invoke automation
- Tactics to sort out the proof context
- Tactics for development purposes
- Compatibility with standard library
- Additional notations for Coq
CoqDSC.Crush
- Argument invOne is a tuple-list of predicates for which we always do inversion automatically.
- The odd-looking check of the goal form is to avoid cases where injection gives a more complex result because of dependent typing, which we aren't equipped to handle here.
- trace is an accumulator recording which instantiations we choose.
- - A tuple-list of lemmas we try inster-ing
- - A tuple-list of predicates we try inversion for
- Wrap Program's dependent destruction in a slightly more pleasant form
- Also prove the lefthand sides of any implications that this exposes, simplifying H to leave out those implications.