Doing case-by-case proofs about match statements in Lean4

Question

In Lean4, I am stuck in a proof with a goal like this:

⊢ (match
    match a :: b with
    | [] => []
    | [x] => [x]
    | x :: xs => x :: [delim] :: intersperse [delim] xs with
  | [] => []
  | a :: as => a ++ join as) =
  delim :: tail

Intuitively to me I would prove this by doing a case-by case analysis of the inner match statement. In other words, I would expect some tactic that would generate three subgoals:

1. Add a :: b = [] as an additional hypothesis, goal of

⊢ (match []
  | [] => []
  | a :: as => a ++ join as) =
  delim :: tail

2. Add a :: b = [x] as an additional hypothesis, goal of

⊢ (match [x]
  | [] => []
  | a :: as => a ++ join as) =
  delim :: tail

3. Add a :: b = x :: xs as an additional hypothesis$,^\dagger$ goal of

⊢ (match x :: [delim] :: intersperse [delim] xs
  | [] => []
  | a :: as => a ++ join as) =
  delim :: tail

Here's a list of some things I have tried to solve this.

1. The split tactic seems to split the outer match rather than the inner match, and it doesn't name any of the hypotheses, which makes it impossible to continue the proof. I can't seem to figure out any way to modify this behavior.
2. Using the cases tactic on the expression being matched: cases h₂: a::b with | nil => ... | cons a b | => .... This does successfully do a case split based on the value of the match expression, but it splits it into the nil and cons cases, rather than the three arms of the match.
3. I attempted to construct a toy problem to experiment with: theorem foo (a:α) (b:List α) (P: b ≠ []): (match a :: b with | [] => [] | [x] => [x] | x :: xs => c) = c. I thought that this theorem would require a case by case analysis, but it turns out simp just solved it! When I look at simp?'s output, it says Try this: simp only [split_match.match_1.eq_3], but the theorem split_match.match_1.eq_3 doesn't seem to actually exist if I try to use it:

invalid field notation, type is not of the form (C ...) where C is a constant
  split_match.match_1
has type
  (motive : List ?m.36429 → Sort ?u.36427) →
    (x : List ?m.36429) →
      (Unit → motive []) →
        ((x : ?m.36429) → motive [x]) → ((x : ?m.36429) → (xs : List ?m.36429) → motive (x :: xs)) → motive x

$\dagger$ I think this hypothesis could be even stronger because we know it didn't match the second case, but I'm not worried about that.

Answer 1

Note, this my not be the most optimal answer, but here is how I would approach this.

Also, note, it is important to provide a MWE when you ask questions like this so that the answerer can plug this into Lean themselves and make sure their answer works. I'm using your foo as my MWE.

All three of your approaches work for foo and you should be able to modify them for your original goal.

1. split. If you want to split by the match statement cases, then yes, I believe this is the way to go. (I'm not sure about splitting by just the inner match. There probably is a way, but the easiest is just to split on the outer match first and then split on the inner match.) You mentioned that the variables are not named. The trick to split (and cases and induction) is that you can name the hypotheses yourself like follows:

   theorem foo (a:α) (b:List α) (P: b ≠ []):
       (match a :: b with | [] => [] | [x] => [x] | x :: xs => c) = c := by
     split  -- split into three cases
     . case h_1 b' h => contradiction -- this case is impossible and obviously so
     . case h_2 b' a' h =>
       -- this case is impossible, but needs some work to show
       cases b -- split on if b is nil or not
       . case nil => contradiction
       . case cons a'' b'' =>
         apply absurd h  -- just need to show that h is false
         simp
     . case h_3 b' a' b'' h1 h2 => rfl  -- the goal is just c = c
   

   The name after each case just comes from what Lean names the goals. As for naming the variables, I just spam a bunch of variable names like a' b' c' ..., and then see what they become in the goal. I go back and clean it up, renaming them to useful names. If you don't need a variable, you can leave it out (if at the end of the list) or name it _.

   Also note that all but one of the three cases was impossible. So I just had to use the contradiction tactic to solve the subgoal. The second case was a bit more tricky, so I did cases on b to prove the hypotheses were inconsistent.

2. cases (or induction in some settings). I would actually recommend this. In this example, and your original use case, most of the match cases can't be reached. It is therefore easier to reason about the objects you are putting into match than the cases of match. For example:

   theorem foo1 (a:α) (b:List α) (P: b ≠ []):
       (match a :: b with | [] => [] | [x] => [x] | x :: xs => c) = c := by
     cases b
     . case nil => contradiction
     . case cons a' b' => rfl
   

   Notice, this proof is much shorter. Also, notice I'm doing cases/induction on b and not a :: b.

3. simp When simp works it is great. Note that in Lean 4, simp will automatically generate lemmas like the ones you saw, which is why they are not visible to you when you don't use simp. It is different in Lean 3 where the lemmas are generated automatically whether you call simp or not, and I saw some discussion of making it possible to add an option have these automatically generated from the start in Lean 4.