Stars and bars

Stream: maths

[Yaël Dillies]

Do you think we could get a version of stars and bars that looks like that?

lemma stars_and_bars {α : Type*} [fintype α] (n : ℕ) :
  card (sym α n) = (card α + n - 1).choose (card α) := sorry

My idea is to show the equivalence between sym and sym'' where

def sym'' {α : Type*} [fintype α] (n : ℕ) : Type* :=
{s : list (option α) // s.length = card α + n - 1 ∧ (s.filter (λ x, x = none)).length = n - 1}

The some a in the list represent stars and the none represent bars.
And then hopefully we can show card sym'' α n = (card α + n - 1).choose (card α) by simultaneous induction on α and n.

[David Wärn]

This sym'' looks too big -- you want the stars to be indistinguishable. I think the right thing to do is prove the theorem only for fin n, where you can say that multisets correspond to sorted lists. Then construct a bijection between sorted lists and "binary vectors" (the thing that nat.choose counts). At least this is the stars-and-bars proof, there might be another proof more amenable to formalisation.

[Mario Carneiro]

What is sym? #mwe

[Mario Carneiro]

docs#sym

[Yaël Dillies]

David Wärn said:

This sym'' looks too big -- you want the stars to be indistinguishable.

Whoops, right.