Grace/Cumulus/NumberTheory/Binomial.g17

Open in Workbench Download source

Imports

Nat

Declarations

Source

1-- Binomial coefficients by Pascal's rule, and their factorial form2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.NumberTheory.Binomial8import Nat910-- The row n = 0 of Pascal's triangle: 1 at k = 0, then 0.11def chooseZero (k : Nat) → Nat12  | zero => 113  | succ(k) => 01415-- Pascal's rule at column k, given the two entries above it: the entry at16-- column 0 is 1, and the entry at column succ(j) is the sum of the entries at17-- columns j and succ(j) of the row above.18def pascalStep (k above left : Nat) → Nat19  | zero, above, left => 120  | succ(j), above, left => add(left, above)2122-- The number of k-element subsets of an n-element set, by Pascal's rule:23-- choose(n + 1, k + 1) = choose(n, k) + choose(n, k + 1).24def choose (n k : Nat) → Nat25  | zero, k => chooseZero(k)26  | succ(n), k => pascalStep(k, choose(n, k), choose(n, predecessor(k)))27  descends n2829-- The binomial coefficient is written n choose k; it binds more loosely30-- than +, so 2 * n + 1 choose k is the coefficient of 2n + 1.31notation infixl 55 "choose" => choose for Nat3233theorem choose.zero_right (n : Nat)34  shows choose(n, 0) = 135proof36  induction n37  | zero => compute38  | succ(k) using ih => settle with choose, pascalStep3940theorem choose.zero_left (k : Nat)41  shows choose(0, succ(k)) = 042proof43  simp [choose, chooseZero]4445theorem choose.succ_succ (n k : Nat)46  shows choose(succ(n), succ(k)) = choose(n, k) + choose(n, succ(k))47proof48  simp [choose, pascalStep, predecessor]4950-- Nothing is chosen above the diagonal.51theorem choose.above (n : Nat)52  shows ∀ k, Nat(k) → choose(n, n + succ(k)) = 053proof54  induction n55  | zero =>56    intros k kNat57    have shape : 0 + succ(k) = succ(k)58      exact add.left_unit at succ(k) with *59    rw shape60    exact choose.zero_left at k with *61  | succ(m) using ih =>62    intros k kNat63    have shape : succ(m) + succ(k) = succ(m + succ(k)) by ring64    rw [shape, choose.succ_succ]65    have first := ih with k, kNat66    have next : succ(m + succ(k)) = m + succ(succ(k)) by ring67    rw next68    have nextNat : Nat(succ(k)) by typecheck69    have second := ih with succ(k), nextNat70    rw [first, second]71    compute7273theorem choose.diagonal (n : Nat)74  shows choose(n, n) = 175proof76  induction n77  | zero => compute78  | succ(k) using ih =>79    rw [choose.succ_succ, ih]80    have zeroNat : Nat(0) by typecheck81    have above := choose.above at k with *82    have vanish := above with 0, zeroNat83    have shape : k + succ(0) = succ(k) by ring84    rw shape at vanish85    rw vanish86    compute8788-- One row of the factorial form: from row m to row succ(m), by induction on89-- the column.90theorem choose.factorial_row (m k : Nat)91  requires row : ∀ i, Nat(i) → choose(m + i, i) * (i! * m!) = (m + i)!92  shows choose(succ(m) + k, k) * (k! * succ(m)!) = (succ(m) + k)!93proof94  induction k95  | zero =>96    have shape : succ(m) + 0 = succ(m) by ring97    rw shape98    rw choose.zero_right99    have zero : 0! = 1 by compute100    rw zero101    ring102  | succ(j) using inner =>103    have shape : succ(m) + succ(j) = succ(succ(m) + j) by ring104    rw shape105    rw choose.succ_succ106    have swap : succ(m) + j = m + succ(j) by ring107    have right := row with succ(j), assumption108    have factorialSucc : ∀ t, Nat(t) → succ(t)! = succ(t) * t!109      intros t tNat110      settle with factorial111    have expandJ := factorialSucc with j, assumption112    have expandM := factorialSucc with m, assumption113    have expandTop := factorialSucc with succ(m) + j, assumption114    rw expandTop115    rw expandJ116    rw expandM117    rw expandM at inner118    rw expandJ at right119    rw ← swap at right120    have regroup : (choose(succ(m) + j, j) + choose(succ(m) + j, succ(j))) * ((succ(j) * j!) * (succ(m) * m!)) = succ(j) * (choose(succ(m) + j, j) * (j! * (succ(m) * m!))) + succ(m) * (choose(succ(m) + j, succ(j)) * ((succ(j) * j!) * m!))121      ring122    rw regroup123    rw inner124    rw right125    ring126127-- Pascal's rule and the factorial form agree: choose(n + k, k) · k! · n! = (n + k)!.128theorem choose.factorial (n : Nat)129  shows ∀ k, Nat(k) → choose(n + k, k) * (k! * n!) = (n + k)!130proof131  induction n132  | zero =>133    intros k kNat134    have shape : 0 + k = k135      exact add.left_unit at k with *136    rw [shape, choose.diagonal]137    have zero : 0! = 1 by compute138    rw zero139    ring140  | succ(m) using ih =>141    intros k kNat142    exact choose.factorial_row at m, k with *143