Equation lemmas are longer generated by a simple match

[eric-wieser]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Compare this Lean 3 code

@[simp]
def foo : ℕ → ℕ
| a := 2 * a

example : foo = λ a, a + a :=
begin
  success_if_fail { simp },  -- only `foo x` is matched by the equation lemma
  funext,
  simp, -- now matches
  sorry
end

vs the same code in Lean 4

@[simp]
def foo : Nat → Nat
| a => 2 * a

example : foo = fun a => a + a :=
by
  simp -- unfolds foo into a lambda
  sorry

The Lean3 behavior was very useful in mathlib; for instance, in the definition of

/-- The transpose of a matrix. -/
def transpose (M : matrix m n α) : matrix n m α
| x y := M y x

it means that simp [transpose] only simplifies terms of the form transpose M i j and not transpose M.

Steps to Reproduce

1. Run the code above in Lean 3 and Lean 4
2. Observe the behavior difference

Expected behavior: Lean 4 behaves like Lean 3 and generates an equation lemma foo a = 2 * a

Actual behavior: Lean 4 generates an equation lemma foo = fun a => 2 * a

Reproduces how often: 100%

Versions

Lean 4.0.0-nightly-2023-01-16

Additional Information

Zulip thread, and an older Zulip message

[eric-wieser]

It seems that match statements are a distraction here, as

@[simp]
def foo (a : Nat) : Nat := 2 * a

results in simp unfolding unapplied foo to fun a => 2 * a just as it did above.