Case splitting inside an argument to an instance method

Stream: lean4

[cmlsharp]

Suppose I have functions with the following structure

def increment? (i : Fin sz) : Option (Fin sz) :=
  if h : i < sz - 1
    then some (⟨i + 1, by omega⟩)
    else none

def iterate (a : Vector α sz) (i : Fin sz) : Vector α sz :=
  match h : increment? i with
  | none => a
  | some j =>
    have : i < j := by grind [increment?]
    iterate a j
termination_by sz - i

and suppose I want to prove a claim like

example  {a : Vector α sz} {h : 0 < sz }: (iterate a ⟨0, h⟩)[0] = a[0]

(obviously in this simplistic case I could just prove that iterate a i = a and this follows, but lets assume thats not the case in general and the arms of this match are more complicated)

What I'd like to be able to do is unfold iterate and then split. And indeed if the claim were something like

opaque g (a : α) : α := a
example  {a : Vector α sz} {h : 0 < sz }: g (iterate a ⟨0, h⟩)  = g a

I'd be able to do that. But as it stands, I get the following error:

▼ 39:5-39:10: error:
Tactic `split` failed: Could not split an `if` or `match` expression in the goal

α : Type u_1
sz : Nat
a : Vector α sz
h : 0 < sz
⊢ (match h_1 : increment? ⟨0, h⟩ with
    | none => a
    | some j =>
      have this := ⋯;
      iterate a j)[0] =
  a[0]

▼ 39:5-39:10: information:
[split.failure] `split` tactic failed to generalize discriminant(s) at
      match h_1 : increment? ⟨0, h⟩ with
      | none => a
      | some j =>
        have this := ⋯;
        iterate a j
    resulting expression was not type correct
    possible solution: generalize discriminant(s) manually before using `split`

I tried various permutations of generalize but I have not been able to find a version that works.

This is not specific to getElem it seems to occur for any type class instance method, but not for plain defs as mentioned above.

I can get what I want with a bit of conv hackery, but surely there must be a better way.

    cases hincr : increment? ⟨0, h⟩
    all_goals
      unfold iterate
      simp only -- gets rid of the 'have this : i < j' line
      conv => lhs; arg 1; rw [hincr]; simp only

Note that while the dependent match makes things more difficult, even

def someTest (a : α) : Option α := none
def f (a : Array α) : Array α :=
  match someTest a with
  | none => a
  | some _ => a ++ a

example {a : Array Nat} {h_nempty : 0 < a.size }
  : (f a)[0] = a[0]
  := by
    unfold f
    split

is sufficient to defeat split, though conv is not required to work around it. This works:

    cases h : (someTest a)
    all_goals
      unfold f
      simp only [h]

I have 2 questions:
(1) What is actually going wrong here and why does split only seem to fail when the match is an argument to an typeclass method?
(2) Is there a better way to do what I'm trying to do here (either in the dependent-match or non-dependent-match) case?

[Aaron Liu]

cmlsharp said:

(1) What is actually going wrong here and why does split only seem to fail when the match is an argument to an typeclass method?

It's probably not that there's a typeclass method, but the something with the match is dependent

[Aaron Liu]

if you have a #mwe I can show you my solution

[cmlsharp]

It's probably not that there's a typeclass method, but the something with the match is dependent

I think you're right, I thought I had a simpler example where this also occurred with ToString, but I can't replicate it now.

here are the examples above in the playground.

[Aaron Liu]

if you're okay with importing mathlib I wrote a tactic for forcing rewrites in dependent positions

import Mathlib.Tactic.DepRewrite

-- EXAMPLE 1
def someTest (a : α) : Option α := none

def f (a : Array α) : Array α :=
  match someTest a with
  | none => a
  | some _ => a ++ a

example {a : Array Nat} {h_nempty : 0 < a.size }
  : (f a)[0] = a[0]
  := by
    unfold f
    obtain ⟨x, hx⟩ : ∃ x, someTest a = x := ⟨_, rfl⟩
    rw! [hx]
    split
    · sorry
    · sorry


-- EXAMPLE 2
def increment? (i : Fin sz) : Option (Fin sz) :=
  if h : i < sz - 1
    then some (⟨i + 1, by omega⟩)
    else none

def iterate (a : Vector α sz) (i : Fin sz) : Vector α sz :=
  match h : increment? i with
  | none => a
  | some j =>
    have : i < j := by grind [increment?]
    iterate a j
termination_by sz - i

example  {a : Vector α sz} {h : 0 < sz }: (iterate a ⟨0, h⟩)[0] = a[0]
  := by
    unfold iterate
    obtain ⟨x, hx⟩ : ∃ x, increment? ⟨0, h⟩ = x := ⟨_, rfl⟩
    rw! [hx]
    split
    · sorry
    · sorry

[cmlsharp]

wow thank you! that's awesome. Unfortunately, this came up in the context of a PR to Batteries, so a Mathlib dependency is probably out of the cards, but this seems really useful. I'll keep it in mind for the future!

[cmlsharp]

(in fact, is this something that could be extracted out into batteries?)

[Jakub Nowak]

Not only batteries, I hope this will be part of core's, and not only for rw but also for e.g. cases or the mentioned split.