case analysis on bounded nat

Stream: general

[Daniel Selsam]

Is there a convenient way of performing case analysis on a bounded nat? For example, given a nat n : nat and a concrete bound h : n < 30, there might be a tactic enum_cases_bounded h that produces 30 subgoals with the ith goal including h_i : n = i.

[Patrick Massot]

tactic#interval_cases

[Daniel Selsam]

The following hits a deterministic timeout:

example (n : nat) (h : n < 10) : true :=
begin interval_cases n, all_goals { trivial } end

Am I the first person to try this on double-digit ranges?

[Markus Himmel]

No, this is a known problem. #12237 is an attempt at a faster version.

[Heather Macbeth]

You can also do this using fin_cases, which seems to be a bit faster in Lean runtime but a bit more unwieldy in terms of number of lines of code.
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Odd.20residues.20mod.208/near/272725327

[Johan Commelin]

#12237 is an attempt at a faster version.

@Kyle Miller since this is not awaiting-review, it doesn't show up on the #queue. Would it make sense to explicitly ping some maintainers (not me, I don't speak meta) to review this?