Commit 2020-12-14 16:39 d36af184

feat(tactic/induction): add induction'/cases'/eliminate_hyp/eliminate_expr tactics (#5027) This PR adds interactive tactics induction' and cases' as well as non-interactive variants eliminate_hyp and eliminate_expr. The tactics are similar to standard induction and cases, but they feature several improvements:

• induction' performs 'dependent induction', which means it takes the indices of indexed inductive types fully into account. This is convenient, for example, for programming language or logic formalisations, which tend to rely heavily on indexed types.
• induction' by default generalises everything that can be generalised. This is to support beginners, who often struggle to identify that a proof requires a generalised induction hypothesis. In cases where this feature hinders more than it helps, it can easily be turned off.
• induction' and cases' generate much more human-friendly names than their standard counterparts. This is, again, mostly to support beginners. Experts should usually supply explicit names to make proof scripts more robust.
• cases' works for some rare goals which cases does not support, but should otherwise be mostly a drop-in replacement (except for the generated names).