Examples

Stream: general

[Michael R Douglas]

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 ?

[Kevin Buzzard]

They ain't there

[Michael R Douglas]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

perm (fin n)

[Kevin Buzzard]

Exactly -- we don't have it.

[Mario Carneiro]

not every combination of definitions has to be a definition

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Kevin Buzzard]

I think Reid is right

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

there exists an injection

[Mario Carneiro]

by abstract nonsense

[Mario Carneiro]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Scott Morrison]

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