The goal of this lecture note is to formalize binomial coefficients, which are listed in the successive lines of Pascal’s triangle:
1
1 1
1 2 1
1 3 3 1
1 4 6 4 1
1 5 10 10 5 1
1 6 15 20 15 6 1
1 7 21 35 35 21 7 1
1 8 28 56 70 56 28 8 1
...
As a warmup exercise – and based on your understanding of binomial coefficients – implement a function that given two Peano numbers, computes the corresponding binomial coefficient:
binomial_coefficient : nat -> nat -> nat
So please stop reading this chapter and don’t look at its resource file, this exercise is an introspective one about what you already know and how actionable it is.
Halcyon: Again with our personal journey.
Pablito: I think we should implement a recursive function.
On the left edge of Pascal’s triangle, all numbers are 1; outside (i.e., on the right of the right edge), they are 0; and inside (including the right edge), they are regulated by Pascal’s rule:
Definition specification_of_binomial_coefficient (binomial_coefficient : nat -> nat -> nat) :=
(forall n : nat,
binomial_coefficient n 0 = 1)
/\
(forall k' : nat,
binomial_coefficient 0 (S k') = 0)
/\
(forall n' k' : nat,
binomial_coefficient (S n') (S k') = binomial_coefficient n' k' + binomial_coefficient n' (S k')).
Pablito: Hum.
Bong-sun: Yes, Pablito?
Pablito: Is it really Pascal’s rule? I mean look at the fourth conjunct:
forall n' k' : nat,
binomial_coefficient (S n') (S k') = binomial_coefficient n' k' + binomial_coefficient n' (S k')
Pablito (continuing): Using the same notation, here Pascal’s rule as found somewhere on the web:
forall n : nat,
0 < n ->
forall k : nat,
0 <= k ->
k <= n ->
binomial_coefficient n k = binomial_coefficient (n - 1) (k - 1) + binomial_coefficient (n - 1) k
Bong-sun: Our specification hardwires the condition 0 < n by quantifying n' and using S n'.
Pablito: Right, and I do get that. But what about k?
Bong-sun: What about k? It comes with conditions, whereas our specification quantifies k' and uses S k'. Same same.
Pablito (vigilant): But what if k is 0?
Bong-sun: Well spotted, Pablito. Pascal’s rule only holds if k is positive, and so what you found online should read:
forall n : nat,
0 < n ->
forall k : nat,
0 < k ->
k <= n ->
binomial_coefficient n k = binomial_coefficient (n - 1) (k - 1) + binomial_coefficient (n - 1) k
Pablito: OK, thanks. And what about the other condition, k <= n?
Dana: The case n < k is treated in Exercise 13. Outside Pascal’s triangle, all numbers are 0, which is consistent with Pascal’s rule.
Being online doesn’t necessarily mean being correct.
In the accompanying .v file, test_binomial_coefficient exploits the first six lines of Pascal’s triangle and test_binomial_coefficient' tests numbers outside Pascal’s triangle.
The following implementation maps two numbers n and k to the corresponding binomial coefficient. It is defined recursively on its first argument and by cases on its second:
Fixpoint binomial_coefficient (n k : nat) : nat :=
match n with
O =>
match k with
O =>
1
| S k' =>
0
end
| S n' =>
match k with
O =>
1
| S k' =>
binomial_coefficient n' k' + binomial_coefficient n' (S k')
end
end.
Prove that binomial_coefficient satisfies the specification of binomial coefficients:
Proposition binomial_coefficient_satisfies_the_specification_of_binomial_coefficient :
specification_of_binomial_coefficient binomial_coefficient.
Prove that outside Pascal’s triangle, the binomial coefficients are 0:
Property about_binomial_coefficients_n_more_than_n :
forall n k : nat,
n < k <-> binomial_coefficient n k = 0.
Prove that on the right edge of Pascal’s triangle, the binomial coefficients are 1:
Property about_binomial_coefficients_n_n :
forall n : nat,
binomial_coefficient n n = 1.
Hint: The lemma proved in Exercise 13 might come handy.
Prove that on the left edge of Pascal’s triangle, the binomial coefficients are 1:
Property about_binomial_coefficients_n_0 :
forall n : nat,
binomial_coefficient n 0 = 1.
Prove the following property of the second left layer of Pascal’s triangle:
Property about_binomial_coefficients_n_1 :
forall n : nat,
binomial_coefficient n 1 = n.
Prove the following property of the second right layer of Pascal’s triangle:
Property about_binomial_coefficients_Sk_k :
forall k : nat,
binomial_coefficient (S k) k = S k.
Prove that each line in Pascal’s triangle is a palindrome:
Property about_binomial_of_sums :
forall a b : nat,
binomial_coefficient (a + b) a = binomial_coefficient (a + b) b.
Prove the following property:
- Property another_square :
- forall n : nat,
- n * n = n + 2 * binomial_coefficient n 2.
Added Exercise 19 and an executive summary after the interlude [15 Jun 2025]
Tightened the specification [04 Apr 2025]
Created [31 Mar 2025]