Counting & logic

Combinations & Pascal’s rule

A recursive program mirrors the two cases in a combinatorial proof.

-- Top 100 #58: Combinations & Pascal’s rule
-- History: First discovery date unknown.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: Partition choices according to whether they contain one distinguished element.
-- Scope: Implements Pascal’s recurrence and proves its defining step plus concrete counts. The factorial formula and set-counting interpretation are not formalized.
-- Source: https://lurch.plus/100/

def choose : Nat → Nat → Nat
  | _, 0 => 1
  | 0, _+1 => 0
  | n+1, k+1 => choose n k + choose n (k+1)

theorem pascal (n k : Nat) :
    choose (n+1) (k+1) = choose n k + choose n (k+1) := by
  rfl

example : choose 5 2 = 10 := by decide
#eval (List.range 7).map (choose 6)

Explanation

`theorem / example`

A named theorem or anonymous example states exactly the claim Lean must check. Read its inputs and assumptions to see the scope.

`decide`

Builds a proof using a decision procedure. Here it checks a concrete arithmetic statement.

`Nat`

Nat contains arbitrary-size natural numbers, including zero. Its subtraction stops at zero.

Background and proof scope

First discovery date unknown

Partition choices according to whether they contain one distinguished element.

Implements Pascal’s recurrence and proves its defining step plus concrete counts. The factorial formula and set-counting interpretation are not formalized.

Historical Top 100 list (reproduced by Lurch)

Expected output

Reference only. Run the file to check its actual result.

[1, 6, 15, 20, 15, 6, 1]

Exercise

Prove choose n 0 = 1 for every n. Then inspect the row for n=8.