Proof review: Sum of nCk over antidiagonal = Fibonacci

Question

Theorem to prove:

The sum of the binomial coefficients over an antidiagonal is a Fibonacci number. More specifically, the $n$th antidiagonal sums to the $n+1$th Fibonacci number, where the antidiagonal is counted from zero and the Fibonacci sequence starts with $F_0 = 0$ and $F_1 = 1$.

$$ \forall\, n \in \mathbb{N}, \quad \sum_{i=0}^{n}{{i}\choose{n-i}} = F_{n+1} $$

(from this code golf challenge)

Image source: Math is Fun - Pascal's triangle

By digging through the mathlib I could formulate this equality as the following:

theorem antidiagonal_choose_sum_is_fib (n : ℕ) :
  ((list.nat.antidiagonal n).map (function.uncurry nat.choose)).sum
  = n.succ.fib

with the proof:

import data.nat.choose.basic
import data.nat.fib
import data.list.defs
import data.list.nat_antidiagonal

lemma fib_ind : forall (P : ℕ -> Prop) (p0 : P 0) (p1 : P 1) (pss : forall m : ℕ, P m -> P m.succ -> P m.succ.succ), forall n : ℕ, P n :=
begin
  intros P p0 p1 pss n,
  have pns : P n /\ P n.succ,
  induction n, tauto, tauto, tauto
end

lemma sum_zip : forall (f g : ℕ -> ℕ) (l : list ℕ), (list.map f l).sum + (list.map g l).sum = (list.map (λx, f x + g x) l).sum :=
begin
  intros, induction l,
  simp,
  simp, rw <- l_ih, ring,
end

lemma sum_eq_elementwise : forall (f g : ℕ -> ℕ) (l : list ℕ), (forall x, x ∈ l -> f x = g x) -> (list.map f l).sum = (list.map g l).sum :=
begin
  introv, induction l,
  simp,
  intro h, simp, rw h l_hd, rw l_ih,
    introv mem_tl, apply h, simp, tauto,
    simp,
end

theorem antidiagonal_choose_sum_is_fib (n : ℕ) :
  ((list.nat.antidiagonal n).map (function.uncurry nat.choose)).sum
  = n.succ.fib :=
begin
  induction n using fib_ind with n_m n_ind0 n_ind1,
  simp,
  simp,
  rw nat.fib_add_two, rw nat.add_one, rw <- n_ind0, rw <- n_ind1,
  unfold list.nat.antidiagonal, simp, repeat {rw nat.add_one},
  rw list.sum_range_succ, rw list.sum_range_succ', rw list.sum_range_succ _ (n_m.succ), simp,
  rw <- add_assoc, rw sum_zip, simp, apply sum_eq_elementwise,
  introv in_range, rw list.mem_range at in_range, have le_n_m := nat.succ_sub (nat.le_of_lt_succ in_range),
  rw le_n_m, apply nat.choose_succ_succ
end

Online demo is here.

Proof outline:

Theorem: $ \forall\, n \in \mathbb{N}, \quad \sum_{i=0}^{n}{{i}\choose{n-i}} = F_{n+1} $.

Use Fibonacci induction.

For $n = 0$ and $n = 1$, use direct evaluation.

For $n = k+2$, assume the equation holds for $n = k$ and $n = k+1$.

Expand $F_{k+3}$ once and substitute the two equations to get $$ \sum_{i=0}^{k+2}{{i}\choose{k+2-i}} = \sum_{i=0}^{k}{{i}\choose{k-i}} + \sum_{i=0}^{k+1}{{i}\choose{k+1-i}} $$

Chop off the first and last terms of the leftmost summation and the last of the rightmost one to get $$ \sum_{i=0}^{k}{{i+1}\choose{k+2-(i+1)}} + {{0}\choose{k+2}} + {{k+2}\choose{0}} = \sum_{i=0}^{k}{{i}\choose{k-i}} + \sum_{i=0}^{k}{{i}\choose{k+1-i}} + {{k+1}\choose{0}} $$

Constant terms evaluate to 1.

Handle the sums element-wise: $$ \forall\, 0 \le i \le k, \quad {{i+1}\choose{k+1-i}} = {{i}\choose{k-i}} + {{i}\choose{k+1-i}} $$

which follows from the identity of Choose.

As a proof review question, any advice to improve the proof is appreciated, including but not limited to:

• a possible better formulation of the theorem
• a possible better translation of the hand-written proof
• a suggestion for a more readable formal proof
• naming of lemmas and theorems (I'm aware that a naming convention exists in mathlib, but I'm not quite sure how it works)
• possible use of better lemmas in the course of the proof (is a more general lemma or a more specific lemma better?)

Answer 1

I'll first go through piece-by-piece and suggest some local improvements.

For the induction principle, when you find yourself doing intros as the first step of a tactic proof, you should strongly consider putting arguments "before the colon" rather than leaving them within universal quantifiers. Another thing is that when you have multiple goals (for example, as produced by have or induction) it is good practice to use curly braces to focus on the goal -- that way when the proof breaks you can more easily figure out what needs fixing. And, a tip: if you are using the same tactic on each goal produced by a tactic, you can use the ; operator.

lemma fib_ind (P : ℕ → Prop)
  (p0 : P 0) (p1 : P 1) (pss : ∀ m : ℕ, P m → P m.succ → P m.succ.succ) (n : ℕ) : P n :=
begin
  have pns : P n /\ P n.succ,
  { induction n; tauto },
  tauto,
end

For naming, we can refer to mathlib itself: it's nat.two_step_induction, so we can replace the tactic proof with the term nat.two_step_induction p0 p1 pss n. Note: the P argument would more commonly be given as an implicit argument.

The next lemma gets a similar treatment, but, with list.map, you can make use of dot notation: l.map f means "since l has type list, use list.map and have l be its first list argument." Since this lemma is about a homomorphism property, I think it would normally be written with the equality flipped, and for naming, this might be unnecessarily long, but sum_map_apply_add_apply would work (one way mathlib names arise is to read off relevant parts of the in-order traversal of the abstract syntax tree). Also, non-terminal simps should be avoided, since if the simp set later changes, you can have a hard time fixing a proof. I used squeeze_simp to figure out which lemmas it was using, and I inserted *, which means "and rewrite using hypothesis from the local context."

lemma sum_map_apply_add_apply (f g : ℕ → ℕ) (l : list ℕ) :
  (l.map (λ x, f x + g x)).sum = (l.map f).sum + (l.map g).sum  :=
begin
  induction l,
  { simp, },
  { simp only [list.sum_cons, list.map, *],
    ring, },
end

However, searching the documentation for "list sum map add", I came across multiset.sum_map_add. The proof in the source code (after interpreting what the to_additive attribute does) essentially carries over to lists. After generalizing it appropriately, this should probably find its way into mathlib:

lemma list.sum_map_add {ι α : Type*} [add_comm_monoid α] {f g : ι → α} (l : list ι) :
  (l.map (λ x, f x + g x)).sum = (l.map f).sum + (l.map g).sum  :=
list.sum_hom₂ _ _ add_add_add_comm (add_zero _) _ _

The next lemma boils down to the fact that l.map f = l.map g (a congruence lemma), so searching for "list map congr" I got this:

lemma sum_eq_elementwise (f g : ℕ → ℕ) (l : list ℕ) (h : ∀ x, x ∈ l → f x = g x) :
  (l.map f).sum = (l.map g).sum :=
begin
  rw list.map_congr h,
end

For the main theorem, there is a lot of unfolding of definitions. It's better to encapsulate those into some additional lemmas, since mathlib style is to try to avoid relying on definitions unless they're considered part of the interface (this isn't always clear). Two lemmas that seem useful are for popping terms off the front and back of the antidiagonal:

lemma list.nat.antidiagonal_succ' (n : ℕ) :
  list.nat.antidiagonal (n + 1) =
  ((list.nat.antidiagonal n).map (prod.map id nat.succ)) ++ [(n + 1, 0)] :=
begin
  simp only [list.nat.antidiagonal, list.range_succ, add_tsub_cancel_left, list.map_append,
    list.append_assoc, tsub_self, list.singleton_append, list.map_map, list.map],
  congr' 1,
  apply list.map_congr,
  simp [le_of_lt, nat.succ_eq_add_one, nat.sub_add_comm] { contextual := tt },
end

lemma list.nat.antidiagonal_succ_succ' (n : ℕ) :
  list.nat.antidiagonal (n + 2) =
  (0, n + 2) :: ((list.nat.antidiagonal n).map (prod.map nat.succ nat.succ)) ++ [(n + 2, 0)] :=
begin
  induction n with n ih,
  { refl, },
  { rw [nat.succ_add, list.nat.antidiagonal_succ, ih],
    simpa, },
end

In these, I'm (somewhat) misusing a feature of simpa, which is that it basically tries refl at the end. (These lemmas should also probably find their way into mathlib, but I'm not too familiar with the list antidiagonal functions. Edit: mathlib#12028 and mathlib#12029)

With these, we can simplify the main proof. I flipped the equality because I imagine that the main use would be to take existing fibonacci numbers and rewrite them into this other form. I also changed n.succ to n + 1 since that tends to be the normal form for arithmetic expressions. By the way, it's common to open function, so uncurry doesn't need to be fully qualified.

theorem fib_eq_sum_choose_antidiagonal (n : ℕ) :
  (n + 1).fib = ((list.nat.antidiagonal n).map (uncurry nat.choose)).sum :=
begin
  induction n using nat.two_step_induction with n h0 h1,
  { refl, },
  { refl, },
  rw [nat.fib_add_two, h0, h1, list.nat.antidiagonal_succ_succ', list.nat.antidiagonal_succ'],
  simpa [←add_assoc, ←list.sum_map_add, uncurry, ←nat.choose_succ_succ],
end

---

Now that we've gone through everything, let's put it all together. We have three lemmas that arguably should be in mathlib already, and then your proof is pretty close to what you said in your outline:

import data.nat.choose.basic
import data.nat.fib
import data.list.defs
import data.list.nat_antidiagonal

open function

lemma list.sum_map_add {ι α : Type*} [add_comm_monoid α] {f g : ι → α} (l : list ι) :
  (l.map (λ x, f x + g x)).sum = (l.map f).sum + (l.map g).sum  :=
list.sum_hom₂ _ _ add_add_add_comm (add_zero _) _ _

lemma list.nat.antidiagonal_succ' (n : ℕ) :
  list.nat.antidiagonal (n + 1) =
  ((list.nat.antidiagonal n).map (prod.map id nat.succ)) ++ [(n + 1, 0)] :=
begin
  simp only [list.nat.antidiagonal, list.range_succ, add_tsub_cancel_left, list.map_append,
    list.append_assoc, tsub_self, list.singleton_append, list.map_map, list.map],
  congr' 1,
  apply list.map_congr,
  simp [le_of_lt, nat.succ_eq_add_one, nat.sub_add_comm] { contextual := tt },
end

lemma list.nat.antidiagonal_succ_succ' (n : ℕ) :
  list.nat.antidiagonal (n + 2) =
  (0, n + 2) :: ((list.nat.antidiagonal n).map (prod.map nat.succ nat.succ)) ++ [(n + 2, 0)] :=
begin
  induction n with n ih,
  { refl, },
  { rw [nat.succ_add, list.nat.antidiagonal_succ, ih],
    simpa, },
end

theorem fib_eq_sum_choose_antidiagonal (n : ℕ) :
  (n + 1).fib = ((list.nat.antidiagonal n).map (uncurry nat.choose)).sum :=
begin
  induction n using nat.two_step_induction with n h0 h1,
  { refl, },
  { refl, },
  rw [nat.fib_add_two, h0, h1, list.nat.antidiagonal_succ_succ', list.nat.antidiagonal_succ'],
  simpa [←add_assoc, ←list.sum_map_add, uncurry, ←nat.choose_succ_succ],
end

---

All that said, using lists isn't the usual way you work with sums in mathlib. Instead, you work with finset and the "big operators." Contingent on the mathlib PR for manipulating antidiagonals, the theorem ends up being just this:

import data.finset.nat_antidiagonal
import data.nat.fib
import algebra.big_operators.basic

open_locale big_operators
open finset

theorem fib_eq_sum_choose_antidiagonal (n : ℕ) :
  (n + 1).fib = ∑ p in nat.antidiagonal n, nat.choose p.1 p.2 :=
begin
  induction n using nat.two_step_induction with n h0 h1,
  { refl, },
  { refl, },
  rw [nat.fib_add_two, h0, h1, nat.antidiagonal_succ_succ', nat.antidiagonal_succ'],
  simp [nat.choose_succ_succ, add_assoc, add_left_comm, sum_add_distrib],
end

After doing the basic manipulations you described in your proof outline, simp ends up doing the heavy lifting. An interesting thing about this tactic is that it's able to put things into a normal form even if the lemmas can potentially form rewrite loops. The add_assoc and add_left_comm lemmas here are giving simp the capability of sorting the additions, as a weak kind of ring. (Usually you'd include add_comm, too, but it wasn't necessary here.)