Definitional equality with patterns

Stream: lean4

[Henrik Böving]

I've got this piece of code:

namespace Test
  inductive Maybe (α : Type u) where
  | none : Maybe α
  | some : α → Maybe α
    deriving Repr

  namespace Maybe
    def apply {α β : Type u} : Maybe (α → β) → Maybe α → Maybe β
    | (some f), (some a) => (some (f a))
    | _, _ => none

    theorem none_apply {x : Maybe α} : apply none x = @none β := by rfl
    theorem apply_none {α β : Type u} {f : Maybe (α → β)} : apply f none = none := by rfl
  end Maybe
end Test

I would expect both theorems to be solved with just rfl but only the first one does, the second fail to be solved by rfl and requires induction/cases to solve. And I'm wondering whether this is a bug? After all there is only one pattern in the function that would allow the result to be some and in none_apply rfl correctly detects this but in apply_none it fails to.

[Scott Morrison]

The patterns you write don't always correspond to the definition Lean compiles them down to. Here it's going to do a case split on the first argument to start, and hence in apply_none rfl can't see what is happening.

[Scott Morrison]

if you #print apply.match_1 you'll get

def Test.Maybe.apply.match_1.{u_1, u_2} : {α β : Type u_1} →
  (motive : Maybe (α → β) → Maybe α → Sort u_2) →
    (x : Maybe (α → β)) →
      (x_1 : Maybe α) →
        ((f : α → β) → (a : α) → motive (some f) (some a)) →
          ((x : Maybe (α → β)) → (x_2 : Maybe α) → motive x x_2) → motive x x_1 :=
fun {α β} motive x x_1 h_1 h_2 =>
  Maybe.casesOn x (h_2 none x_1) fun a => Maybe.casesOn x_1 (h_2 (some a) none) fun a_1 => h_1 a a_1

[Scott Morrison]

(To guess to look at apply.match_1, if you have a copy of Mathlib4 you can import Mathlib.Tactic.PrintPrefix and then use #print prefix apply to see that automatically generated auxiliary definitions.)

[Reid Barton]

I'm pretty sure you can't make them both definitional equalities, regardless of how you defined apply (other than apply f x = none of course)