## Stream: maths

### Topic: binomial coefficients

#### Kevin Buzzard (Nov 07 2018 at 17:36):

Preparing a lecture on the binomial and multinomial theorem. For pedagogical reasons I will not prove the binomial theorem the way it's proved in Lean (although the students who come to the "extra material" session will see the Lean proof). In Lean I guess the binomial coefficient $\binom{n}{r}$ is defined to be $\frac{n!}{r!(n-r)!}.$ So is there in Lean a proof that $\binom{n}{r}$ equals the number of $r$-element subtypes of a a type of size $n$? [this is my definition of the binomial coefficient in my lectures]

#### Johan Commelin (Nov 07 2018 at 17:40):

Do we know that the powerset of a type of size n has size 2 ^ n?

#### Johan Commelin (Nov 07 2018 at 17:40):

@Kevin Buzzard Wouldn't it make sense to define $n \choose r$ via Pascal's triangle?

#### Johannes Hölzl (Nov 07 2018 at 17:48):

it is defined recursively in mathlib (in mathlib/data/nat/choose.lean):

def choose : ℕ → ℕ → ℕ
| _             0 := 1
| 0       (k + 1) := 0
| (n + 1) (k + 1) := choose n k + choose n (succ k)


#### Kevin Buzzard (Nov 07 2018 at 17:49):

Sure, that would be another way; then you can prove it's what I said it is by induction on n. Hmm and I guess you could then prove the result about the subsets of size r of a set of size n by induction on n.

#### Kevin Buzzard (Nov 07 2018 at 17:49):

I guess I was just checking that everything I said today was in Lean. I am giving this awful proof of the binomial theorem of the form "imagine multiplying out (a+b)(a+b)(a+b)...(a+b) n times -- now think about what the general term looks like? You choose r brackets and choose a from them, and choose b from the rest -- done"

#### Kevin Buzzard (Nov 07 2018 at 17:51):

but actually I think everything is either there or could be there. @Johan Commelin the sum of the binomial coefficients being $2^n$ is easy: you can deduce it from the binomial theorem with $a=b=1$ ;-)

#### Johan Commelin (Nov 07 2018 at 17:51):

Sure. But that's not exactly what I asked :wink:

#### Bryan Gin-ge Chen (Nov 07 2018 at 17:52):

I think what you asked for is here.

#### Kevin Buzzard (Nov 07 2018 at 17:53):

...as long as you can prove that the size of a subset is at most the size of the set (which I am pretty sure is there) and the result about subsets of size r (which should be fine by induction on n).

#### Bryan Gin-ge Chen (Nov 13 2018 at 18:06):

So is there in Lean a proof that $\binom{n}{r}$ equals the number of $r$-element subtypes of a type of size $n$?

I couldn't find this in mathlib so I've been working off-and-on on this. I finally have a proof, but it seems excessively long and ugly. Well, actually what I have is a proof of this:

lemma card_subsets_of_range_eq_choose (n k : ℕ) :
card ((powerset (range n)).filter (λ t, card t = k)) = choose n k :=


(what should be the name?) though what you really want is this:

lemma card_subsets_card_eq_choose  {s : finset α} (k : ℕ) : card ((powerset s).filter (λ t, card t = k)) = choose (card s) k :=
sorry


Last time I ran into something like this, @Simon Hudon ended up writing a bunch of stuff for me which is now in the tutorials branch. This one's probably much easier but I haven't tried to tackle it yet...

Anyways, if anyone wants to golf this down to something reasonable or give advice on making it nicer, I'd really appreciate it!

#### Mario Carneiro (Nov 13 2018 at 18:08):

I would hope to have a function on list that constructs all k element sublists

#### Bryan Gin-ge Chen (Nov 13 2018 at 18:09):

Oh that sounds like a good idea.

#### Mario Carneiro (Nov 13 2018 at 18:10):

I don't think we have it

#### Mario Carneiro (Nov 13 2018 at 18:10):

The nice thing about this is that the proof that this list has length choose n k will be obvious from the construction

#### Mario Carneiro (Nov 13 2018 at 18:11):

and the rest is just lifting to the quotient

#### Bryan Gin-ge Chen (Nov 13 2018 at 18:11):

right, this is like the approach to finite partitions you suggested before that I still haven't managed to do

#### Chris Hughes (Nov 13 2018 at 18:45):

@Bryan Gin-ge Chen

def sublists_of_length {α : Type*} : Π (l : list α) (n : ℕ), list (list α)
| l      0     := [[]]
| []     (n+1) := []
| (a::l) (n+1) := (sublists_of_length l n).map (list.cons a) ++
(sublists_of_length l (n + 1))


@Mario Carneiro The definition of list.sublists in mathlib is totally incomprehensible to me, but is faster than the most natural definition. This approach to sublist_of_length is presumably not the fastest. What's the general policy on fast definitions versus comprehensible definitions?

#### Mario Carneiro (Nov 13 2018 at 18:45):

fast is better than comprehensible

#### Mario Carneiro (Nov 13 2018 at 18:46):

you can often prove the comprehensible definition as a lemma though

#### Mario Carneiro (Nov 13 2018 at 18:46):

I think the definition of list.sublists is based on haskell's

#### Chris Hughes (Nov 13 2018 at 18:46):

Even if fast means much longer proofs?

#### Mario Carneiro (Nov 13 2018 at 18:47):

yes, although we can also retrofit a faster definition

#### Johannes Hölzl (Nov 13 2018 at 18:47):

for me comprehensible is better than fast. For fast we often need a different solution anyway

#### Johannes Hölzl (Nov 13 2018 at 18:48):

With Lean4 :four_leaf_clover: we hopefully can simply redefine constants for fast evaluation

#### Mario Carneiro (Nov 13 2018 at 18:48):

Note that in the case of sublists there is actually a separate version sublists' that is basically the comprehensible one, to which we prove equivalence

#### Johannes Hölzl (Nov 13 2018 at 18:48):

Hm, then it would be better to have sublist to be the comprehensible one?!

#### Mario Carneiro (Nov 13 2018 at 18:49):

The idea is that the default one should be VM-fast

#### Mario Carneiro (Nov 13 2018 at 18:49):

because this is in the computational part

#### Mario Carneiro (Nov 13 2018 at 18:50):

(there is an additional complication, in that sublists and sublists' are not equal but differ by a complicated permutation)

#### Mario Carneiro (Nov 13 2018 at 18:51):

They actually both have fast VM definitions, but sublists is faster

#### Mario Carneiro (Nov 13 2018 at 18:51):

and sublists' has nicer equation lemmas

#### Mario Carneiro (Nov 13 2018 at 19:14):

here's a faster version of the same definition:

def sublists_of_length_aux {α : Type*} : list α → ℕ → (list α → list α) → list (list α) → list (list α)
| l      0     f r := f [] :: r
| []     (n+1) f r := r
| (a::l) (n+1) f r := sublists_of_length_aux l n (f ∘ list.cons a)
(sublists_of_length_aux l (n + 1) f r)

def sublists_of_length {α : Type*} (l : list α) (n : ℕ) : list (list α) :=
sublists_of_length_aux l n id []


the idea is to define (sublists_of_length l n).map f ++ r by recursion without stacking recursive calls to map or append

#### Mario Carneiro (Nov 13 2018 at 19:15):

You can prove without too much difficulty that sublists_of_length_aux l n f r = (sublists_of_length l n).map f ++ r and then you can prove your equation lemmas as theorems

#### Jeremy Avigad (Nov 15 2018 at 01:07):

We used to have this in Lean 2 (but it would be nice to have cleaner proofs).
https://github.com/leanprover/lean2/blob/master/library/theories/combinatorics/choose.lean#L208-L220

#### Bryan Gin-ge Chen (Nov 19 2018 at 17:28):

You can prove without too much difficulty that sublists_of_length_aux l n f r = (sublists_of_length l n).map f ++ r and then you can prove your equation lemmas as theorems

Could I get a hint on this step? I'm not sure what to do even to get started:

def sublists_of_length_aux {α : Type*} : list α → ℕ → (list α → list α) → list (list α) → list (list α)
| l      0     f r := f [] :: r
| []     (n+1) f r := r
| (a::l) (n+1) f r := sublists_of_length_aux l n (f ∘ list.cons a)
(sublists_of_length_aux l (n + 1) f r)

def sublists_of_length {α : Type*} (l : list α) (n : ℕ) : list (list α) :=
sublists_of_length_aux l n id []

lemma foo {α : Type*} : ∀(l : list α) (n : ℕ) (f : list α → list α) (r : list (list α)),
sublists_of_length_aux l n f r = (sublists_of_length l n).map f ++ r
| l 0 f r :=
begin
--unfold sublists_of_length_aux,
sorry
end
| [] (n+1) f r := sorry
| (a::l) (n+1) f r := sorry


I was hoping I could make the first one refl, but it seems I need to do something else first, and I'm having trouble working with the definitions.

#### Mario Carneiro (Nov 19 2018 at 17:49):

ah, it looks like lean did a case split on l first, then n, in the definition of sublists_of_length_aux, so that the first equation isn't true by refl but rather by cases l; refl

#### Mario Carneiro (Nov 19 2018 at 17:49):

you can fix this by swapping the order of the first two arguments to sublists_of_length_aux

#### Bryan Gin-ge Chen (Nov 19 2018 at 17:55):

Cool, that did the trick.

#### Mario Carneiro (Nov 19 2018 at 18:01):

but actually I think you want to generalize the lemma a bit to prove it:

def sublists_of_length_aux {α : Type*} : ℕ → list α → (list α → list α) → list (list α) → list (list α)
| 0     l      f r := f [] :: r
| (n+1) []     f r := r
| (n+1) (a::l) f r := sublists_of_length_aux n l (f ∘ list.cons a)
(sublists_of_length_aux (n + 1) l f r)

def sublists_of_length {α : Type*} (l : list α) (n : ℕ) : list (list α) :=
sublists_of_length_aux n l id []

lemma foo {α : Type*} : ∀ (n : ℕ) (l : list α) (f g : list α → list α) (r s : list (list α)),
sublists_of_length_aux n l (g ∘ f) (r.map g ++ s) =
(sublists_of_length_aux n l f r).map g ++ s
| 0     l      f g r s := rfl
| (n+1) []     f g r s := rfl
| (n+1) (a::l) f g r s := by unfold sublists_of_length_aux;
rw [foo, show ((g ∘ f) ∘ list.cons a) = (g ∘ f ∘ list.cons a), by refl, foo]


The theorem you want is now a simple corollary

#### Jeremy Avigad (Apr 07 2019 at 23:00):

I wrote a proof that the cardinality of the collection of k-subsets of an n-element set is choose n k: https://gist.github.com/avigad/d9eef0fed9bb8b8ee4b03daafe604d53

It seems more complicated than it should be. Can anyone do better?

#### Bryan Gin-ge Chen (Apr 07 2019 at 23:07):

There's an older thread on this here. I never managed to finish @Mario Carneiro 's suggested proof, unfortunately.

#### Mario Carneiro (Apr 07 2019 at 23:11):

I think that it is worth it to do the list version of this first, as in the other thread. This gives you a useful list function in addition to proving this theorem

#### Mario Carneiro (Apr 07 2019 at 23:12):

It will probably be larger in terms of LOC but there won't be any big "hotspot" theorem with a huge line count, it breaks into a bunch of 3 line lemmas

#### Jeremy Avigad (Apr 07 2019 at 23:24):

It looks like you will need lots of annoying facts relating finsets and nodup lists, and finsets of finsets vs. lists of lists. You'd have to translate statements about powerset, filter, cardinality, etc. It doesn't sound like fun.

It is a shame that the textbook proof is so long. All the steps are straightforward, but it is painful to have to spell them out. It's a good test case for automation.

#### Mario Carneiro (Apr 07 2019 at 23:27):

Most of that work is already done

#### Mario Carneiro (Apr 07 2019 at 23:27):

there are already theorems like that about nodup lists, properties of list.sublists and so on

#### Mario Carneiro (Apr 07 2019 at 23:28):

why is choose in root namespace?

#### Jeremy Avigad (Apr 07 2019 at 23:32):

I don't know. Where should it be? The name conflicts with finset.choose.

#### Mario Carneiro (Apr 07 2019 at 23:57):

nat.choose of course

#### Mario Carneiro (Apr 07 2019 at 23:58):

all the other nat functions are in the nat namespace

#### Mario Carneiro (Apr 08 2019 at 01:14):

See #899. As I suspected, the total line count is more, but none of the individual theorems is very long, only about 10 lines at most, and there is more reusability for the list and multiset counterparts

#### Jeremy Avigad (Apr 08 2019 at 01:26):

Nice. But I still think it is a shame that there isn't a more elegant path through finset. Rewriting finite combinatorics in terms of lists isn't the best way to make friends and influence others.

#### Mario Carneiro (Apr 08 2019 at 01:26):

I think that the performance improvement is worth it

#### Mario Carneiro (Apr 08 2019 at 01:27):

filtering all subsets is kind of a bad way to generate these lists

#### Mario Carneiro (Apr 08 2019 at 01:28):

There is certainly a way to do it directly, but then you have to do a lot of reasoning about the sizes of things; here the fact that the size of it is choose is easy because it directly reflects the combinatoric description of how you make a list of all subsets

#### Mario Carneiro (Apr 08 2019 at 01:29):

Also I prefer to avoid insert and such, because you are always dealing with things not being elements of other things

#### Scott Morrison (Apr 08 2019 at 01:31):

I like Mario's proof a lot; it's got that inevitable feel to it. At the same time I appreciate Jeremy's point: mathematicians are going to take some time to get used to list being more important than finset.

#### Jeremy Avigad (Apr 08 2019 at 01:57):

Mario, I don't buy the claim about "reflecting the combinatoric description". Given the recursive definition description of choose, the set-based argument is a one-liner: if a is an arbitrary element of a set s with n + 1 elements, then divide the (k+1)-element subsets of s into the ones that contain a, and the ones that don't. The definition of subsets_len via subsets_len_aux is clever and it makes for a nice formalization, but it distracts from the combinatorial / set-theoretic intuition. You'll never convince combinatoricists to start writing papers that way.

#### Mario Carneiro (Apr 08 2019 at 02:11):

What I mean by "reflecting the combinatorics": Consider how you would give the combinatoric bijection. You have a finite set, and you are making a list of all the subsets of length k; you first list all the ones that don't contain some arbitrary element a, then all the ones that do. A little reflection reveals that you don't need any of the structure of finite sets for this, so you may as well do it on lists. Now you want to define a function sublists_len k l such that sublists_len 0 l = [[]], and sublists_len (k+1) (a::l) = sublists_len (k+1) l ++ map (a::) (sublists_len k l), because we have split the problem into the size k+1 elements in l and the size k elements of l with a appended. This is exactly the definition of sublists_len I give (with a slight optimization so that you don't have to nest maps). As a result, it's trivial to prove a statement about the length being choose n k

#### Mario Carneiro (Apr 08 2019 at 02:12):

The proof is very combinatoric and constructive

#### Mario Carneiro (Apr 08 2019 at 02:15):

You could actually stop there, but in the interest of getting closer to your version, I also lift the list function to a function on multisets and finsets. There isn't really any added content there, it's just restating facts in the new context. There are some additional observations to be made about how the list function preserves permutations and nodups so that the constructions lift, but that is relatively simple

#### Mario Carneiro (Apr 08 2019 at 02:16):

The point I want to make is that I'm not proving a theorem, I'm constructing a function

#### Mario Carneiro (Apr 08 2019 at 02:24):

It is possible that you are getting hung up on the strange definition sublists_len_aux. If so I would encourage you to ignore it and look only at sublists_len_zero, sublists_len_succ_nil, and sublists_len_succ_cons as the equation lemmas, because that's what they are

#### Kenny Lau (Apr 08 2019 at 02:35):

it's a simple corollary of the orbit-stabilizer theorem... :P

#### Kevin Buzzard (Apr 08 2019 at 06:02):

Stepping back a bit, I wonder whether dependent type theory is not really suited to combinatorial arguments like this, although I know sufficiently little about other formalisations of mathematics to know whether any of them would be any better. Something I learnt recently is that simple type theory seems to be not suitable for developing the theory of schemes, and I guess what's going on is that different formalisations of the foundations are better suited to different (possibly overlapping) areas.

#### Mario Carneiro (Apr 08 2019 at 06:03):

Finite combinatorics is usually a strong point in DTT. That's why every introductory example has you doing stuff with nat

#### Mario Carneiro (Apr 08 2019 at 06:04):

Type dependencies don't really come up here

#### Scott Morrison (Apr 08 2019 at 06:05):

I think the problem in this example is more along the "programs / proofs" axis than the "DTT / something else" axis.

#### Scott Morrison (Apr 08 2019 at 06:06):

Mario has written a "maths as programs" proof.

#### Kevin Buzzard (Apr 08 2019 at 06:08):

Maybe type theory itself isn't suited to combinatorics?

#### Kevin Buzzard (Apr 08 2019 at 06:08):

Would this all be easier in ZFC?

#### Mario Carneiro (Apr 08 2019 at 06:16):

I can show you http://us2.metamath.org/mpeuni/hashbclem.html but I don't think you are in a position to say whether this proof is easier or harder than the lean proof

#### Mario Carneiro (Apr 08 2019 at 06:16):

It is most similar to Jeremy's proof

#### Mario Carneiro (Apr 08 2019 at 06:18):

the core of the proof is construction of a bijection from { x \sub A | a e. x /\ #x = n + 1 } to {y \sub A | #y = n } by showing that x |-> x / {a} and y |-> y u. {a} are inverse

#### Mario Carneiro (Apr 08 2019 at 06:20):

Personally, I prefer the "program" proof. The style could be mimicked in ZFC with a bunch of new definitions

Last updated: May 19 2021 at 02:10 UTC