Formalizing finite sets

Posted on May 27, 2022

Combinatorics studies mathematical structures by counting. Counting may seem like a benign activity, but the same rigor necessary to prevent double- or under-counting mistakes arguably underpins all of mathematics.1

Combining my two favorite topics, I’ve always wanted to mechanize combinatorics in Coq.2 An immediate challenge is to formalize the idea of “set”.3 We have to be able to define the set of things we want to count. It turns out that there are at least two ways of encoding sets in type theory: sets as types, and sets as predicates. They are suitable for defining different classes of operations: sums (disjoint union) are a natural operation on types, while unions and intersections are naturally defined on predicates.

The interplay between these two notions of sets, and finiteness, will then let us prove the standard formula for the cardinality of unions, aka. the binary inclusion-exclusion formula:

#|X ∪ Y| = #|X| + #|Y| - #|X ∩ Y|
Imports and options
From Coq Require Import ssreflect ssrbool.

Set Implicit Arguments.

Sets as types

The obvious starting point is to view a type as the set of its inhabitants.

How do we count its inhabitants? We will say that a set A has cardinality n if there is a bijection between A and the set {0 .. n-1} of natural numbers between 0 and n-1.

Bijections

A bijection is a standard way to represent a one-to-one correspondence between two sets, with a pair of inverse functions. We define the type bijection A B as a record containing the two functions and a proof of their inverse relationship.

Record is_bijection {A B} (to : A -> B) (from : B -> A) : Prop :=
  { from_to : forall a, from (to a) = a
  ; to_from : forall b, to (from b) = b }.

Record bijection (A B : Type) : Type :=
  { bij_to : A -> B
  ; bij_from : B -> A
  ; bij_is_bijection :> is_bijection bij_to bij_from }.

Infix "<-->" := bijection (at level 90) : type_scope.

We say that A and B are isomorphic when there exists a bijection between A and B. Isomorphism is an equivalence relation: reflexive, symmetric, transitive.4

A: Type

A <--> A
Admitted. (* Easy exercise *)
A, B: Type

A <--> B -> B <--> A
Admitted. (* Easy exercise *)
A, B, C: Type

A <--> B -> B <--> C -> A <--> C
Admitted. (* Easy exercise *) Infix ">>>" := bijection_trans (at level 40).

Finite sets

Our “bijective” definition of cardinality shall rely on a primitive, canonical family of finite types {0 .. n-1} that is taken for granted. We can define them as the following sigma type, using the familiar set comprehension notation, also known as ordinal in math-comp:

Definition fin (n : nat) : Type := { p | p < n }.

An inhabitant of fin n is a pair of a p : nat and a proof object of p < n. Such proofs objects are unique for a given p and n, so the first component uniquely determines the second component, and fin n does have exactly n inhabitants.5

Finiteness

We can now say that a type A has cardinality n if there is a bijection between A and fin n, i.e., there is an inhabitant of A <--> fin n. Note that this only defines finite cardinalities, which is fine for doing finite combinatorics. Infinity is really weird so let’s not think about it.

As a sanity check, you can verify the cardinalities of the usual suspects, bool, unit, and Empty_set.


bool <--> fin 2
Admitted. (* Easy exercise *)

unit <--> fin 1
Admitted. (* Easy exercise *)

Empty_set <--> fin 0
Admitted. (* Easy exercise *)

A type A is finite when it has some cardinality n : nat. When speaking informally, it’s common to view finiteness as a property, a thing that a set either is or is not. To prove finiteness is merely to exhibit the relevant data: a number to be the cardinality, and an associated bijection (which we call an enumeration of A, enum for short). Hence we formalize “finiteness” as the type of that data.

Record is_finite (A : Type) : Type :=
  { card : nat
  ; enum : A <--> fin card }.

Further bundling is_finite A proofs with their associated set A, we obtain a concept aptly named “finite type”.6 A finite type is a type A paired with a proof of is_finite A.

Record finite_type : Type :=
  { ft_type :> Type
  ; ft_is_finite :> is_finite ft_type }.

We leverage coercions (indicated by :>) to lighten the notation of expressions involving finite_type.

The first coercion ft_type lets us use a finite_type as a Type. So if E : finite_type, we can write the judgement that “e is an element of E” as e : E, which implicitly expands to the more cumbersome e : ft_type E.

Similarly, the second coercion ft_is_finite lets us access the evidence of finiteness without naming that field. In particular, we can write the cardinality of E : finite_type as card E, as if card were a proper field of E rather than the nested record it actually belongs to. This is a convenient mechanism for overloading, letting us reuse the name card(inality) even though records technically cannot have fields with the same name. With that, we define #|A| as sugar for card A:

Notation "'#|' A '|'" := (card A).
Some notation boilerplate
Declare Scope fintype_scope.
Delimit Scope fintype_scope with fintype.
Bind Scope fintype_scope with finite_type.

Uniqueness of cardinality

The phrase “cardinality of a set” suggests that cardinality is an inherent property of sets. But now we’ve defined “finite type” essentially as a tuple where the cardinality is just one component. What’s to prevent us from putting a different number there, for the same underlying type?

We can prove that this cannot happen. Cardinality is unique: any two finiteness proofs for the same type must yield the same cardinality.

(The proof is a little tedious and technical.)

A: Type
F1, F2: is_finite A

#| F1 | = #| F2 |
Admitted. (* Intermediate exercise *)

A slightly more general result is that isomorphic types (i.e., related by a bijection) have the same cardinality. It can first be proved in terms of is_finite, from which a corollary in terms of finite_type follows.

A, B: Type
FA: is_finite A
FB: is_finite B

A <--> B -> #| FA | = #| FB |
Admitted. (* Like card_unique *)
A, B: finite_type

A <--> B -> #| A | = #| B |
A, B: finite_type

A <--> B -> #| A | = #| B |
apply card_bijection. Qed.

The converse is also true and useful: two types with the same cardinality are isomorphic.

A, B: Type
FA: is_finite A
FB: is_finite B

#| FA | = #| FB | -> A <--> B
Admitted. (* Easy exercise *)
A, B: finite_type

#| A | = #| B | -> A <--> B
A, B: finite_type

#| A | = #| B | -> A <--> B
apply bijection_card. Qed.

Operations on finite sets

Sum

The sum of sets is also known as the disjoint union.

Inductive sum (A B : Type) : Type :=
| inl : A -> A + B
| inr : B -> A + B
where "A + B" := (sum A B) : type_scope.

sum is a binary operation on types. We must work to make it an operation on finite types.

There is a bijection between fin n + fin m (sum of sets) and fin (n + m) (sum of nats).

n, m: nat

fin n + fin m <--> fin (n + m)
Admitted. (* Intermediate exercise *)

The sum is a bifunctor.

A, A', B, B': Type

A <--> B -> A' <--> B' -> A + A' <--> B + B'
Admitted. (* Easy exercise *)

Combining those facts, we can prove that the sum of two finite sets is finite (finite_sum), and the cardinality of the sum is the sum of the cardinalities (card_sum).

Definition is_finite_sum {A B} (FA : is_finite A) (FB : is_finite B)
  : is_finite (A + B) :=
  {| card := #|FA| + #|FB|
  ;  enum := bijection_sum (enum FA) (enum FB) >>> bijection_sum_fin |}.

Definition finite_sum (A B : finite_type) : finite_type :=
  {| ft_type := A + B ; ft_is_finite := is_finite_sum A B |}.

Infix "+" := finite_sum : fintype_scope.
A, B: finite_type

#| (A + B)%fintype | = #| A | + #| B |
A, B: finite_type

#| (A + B)%fintype | = #| A | + #| B |
reflexivity. Qed.

Product

The cartesian product has structure dual to the sum.

Inductive prod (A B : Type) : Type :=
| pair : A -> B -> A * B
where "A * B" := (prod A B) : type_scope.
Coq code
n, m: nat

fin n * fin m <--> fin (n * m)
Admitted. (* Intermediate exercise *)
A, A', B, B': Type

A <--> B -> A' <--> B' -> A * A' <--> B * B'
Admitted. (* Easy exercise *) Definition is_finite_prod {A B} (FA : is_finite A) (FB : is_finite B) : is_finite (A * B) := {| card := #|FA| * #|FB| ; enum := bijection_prod (enum FA) (enum FB) >>> bijection_prod_fin |}. Definition finite_prod (A B : finite_type) : finite_type := {| ft_type := A * B ; ft_is_finite := is_finite_prod A B |}. Infix "*" := finite_prod : fintype_scope.
A, B: finite_type

#| (A * B)%fintype | = #| A | * #| B |
A, B: finite_type

#| (A * B)%fintype | = #| A | * #| B |
reflexivity. Qed.

Sets as predicates

Two other common operations on sets are union and intersection. However, those operations don’t fit in the view of sets as types. While set membership x ∈ X is a proposition, type inhabitation x : X is a judgement, which is a completely different thing,7 so we need a different approach.

The idea of set membership x ∈ X as a proposition presumes that x and X are entities that exist independently of each other. This suggests that there is some “universe” that elements x live in, and the sets X under consideration are subsets of that same universe. We represent the universe by a type A, and sets (i.e., “subsets of the universe”) by predicates on A.

Definition set_of (A : Type) := (A -> bool).

Hence, if x : A is an element of the universe, and X : set A is a set (subset of the universe), we will denote set membership x ∈ X simply as X x (x satisfies the predicate X).

Those predicates are boolean, i.e., decidable. This is necessary in several constructions and proofs here, notably to prove that the union or intersection of finite sets is finite. We rely on a coercion to implicitly convert booleans to Prop: is_true : bool >-> Prop, which is exported by ssreflect.

Union, intersection, complement

Those common set operations correspond to the usual logical connectives.

Section Operations.

Context {A : Type}.

Definition union' (X Y : set_of A) : set_of A := fun a => X a || Y a.
Definition intersection' (X Y : set_of A) : set_of A := fun a => X a && Y a.
Definition complement' (X : set_of A) : set_of A := fun a => negb (X a).

End Operations.

Define the familiar infix notation for union and intersection.

Declare Scope set_of_scope.
Delimit Scope set_of_scope with set_of.
Bind Scope set_of_scope with set_of.

Infix "∪" := union' (at level 40) : set_of_scope.
Infix "∩" := intersection' (at level 40) : set_of_scope.

Finiteness

Again, we will characterize finite sets using bijections to fin n. We first transform the set X into a type to_type X, so we can form the type of bijections to_type X <--> fin n. Like fin, we define to_type A as a sigma type. Thanks to the predicate X being boolean, there is at most one proof p : X a for each a, so the type { a : A | X a } has exactly one inhabitant for each inhabitant a : A satisfying X a.

Definition to_type {A : Type} (X : set_of A) : Type := { a : A | X a }.

Coercion to_type : set_of >-> Sortclass.

We obtain a notion of finite set by imitating the structure of finite_type. The set-as-predicate X is finite if the set-as-type to_type X is finite.

Record finite_set_of (A : Type) : Type :=
  { elem_of :> set_of A
  ; fso_is_finite :> is_finite (to_type elem_of)
  }.

Similarly, a finite_type_of can be coerced to a finite_type.

Definition to_finite_type {A} (X : finite_set_of A) : finite_type :=
  {| ft_type := elem_of X
  ;  ft_is_finite := X |}.

Coercion to_finite_type : finite_set_of >-> finite_type.

Finite unions and intersections

We then prove that the union and intersection of finite sets are finite. This is actually fairly challenging, since proving finiteness means to calculate the cardinality of the set and to construct the associated bijection. Unlike sum and product, there is no simple formula for the cardinality of union and intersection. One candidate may seem to be the binary inclusion-exclusion formula:

#|X ∪ Y| = #|X| + #|Y| - #|X ∩ Y|

But that only gives the cardinality of the union in terms of the intersection, or vice versa, and we don’t know either yet.

Rather than constructing the bijections directly, we decompose the proof. The intuition is that X ∪ Y and X ∩ Y can easily be “bounded” by known finite sets, namely X + Y and X respectively. By “bounded”, we mean that there is an injection from one set to the other.

The standard definition of injectivity is via an implication f x = f y -> x = y. However, a better definition for our purposes comes from a one-sided inverse property: a function f : A -> B is a section if there exists another function g : B -> A (called a retraction) such that g (f x) = x. Every section is an injection, but the converse requires the law of excluded middle.

Record is_section {A B} (to : A -> B) (from : B -> A) : Prop :=
  { s_from_to : forall a, from (to a) = a }.

Record section (A B : Type) : Type :=
  { s_from : A -> B
  ; s_to : B -> A
  ; s_is_section : is_section s_from s_to }.

The point is that, given a section to a finite set, section A (fin n), we can construct a bijection A <--> fin m for some m, that is smaller than n. We formalize this result with a proof-relevant sigma type.

A: Type
n: nat

section A (fin n) -> {m : nat & A <--> fin m}
Admitted. (* Hard exercise *)

This construction is rather involved. It is much more general than when we were looking specifically at union and intersection, but at the same time it is easier to come up with as it abstracts away the distracting details of those operations.

Now there is a section from X ∪ Y to X + Y, and from X ∩ Y to X.

A: Type
X, Y: set_of A

section (X ∪ Y)%set_of (X + Y)
Admitted. (* Easy exercise *)
A: Type
X, Y: set_of A

section (X ∩ Y)%set_of X
Admitted. (* Easy exercise *)

We can then rely on the finiteness of X and X + Y to extend those sections to fin n for some n via the following theorem:

A, B, C: Type

section A B -> B <--> C -> section A C
Admitted. (* Easy exercise *)
A: Type
X, Y: finite_set_of A

section (X ∪ Y)%set_of (fin (#| X | + #| Y |))
A: Type
X, Y: finite_set_of A

section (X ∪ Y)%set_of (fin (#| X | + #| Y |))
A: Type
X, Y: finite_set_of A

section (X ∪ Y)%set_of ?B
A: Type
X, Y: finite_set_of A
?B <--> fin (#| X | + #| Y |)
A: Type
X, Y: finite_set_of A

section (X ∪ Y)%set_of ?B
apply section_union.
A: Type
X, Y: finite_set_of A

X + Y <--> fin (#| X | + #| Y |)
apply is_finite_sum. Qed.
A: Type
X, Y: finite_set_of A

section (X ∩ Y)%set_of (fin #| X |)
A: Type
X, Y: finite_set_of A

section (X ∩ Y)%set_of (fin #| X |)
A: Type
X, Y: finite_set_of A

section (X ∩ Y)%set_of ?B
A: Type
X, Y: finite_set_of A
?B <--> fin #| X |
A: Type
X, Y: finite_set_of A

section (X ∩ Y)%set_of ?B
apply section_intersection.
A: Type
X, Y: finite_set_of A

X <--> fin #| X |
apply enum. Qed.

Finally, by section_bijection, we obtain finiteness proofs of union' and intersection', which let us define union and intersection properly as operations on finite sets.

A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

is_finite (X ∪ Y)%set_of
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

is_finite (X ∪ Y)%set_of
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

section (X ∪ Y)%set_of (fin ?Goal)
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

section (X ∪ Y)%set_of (X + Y)
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y
X + Y <--> fin ?Goal
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

section (X ∪ Y)%set_of (X + Y)
apply section_union.
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

X + Y <--> fin ?Goal
apply (is_finite_sum FX FY). Qed.
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

is_finite (X ∩ Y)%set_of
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

is_finite (X ∩ Y)%set_of
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

section (X ∩ Y)%set_of (fin ?Goal)
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

section (X ∩ Y)%set_of ?B
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y
?B <--> fin ?Goal
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

section (X ∩ Y)%set_of ?B
apply section_intersection.
A: Type
X, Y: set_of A
FX: is_finite X
FY: is_finite Y

X <--> fin ?Goal
apply (enum FX). Qed. Definition union {A} (X Y : finite_set_of A) : finite_set_of A := {| fso_is_finite := is_finite_union X Y |}. Definition intersection {A} (X Y : finite_set_of A) : finite_set_of A := {| fso_is_finite := is_finite_intersection X Y |}.
Declare Scope fso_scope.
Delimit Scope fso_scope with fso.
Bind Scope fso_scope with finite_set_of.

Infix "∪" := union (at level 40) : fso_scope.
Infix "∩" := intersection (at level 40) : fso_scope.

Hereafter, and will denote finite unions and intersections.

#[local] Open Scope fso_scope.

Inclusion-exclusion

#|X ∪ Y| = #|X| + #|Y| - #|X ∩ Y|

To prove that formula, it’s probably not a good idea to look at how and compute their cardinalities. A better idea is to construct a bijection, which implies an equality of cardinalities by card_bijection.

To start, subtractions are bad, so we rewrite the goal:

#|X ∪ Y| + #|X ∩ Y| = #|X| + #|Y|

Now we look for a bijection (X ∪ Y) + (X ∩ Y) <--> X + Y. It gets a bit tricky because of the dependent types.

A: Type
X, Y: finite_set_of A

(X ∪ Y)%set_of + (X ∩ Y)%set_of <--> X + Y
Admitted. (* Hard exercise *)

Isomorphic sets have the same cardinality (by theorem card_bijection_finite_type). The resulting equation simplifies to the binary inclusion-exclusion identity, because #|A + B| equals #|A| + #|B| definitionally. So the proof consists simply of applying that theorem with the above bijection.

A: Type
X, Y: finite_set_of A

#| X ∪ Y | + #| X ∩ Y | = #| X | + #| Y |
A: Type
X, Y: finite_set_of A

#| X ∪ Y | + #| X ∩ Y | = #| X | + #| Y |
A: Type
X, Y: finite_set_of A

(X ∪ Y + X ∩ Y)%fintype <--> (X + Y)%fintype
apply inclusion_exclusion_bijection. Qed.

Conclusion

To formalize mathematics, it’s often useful to revisit our preconceptions about fundamental concepts. To carry out even basic combinatorics in type theory, it’s useful to distinguish two views of the naive notion of set.

For example, when we say “union”, we really mean one of two things depending on the context. Either the sets are obviously disjoint, so we really mean “sum”: this corresponds to viewing sets as types. Or we implicitly know that the two sets contain the same “type” of elements a priori, so the overlap is something we have to worry about explicitly: this corresponds to viewing sets as predicates on a given universe.