Small examples involving binomial coefficients
[newbies recursion examples Isar Fibonacci The binomial coefficients, which appear in the binomial theorem, have numerous applications in combinatorics and the analysis of algorithms. Donald E Knuth wrote extensively about them in the book Concrete Mathematics. They are the elements of Pascal’s triangle and satisfy a great many mathematical identities. Let’s prove some of them using Isabelle/HOL. These and many more are available built-in.
Warming up
Let’s recall the definition of the binomial coefficient “n choose k”, which denotes how many k-element subsets can be chosen from an n-element set:
\[\begin{gather*} \binom{n}{k} = \frac{n!}{k!(n-k)!}. \end{gather*}\]There follow a number of trivial properties, such as
\[\begin{gather*} (n-k)\binom{n}{k} = n\binom{n-1}{k}. \end{gather*}\]Slightly deeper is the following claim, that the sum of a row of Pascal’s triangle is a power of 2:
\[\begin{gather*} \sum_{k\le n} \binom{n}{k} = 2^n. \end{gather*}\]It’s trivial for us to prove because the binomial theorem—already available in Isabelle/HOL—expresses $(x+y)^n$ in terms of binomial coefficients. We can express the desired sum by putting $x=y=1$ in that theorem. Observe the syntax for instantiating variables in a theorem.
lemma choose_row_sum: "(∑k≤n. n choose k) = 2^n" using binomial [of 1 1 n] by (simp add: numeral_2_eq_2)
Many other identities are trivial inductions. These two are hardly worth a discussion.
lemma sum_choose_lower: "(∑k≤n. (r+k) choose k) = Suc (r+n) choose n" by (induction n) auto
lemma sum_choose_upper: "(∑k≤n. k choose m) = Suc n choose Suc m" by (induction n) auto
Manipulating a summation
The following little identity does not require induction, since it uses one of the identities just proved. But its first step is a little tricky: the index variable, $k$, is replaced by $m-k$. Such manipulations frequently require the user to tear out their hair.
lemma sum_choose_diagonal: assumes "m≤n" shows "(∑k≤m. (n-k) choose (m-k)) = Suc n choose m" proof - have "(∑k≤m. (n-k) choose (m-k)) = (∑k≤m. (n-m+k) choose k)" using sum.atLeastAtMost_rev [of "λk. (n - k) choose (m - k)" 0 m] by (simp add: atMost_atLeast0 ‹m≤n›) also have "… = Suc (n-m+m) choose m" by (rule sum_choose_lower) also have "… = Suc n choose m" using assms by simp finally show ?thesis . qed
Proving the subset of a subset identity
Intuitively, the identity $\binom{n}{m} \binom{m}{k} = \binom{n}{k} \binom{n-k}{m-k}$ concerns the number of ways to choose $k$ elements out of $m$ elements that were originally chosen out of $n$. It’s equivalent to the number of ways of immediately choosing $k$ out of $n$ times the number of ways of choosing the leftover $m-k$ elements out of the original, unwanted $n-k$ elements. Or something. Such intuitive arguments are a nightmare to formalise, but fortunately this proof is a fairly simple calculation.
It relies on a basic divisibility property: that $k!(n-k)!$ divides $n!$ provided $k\le n$. The divisor is precisely $\binom{n}{k}$, a fact proved in the main library. (And it doesn’t follow from the definition of $\binom{n}{k}$, but rather justifies that definition.)
Now we can prove our identity by expressing binomial coefficients in terms of factorials. It’s just a chain of identities, called in Isar a calculational proof.
lemma choose_mult_lemma: "((m+r+k) choose (m+k)) * ((m+k) choose k) = ((m+r+k) choose k) * ((m+r) choose m)" (is "?lhs = _") proof - have "?lhs = fact(m+r+k) div (fact(m+k) * fact(m+r-m)) * (fact(m+k) div (fact k * fact m))" by (simp add: binomial_altdef_nat) also have "… = fact(m+r+k) * fact(m+k) div (fact(m+k) * fact(m+r-m) * (fact k * fact m))" by (metis add_implies_diff add_le_mono1 choose_dvd diff_cancel2 div_mult_div_if_dvd le_add1 le_add2) also have "… = fact(m+r+k) div (fact r * (fact k * fact m))" by (auto simp: algebra_simps fact_fact_dvd_fact) also have "… = (fact(m+r+k) * fact(m+r)) div (fact r * (fact k * fact m) * fact(m+r))" by simp also have "… = (fact(m+r+k) div (fact k * fact(m+r)) * (fact(m+r) div (fact r * fact m)))" by (smt (verit) fact_fact_dvd_fact div_mult_div_if_dvd mult.assoc mult.commute) finally show ?thesis by (simp add: binomial_altdef_nat mult.commute) qed
Above, we avoided subtraction in favour of addition, a trick that frequently simplifies our work. Now it’s trivial to derive the “subset of a subset” identity in its traditional form, $\binom{n}{m} \binom{m}{k} = \binom{n}{k} \binom{n-k}{m-k}$.
lemma choose_mult: "k ≤ m ⟹ m ≤ n ⟹ (n choose m) * (m choose k) = (n choose k) * ((n - k) choose (m - k))" using choose_mult_lemma [of "m-k" "n-m" k] by simp
An easy tricky proof
In Concrete Mathematics, the authors remark
There is a way to partially sum the row elements [of Pascal’s triangle] if they have been multiplied by their distance from the centre.
They give the following formula (numbered 5.18):
\[\begin{gather*} \sum_{k\le m}\binom{r}{k}\left(\frac{r}{2}-k\right) = \frac{m+1}{2}\binom{r}{m+1}. \end{gather*}\]And they remark, “this formula is easily verified by induction on m”. Dangerous words. They certainly provoked me to try formulaic induction/simplification steps that exploded the formula into chaos. When that happens, it’s best to try to work out the steps on paper first. I eventually arrived at the following, which quite possibly is the proof they omitted.
lemma choose_row_sum_weighted: "(∑k≤m. (r choose k) * (r/2 - k)) = (Suc m)/2 * (r choose (Suc m))" proof (induction m) case 0 show ?case by simp next case (Suc m) have "(∑k≤Suc m. real (r choose k) * (r/2 - k)) = ((r choose Suc m) * (r/2 - (Suc m))) + (Suc m) / 2 * (r choose Suc m)" by (simp add: Suc) also have "… = (r choose Suc m) * (real r - (Suc m)) / 2" by (simp add: field_simps) also have "… = Suc (Suc m) / 2 * (r choose Suc (Suc m))" proof (cases "r ≥ Suc m") case True with binomial_absorb_comp[of r "Suc m"] show ?thesis by (metis binomial_absorption mult.commute of_nat_diff of_nat_mult times_divide_eq_left) qed (simp add: binomial_eq_0) finally show ?case . qed
I can’t help but remark that with Certain Other Proof Assistants, working out the proof first on paper is standard practice. Then what value are they getting from their so-called assistant?
An identity involving Fibonacci numbers
Every time you turn around, the Fibonacci numbers pop up again:
\[\begin{gather*} \sum_{k\le m}\binom{n-k}{k} = F_{n+1} \end{gather*}\]We’ve seen Fibonacci numbers in a previous post. Isabelle accepts the recursive definition,
\[\begin{align} F_0 &= 0\\ F_1 &= 1\\ F_{n+2} &= F_n + F_{n+1}, \end{align}\]We have also seen that when you have to prove something about a recursive function, it’s often best to use the induction rule that Isabelle supplies with your function definition. And that is the case here.
First, we need a couple of trivial lemmas to let us adjust the upper bound of the sum, deleting a null term and shifting everything down.
lemma sum_drop_zero: "(∑k≤Suc n. if 0<k then (f (k - 1)) else 0) = (∑j≤n. f j)" by (induction n) auto
lemma sum_choose_drop_zero: "(∑k≤Suc n. if k = 0 then 0 else (Suc n - k) choose (k - 1)) = (∑j≤n. (n-j) choose j)" by (rule trans [OF sum.cong sum_drop_zero]) auto
Armed with this fact, the identity is easy to prove.
lemma ne_diagonal_fib: "(∑k≤n. (n-k) choose k) = fib (Suc n)" proof (induction n rule: fib.induct) case 1 show ?case by simp next case 2 show ?case by simp next case (3 n) have "(∑k≤Suc n. Suc (Suc n) - k choose k) = (∑k≤Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))" by (rule sum.cong) (simp_all add: choose_reduce_nat) also have "… = (∑k≤Suc n. Suc n - k choose k) + (∑k≤Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))" by (simp add: sum.distrib) also have "… = (∑k≤Suc n. Suc n - k choose k) + (∑j≤n. n - j choose j)" by (metis sum_choose_drop_zero) finally show ?case using 3 by simp qed
Postscript
As usual, the Isabelle theory is available to download.
Knuth notes that we can generalise binomial coefficients so that the top number is real or complex. This generalisation (accomplished via type classes) is also available in Isabelle/HOL.
There’s even an introduction to binomial coefficients aimed at younger mathematicians.