typeclass inference from inside structures

Stream: general

[Vaibhav Karve]

I have the following MWE:

variable α : Type

structure mystruct (α : Type) :=
[dec_eq : decidable_eq α]
(f : α → α → Prop := sorry) -- suppose this is only well-defined if α has dec_eq

instance one   [decidable_eq α] : decidable_eq (α×α) := by apply_instance
instance two   (s : mystruct α) : decidable_eq (α×α) := by apply_instance -- error
instance three (s : mystruct α) : decidable_eq (α×α) :=
  @prod.decidable_eq α α s.dec_eq s.dec_eq

one and three work but two doesn't. I think this is because dec_eq is inside my struct and Lean's typeclass inference does not unfold it? Can I make two work "automatically"? Or do I need to change my structure definition?

[Vaibhav Karve]

I also tried writing

structure mystruct (α : Type) extends (decidable_eq α) :=
(f : α → α → Prop := sorry)

but that doesn't work because Lean complains that decidable_eq is not a structure, (even though I think it should be -- since it is a typeclass? :thinking: )

[Mario Carneiro]

it is a @[class] def, not a structure

[Mario Carneiro]

If you want to embed deicdable_eq, you can do it as in the MWE, if you add attribute [instance] mystruct.dec_eq

[Mario Carneiro]

actually this won't work unless mystruct is also a class

[Mario Carneiro]

If you want to keep mystruct as a structure, then you should probably take the dec_eq out of the structure and just have it as a separate typeclass argument to your theorems

[Vaibhav Karve]

Like this?

structure mystruct (α : Type) :=
(f [decidable_eq α] : α → α → Prop := sorry)

[Mario Carneiro]

like this

structure mystruct (α : Type) :=
(f : α → α → Prop := sorry)

[Mario Carneiro]

that := sorry is suspicious btw, I don't think that means what you think. You aren't supposed to be giving a definition at that position

[Vaibhav Karve]

Oh yeah, you are right about that, I should remove that sorry.

[Vaibhav Karve]

Mario Carneiro said:

it is a @[class] def, not a structure

Two followup questions from this:

• Why doesn't @[class] show up when I #print decidable_eq?
• Under what circumstances would I want to make @[class] defs of my own. I think I understand when I want @[class] structures, but not defs.

[Mario Carneiro]

Oh, actually decidable_eq isn't a class, it is a reducible def. The class is decidable

[Mario Carneiro]

a @[class] def is defeq to its definition. This is occasionally useful

[Mario Carneiro]

But I don't think it is unreasonable to default to using class instead

[Vaibhav Karve]

Okay. Thanks for answering all my questions.