faster interval_cases

Stream: metaprogramming / tactics

[Kyle Miller]

I spent some time today making a faster interval_cases (draft at #12237). It focuses on just ℕ, ℤ, and ℕ+.

Some examples:

-- takes about 6 seconds
example (n : ℕ) (h : 3 ≤ n ∧ n ≤ 40) : (22^n + 8) % 24 = 0 :=
begin
  interval_cases' n; norm_num,
end

-- can make use of additional hypotheses, including conjunctions of inequalities
example (n : ℕ) (h : n ∈ set.Ico 1 4) : n * n < 16 :=
begin
  interval_cases' n using [set.mem_Ico.mp h]; norm_num
end

-- can merge hypotheses
example (n : ℕ) (h1 : 5 < n) (h2 : 10 < n) (h3 : n ≤ 20) (h4 : n < 11) : n = 11 :=
by interval_cases' n

-- can operate on expressions in addition to variables
example (n : ℕ) (f : ℕ → ℤ) (w₁ : f n > -2) (w₂ : f n < 2) : f n ∈ ({-1, 0, 1} : set ℤ) :=
begin
  interval_cases' f n with h; simp [h],
end

-- substitutes variables everywhere like before
lemma mod8_odd' (b : ℤ) (hlo : 0 ≤ b) (hhi : b < 8) (hodd : odd b) :
  b = 1 ∨ b = 3 ∨ b = 5 ∨ b = 7 :=
begin
  rw int.odd_iff at hodd,
  interval_cases' b; norm_num at hodd; norm_num,
end

[Kyle Miller]

I'm not sure I've implemented things involving proof construction or goal management correctly. (And I'm sure there are better ways to go about it.)

The mk_prop function builds up a proof of the disjunction n = 4 \/ n = 5 \/ ... \/ n = 10 \/ false given bounds 4 <= n and n < 11, using a lot of norm_num to tie things together.

Then, this is split up using a tactic I made called cases_subst. I built it out of the first tactics I could figure out how to string together:

meta def cases_subst : expr → tactic unit
| e := do
  t ← infer_type e,
  match t with
  | `(false) := do h ← to_expr ``(false.elim %%e),
                   tactic.exact h
  | `(_ ∨ _) :=
    focus1 (do [(_, [a]), (_, [b])] ← tactic.cases e,
               focus' [try_core (subst a) >> pure (), cases_subst b])
  | _ := try_core (subst e) >> pure ()
  end

[Kyle Miller]

@Scott Morrison Do you have any thoughts about speeding interval_cases up like this? Are there any other types interval_cases has been used on in practice? (I've neglected fin n, but I wonder whether it make sense to instead do interval_cases on the underlying nat.)

[Eric Rodriguez]

@Mario Carneiro was talking about this a couple days ago, maybe he has some ideas

[Mario Carneiro]

I was not really sure what to do about fin n. It's possible to have the tactic produce fin numerals, but it seems like that is unlikely to be what the user wants because of all the modulo inside

[Kyle Miller]

Any thoughts on whether I should pursue this version of interval_cases further? (Maybe I should update the PR to replace interval_cases rather than having a parallel interval_cases' and check that it works as a drop-in replacement?)