The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

>> 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

Wow -- this looks really nice!  It seems to solve one of the main issues with 
Aaron's tactics -- that you have to hand-code the list of constructors for 
each inductive type.  

Any chance this feature could eventually be included in Coq by default?

     - B


> 
> 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