Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: faster interval_cases


Kyle Miller (Feb 23 2022 at 04:13):

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 (Feb 23 2022 at 04:24):

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 (Feb 23 2022 at 04:28):

@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 (Feb 23 2022 at 08:10):

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

Mario Carneiro (Feb 23 2022 at 08:12):

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 (Feb 28 2022 at 17:53):

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


Last updated: Dec 20 2023 at 11:08 UTC