# Zulip Chat Archive

## Stream: maths

### Topic: Does `classical` break `interval_cases`?

#### Kevin Buzzard (Apr 08 2020 at 20:20):

import tactic example (n : ℕ) (hn : n ≤ 4) : false := begin classical, interval_cases n, repeat {sorry} end /- cases tactic failed, it is not applicable to the given hypothesis state: n : ℕ, hn : n ≤ 4, _inst : Π (a : Prop), decidable a, lh : n ∈ tactic.interval_cases.set_elems (set.Ico ⊥ (4 + 1)) ⊢ false -/

If you comment out `classical`

it works fine.

#### Kevin Buzzard (Apr 08 2020 at 20:49):

Another `interval_cases`

issue:

import tactic group_theory.order_of_element example (G : Type) [fintype G] [group G] [decidable_eq G] (g : G) (h : order_of g ≤ 2) : false := begin interval_cases (order_of g), repeat {sorry} end

You would expect to get three cases `order_of g = 0,1,2`

. But I think `simp`

or something got to the middle case:

3 goals G : Type, _inst_1 : fintype G, _inst_2 : group G, _inst_3 : decidable_eq G, g : G, h : order_of g ≤ 2, lh : order_of g = 0 ⊢ false G : Type, _inst_1 : fintype G, _inst_2 : group G, _inst_3 : decidable_eq G, h : order_of 1 ≤ 2 ⊢ false G : Type, _inst_1 : fintype G, _inst_2 : group G, _inst_3 : decidable_eq G, g : G, h : order_of g ≤ 2, lh : order_of g = 2 ⊢ false

Lean has eliminated the hypothesis that the order of g is 1, and replaced g with the identity. Which is fine, I guess, but perhaps not what I expected.

#### Scott Morrison (Apr 09 2020 at 01:57):

This is probably my fault in some way. :-) I'm not sure I'll have time to look at it today. If no one else jumps in, creating and assigning an issue to me would be great. `interval_cases`

is built on top of `fin_cases`

, and both are pretty simple tactics (which can be "decompiled" by hand into a string of other tactic invocations), so it's probably not too hard to find where we're over simplifying.

#### Kevin Buzzard (Apr 09 2020 at 08:00):

Last updated: May 18 2021 at 07:19 UTC