Learning set theory through Coq (part 1)

Overview of the series

This is the first in a series of posts about how to use the Coq.Sets.* modules. Specifically this series will focus on translating the notations and concepts from set theory into Coq syntax.

The intended reader is expected to have little preexiting knowledge of set thoery, but is comfortable with Coq syntax knowledge. For learning Coq syntax, here are some excellent books on the subject:

Software Foundations
Interactive Theorem Proving and Program Development
Certified Programming with Dependent Types

Good documentation for Coq's standard library is difficult find. A thorough explanation of a module almost involves a books worth of information for the math behind it. This is a daunting task. Instead trying to write an entire book, I will attempt to bridge between an existing book on set theory and the Coq syntax. This series of posts follows along with Set theory and topology. An introduction to the foundations of analysis. Part I: Sets, relations, numbers by Felix Nagel, which is freely available online.

Each post will translates the concepts from a section of the book. Key concepts that do not translate well will be discussed in detail. However, for most concepts, their notation and translation will simply be listed in a table/cheat sheet.

The set theory book contains some definitions that are lacking in Coq's standard library. For these cases, I will provide a new Coq definition. In the translation table, these definitions are preceded by an asterisk. After the table, the Coq source for those definitions is attached to this post.

The exercises from the book will be translated into Coq syntax. A template Coq source file will be included inline with the post. Where ever the template says 'admit', the reader is expected to fill in this part with the completed proof. The solutions are attached as a .v file to the end of the post. I recommend reviewing the solutions if you are stuck, and even after completing the proof for examples of how to structure proofs.

When an exercise duplicates a theorem already in the standard library, the standard name for the theorem will be listed in the template. Of course the reader should not use that particular theorem to complete the exercise!

This post covers up to page 17 (through lemma 1.21).

Subsets

A subset is defined by examining all of the elements of the parent set, and only keeping the ones that meet the criteria for that subset. That criteria is a proposition (mathematical statement) that is called a predicate.

In type theory, a sigma type is a special kind of pair. The first component of the sigma is a parent type (e.g. the set of natural numbers). The second component is a predicate (e.g. the number is greater than 5) that restricts which instances of the parent type are accepted. Instances of the sigma type contain an instance from the parent type (e.g. 6), along with a proof that the predicate is met (e.g. le_S (le_n 5)) ).

Often a set is translated as a type in type theory -- sets have elements and types have instances. A subset is translated into a sigma type. This blog has some examples of how to use sigma types.

Representing subsets as sigma types breaks in a few cases. One is that instances of the sigma type are different from instances of the parent type. Instances of the sigma type have to be projected to pull out an instance of the parent type.

This type distinction becomes more apparent when subsets of subsets are considered. Let's start with a set called $A$, which is the natural numbers. $B$ is a subset of $A$ that contains only that are greater than 5. From $B$, a more restricted subset is created, called $C$. $C$ contains the natural numbers that are greater than 6.
\[ \begin{aligned}
A&=\mathbb{N} \\
B&=\{a \in A: a \gt 5 \} \\
C&=\{a \in B: a \gt 6 \} \\
\end{aligned} \]

The subset relation is transitive. So all of the elements in $C$ are also in $A$.
\[ \begin{aligned}
B &\subset A \\
C &\subset B \\
C &\subset A
\end{aligned} \]

$C$ could be translated as a sig of $B$. In this case, instances of $C$ are no longer instances of $A$. An alternative is to pair $C$'s predicate with $B$'s predicate using sig2. In this case, an instance of $A$ can be pulled out from an instance of $C$, but $C$ does not directly contain instances of $B$ in it.

Another problem with saying subsets are sigma types is with the power set. Describing every possible sigma type for $A$ is a dependent type. So one cannot write a function that has a single parameter, and that parameter is any possible sigma type for $A$. Instead the function would need two parameters: one for the predicate and one for the sigma type.

To fill these gaps, Coq has another subset-like object called an Ensemble. The Ensemble is really just the predicate for the subset. To write a function that takes an element from an Ensemble, it can be wrapped in a sigma type.

The Coq.Sets library is awkward to use because the parent of the Ensemble needs to be passed everywhere. Ideally it would be an implicit parameter instead, but I didn't write the library...

Set equality

The previous section discussed why sets are represented as Ensembles, which are really a type of function. Coq's default equality is intensional equality, in which two functions are the same if they are judgementally equal (which basically means they have the same definition once the functions they call are inlined).

In ZF set theory, the extensionality axiom (axiom 1.2 in the book) says that two sets are equal if they contain exactly the same elements. This is the same as saying two functions are the same if they always return the same output for the same input. So extensional and intensional equality are different.

Unfortunately Coq.Sets.Ensembles adds the Extensionality_Ensembles axiom, which could escape and apply to more than just Ensembles.

Definition translations

For the following table, let $A, B \subset U$, and let $\mathcal{C}$ be a system of subsets of $U$.

Set theory notation	Pronunciation	Coq syntax
$\{x : U | P(x)\}$	the set of all $x$ from $U$ such that $P$ is true for $x$	fun x : U => P x (to represent the set as an Ensemble) {x : U | P x} (to represent the set as a sig type)
$a \in A$	$a$ is an element of $A$	In U A a
$a \notin A$	$a$ is not an element of $A$	~ In U A a
$A = B$	$A$ equals $B$	Same_set U A B, or using the Extensionality_Ensembles axiom, A = B
$A \subset B$	$A$ is a subset of $B$	Included U A B (Note this only works when (A B : Ensemble U), otherwise use Full_set to convert U into an Ensemble.)
$A \supset B$	$A$ is a superset of $B$, or $A$ contains $B$	Included U B A (Note this only works when (A B : Ensemble U), otherwise use Full_set to convert U into an Ensemble.)
$A \subsetneq B$	$A$ is a proper subset of $B$	Strict_Included U A B (Note this only works when (A B : Ensemble U), otherwise use Full_set to convert U into an Ensemble.)
let $A \subset U$	let $A$ be a subset of $U$	Variable A : Ensemble U.
let $A \subset U \wedge A = U$	let $A$ be the full set of $U$	Definition A : Ensemble U := Full_set U
$\emptyset$	empty set	Empty_set U (Note there is a unique empty set for every type U.)
$A \cup B$	union of $A$ and $B$	Union U A B
$A \cap B$	intersection of $A$ and $B$	Intersection U A B
$\bigcup \mathcal{C}$	union of $\mathcal{C}$	*Big_union C
$\bigcap \mathcal{C}$	intersection of $\mathcal{C}$	*Big_intersection C
$A \cap B = \emptyset$	$A$ and $B$ are disjoint	Disjoint U A B
$A \setminus B$	difference of $A$ and $B$	Setminus U A B
$A^c$	complement of $A$ in $U$	Complement U A

Other notable definitions: Union_introl, Union_intror, and Intersection_intro.

Notable theorems

For the following table, let $A, B \subset U$.

Set theory notation	Name	Coq name
$A \cup B = B \cup A$	union commutativity	Union_commutative
$A \cap B = B \cap A$	intersection commutativity	Intersection_commutative
$A \cup (B \cup C) = (A \cup B) \cup C$	union associativity	Union_associative
$A \cap (B \cap C) = (A \cap B) \cap C$	intersection associativity	Intersection_associative
$A \cap (B \cup C) = (A \cap B) \cup (A \cap C)$	distributivity	Distributivity
$A \cup (B \cap C) = (A \cup B) \cap (A \cup C)$	distributivity	Distributivity'

Extensions to Coq library: sets_part1.v

Exercises

Require Import Coq.Sets.Ensembles.

Section Lemma_1_18.

Variable U : Type.

Variable (A B C : Ensemble U).

(* This is the same as Union_commutative *)
Lemma i_a : Union U A B = Union U B A.
Proof.
  admit.
Qed.

(* This is the same as Intersection_commutative *)
Lemma i_b : Intersection U A B = Intersection U B A.
Proof.
  admit.
Qed.

(* This is the same as Union_associative *)
Lemma ii_a : Union U A (Union U B C) = Union U (Union U A B) C.
Proof.
  admit.
Qed.

(* This is the same as Intersection_associative *)
Lemma ii_b : Intersection U A (Intersection U B C) = Intersection U (Intersection U A B) C.
Proof.
  admit.
Qed.

(* This is the same as Distributivity *)
Lemma iii_a :
    Intersection U A (Union U B C) =
    Union U (Intersection U A B) (Intersection U A C).
Proof.
  admit.
Qed.

(* This is the same as Distributivity' *)
Lemma iii_b :
    Union U A (Intersection U B C) =
    Intersection U (Union U A B) (Union U A C).
Proof.
  admit.
Qed.

(* Using intuitionistic logic, it is possible to prove that
   (A intersection B) is a subset of (A \ (A \ B)), but proving the converse
   requires classical logic. *)
Lemma iv_constructive :
    Included U (Intersection U A B) (Setminus U A (Setminus U A B)).
Proof.
  admit.
Qed.

(* Either add this one classical axiom only to this section *)
Hypothesis NNPP : forall p:Prop, ~ ~ p -> p.
(* or uncomment the following line to import all of Classical_Prop for this
   whole module *)
(* Require Import Coq.Logic.Classical_Prop. *)
Lemma iv : Setminus U A (Setminus U A B) = Intersection U A B.
Proof.
  admit.
Qed.

End Lemma_1_18.

Section Lemma_1_19.

Variable X : Type.

Variable (A B : Ensemble X).

(* This half is provable using intuitionistic logic *)
Lemma a_constructive :
    Included X (Union X (Complement X A) (Complement X B))
    (Complement X (Intersection X A B)).
Proof.
  admit.
Qed.

Hypothesis NNPP : forall p:Prop, ~ ~ p -> p.

Lemma a :
    Complement X (Intersection X A B) =
    Union X (Complement X A) (Complement X B).
Proof.
  admit.
Qed.

(* This half is provable using intuitionistic logic *)
Lemma b_constructive :
    Included X (Intersection X (Complement X A) (Complement X B))
    (Complement X (Union X A B)).
Proof.
  admit.
Qed. 

Lemma b :
    Complement X (Union X A B) = 
    Intersection X (Complement X A) (Complement X B).
Proof.
  admit.
Qed.

End Lemma_1_19.

Solutions: sets_part1_exercises.v