applying theorem statements that contain "match"

Stream: new members

[Paul Nelson]

I'm curious whether there's a direct way to resolve the type mismatch in the first example below. The error message is not helpful, because the "expected" and "found" types are identical (or at least have identical textual descriptions).

A practical workaround is to absorb the match statement into a definition, like in the second example, which makes me wonder whether it's an anti-pattern to use "match" in theorem statements in the first place. Is that the case?

import Mathlib

theorem thm1
  (I : Type)
  (i : I ⊕ I)
  :
  0 = match i with
      | Sum.inl _ => 0
      | Sum.inr _ => 0
  := by sorry

example
  (n : ℕ)
  (i : Fin n ⊕ Fin n)
  :
  0 = match i with
      | Sum.inl _ => 0
      | Sum.inr _ => 0
  := by
  exact thm1 (Fin n) i -- type mismatch
  sorry

def fn (I : Type) : I ⊕ I → ℕ
  | Sum.inl _ => 0
  | Sum.inr _ => 0

theorem thm2
  (I : Type)
  (i : I ⊕ I)
  :
  0 = fn I i
  := by sorry

example
  (n : ℕ)
  (i : Fin n ⊕ Fin n)
  :
  0 = fn (Fin n) i
  := by
  exact thm2 (Fin n) i

[Paul Nelson]

I guess one can work around this using rw, at least when the match statement appears on at most one side of the equation:

  rw [thm1 (Fin n) i]
  induction' i with i
  case inl => rfl
  case inr => rfl

But it'd be convenient to be able to apply the theorem directly in more complicated settings

[Joachim Breitner]

The problem is that for both match statements, the laborator creates a custom match function (thm1.match_1 and _example.match_1), and they are not definitionaly equal (at least not at normal reduction setting):

import Mathlib

theorem thm1
  (I : Type)
  (i : I ⊕ I)
  :
  0 = match i with
      | Sum.inl _ => 0
      | Sum.inr _ => 0
  := by sorry



set_option pp.match false
theorem test
  (n : ℕ)
  (i : Fin n ⊕ Fin n)
  :
  0 = match i with
      | Sum.inl _ => 0
      | Sum.inr _ => 0
  := by
  -- exact thm1 (Fin n) i -- type mismatch
  sorry

example : (fun n => thm1.match_1 (I := Fin n)) = @test.match_1 := by
  -- rfl fails
  ext n
  -- rfl fails
  unfold thm1.match_1
  unfold test.match_1
  rfl

[Joachim Breitner]

But the take away is that, yes, probably an anti-pattern to have such match statements and hope they will be equal to others.