Auxiliary Typeclasses in Lean

Question

It's a common theme in Mathlib to use some auxiliary typeclass to define the one we actually want to use. For example, to define PseudoMetricSpace we use the typeclass Dist given by the following:

@[ext]
class Dist (α : Type _) where
  dist : α → α → ℝ

From what I understand this definition of Dist doesn't come with any of the properties we'd like to be associated with a pseudometric. We then let PseudoMetricSpace be an extension of Dist where dist has all the desired properties. My question is what was the point of starting with the typeclass Dist? I.e., couldn't we just include the definition of dist with type α → α → ℝ inside PseudoMetricSpace and take it along with any further extensions (say, to MetricSpace)?

My intuition is that it probably helps establish a nice base for anything that needs a dist function. Right or wrong, can you give an example of why this auxiliary Dist is necessary/appealing?

Answer 1

This is done so that formalization matches mathematical practice. Defining only PseudoMetricSpace directly with dist would correspond to the real-life situation where, as soon as you called a map “distance” everyone would jump in your face and demand that you do not utter another sentence until you prove it really has the required properties of a distance. You would not be allowed to say “let me just prove a lemma first”.

The phenomenon is more visible when a standard notion is associated with standard notation (which it is not for distance). For example, if you use the symbol $\leq$, most people will assume that it denotes (at least) a preorder, but will allow you to postpone the proof. This is precisely how mathlib treats the situation: it has the type class LE which is used to introduce the symbol ≤, and another type class Preorder which extends LE by the properties of a preorder.

More generally, formalized mathematics exposes all sorts of social conventions and makes them explicit. Of course, you can think of them as "clever engineering".