Zulip Chat Archive

Stream: general

Topic: typeclass inference from inside structures


view this post on Zulip Vaibhav Karve (Mar 22 2020 at 18:51):

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?

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 18:55):

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: )

view this post on Zulip Mario Carneiro (Mar 22 2020 at 18:57):

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 18:58):

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 18:59):

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 19:01):

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

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 19:04):

Like this?

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 19:04):

like this

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 19:05):

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

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 19:09):

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

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 19:12):

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.

view this post on Zulip Mario Carneiro (Mar 22 2020 at 19:14):

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 19:16):

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

view this post on Zulip Mario Carneiro (Mar 22 2020 at 19:17):

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

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 19:24):

Okay. Thanks for answering all my questions.


Last updated: May 09 2021 at 19:11 UTC