4
$\begingroup$

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?

$\endgroup$

1 Answer 1

5
$\begingroup$

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".

$\endgroup$
4
  • 1
    $\begingroup$ It also seems that from a formalization point of view, sticking to this approach of having a hierarchy of structures consisting of many small steps of generalization and making definitions/theorems at the highest level of generality possible makes for more robust developments, because following it makes it easier to come back and change a hierarchy of structures after the fact. $\endgroup$ May 30, 2023 at 14:19
  • $\begingroup$ I see, so the point is that Dist claims the name dist and primes us for introducing a dist with all the right properties of a pseudometric? This allows us to separate the claim and the demonstration of its properties? $\endgroup$
    – Alex Byard
    May 30, 2023 at 15:13
  • $\begingroup$ @MevenLennon-Bertrand: Of course there will be additional benefits of good engineering. $\endgroup$ May 30, 2023 at 18:58
  • 1
    $\begingroup$ @AlexByard: precisely. $\endgroup$ May 30, 2023 at 18:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.