## 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):

#2367

Last updated: May 18 2021 at 07:19 UTC