Stars and bars revisited

Stream: general

[Eric Wieser]

In #11162, we have a PR that claims to "prove" stars and bars.

However, I'd argue that "stars and bars" is really a tool for solving combinatorics problems, not a specific problem, which goes roughly as:

• Translate your problem into an analogous problem about stars and bars (by constructing an explicit isomorphism between your problem state, and a stars and bars type
• Solve the stars and bars problem

Do we want a stars_and_bars type?

[Eric Wieser]

Here's what such a type could look like:

import data.fintype.card
import data.fin.tuple
import data.fin.vec_notation

open_locale big_operators

inductive stars_and_bars : ℕ → ℕ → Type
| nil : stars_and_bars 0 0
| star {s b} (x : stars_and_bars s b) : stars_and_bars (nat.succ s) b
| bar {s b} (x : stars_and_bars s b) : stars_and_bars s (nat.succ b)

namespace stars_and_bars

def stars : Π {s b : ℕ}, stars_and_bars s b → Π s', stars_and_bars (s + s') b
| s b x 0 := x
| s b x (s' + 1) := (x.stars s').star

def bars : Π {s b : ℕ}, stars_and_bars s b → Π b', stars_and_bars s (b + b')
| s b x 0 := x
| s b x (b' + 1) := (x.bars b').bar

protected def repr_aux : Π {s b : ℕ}, stars_and_bars s b → string
| _ _ (nil)      := ""
| _ _ (star x) := "⋆" ++ repr_aux x
| _ _ (bar x) := "|" ++ repr_aux x

instance {s b : ℕ}  : has_repr (stars_and_bars s b) :=
⟨λ s, "(" ++ s.repr_aux ++ ")"⟩

end stars_and_bars

/-- Convert a `k`-tuple summing to `n` to a star and bar representation, by inserting bars
between the elements. -/
def tuple_to_stars_and_bars : Π {n : ℕ} {k : ℕ},
  {x : fin k.succ → ℕ // ∑ i, x i = n} → stars_and_bars n k
| n 0 ⟨f, rfl⟩ := by simpa using stars_and_bars.nil.stars (f 0)
| n (k + 1) ⟨f, hf⟩ := begin
  rw [fin.sum_univ_succ, add_comm] at hf,
  subst hf,
  exact (tuple_to_stars_and_bars ⟨fin.tail f, rfl⟩).bar.stars (f 0),
end

#eval tuple_to_stars_and_bars ⟨![2, 1, 3], (sorry : _ = 6)⟩  -- (⋆⋆|⋆|⋆⋆⋆)

[Eric Wieser]

PR'd as #13063

[Yaël Dillies]

What does it buy us exactly?

[Eric Wieser]

My hope was that translating to and from stars_and_bars would be a bit easier than it turned out to be

[Eric Wieser]

Unfortunately the equation compiler doesn't produce nice equation lemmas for this type

[Eric Wieser]

The main motivation was that it allows to you write "I'm going to argue this by stars and bars" in the lean code itself

[Julian Berman]

Imprecise question I'm sure, but if I can ask it anyhow, is a reasonable "generalization" of representing stars and bars finding a way to represent all of the twelvefold way (or the even-more-number-way-generalizations) of which stars and bars is one case? Or are all of those going to be vastly different anyhow?

[Kyle Miller]

@Julian Berman Just want to mention that the main result in the PR is to show that card (sym α k) = (card α + k - 1).choose k, which basically fits into the twelvefold way since sym α k may be regarded as the type of functions fin k -> α modulo permutations of the domain. There are lots of ways to represent functions between finite types, so whether this counts is subjective. (It would probably be nice to have a "direct" formalization of the twelvefold way, too.)

[Kyle Miller]

@Eric Wieser I'd like to see something like your variant of stars and bars, since that's the one I'm familiar with, and I agree that it could be useful to solve combinatorics problems. I don't think we should replace #11162 with it, though, since that one is (more or less) giving the cardinality of one of of the cases of the twelvefold way.

[Eric Wieser]

I definitely wasn't suggesting losing the results in #11162, just maybe actually using stars and bars in the proof somehow

[Eric Wieser]

I had a go at adding the additional result that actually motivated this thread in branch#eric-wieser/stars-and-bars-dependent-hell, that stars_and_bars s b ≃ {f : fin b.succ → ℕ // ∑ i, f i = s}. As the name of the branch suggest, I was not able to show the equivalence

[Kyle Miller]

Could you instead try showing it's equivalent to sym (fin b.succ) s? That's defined to be {m : multiset (fin b.succ) // m.card = s}.

[Kyle Miller]

I'm not sure if that's easier, but then what happens is #11162 would give you the cardinality of stars_and_bars.

[Eric Wieser]

The cardinality of stars_and_barsis already in the PR