## Stream: general

### Topic: Examples

#### 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 ?

They ain't there

#### 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?

#### 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.

#### 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.

#### Mario Carneiro (Apr 04 2020 at 15:39):

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

#### Kevin Buzzard (Apr 04 2020 at 15:40):

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

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

#### Mario Carneiro (Apr 04 2020 at 15:41):

perm (fin n)

#### Kevin Buzzard (Apr 04 2020 at 15:41):

Exactly -- we don't have it.

#### Mario Carneiro (Apr 04 2020 at 15:42):

not every combination of definitions has to be a definition

#### Kevin Buzzard (Apr 04 2020 at 15:42):

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

#### Mario Carneiro (Apr 04 2020 at 15:43):

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

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

#### Kevin Buzzard (Apr 04 2020 at 15:44):

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

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

#### Mario Carneiro (Apr 04 2020 at 15:46):

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

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

#### Patrick Massot (Apr 04 2020 at 15:47):

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

#### 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?

#### Kevin Buzzard (Apr 04 2020 at 15:47):

I think Reid is right

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

#### Kevin Buzzard (Apr 04 2020 at 15:48):

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

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

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

#### Mario Carneiro (Apr 04 2020 at 15:49):

there exists an injection

#### Mario Carneiro (Apr 04 2020 at 15:49):

by abstract nonsense

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

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

#### 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.

#### Rob Lewis (Apr 04 2020 at 16:47):

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

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