binomial coefficients

Stream: maths

[Kevin Buzzard]

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]

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

[Johan Commelin]

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

[Johannes Hölzl]

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]

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]

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]

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]

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

[Bryan Gin-ge Chen]

I think what you asked for is here.

[Kevin Buzzard]

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

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]

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

[Mario Carneiro]

maybe we have it already?

[Bryan Gin-ge Chen]

Oh that sounds like a good idea.

[Mario Carneiro]

I don't think we have it

[Mario Carneiro]

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]

and the rest is just lifting to the quotient

[Bryan Gin-ge Chen]

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

[Chris Hughes]

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

fast is better than comprehensible

[Mario Carneiro]

you can often prove the comprehensible definition as a lemma though

[Mario Carneiro]

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

[Chris Hughes]

Even if fast means much longer proofs?

[Mario Carneiro]

yes, although we can also retrofit a faster definition

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

because this is in the computational part

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

and sublists' has nicer equation lemmas

[Mario Carneiro]

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]

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]

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]

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]

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]

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

[Bryan Gin-ge Chen]

Cool, that did the trick.

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

Most of that work is already done

[Mario Carneiro]

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

[Mario Carneiro]

why is choose in root namespace?

[Jeremy Avigad]

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

[Mario Carneiro]

nat.choose of course

[Mario Carneiro]

all the other nat functions are in the nat namespace

[Mario Carneiro]

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]

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]

I think that the performance improvement is worth it

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Scott Morrison]

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]

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]

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]

The proof is very combinatoric and constructive

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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]

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

[Mario Carneiro]

Type dependencies don't really come up here

[Scott Morrison]

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

[Scott Morrison]

Mario has written a "maths as programs" proof.

[Kevin Buzzard]

Maybe type theory itself isn't suited to combinatorics?

[Kevin Buzzard]

Would this all be easier in ZFC?

[Mario Carneiro]

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]

It is most similar to Jeremy's proof

[Mario Carneiro]

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]

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