Zulip Chat Archive

Stream: general

Topic: Examples


view this post on Zulip Michael R Douglas (Apr 04 2020 at 15:17):

Examples are an important part of mathematics - to test one's conjectures, help think concretely, etc.
Could people point out to me definitions of examples of the objects and structures defined in mathlib?
I have not found them. For example I typed in "sphere" to the Github search, with the response:
We couldn’t find any code matching 'sphere' in leanprover-community/mathlib
Perhaps they are in a different repository ?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:20):

They ain't there

view this post on Zulip Michael R Douglas (Apr 04 2020 at 15:21):

If someone wrote examples, should they go in mathlib? In the same file as the general definition? In another file? In another repository?

view this post on Zulip Reid Barton (Apr 04 2020 at 15:36):

Important examples (like spheres as manifolds) that will be used in future theorems should certainly go into mathlib.
File organization is mostly a matter of how large things are--if you can define your example in 5 lines, maybe it can go in the same file as the general definition, but if you have a lot to say about it, then it should probably go in its own file.

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:37):

Undergraduates often ask me where all the finite groups are. As far as I know we don't even have the symmetric groups S_n.

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:39):

We do, it's called perm in data.equiv.basic

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:40):

It's not, because that doesn't take n

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:41):

And there are a whole bunch of theorems about S_n like e.g. they're solvable for n<=4 and non-solvable for n>=5

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:41):

perm (fin n)

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:41):

Exactly -- we don't have it.

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:42):

not every combination of definitions has to be a definition

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:42):

Yes but historically important definitions like SnS_n should be definitions if we want mathematics undergraduates to find a library which they can understand and use.

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:43):

I think that perm is that (the name could be better)

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:43):

Just like how matrices are defined over fintypes, we would want to do the same here. So it really is just perm A where fintype A

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:44):

But then the theorem becomes much uglier. My n >= 5 becomes your fintype.card A >= 5.

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:45):

I don't deny it. But this tends to be shortsighted thinking, and we end up refactoring later anyway

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:46):

You can always prove the ugly version first and deduce the fin n version

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:46):

it's OK, because Scott is going to write a tactic which proves solvable (perm (fin n)) iff solvable (perm A) when A.card = n

view this post on Zulip Patrick Massot (Apr 04 2020 at 15:47):

Somewhere deep in the PR list sit more group examples (by Neil).

view this post on Zulip Reid Barton (Apr 04 2020 at 15:47):

wouldn't you want to prove the fin n version first and then deduce the "general" version?

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:47):

I think Reid is right

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:47):

The proof is that n>=5 so there's an injection perm(fin 5) -> perm(fin n) and perm(fin 5) is non-solvable by dec_trivial

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:48):

We can get that compiling on the Azure cloud and then never worry about it again

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:48):

well with that proof you could do the same thing with an injection from perm(fin 5) -> perm A

view this post on Zulip Kevin Buzzard (Apr 04 2020 at 15:49):

oh but it would be much more hassle finding the injection, you'd need the axiom of choice or something

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:49):

there exists an injection

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:49):

by abstract nonsense

view this post on Zulip Mario Carneiro (Apr 04 2020 at 15:50):

pretty sure you can get some mathlib statement off the shelf that gives you the exact function you want

view this post on Zulip Rob Lewis (Apr 04 2020 at 16:30):

For what it's worth, there is a folder archive/examples, where we decided to put things with pedagogical value that were too specific to really be part of mathlib. There's exactly one file there right now. https://github.com/leanprover-community/mathlib/tree/master/archive/examples

view this post on Zulip Michael R Douglas (Apr 04 2020 at 16:46):

Thanks! Perhaps there should be a directory structure in archive/examples parallel to that of mathlib.

view this post on Zulip Rob Lewis (Apr 04 2020 at 16:47):

I think we need more than one example before it comes to that.

view this post on Zulip Scott Morrison (Apr 05 2020 at 01:54):

Another place to put examples which will not be used for further theory building is the tutorial directory, which deserves much more content.


Last updated: May 08 2021 at 10:12 UTC