How to count

First: what do we mean by counting the elements of a type? Letʼs start with defining a type with a specified number of elements:

-- `fin n` A type that has `n` inhabitants
def fin : ℕ → Type := λ(n : ℕ), Σ(m : ℕ), m < n

It is defined as dependently-typed function that takes a natural number n to a subtype of the natural numbers which are less than n. This means that fin 0 is a type with no inhabitants, and fin 1 only has one (⟨0, zero_lt_one⟩, where the angle brackets denote constructing an element of the subtype with value 0 and zero_lt_one : 0 < 1 the proof required by the subtype), etc. In order to count the inhabitants, we want to be able to say that a given type is isomorphic to fin n for some n:

@[class] structure fintype (t : Type) :=
(card : ℕ)
(equiv_fin : trunc (t ≃ fin card))

(original: https://github.com/leanprover-community/mathlib/blob/d5de80376088954d592a59326c14404f538050a1/src/data/fintype.lean#L14-L20) (Notes on what finite means constructively: https://ncatlab.org/nlab/show/finite+set)

This is a typeclass; without getting too deep into it, it provides a way to access canonical members of a specific type: in this case, the cardinality card t of a type t along with a bijection that proves that t has as many elements as fin (card t) (trunc here just means that we donʼt get to inspect the details of the bijection, we can only prove results that are independent of its particular value). Note that card t is unique for each type t, if it exists, so we are more or less justified in abusing notation and treating it as a function Type → ℕ, ommitting the proof, like in conventional math notation. (There are type-theoretic reasons why this is okay, regarding inferring typeclass instances and their uniqueness, but I wonʼt go into details here.)

notation `|` t `|` := card t

Algebraic types

I will state the corresponding types and propositions without any proofs:

structure prod (α : Type) (β : Type) : Type :=
(fst : α) (snd : β)

notation α × β := prod α β

lemma card_prod (α β : Type) [fintype α] [fintype β] : |α × β| = |α| * |β| .

inductive sum (α : Type) (β : Type) : Type
| inl {} (val : α) : sum
| inr {} (val : β) : sum

notation α ⊕ β := sum α β

lemma card_sum (α β : Type) [fintype α] [fintype β] : |α ⊕ β| = |α| + |β| .

-- functions α → β are built-in and so need no definition

lemma card_exp (α β : Type) [fintype α] [fintype β] : |α → β| = |β| ^ |α| .

(definitions adapted from https://github.com/leanprover-community/lean/blob/6ed0977fcbc14354c86240cec7f8ef20842d0b5c/library/init/core.lean)

It turns out this is about all there is for algebraic data types, they all can be made out of these basic building blocks (products, sums, expontentials); we will need a more powerful type system to encode more combinatorial functions.

Dependent types

(a.k.a. Propositions, predicates, and proofs!)

def injective {α β : Type} (f : α → β) : Prop := ∀ (a₁ a₂ : α), f a₁ = f a₂ → a₁ = a₂

notation α ↪ β := Σ(f : α → β), injective f

def surjective {α β : Type} (f : α → β) : Prop := ∀ (b : β), ∃ (a : α), f a = b

notation α ↠ β := Σ(f : α → β), surjective f

def bijective {α β : Type} (f : α → β) := injective f ∧ surjective f

notation α ↔︎ β := Σ(f : α → β), bijective f

def F : ℕ → ℕ
| 0 := 1
| (n+1) := (n+1)*F n

notation n `!` := F n

def P : ℕ → ℕ → ℕ := λ(n k : ℕ), if n ≥ k then n! / (n-k)! else 0

lemma card_injective (α β : Type) [fintype α] [fintype β] : |α ↪ β| = P |β| |α| .

def S : ℕ → ℕ → ℕ
| 0 0 := 1
| 0 (k+1) := 0
| (n+1) 0 := 0
| (n+1) (k+1) := S n k + (k+1) * S n (k+1)

def SP : ℕ → ℕ → ℕ := λ(n k : ℕ), k! * S n k

lemma card_surjective (α β : Type) [fintype α] [fintype β] : |α ↠ β| = SP |α| |β| .

def B : ℕ → ℕ → ℕ
| n n = F n
| _ _ = 0

lemma card_bijective (α β : Type) [fintype α] [fintype β] : |α ↔︎ β| = B |α| |β| .

def permutation_related {α β : Type} (f g : α ↪︎ β) : Prop :=
  -- compose the underlying functions, not the whole subtype
  ∃(h : α ↔︎ α), f.fn = g.fn ∘ h.fn

def img_from (α β : Type) := Quotient (α ↪︎ β) permutation_related

-- nonstandard notation:
notation α ↬ β := img_from α β

def C : ℕ → ℕ → ℕ := λ(n k : ℕ), P n k / k!

lemma card_img (α β : Type) [fintype α] [fintype β] : |α ↬ β| = C |β| |α| .

def img_from' (α β : Type) := Σ(p : β → Bool), trunc (α ↔︎ (Σ(b : β), p b = True))

Data structures

Of course, we donʼt have to only be considering functions. It turns out that many combinatorial objects are modelled by list-like structures. See the Inductive Types file for more info about inductive types.

Letʼs start with lists, which are a great building block for all sorts of containers:

inductive list (t : Type) : Type
| nil : list
| cons {} : t → list t → list t

(original: https://github.com/leanprover-community/lean/blob/6ed0977fcbc14354c86240cec7f8ef20842d0b5c/library/init/core.lean#L298-L300)

One important function is the length function; in fact, any parametric function that looks like Π {t : Type}, list t → r for some result type r, can be factored through the length function (meaning it must be f ∘ length, for some f : ℕ → r):

def length {t : Type} : list t → ℕ
| nil := zero
| (cons _ t) := succ (length t)

(original: https://github.com/leanprover-community/lean/blob/6ed0977fcbc14354c86240cec7f8ef20842d0b5c/library/init/data/list/basic.lean#L75-L77)

There are two main directions we can go from here, and they are both orthogonal and compatible, and furthermore they both can be expressed via subtypes and quotients: 1. Get rid of the inherent ordering of the lists, in order to build finite (multi)sets: 1. As a quotient, this means filtering by the equivalence relation that identifies two underlying lists that are merely permutations of each other. 2. As a subtype, it is less elegant: it means requiring an ordering on the elements of the list, and asking that all elements of the underlying list are ordered (which is also potentially computationally expensive). 2. Get rid of the possible duplication of elements in the list, in order to build lists without duplicates and plain finite sets: 1. As a quotient, this means asking that all eliminators ignore the fact that an element of the underlying list may appear more than once. 2. As a subtype, this means asking that no elements of the underlying list repeats, and this is actually more elegant, since type theory always has a notion of equality on a type.

So we typically see that a multiset is defined as a quotient of a list, and a finite set is defined as a subtype of a multiset (one needs to prove that the property of having no duplicates respects the lack of order of the multiset, of course). And of course, length respects the quotient types, so with some (justified) abuse of notation we will use it for all these types.

But, regardless of the particular definitions, we can see that these types mirror the kinds of questions we were asking about with combinatorics:

• Lists of fixed length n : ℕ with elements in t : Type (often called vectors) are counted by |t|^n
• Lists of fixed length n : ℕ with elements in t : Type without duplicates (perhaps called distinct vectors) are counted by P |t| n
• Sets of fixed length n : ℕ with elements in t : Type are counted by C |t| n

Still, the semantics we gave using functions above are more general, in that n does not have to be a natural number, but can be the cardinality of any type, meaning their semantics possibly extend to infinite cardinalities too. For example, we would have to modify the underlying datatypes from inductive lists to coinductive streams in order to pull of a feat like asking for a countable subset of real numbers, but it is clear that the function-based approach works for that. Whether it is the “right” generalization is a matter of debate, though.