Counting in two ways

Question

I’ve been thinking lately about counting-in-two-ways proofs.

For example, we can prove the identity $$2^n = \sum_{k=0}^n \binom n k$$ just by noting these are just two ways to count the number of subsets of an $n$ element set. The left-hand-side corresponds to building a subset by independently choosing whether each of the $n$ elements is in the set. The right-hand-side corresponds to building a subset by first choosing the size $k$ of the set and then choosing which of the $\binom n k$ possible $k$-element subsets it is. This is just one example of a very powerful proof method.

While there is no doubt this is a rigorous proof, it doesn’t seem immediately obvious how to formalize such proofs in a way which is true to the spirit of counting in two ways (and ideally as easy to write down once one has build up basic tools for counting finite sets).

Has anyone put in significant effort into formalizing counting-in-two-ways proofs?

If so what has been learned from the exercise?

Answer 1

One lesson may be that not all proofs are meant to be formalized. The gap between an informal proof and a formal proof is often substantial, and you could reasonably treat this as an extreme instance of that phenomenon. Counting in two ways gives you an informal starting point. You can gradually refine it into a fully algebraic proof that is then straightforward to formalize, rather than come up with that latter proof from scratch.

But maybe you don't trust what random strangers on the internet tell you. You have to suffer through the pain of doing combinatorics in type theory yourself to learn a lesson. Let's start by saying that "counting" the number of elements in a set $A$ is to establish an equivalence of types, or pardon my French, a bijection $A = \overline{n}$, where $\overline{n}$ is the prototypical set with $n$ elements, $\overline{n} {\;:=} \left\{m \in \mathbb{N} \mid m < n \right\}$. Thus, counting $A$ is to establish a correspondence between $A$ and some reference set of numbers $0\dots n-1$. We can pun bijections and equality thanks to univalence, but all of this is also formalizable in non-univalent type theories by not interpreting the $=$ between types literally as equality.

Counting $A$ in two ways is to find two equivalences $A = \overline{n}$ and $A = \overline{m}$, which lets us conclude the equality between natural numbers $n = m$ via transitivity and a theorem which is really fun to prove:

$${\textrm{inj-fin}} : \overline{n} = \overline{m} \to n = m$$

Refining the idea further, we could also say that counting the same set in two ways is to give two equivalent descriptions of it, as different sequences of choices, each corresponding to a different type leading to different expressions for their cardinalities. $A = B$, $A = \overline{n}$, and $B = \overline{m}$, implying $n = m$.

Here the power $2^n$ is encoded by vectors of $n$ booleans $\mathbf{2}$:

$${\textrm{card-pow}} : \mathbf{2}^n = \overline{2^n}$$

and the binomial coefficient ${n}\choose{k}$ is encoded by those vectors with $k$ ones:

$${\textrm{card-choose}} : \left\{v \in \mathbf{2}^n \mid \left|v\right|_1 = k \right\} = \overline{{n}\choose{k}}$$

So we can count the powerset either via its canonical cardinality $2^n$, or via a bijection to the sum of binomial coefficients:

$${\textrm{power2choose}} : \mathbf{2}^n = \sum_{k \leq n} \left\{v \in \mathbf{2}^n \mid \left|v\right|_1 = k \right\}$$

The final theorem follows from the above facts and the equivalence between sums of types and sums of cardinalities:

$${\textrm{card-sum}} : (\forall i\leq n, f(i) = \overline{g(i)}) \to \sum_{k\leq n} f(k) = \overline{\sum_{k \leq n} g(k)}$$

yielding

$${\textrm{binomial-sum}} : 2^n = \sum_{k\leq n} {n\choose k}$$

Now we have all the pieces in place, we can see that most of the work in the informal "count in two ways" proof of that final identity really happens in the theorem $\textrm{power2choose}$, a bijection between two types. The direct construction is left as an exercise; it either ends up being a mess or as a disguised version of the purely algebraic proof.

But there is one more idea in the informal proof that we can formalize, which is that the binomial coefficients represent a partition of the powerset, indexed by the size of the subsets. We can refactor that idea into one more theorem, equating a set with the sum of its fibers:

$$\textrm{partition} : \forall A, \forall B, \forall f : A \to B, A = \sum_{b : B} \left\{ a : A \mid f(a) = b \right\}$$

Contemplate the resemblance with $\textrm{power2choose}$.

To summarize everything, a lot of sightseeing, but maybe not the shortest path from point A to point B.

But if we have a short path and a long path, why not consider the short one as as shortcut over the longer one? By turning the "count in two ways" argument on its head, we can use an algebraic identity in $\mathbb{N}$ to construct an otherwise complex bijection, via the converse of $\textrm{inj-fin}$:

$$\textrm{cong} : n = m \to \overline{n} = \overline{m}$$

This is perhaps another lesson. The $\textrm{binomial-sum}$ gives us the $\textrm{power2choose}$.

Answer 2

I see the work on Combinatorial Species as being a vast generalization of that. The various series associated to a species give you different kinds of ways of counting.

The example worked out in full detail in the answer by Lia-yao Xia is the kind of thing that can be abstract to the level of Species. See the book Combinatorial Species and Tree-like Structures for much more.

Answer 3

Here's a connection with some existing work in type theory. Consider this inductive type, whose values are meant to correspond to finite subtypes of an $n$-valued type:

data Sub : ℕ → Set where
  base : Sub 0
  take : Sub n → Sub (suc n)
  drop : Sub n → Sub (suc n)

Now, consider a type for identifying a size-$m$ subtype of a size-$n$ type. Note that values of, say, $Σ\ (\mathsf{Fin}\ m → \mathsf{Fin}\ n)\ \mathsf{Injective}$ do not uniquely identify such things, so you actually need a more canonical representation (or quotient) if you want that:

data Choose_from_ : ℕ → ℕ → Set where
  base : Choose 0 from 0
  take : Choose m from n → Choose suc m from suc n
  drop : Choose m from n → Choose     m from suc n

Now, it's pretty easy to prove that $\mathsf{Sub}\ n$ is equivalent to $Σ_{m : ℕ} (\mathsf{Choose}\ m\ \mathsf{from}\ n)$. However, you likely don't even need a proof to believe that, because these data declarations are exactly the same except for the indexing.

So, one idea you might have is that you shouldn't even need to write these identical-with-different-indexing data declarations. It should just be possible to somehow derive one from the other, and we could automatically recognize that they are equivalent. This is the sort of idea explored in Ornamental Algebras, Algebraic Ornaments, by Conor McBride (from the comments), and subsequent work (a lot of which seems to involve Pierre-Evariste Dagand).

This realization is also easily seen in categorical meanings of dependent types. If you imagine these indexed families are represented by display maps like $\mathsf{Total} → \mathsf{Index}$, then it's pretty straight forward to notice that both $\mathsf{Sub}$ and $\mathsf{Choose\_from\_}$ can be represented using the same total space—finite binary sequences. You get $\mathsf{Sub}$ by using $\mathsf{length} : \mathsf{Bin} → ℕ$ as the display map, and $\mathsf{Choose\_from\_}$ by using $\langle \mathsf{length}, \mathsf{popcount} \rangle : \mathsf{Bin} → ℕ × ℕ$ (where $\mathsf{popcount}$ counts the number of 1 bits). Then it is straight forward that composing the latter with the first projection ($π_1$) gives the former, but post-composition by $π_1$ is the categorical semantics of $Σ$ for these sorts of display maps.

I'm not aware of any proof assistants that have tried to build around ornaments more seriously. That may just be lack of my knowledge, though.

Oh, also, the above of course leaves out anything relating these purpose-built types back to $\mathsf{Fin} (2^n)$ and $\mathsf{Fin} {n \choose k}$ which I think is the much harder part. As I said, it's really easy to prove the specialized types are equivalent, while showing they are equivalent to $\mathsf{Fin}\ N$ involves a lot of fiddly arithmetic. The equivalence for $n \choose k$ in particular seems like it could be a lot of work. It's easy to come up with a recursive formula that would match the number of values of $\mathsf{Choose}\ k\ \mathsf{from}\ n$, but that doesn't resemble the usual definition as a ratio of naturals that happens to be a natural.