Counting & logic

Count subsets with bit strings

Build every binary membership pattern and prove its count by induction.

-- Top 100 #52: Count subsets with bit strings
-- History: First discovery date unknown.
-- Dates identify historical milestones, not the date of this Lean proof.
-- Fact: A subset is encoded by one yes/no choice for each element.
-- Scope: Proves the length of the generated n-bit membership patterns is 2^n. The separate bijection to abstract finite sets is explained, not formalized.
-- Source: https://lurch.plus/100/

def patterns : Nat → List (List Bool)
  | 0 => [[]]
  | n+1 => (patterns n).map (true :: ·) ++ (patterns n).map (false :: ·)

theorem pattern_count (n : Nat) : (patterns n).length = 2^n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    simp only [patterns, List.length_append, List.length_map, ih, Nat.pow_succ]
    omega

#eval (patterns 5).length

Explanation

`List Bool`

A list of Boolean values records whether each element belongs to a subset. patterns n generates the membership patterns for n elements.

`induction n with`

Proves the count for zero elements, then uses the count for n elements to prove the count for n + 1.

`simp only · omega`

The listed lemmas reduce list lengths and expand the power. omega finishes the remaining arithmetic equality.

Background and proof scope

First discovery date unknown

A subset is encoded by one yes/no choice for each element.

Proves the length of the generated n-bit membership patterns is 2^n. The separate bijection to abstract finite sets is explained, not formalized.

Historical Top 100 list (reproduced by Lurch)

Expected output

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

Exercise

Inspect patterns 3. Read each bit string as a subset of a three-element set.