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

Announcements
1

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

Main page and documentation: https://github.com/Matafou/LibHyps

SHORT DESCRIPTION:

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
    changes.
  • create a subgoal with the nth premise of a hypothesis (forward reasoning without
    copy-paste).
  • 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

QUICK TEST:

Require Import LibHyps.LibHyps.

Demo file https://github.com/Matafou/LibHyps/blob/master/LibHyps/LibHypsDemo.v

Best regards,
Pierre Courtieu

1 Like
2

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.)
3

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).
  !intros.
  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.
...