Zulip Chat Archive

Stream: general

Topic: structure vs. subtype


view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:04):

write the appropriate simp lemmas yourself :)

view this post on Zulip Sean Leather (Jul 04 2018 at 09:04):

Which simp lemmas?

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:05):

oh, I thought you meant simp lemma by simple lemma

view this post on Zulip 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⟩⟩

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:06):

erase "simp" from my advice

view this post on Zulip Sean Leather (Jul 04 2018 at 09:07):

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

view this post on Zulip Sean Leather (Jul 04 2018 at 09:07):

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

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:08):

then don't choose :P

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:10):

write both

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:10):

don't use choice

view this post on Zulip Sean Leather (Jul 04 2018 at 09:11):

Why, Kenny?

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:11):

choice is non-constructive

view this post on Zulip Sean Leather (Jul 04 2018 at 09:12):

It's a decidable choice.

view this post on Zulip Sean Leather (Jul 04 2018 at 09:13):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:15):

never use choice

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:15):

even when it's decidable

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:15):

it's evil

view this post on Zulip Johan Commelin (Jul 04 2018 at 09:15):

Kenny, why did you choose to enroll at Imperial?

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:15):

I didn't choose

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:16):

it just happened

view this post on Zulip Johan Commelin (Jul 04 2018 at 09:16):

Just like you trolling this thread just happens

view this post on Zulip Kenny Lau (Jul 04 2018 at 09:16):

lol

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 04 2018 at 09:20):

Kevin, yes, and then write a solid API.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 04 2018 at 09:22):

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

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Sean Leather (Jul 04 2018 at 09:24):

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

view this post on Zulip 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