LibHyps 1.0: tactics for manipulation of (groups of) hypothesis

This Library provides several coq tactics and tacticals to deal with
hypothesis during a proof.

Main page and documentation:


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.


opam install coq-libhyps


Require Import LibHyps.LibHyps.

Demo file

Best regards,
Pierre Courtieu

1 Like

This is very nice, thanks!

When trying to replay the proof scripts, I

  1. Found a minor typo in the comment introducing <=-tactics, which has = instead of <=
  2. 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).
  onAllHyps move_up_types.
  (* 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.