Inferring typeclass instances for structure member types

Stream: new members

[jay kruer]

Hello Leanlip! (Zulean?)

I'm a recovering Coq user beginning to work with Lean. I see that there are many topics about instance resolution failure, but flipping through them I don't see any topics covering the general issue I have.

I've defined the following structure for Mealy machines along with a trivial example machine.

structure mealy :=
mk :: (state: Type)
      (ι : Type) -- input alphabet \iota
      (ω : Type) -- output alphabet \omega
      (tr : state × ι -> state × ω)
      (init : state)

-- an example mealy machine
def M : mealy := mealy.mk ℕ ℕ ℕ (λ p, let σ := p.1 in
                                       let i := p.2 in
                                       (p.1+p.2, p.1+p.2)) 0

That is great, but when I try to say anything about M, I run into problems. Stating the following theorem results in instance resolution failures for has_lt M.state, has_zero M.state, and has_one M.ι, but M.state and M.ι are both nat, so I'm a bit at a loss. One thing I've tried is opening mealy before stating this theorem, which didn't help.

theorem silly :  (M.tr (M.init, 1)).1 > 0

[Adam Topaz]

lean doesn't unfold defs so eagerly. But you can add the necessary instances as follows:

instance : semiring M.ι :=
nat.semiring

instance : semiring M.state :=
nat.semiring

instance : has_lt M.state :=
nat.has_lt

theorem silly :  (M.tr (M.init, 1)).1 > 0 := sorry

[Adam Topaz]

alternatively, change def to abbreviation in the definition of M.

[Adam Topaz]

That essentially has the effect of making the definition reducible, so typeclass resolution can see through the definition.

[Jireh Loreaux]

Or make state, ι and ω parameters in the definition.

[Adam Topaz]

Yeah, that would be a good approach as well.

[Jireh Loreaux]

Which, IMHO, makes the most sense (because then you won't have to write these instances every time, or deal with some of the potential headaches of reducible seeing through "too much"). But I don't know much about mealy machines.

[Jireh Loreaux]

I guess it primarily depends on whether you ever want non-standard type classes on these types than the ones with which they naturally come equipped.

[Reid Barton]

ι and ω should probably be parameters of the type anyways, because what good is a machine if you don't know what you can connect it to? But for state there could be very good reasons to keep it as a field, that are more important than being able to evaluate toy examples without writing auxiliary instances.