feat(tactic/nat_cases): a tactic to case bash inequalities on natural numbers

[semorrison]

From tactics.md:

### nat_cases
`nat_cases n` searches for upper and lower bounds on a ℕ variable `n`, and if an
upper bound is found, splits into separate cases for each possible value of `n`.

As an example, in
```
example (n : ℕ) (w₁ : n ≥ 3) (w₂ : n < 5) : n = 3 ∨ n = 4 :=
begin
  nat_cases n,
  all_goals {simp}
end
```
after `nat_cases n`, the goals are `3 = 3 ∨ 3 = 4` and `4 = 3 ∨ 4 = 4`.

[ChrisHughes24]

Will/should this work on a proof about say n % 3, given a proof that n % 3 < 3?

[jcommelin]

Nice! This is a tactic that I've wished I had access to several times before. How hard would it be to generalize this to int, fin N, pnat, with_top nat, etc...? I don't see a very nice way to generalize these... Maybe we need a has_succ class? Such a class would include an axiom that says that you can enumerate all n satisfying a ≤ n and n < b, by a finite number of succ-applications to a.
This would work even for with_top nat, due to the assymetry between a and b. It wouldn't work for with_bot int...

[robertylewis]

I haven't fully processed what's going on here, but some quick comments.

At the very least, nat_cases is overcomplicated. Once you get a_prf and b_prf, feed them into cases_of_bound and you're done:

meta def cases_of_bound (hl hu : expr) : tactic unit :=
to_expr ``(list.Ico.mem.2 ⟨%%hl, %%hu⟩) >>= note_anon >>= fin_cases_at none 

It would be way nicer to use omega in place of linarith, but I think the various bugs rule that out right now (#1484).

The more general way to do this is with fintypes. For various types, we can provide fintype (or set.finite?) instances for set.Ico, set.Icc, etc, and for some types even set.Iic etc. Calling fin_range n should search the context for bounds on n; prove n is in the appropriate interval; find the finite instance and extract a list; prove n is in that list; and call fin_cases on that proof as above.

I just tried this very quickly. (Not exactly this; writing it out has clarified things a bit.) It works, but simultaneously does too much and too little kernel reduction. (It's too slow, and numeral addition isn't reduced.)

[semorrison]

After a bit of a delay, I think I've finished this off, and would like a new review!

(I'm not quite sure what the best protocol is here: I was tempted to just make a new PR, so we don't get tangled up by the old discussion.)

[bryangingechen]

This looks great! I think it should be added to tactic.default. It looks like it imports too much for tactic.basic, but I'm not sure what the rules are.

[robertylewis]

What are the restrictions on the type of n?

[semorrison]

I've improved the documentation in both tactics.md and in the module doc-string, that hopefully explain exactly the restrictions.

[robertylewis]

I'm not exactly sure what you mean here. Is this saying that a single hypothesis n < 10 is okay for n : nat?

[semorrison]

Yes, that's the case. I've clarified this part of the documentation.

[semorrison]

@bryangingechen, I've added this to tactic.default, thanks for the suggestion.

[bryangingechen]

Was there anything else missing other than the doc changes @robertylewis requested? Let's get this merged!

[semorrison]

I don't have any plans to add anything at this point, so if people are happy it would be good to merge it.

[robertylewis]

Sorry, I've had too many threads going this week. I promise to give this a full review (and hopefully merge) by early next week at the latest.