Zulip Chat Archive

Stream: maths

Topic: Does `classical` break `interval_cases`?


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 09 2020 at 08:00):

#2367


Last updated: May 18 2021 at 07:19 UTC