Limit @[simp] to arguments that reduce pattern matching

Stream: new members

[David Richter]

Hi, it seems to me that when I mark a recursive function as @[simp] it makes simp unfold when the arguments reduces the pattern matching, however, when I mark a non-recursive function as @[simp] it makes simp unfold the function always(?).

For example write:

@[simp] def foo: Bool ⊕ Bool → Nat
  | .inl a => if a then 1 else 2
  | .inr b => if b then 3 else 4

theorem test (h: x = y): foo x = foo y := by
  simp
  sorry

and observe that the proof goal is now

(match x with
  | Sum.inl a => if a = true then 1 else 2
  | Sum.inr b => if b = true then 3 else 4) =
  match y with
  | Sum.inl a => if a = true then 1 else 2
  | Sum.inr b => if b = true then 3 else 4

which is kinda long.

Is there an easy way to mark a definition to only simp away, when its arguments pattern match?

I found a reasonably short way by redefining the eq_n's with a simp attribute:

def foo: Bool ⊕ Bool → Nat
  | .inl a => if a then 1 else 2
  | .inr b => if b then 3 else 4
@[simp] def foo.eq_1' := @foo.eq_1
@[simp] def foo.eq_2' := @foo.eq_2

Now simp doesnt artificially unfold foo to make the goal longer, only after case analysis foo reduces:

theorem test (h: x = y): foo x = foo y := by
  try simp
  cases x
  simp
  cases x
  simp
  sorry

Yay!

But if there is a different way that is nicer that would be cool, for example something like this would be nice:

@[simp_eqs] def foo: Bool ⊕ Bool → Nat
  | .inl a => if a then 1 else 2
  | .inr b => if b then 3 else 4

Maybe such an annotation already exists, i just haven't found it? How do you handle simp annotations on non-recursive functions?

[David Richter]

I found a shorter workaround, avoiding the redefinition:

def foo: Bool ⊕ Bool → Nat
  | .inl a => if a then 1 else 2
  | .inr b => if b then 3 else 4
attribute [simp] foo.eq_1 foo.eq_2

But it still requires some typing sadly, let me know if there is something else I'm missing out on :)