How to access typeclass values?

Stream: new members

[Nicholas Dyson]

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]

You want ∀ (t : Type) [inhabited t], inhabited.default t = inhabited.default t

[Mario Carneiro]

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]

class inhabited' (α : Type _) :=
(default [] : α)

example (α) [inhabited' α] : inhabited'.default α = inhabited'.default α := rfl

[Mario Carneiro]

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]

Thank you this was very helpful.