Stream: new members
Nicholas Dyson (Dec 04 2020 at 14:47):
I'm just learning how to use typeclasses in Lean, and the documentation seems sparse. Specifically, how do I refer to elements from the typeclass definition when proving results about all types that are a member of a typeclass?
As a simple example, suppose I have the default "inhabited" class:
class inhabited (α : Type _) := (default : α)
And suppose I want to define and prove the utterly trivial result that for any type that is a member of the "inhabited" class, the default element is equal to itself. I have no idea what the syntax for this would be. In an informal syntax (because if I knew how to express these concepts in Lean syntax, I wouldn't be asking this question), what I'm aiming for is expressing something like:
(∀ t : Type) [(inhabited t) -> (t.default = t.default)]
if that makes sense. So what I need is to
- declare a lemma over an arbitrary type t so long as that type is a member of a given typeclass, and then
- access the values of type t that the typeclass definition tells us exist.
Hope that makes sense, I'm finding this a challenging concept to explain. Thank you very much for any advice.
Mario Carneiro (Dec 04 2020 at 14:52):
∀ (t : Type) [inhabited t], inhabited.default t = inhabited.default t
Mario Carneiro (Dec 04 2020 at 14:54):
except that won't work directly because of typeclass caching, so you have to insert a
by exactI to make typeclass inference work:
∀ (t : Type) [inhabited t], by exactI inhabited.default t = inhabited.default t
Mario Carneiro (Dec 04 2020 at 14:57):
class inhabited' (α : Type _) := (default  : α) example (α) [inhabited' α] : inhabited'.default α = inhabited'.default α := rfl
Mario Carneiro (Dec 04 2020 at 14:58):
I had to put
 in in order to make the alpha explicit in
default; the alternative would be
class inhabited' (α : Type _) := (default : α) example (α) [inhabited' α] : (inhabited'.default : α) = inhabited'.default := rfl
Nicholas Dyson (Dec 04 2020 at 16:45):
Thank you this was very helpful.
Last updated: May 14 2021 at 04:22 UTC