structure vs. subtype

Stream: general

[Sean Leather]

I was wondering why one would choose a structure over a subtype (or vice versa) for finset or any similar construction. It seems like the two are equivalent, but I might be missing something. I don't see an advantage for using a structure. Using a subtype gives you a few existing simple lemmas that you wouldn't have to write, but that's the only advantage I see, and it's relatively minor.

[Kenny Lau]

write the appropriate simp lemmas yourself :)

[Sean Leather]

Which simp lemmas?

[Kenny Lau]

oh, I thought you meant simp lemma by simple lemma

[Sean Leather]

No, I meant init/data/subtype/basic.lean, which is all the support I've found for subtype:

import init.logic
open decidable

universes u

namespace subtype

def exists_of_subtype {α : Type u} {p : α → Prop} : { x // p x } → ∃ x, p x
| ⟨a, h⟩ := ⟨a, h⟩

variables {α : Type u} {p : α → Prop}

lemma tag_irrelevant {a : α} (h1 h2 : p a) : mk a h1 = mk a h2 :=
rfl

protected lemma eq : ∀ {a1 a2 : {x // p x}}, val a1 = val a2 → a1 = a2
| ⟨x, h1⟩ ⟨.(x), h2⟩ rfl := rfl

@[simp] lemma eta (a : {x // p x}) (h : p (val a)) : mk (val a) h = a :=
subtype.eq rfl

end subtype

open subtype

instance {α : Type u} {p : α → Prop} {a : α} (h : p a) : inhabited {x // p x} :=
⟨⟨a, h⟩⟩

[Kenny Lau]

erase "simp" from my advice

[Sean Leather]

Sure, you could write these yourself, which is why I said the advantage is relatively minor.

[Sean Leather]

So, given that, I'm wondering why choose one or the other.

[Kenny Lau]

then don't choose :P

[Sean Leather]

Oh, there are at least a couple other options, of course, depending on what you want: exists and (p)sigma.

[Sean Leather]

But, still, you have to make choice, assuming you want to do something and not nothing. :stuck_out_tongue_winking_eye:

[Kenny Lau]

write both

[Kenny Lau]

don't use choice

[Sean Leather]

Why, Kenny?

[Kenny Lau]

choice is non-constructive

[Sean Leather]

It's a decidable choice.

[Sean Leather]

Note that I'm talking about constructing something. :simple_smile:

[Sean Leather]

I was wondering why one would choose a structure over a subtype (or vice versa) for finset or any similar construction.

[Kenny Lau]

never use choice

[Kenny Lau]

even when it's decidable

[Kenny Lau]

it's evil

[Johan Commelin]

Kenny, why did you choose to enroll at Imperial?

[Kenny Lau]

I didn't choose

[Kenny Lau]

it just happened

[Johan Commelin]

Just like you trolling this thread just happens

[Kenny Lau]

lol

[Kevin Buzzard]

In CS they choose things all the time -- even to the point of breaking symmetry. For example they chose lt to be the important one and define gt through it. Here it doesn't matter which one to choose, but they had to choose one.

[Kevin Buzzard]

For making more complex structures, it is dawning on me more and more that you do have to make a design decision -- what the "fundamental" way of doing it is -- and then you build other things on top. But I guess you only prove the lemmas for one implementation and then deduce for the others.

[Johan Commelin]

Kenny, I suggest that it just happens that you read the following article in the Journal of the American Philosophical Association: https://www.cambridge.org/core/journals/journal-of-the-american-philosophical-association/article/aristotle-on-trolling/540BB557C82186C33BFFB61E35A0B5B6

[Johan Commelin]

Kevin, yes, and then write a solid API.

[Kevin Buzzard]

So the question is that in any specific case, e.g. fintype, topological spaces, valuations, whatever -- which construction do you make "fundamental"? And this seems to me to be a very delicate question.

[Johan Commelin]

I am currently trying to grasp the math-API to mixed Hodge modules. There really is a lot of API there. A huge black box behind it, but a solid API.

[Johan Commelin]

Kevin, if the API is good, the question becomes a bit less delicate, I hope.

[Johan Commelin]

But lots of parts in mathlib are lacking good API's. (And I myself am very bad at writing good API's.)

[Sean Leather]

So the question is that in any specific case, e.g. fintype, topological spaces, valuations, whatever -- which construction do you make "fundamental"? And this seems to me to be a very delicate question.

For my question, I can only see a slight practical advantage to choosing subtype over structure. I was wondering if there was anything deeper.

[Sean Leather]

By the way, this :arrow_up: is me trying to stay on the topic of the thread. :wink:

[Sean Leather]

Though I'm happy to see other threads branch off on related topics.

[Sean Leather]

The results of my finset structure → subtype experiment: https://github.com/leanprover/mathlib/pull/183