products of sets

Stream: new members

[Simon Pepin Lehalleur]

I have just started playing around with lean and I have a very basic question. From what I understand, the easy way to work with types in Lean (without universes) is to write s : set Type. But then when I form s \times s, it is of type Type \times Type. How can I make s \times s into a term of type Type ? Naively, I want the product of sets to be a set! Same question with finset.

[Sebastien Gouezel]

are you looking for set.prod?

[Chris Hughes]

Using set Type is quite unusual. It's probably not the best way to do what you want to do.

[Sebastien Gouezel]

Reading your question again, I think you are confused. If you want to define a Type α, you just write α : Type. If you want to define a set inside α, write s : set α.

[Simon Pepin Lehalleur]

Thanks! How can I insert lean code in a reply? I want to work with a (finite) set s and define a directed graph on it by specifying an adjacency function s \times s -> Prop.

[Chris Hughes]

Using

```lean
my code
```

[Andrew Ashworth]

you will see an explanation of all formatting commands by clicking the "A" at the bottom of the screen, next to the smiley face

[Simon Pepin Lehalleur]

Thanks!

[Kevin Buzzard]

Lean works with type theory, not set theory. Mathematicians like us have this background where we think everything is a set. If we were in mathematician-land and you said to me "I want a set s and an adjacency function on it, can you do that in Lean for me?" I would not use set at all -- I would let s be a type.

[Kevin Buzzard]

Lean does have this set thing, but it really means "subset". So if you write s: set alpha then you are really thinking of s as a subset of alpha or a subtype of alpha or whatever you want to call it. Types in Lean are pretty much the same as what normal mathematicians think of as sets, with the following weird different: two types can never have any elements in common. This sounds a bit shocking at first, but my guess is that in your case you can let s be a type.

[Mario Carneiro]

Technically that statement is not well formed

[Mario Carneiro]

The statement "types A and B are disjoint" does not typecheck

[Simon Pepin Lehalleur]

Do you have nice examples of combinatorics of finite sets in lean which I could learn from?

[Johan Commelin]

@Simon Pepin Lehalleur It might come as a bit of a surprise, but finite sets are actually quite hard to manage for a theorem prover.

[Johan Commelin]

And there are different ways to "impose" finiteness.

[Johan Commelin]

If you have a type X : Type, you can tell Lean that it is finite by adding [fintype X] as hypothesis.

[Kevin Buzzard]

All of the "different" ways are of course the same, but in constructive maths they're probably different.

[Johan Commelin]

So you could try to define arbitrary graphs, using some type G. And then if you add [fintype G] in some theorem then it will automatically be a finite graph.

[Simon Pepin Lehalleur]

Such a type then has a cardinality in nat? And is fintype inherited by subsets?

[Kevin Buzzard]

by subtypes? ;-) Yes, I should think so.

[Kevin Buzzard]

And yes, the cardinality would be in nat.

[Kevin Buzzard]

import data.fintype

example (G : Type) [fintype G] (P : G → Prop) : fintype {g : G // P g} := by apply_instance -- fails

ha ha it fails.

#check fintype.card
/-
fintype.card : Π (α : Type u_1) [_inst_1 : fintype α], ℕ
-/

At least that part worked.

The reason finite stuff is hard to work with in type theory is that a finset X (a finite subset of X) is defined to be a list of elements of X, plus a proof that the elements in the list are all different to each other, modulo the equivalence relation given by permutation of elements of the list (a list is ordered).

[Kevin Buzzard]

If your basic object is a type, and your basic ways of building types are inductive types and function types (which is what we have in Lean), then you have to readjust a little. Finite sets are not hard to work with, but that is only because computer scientists wrote thousands of lines of code to enable mathematicians to work with them:

https://github.com/leanprover-community/mathlib/blob/master/src/data/fintype.lean

which relies on

https://github.com/leanprover-community/mathlib/blob/master/src/data/finset.lean

which relies on

https://github.com/leanprover-community/mathlib/blob/master/src/data/multiset.lean

and that is already about 6000 lines.

A subtype of a finite type should be finite -- I'm sure that will be in there somewhere; I just failed to prove it myself.

[Kevin Buzzard]

The issue is that finiteness turns out to be a subtle business, apparently, in type theory.

[Johan Commelin]

@Simon Pepin Lehalleur Here is a little catalogue:

• There is finset. If you write s : finset X for some arbitrary type X, then you express that you have a finite set of elements of type X. Kevin just told you how it is implemented.
• There is finite. If you hae s : set X, then finite s expresses that the arbitrary set s is actually finite. There are functions that turn s into a finset X given a proof of finite s, and vice versa: if you have s : finset X, then you can view s as a set X (by coercion, so it's quite transparent) and you there will be a lemma that says that this s is finite.
• There is fintype. This expresses that a certain type is finite. This uses the type class system, which in theory means that lots of things inherite fintype (e.g. a product of fintypes is a fintype). I think that Kevin's example above should work, I'm not sure why it fails.

[Marc Huisinga]

iirc the statement "subsets of finite sets are finite" is also equivalent to LEM (http://math.andrej.com/2009/09/07/constructive-stone-finite-sets/)

[Johan Commelin]

I wouldn't be surprised if Simon is not interested in that at all... :stuck_out_tongue_wink:

[Johan Commelin]

@Simon Pepin Lehalleur Do you have a particular goal in mind?

[Bryan Gin-ge Chen]

Do you have nice examples of combinatorics of finite sets in lean which I could learn from?

A while back I wrote this file on partitions of finite sets (with lots of help from Zulip!). It was meant to address a challenge of @Neil Strickland's. Since then Neil has shared quite a few Lean files of his own in a combinatorics directory here (including, among lots of other things, an alternative and probably nicer version of partitions).

[Simon Pepin Lehalleur]

I want to work my way towards stating Ramsey's theorem.

[Johan Commelin]

Aha, that seems like a nice challenge

[Johan Commelin]

We haven't done any graph theory so far...

[Simon Pepin Lehalleur]

My first idea was to look at category theory, but that looked very tricky... I thought finite sets would be easier!

[Johan Commelin]

The foundations of category theory are there. @Scott Morrison is working on monoidal categories. We have the basic framework of limits/colimits.

[Johan Commelin]

@Simon Pepin Lehalleur I just remember that Jeremy recently talked about some graph-theoretic things in Lean: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Type.20classes.20again/near/167340123

[Johan Commelin]

You might find some useful things there.

[Kevin Buzzard]

My first idea was to look at category theory, but that looked very tricky... I thought finite sets would be easier!

I think that stating Ramsey's theorem is a very nice first project. Here is what will happen: you will try to write down mathematics, but in many cases to get from one step to the next (e.g. A and B are finite, hence A union B is finite) -- steps which a mathematician would say "it's obvious" -- you will need to apply a function. The thousands of lines of code which I linked to above are the community's attempt to write down every function you would ever need. So the main difficulty you will face (when you have learned the basic syntax etc) is that you don't know the names of any functions. There are four ways to deal with this problem. First, you can just ask here. Second, you can learn how to use the tactic which searches the library for the function you need. Third, you can begin to learn the logic which computer scientists use when naming these functions, and then fourth, when it is all beginning to make enough sense for this not to be a terrifying option -- you can just read the library code yourself. This is exactly how I learnt to use Lean (apart from the fact that the tactic which searches through the library didn't exist 2 years ago :-) )

[Mario Carneiro]

the reason kevin's example failed is because he didn't say P is decidable or use classical magic

[Kevin Buzzard]

import data.fintype

local attribute [instance, priority 0] classical.prop_decidable

noncomputable theory

example (G : Type) [fintype G] (P : G → Prop) : fintype {g : G // P g} := by apply_instance -- works

This file now says: (1) import the file which does finite types. (2) and (3): switch on mathematician mode. (4) a subtype of a finite type is finite.

[Kevin Buzzard]

The computer scientists still believe in the Curry-Howard correspondence, so instead of a proof that a subset of a finite set is finite, they want an algorithm.

[Kevin Buzzard]

You can tell them not to be so demanding with those lines 2 and 3.

[Patrick Massot]

Lean does have this set thing, but it really means "subset". So if you write s: set alpha then you are really thinking of s as a subset of alpha or a subtype of alpha or whatever you want to call it.

I think this is a misleading way of explaining this difference, which is biased by our set theoretic foundations background. It's some kind of accident that set theoretic foundations make no difference at all between sets that come up in real life and weird collections like $\{1, \mathbb{R}, \sin\}$. It's because everything is a set and almost everything can be put inside a set. In type theory you can talk about such sets but you'll have to struggle a bit, which I think is fair. However you won't have to struggle to discuss sets whose elements are real numbers, or sets whose elements are functions from real numbers to real numbers. And you shouldn't think of them as subsets of anythings. They are homogeneous collections of things of the same type.