How to propagate `@[simp, reducible]` through instances?

Stream: general

[Andrej Bauer]

Why does Lean 4 ignore @[simp, reducible] in this case?

inductive Cow (α : Type) : Type
 | tail : Cow α
 | horn : α → Cow α

@[simp, reducible]
def Cow.le {α : Type} [LE α]: Cow α → Cow α → Prop :=
  fun x y =>
    match x with
    | .tail => true
    | .horn a =>
      match y with
      | .tail => false
      | .horn b => a ≤ b

instance CowLT (α : Type) [LE α] : LE (Cow α) where
  le := Cow.le

lemma Cow.moo (α : Type) [LE α] (x y : α) :
  horn x ≤ horn y → x ≤ y := by simp -- this does not work

If I replace horn x ≤ horn y in the lemma with Cow.le then by simp works.

[Eric Wieser]

You presumably need to mark CowLT [sic] reducible too

[Andrej Bauer]

Ah yes, that works. But what if the instance had many fields, can I annotate only some of them?

[Eric Wieser]

What's the motivation for making it reducible?

[Andrej Bauer]

I suspect I don't understand when reducible should be used.

[Eric Wieser]

I'm not sure many people do; it's use pretty sparingly and somewhat arbitrarily in mathlib

[Eric Wieser]

Most of the time it's only used to alias a function or type with another name

[Eric Wieser]

I don't know if there are any places where it is used on instances.

[Eric Wieser]

Incidentally, your Cow looks like docs4#WithBot

[Andrej Bauer]

Yes, I know, I wanted a self-contained example. It's more polite that way.

[Eric Wieser]

Andrej Bauer said:

Ah yes, that works. But what if the instance had many fields, can I annotate only some of them?

You can mark the instance as reducible and make all but some of the fields defined in terms of a not-reducible implementation

[Kyle Miller]

One thing you can do is put @[simp] on the instance (no need for reducible anywhere), though it's not clear to me whether this is the correct design.

import Std.Logic

inductive Cow (α : Type) : Type
 | tail : Cow α
 | horn : α → Cow α

@[simp]
def Cow.le {α : Type} [LE α]: Cow α → Cow α → Prop :=
  fun x y =>
    match x with
    | .tail => true
    | .horn a =>
      match y with
      | .tail => false
      | .horn b => a ≤ b

@[simp]
instance CowLT (α : Type) [LE α] : LE (Cow α) where
  le := Cow.le

theorem Cow.moo (α : Type) [LE α] (x y : α) :
  horn x ≤ horn y → x ≤ y := by simp

[Kyle Miller]

A problem with this is that simp will always turn LE for Cow into Cow.le, which isn't great. Another solution, which isn't great but at least limits the scope, is to not use @[simp] and instead give simp the definitions manually.

theorem Cow.moo (α : Type) [LE α] (x y : α) :
  horn x ≤ horn y → x ≤ y := by simp [LE.le, Cow.le]