This Library provides several coq tactics and tacticals to deal with
hypothesis during a proof.
Main page and documentation: https://github.com/Matafou/LibHyps
Among manipulations on hypothesis we provide:
- Automatically give better names to hypothesis. The name is computed
from the type of the hypothesis so that it resists lots of script
- create a subgoal with the nth premise of a hypothesis (forward reasoning without
- move up non-prop hypothesis, to focus on properties
- apply subst, revert.
- any tactic taking a hypothesis name as parameter
These manipulations can be applied:
- to one hyp
- to all hyps
- to “new” hyps after some tactics.
QUICK INSTALL USING OPAM
opam install coq-libhyps
Require Import LibHyps.LibHyps.