Match pattern refutations

Stream: lean4

[Ryan Lahfa]

Consider the following MWE:

structure S where
  n: ℤ

def m (s: S): ℤ := s.n

def test1 (s: S) := match (m s) with
  | 2 => 1
  | _ => 0

theorem test1_eq (s: S): s.n = 2 -> test1 s = 1 := by
  intro H
  simp [test1]
  match (m s) with
  | 2 => rfl
  | _ => sorry -- what to do here?

Is there a way in Lean 4 (or plans) to support something that enable a user to refute _in_ the fallthrough case, that is the value of the matched is not equal to any of the previous case?

Or is there a guideline on how to do this sort of reasoning on functions? I know that split can explode the match in multiple cases and add the correct hypothesis, but in my non-trivial example, I have more cases and split-ing this way is undesirable. by_cases would work only for 2 branches, not N branches, I would assume.

[František Silváši 🦉]

Many ways to skin this particular cat.
You can for example name the m s in the match:

...
  match h : m s with
  | 2 => rfl
  | x => simp [h.symm, m, *]

[Ryan Lahfa]

Oh, I didn't know we could name the hypothesis in match, awesome.

[Ryan Lahfa]

František Silváši 🦉 said:

Many ways to skin this particular cat.
You can for example name the m s in the match:

...
  match h : m s with
  | 2 => rfl
  | x => simp [h.symm, m, *]

Actually, this technique make use of the fact that you can reprove the conclusion in the fallthrough case, that's not always the case, especially if the proof in one of the branch can be particularly complicated, is there a way to obtain an hypothesis that the previous cases are neither of those? I can craft a more complicated MWE that prevent a user to use this sort of technique, I'd say.

[František Silváši 🦉]

(2242) #lean4 > ✔ unreachable match case - Lean - Zulip (zulipchat.com)

[Ryan Lahfa]

František Silváši 🦉 said:

(2242) #lean4 > ✔ unreachable match case - Lean - Zulip (zulipchat.com)

Awesome, thanks!

[František Silváši 🦉]

To add an extra 2 cents here - practically speaking, IME, split is usually the best way to do this _anyway_, and then manually cleaning up your proof state. Alternatively, rewrite with something first so that split splits in the manner you desire.

[Ryan Lahfa]

Yep, that makes sense.