Refinements as structures vs. subtypes

Stream: new members

[Will Crichton]

I found it interesting that Fin n is represented as a structure:

structure Fin (n : Nat) where
  val  : Nat
  isLt : val < n

And NNReal is represented as a quotient subtype:

def NNReal := { r : ℝ // 0 ≤ r }

When would one pick one or the other kind of representation? Is there a good reason that Fin is not a quotient subtype, or that NNReal is not a structure?

[Matt Diamond]

(I don't have an answer to your question but I would use the term "subtype" instead of "quotient")

[Matt Diamond]

(it's a good question though)

[Eric Wieser]

Fin used to be a subtype, but it was changed at some point; the git history hopefully holds the answer.

[Will Crichton]

Hmm I went back 8 years and could only find a structure-based definition of Fin, unless there was a different Fin definition (like the inductive Fin2).

[Eric Wieser]

It was changed in leanprover-community/lean3#761

[Eric Wieser]

Here's the discussion

[Jireh Loreaux]

One reason for this is that a lot of the instances for NNReal are derived from generic ones about the subtype of nonnegative elements in ordered rings, or variations thereof. In contrast, there is no such general framework that would apply to Fin.

Moreover, making NNReal a subtype gives automatic access to all the subtype API.