Zulip Chat Archive

Stream: general

Topic: case analysis on bounded nat

Daniel Selsam (Feb 27 2022 at 19:01):

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 (Feb 27 2022 at 19:02):


Daniel Selsam (Feb 27 2022 at 19:28):

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 (Feb 27 2022 at 19:38):

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

Heather Macbeth (Feb 27 2022 at 20:39):

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.

Johan Commelin (Feb 28 2022 at 05:35):

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

Last updated: Aug 03 2023 at 10:10 UTC