Zulip Chat Archive

Stream: maths

Topic: binomial coefficients


view this post on Zulip 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 (nr)\binom{n}{r} is defined to be n!r!(nr)!.\frac{n!}{r!(n-r)!}. So is there in Lean a proof that (nr)\binom{n}{r} equals the number of rr-element subtypes of a a type of size nn? [this is my definition of the binomial coefficient in my lectures]

view this post on Zulip Johan Commelin (Nov 07 2018 at 17:40):

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

view this post on Zulip Johan Commelin (Nov 07 2018 at 17:40):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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 2n2^n is easy: you can deduce it from the binomial theorem with a=b=1a=b=1 ;-)

view this post on Zulip Johan Commelin (Nov 07 2018 at 17:51):

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

view this post on Zulip Bryan Gin-ge Chen (Nov 07 2018 at 17:52):

I think what you asked for is here.

view this post on Zulip 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).

view this post on Zulip Bryan Gin-ge Chen (Nov 13 2018 at 18:06):

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

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!

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:08):

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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:09):

maybe we have it already?

view this post on Zulip Bryan Gin-ge Chen (Nov 13 2018 at 18:09):

Oh that sounds like a good idea.

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:10):

I don't think we have it

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:11):

and the rest is just lifting to the quotient

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:45):

fast is better than comprehensible

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:46):

you can often prove the comprehensible definition as a lemma though

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:46):

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

view this post on Zulip Chris Hughes (Nov 13 2018 at 18:46):

Even if fast means much longer proofs?

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:47):

yes, although we can also retrofit a faster definition

view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Nov 13 2018 at 18:48):

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

view this post on Zulip 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

view this post on Zulip Johannes Hölzl (Nov 13 2018 at 18:48):

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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:49):

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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:49):

because this is in the computational part

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:51):

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

view this post on Zulip Mario Carneiro (Nov 13 2018 at 18:51):

and sublists' has nicer equation lemmas

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Nov 19 2018 at 17:55):

Cool, that did the trick.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 07 2019 at 23:27):

Most of that work is already done

view this post on Zulip Mario Carneiro (Apr 07 2019 at 23:27):

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

view this post on Zulip Mario Carneiro (Apr 07 2019 at 23:28):

why is choose in root namespace?

view this post on Zulip Jeremy Avigad (Apr 07 2019 at 23:32):

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

view this post on Zulip Mario Carneiro (Apr 07 2019 at 23:57):

nat.choose of course

view this post on Zulip Mario Carneiro (Apr 07 2019 at 23:58):

all the other nat functions are in the nat namespace

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 08 2019 at 01:26):

I think that the performance improvement is worth it

view this post on Zulip Mario Carneiro (Apr 08 2019 at 01:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 08 2019 at 02:12):

The proof is very combinatoric and constructive

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 08 2019 at 02:35):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 08 2019 at 06:04):

Type dependencies don't really come up here

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 08 2019 at 06:06):

Mario has written a "maths as programs" proof.

view this post on Zulip Kevin Buzzard (Apr 08 2019 at 06:08):

Maybe type theory itself isn't suited to combinatorics?

view this post on Zulip Kevin Buzzard (Apr 08 2019 at 06:08):

Would this all be easier in ZFC?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 08 2019 at 06:16):

It is most similar to Jeremy's proof

view this post on Zulip 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

view this post on Zulip 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