## Stream: general

### Topic: structure vs. subtype

#### Sean Leather (Jul 04 2018 at 09:03):

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 (Jul 04 2018 at 09:04):

write the appropriate simp lemmas yourself :)

#### Sean Leather (Jul 04 2018 at 09:04):

Which simp lemmas?

#### Kenny Lau (Jul 04 2018 at 09:05):

oh, I thought you meant simp lemma by simple lemma

#### Sean Leather (Jul 04 2018 at 09:06):

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⟩⟩


#### Sean Leather (Jul 04 2018 at 09:07):

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

#### Sean Leather (Jul 04 2018 at 09:07):

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

#### Kenny Lau (Jul 04 2018 at 09:08):

then don't choose :P

#### Sean Leather (Jul 04 2018 at 09:10):

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

#### Sean Leather (Jul 04 2018 at 09:10):

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

write both

don't use choice

Why, Kenny?

#### Kenny Lau (Jul 04 2018 at 09:11):

choice is non-constructive

#### Sean Leather (Jul 04 2018 at 09:12):

It's a decidable choice.

#### Sean Leather (Jul 04 2018 at 09:13):

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

#### Sean Leather (Jul 04 2018 at 09:13):

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

never use choice

#### Kenny Lau (Jul 04 2018 at 09:15):

even when it's decidable

it's evil

#### Johan Commelin (Jul 04 2018 at 09:15):

Kenny, why did you choose to enroll at Imperial?

I didn't choose

it just happened

#### Johan Commelin (Jul 04 2018 at 09:16):

Just like you trolling this thread just happens

lol

#### Kevin Buzzard (Jul 04 2018 at 09:17):

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 (Jul 04 2018 at 09:19):

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 (Jul 04 2018 at 09:20):

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 (Jul 04 2018 at 09:20):

Kevin, yes, and then write a solid API.

#### Kevin Buzzard (Jul 04 2018 at 09:20):

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 (Jul 04 2018 at 09:21):

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 (Jul 04 2018 at 09:22):

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

#### Johan Commelin (Jul 04 2018 at 09:22):

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

#### Sean Leather (Jul 04 2018 at 09:22):

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 (Jul 04 2018 at 09:23):

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

#### Sean Leather (Jul 04 2018 at 09:24):

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

#### Sean Leather (Jul 09 2018 at 11:54):

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

Last updated: May 16 2021 at 05:21 UTC