The Coq mailing list

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

Dear list

I would like to announce the birth of the not even 0.1alpha version of
a plugin extending the (S*)Case tactic by Aaron Bohannon from UPenn.

The initial version can be found here
http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab27
and the extension via a plugin here: https://github.com/pilki/cases

The main feature is to build the foo_cases tactics automatically for
any inductive foo.

It also provides a "string of trm in H" tactics that builds a coq
string from any coq term, which can be useful to build nice automatic
Case tactics.

More detailed example can be found in the example file
https://github.com/pilki/cases/blob/master/test-suite/case_tactics_ex.v

The big limitation is that I don't deal with the inversion tactic,
since it does not always produce the same number of subgoal. The only
way I see to do this is to hack the inversion tactic so that it
produces a dummy True sub goal for each discarded branch. But hacking
the inversion tactic seems a bit overkill to me.

Does anyone have any idea on this?

Alexandre Pilkiewicz