The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

It is quite likely that such features make their way to Coq. Though not for the next release I'm afraid.



Arnaud Spiwack

On 26 April 2011 18:41, Benjamin C. Pierce <bcpierce AT cis.upenn.edu> wrote:

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