The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

2011/3/21 Benjamin C. Pierce 
<bcpierce AT cis.upenn.edu>:
>>> * You can use a good indentation
>
> I find Aaron Bohannon's Case tactics to be extremely helpful for this.

And this gives me a new occasion to advertise for my extension of those 
tactics!
https://github.com/pilki/cases

It allows you to:

* like Aaron's tactic, comment your proof scripts and make your proof
scripts more robust, through those comments

* Automatically tag the subcases of an induction: if n is of type nat,
induction' n as [|p] tags the first subcase with "O" and the second
with "S p". This works with any inductive without extra work.

* Automatically tag subgoals when a lemma/constructor has named
hypothesis: if you have a lemma
Lemma lt_is_le: forall m n (LT:m < n), m <= n). omega. Qed.
Then "apply' lt_is_le" produces a sugboal taged "LT".

This is obviously way more usefull when you have many subgoals, with
several of them being proved automatically (by auto for example). And
if one day, auto proves less, or more goals, the proof script fails
loudly exactly where the problem occurs.

* Automatically generate a tag from the names of arguments:
with the simpl tactic:

Ltac destr_eq_nat_dec n1 n2 :=
  string_of n1 (fun strn1 =>
  string_of n2 (fun strn2 =>
  destruct (eq_nat_dec n1 n2);
    [ fst_Case_tac (strn1 ^^ " = " ^^ strn2)
    | fst_Case_tac (strn1 ^^ " <> " ^^ strn2)])).

if you write "destr_eq_nat n 42", the first subgoal is taged with "n =
42" and the second with "n <> 42"

* with a small emacs function (included in the distribution), you can
import those tags directly in your proof script without typing them

Cheers

Alexandre