Commit 2020-12-14 16:39 d36af184

View on Github →

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

Estimated changes

added inductive Even
added inductive Fin
added def List.append
added inductive List
added inductive Two
added inductive Vec.eq
added inductive Vec
added def accufact
added theorem accufact_1_eq_fact
added inductive expressions.exp
added theorem expressions.subst_Var
added theorem fraction.ext
added structure fraction
added inductive le
added inductive
added theorem less_than.lt_lte
added inductive less_than.lte
added inductive lt
added inductive nat_or_positive
added theorem not_even_2_mul_add_1
added theorem not_sorted_17_13
added inductive palindrome.palindrome
added inductive rose.nonempty
added inductive rose
added inductive rose₁
added inductive semantics.big_step
added inductive semantics.small_step
added theorem
added theorem
added theorem
added def semantics.state
added inductive semantics.stmt
added inductive sorted
added theorem star.head
added theorem star.head_induction_on
added inductive star
added inductive
added inductive ℕ'
added def ℕ₂.plus
added inductive ℕ₂