fin_cases on Finset.Ioc

Stream: general

[shortc1rcuit]

For part of a proof I need to show that given x : Equiv.Perm (Fin (k + 1)) and x 0 ∈ Finset.Iic 1 then x 0 = 0 ∨ x 0 = 1. This should be doable with the fin_cases tactic but for some reason this fails with a nasty error. Is there a way to get this to work/a different way to prove this?

import Mathlib.Logic.Equiv.Defs
import Mathlib.Order.Interval.Finset.Fin
import Mathlib.Tactic

example (x : Equiv.Perm (Fin (k + 1))) (hx : x 0 ∈ Finset.Iic 1) : x 0 = 0 ∨ x 0 = 1 := by
  fin_cases hx
  /-tactic 'cases' failed, nested error:
  dependent elimination failed, failed to solve equation
    List.map (⇑Fin.orderIsoSubtype.symm.toEmbedding)
      (List.map (⇑{ toFun := fun x => ⟨↑x, ⋯⟩, inj' := ⋯ })
        (List.pmap Subtype.mk
          (List.filter (fun b => decide ((fun i => i < k + 1) b))
            (List.range' (↑(Fin.orderIsoSubtype 0)) (↑(Fin.orderIsoSubtype 1) + 1 - ↑(Fin.orderIsoSubtype 0))))
          ⋯)) =
    x 0 :: as✝
  at case List.Mem.head-/
  sorry

[Yury G. Kudryashov]

I guess it tries to substitute and fails

[shortc1rcuit]

I guess? But I'm not sure how else I can show this.

[Kevin Buzzard]

Slightly simpler example:

import Mathlib.Tactic

example (k : ℕ) (x : Fin (k + 1)) (hx : x ∈ Finset.Iic 1) : True := by
  fin_cases hx -- same incomprehensible error

[Daniel Weber]

import Mathlib.Tactic

variable (k : ℕ)

example (x : Finset.Iic (1 : Fin (k + 1))) : True := by
  fin_cases x

also fails.

[Kevin Buzzard]

Aah -- the definition of 1 depends (in some sense) on whether k = 0 or k > 0. Bumping up k to remove this ambiguity results in an even cooler error :-)

import Mathlib.Tactic

example (k : ℕ) (x : Fin (k + 2)) (hx : x ∈ Finset.Iic 1) : True := by
  fin_cases hx
/-
(kernel) declaration has metavariables '_example'
-/

I think this means that the thing-that-happens-before-the-kernel thinks the proof is done; if you add sorry then you get the error saying that there are no goals to be solved. I don't know if the two errors are related or different.

[Daniel Weber]

import Mathlib.Tactic

variable (k : ℕ)

example (x : Finset.Iic (1 : Fin (k + 2))) : True := by
  fin_cases x

also produces this error, as does

import Mathlib.Tactic

variable (k : ℕ)

example (x : Finset.Iic (1 : Fin (k + 1))) : True := by
  cases k; trivial
  fin_cases x

[shortc1rcuit]

Ok I've found a workaround for this

lemma foo (x : Fin (k + 2)) (hx : x ≤ 1) : x = 0 ∨ x = 1 := by
  obtain hx | rfl := le_iff_lt_or_eq.mp hx
  · left; rwa [←Fin.val_eq_val, Fin.val_zero, ←Nat.lt_one_iff, ←Fin.val_one, ←Fin.lt_iff_val_lt_val]
  · right; rfl

[Yury G. Kudryashov]

Could you please file a bug at GitHub? While you have a workaround for your case, we should fix the issue some day.

[shortc1rcuit]

I'll also note that this doesn't fail

import Mathlib.Tactic

example (k : ℕ) (x : Fin (k + 3)) (hx : x ∈ Finset.Icc 0 1) : True := by
  fin_cases hx
  sorry
  sorry

However, I feel it should also work with k + 2

[Kevin Buzzard]

So with k+3 there is no errors, with k+2 there is a very obscure error and with k+1 there is a different very obscure error. Nice! Maybe open an issue against the mathlib4 github repo?

[shortc1rcuit]

With k + 1 it makes sense since when k = 0, we're dealing with Fin 1, where 0 is the only element, but when k > 1, 0 and 1 are distinct. Thus the number of cases isn't fixed, which I'm guessing is why fin_cases fails there.

[shortc1rcuit]

I'm opening an issue on github and I'll link it back to here.

[shortc1rcuit]

Created