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.
Demo file https://github.com/Matafou/LibHyps/blob/master/LibHyps/LibHypsDemo.v
This is very nice, thanks!
When trying to replay the proof scripts, I
- Found a minor typo in the comment introducing
<=-tactics, which has
= instead of
- Hit an error on the first
decompose call, whose hypothesis is not named in the same way on my machine (8.9.0) and in the source file. (This may be related to the
rename_depth setting that we play with just before, but I didn’t find a depth setting that makes the naming match: either the boolean part is more detailed, or the arithmetic part is less detailed than in the Demo name.)
Thanks! Indeed the demo file is broken. I will fix this soon.
It should read like this:
(* Let us have really big names. *)
Ltac rename_depth ::= constr:(5).
(* decompose and revert all new hyps *)
decompose [ex and] h_ex_and_neq_true_andb_false_true_and_le_w_w_eq_w_x ;!; revertHyp.