Zulip Chat Archive

Stream: new members

Topic: products of sets


view this post on Zulip Simon Pepin Lehalleur (Jun 15 2019 at 10:02):

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.

view this post on Zulip Sebastien Gouezel (Jun 15 2019 at 10:04):

are you looking for set.prod?

view this post on Zulip Chris Hughes (Jun 15 2019 at 10:06):

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

view this post on Zulip Sebastien Gouezel (Jun 15 2019 at 10:06):

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

view this post on Zulip Simon Pepin Lehalleur (Jun 15 2019 at 10:09):

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.

view this post on Zulip Chris Hughes (Jun 15 2019 at 10:12):

Using

```lean
my code
```

view this post on Zulip Andrew Ashworth (Jun 15 2019 at 10:12):

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

view this post on Zulip Simon Pepin Lehalleur (Jun 15 2019 at 10:18):

Thanks!

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 11:24):

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.

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 11:26):

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.

view this post on Zulip Mario Carneiro (Jun 15 2019 at 11:31):

Technically that statement is not well formed

view this post on Zulip Mario Carneiro (Jun 15 2019 at 11:32):

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

view this post on Zulip Simon Pepin Lehalleur (Jun 15 2019 at 12:14):

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 12:15):

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 12:16):

And there are different ways to "impose" finiteness.

view this post on Zulip Johan Commelin (Jun 15 2019 at 12:16):

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

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 12:17):

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 12:17):

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.

view this post on Zulip Simon Pepin Lehalleur (Jun 15 2019 at 12:22):

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

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 12:22):

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

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 12:22):

And yes, the cardinality would be in nat.

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 12:26):

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

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 12:30):

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.

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 12:31):

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 12:33):

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

view this post on Zulip Marc Huisinga (Jun 15 2019 at 12:33):

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/)

view this post on Zulip Johan Commelin (Jun 15 2019 at 12:36):

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 12:46):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 15 2019 at 13:01):

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

view this post on Zulip Simon Pepin Lehalleur (Jun 15 2019 at 13:04):

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 13:07):

Aha, that seems like a nice challenge

view this post on Zulip Johan Commelin (Jun 15 2019 at 13:08):

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

view this post on Zulip Simon Pepin Lehalleur (Jun 15 2019 at 13:09):

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 13:24):

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

view this post on Zulip Johan Commelin (Jun 15 2019 at 13:26):

@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

view this post on Zulip Johan Commelin (Jun 15 2019 at 13:26):

You might find some useful things there.

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 13:30):

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 :-) )

view this post on Zulip Mario Carneiro (Jun 15 2019 at 13:47):

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

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 13:49):

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.

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 13:50):

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.

view this post on Zulip Kevin Buzzard (Jun 15 2019 at 13:51):

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

view this post on Zulip Patrick Massot (Jun 15 2019 at 14:14):

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,R,sin}\{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.


Last updated: May 14 2021 at 04:22 UTC