Learning set theory through Coq (part 3)

This post covers through page 34 (through definition 2.8).

Relations

A binary relation describes a property that pairs of elements could possess. In set theory the binary relation is expressed as a set of ordered pairs. If the pair meets the criteria defined by the relation, it is in the set. For example, this relation describes pairs of natural numbers where the pair adds up to 10: $\{(n,m) \in \mathbb{N \times N} : n + m = 10 \}$. The advantage of defining a relation this way is that all of the usual set operators, such as $\cup$, work well between relations.

Relations in Coq are a mess. There are 4 different names for binary homogeneous relations in different modules. A binary homogeneous relation takes exactly 2 operands (similar to an ordered pair), and each of those operands have the same type. There is a fifth relation-like type in Coq, predicate, which supports an arbitrary number of operands, and they can be heterogeneous. The problem with predicate is that almost none of the functions in the module can use it. Furthermore the convenience notations to define a specific predicate are locally defined in Coq.Classes.RelationClasses; they are not available outside of the module.

Type	Name	Module
binary homogeneous relation	Relation	Coq.Sets.Relations_1
binary homogeneous relation	Rel	Coq.Sets.Partial_Order
binary homogeneous relation	relation	Coq.Relations.Relation_Definitions
binary homogeneous relation	binary_relation	Coq.Classes.RelationClasses
heterogenous relation	predicate	Coq.Classes.RelationClasses

Similar to Ensemble, relations in Coq are functions that return a Prop, and that Prop describes whether the pair meets the criteria of the relation. The problem is that the relation is not defined as an Ensemble of a pair. Instead it is a function that takes takes two arguments, that is, forall T : Type, T -> T -> Prop. Describing that with Ensemble, the definition becomes T -> Ensemble(T), that is a function that returns an ensemble. Note this is not implicitly convertible with either Ensemble (T * T) (ensemble of a pairs) or Ensemble (T -> T) (ensemble of functions that take a T and return a T). Translating that function-style representation back to set theory, the previous example of pairs of numbers that add to 10 would look like, $\{(n,M) \in \mathbb{N} \times \mathcal{P}(\mathbb{N}) : \forall m \in \mathbb{N}, n + m = 10 \iff m \in M \}$. The disadvantage of this representation is that the regular set operations aren't useful on it. The advantage of this representation in Coq is that the relations behave like normal curried functions.
The prod_curry function can convert Coq's function-style relation to a pair-style relation, specifically an Ensemble (T * T). In reverse, a pair-style relation can be converted to function-style relation with prod_uncurry. Note that prod_curry and prod_uncurry seem to be reversed relative to Haskell's curry and uncurry functions. prod_uncurry actually curries a function, and prod_curry actually uncurries a function.

It is possible to manipulate relations by uncurrying them and using the Ensemble operations (like Union), then currying the result to convert it back to a function-style relation. Additionally, Coq has functions that work directly with relations. My goal for this series of posts was to stick with the Coq.Sets.* modules, but it turns out that Coq.Sets.Relations_1 is practically unusable due to all the missing manipulations for relations. Instead in this series of posts I will use Coq.Classes.RelationClasses for relations and continue to use Coq.Sets for Ensembles.

Cartesian product

The Cartesian product generates a relation from two sets. The relation contains every possible combination of an element from the left set with an element from the right set. There is some ambiguity as to how to translate to type theory, because the two input sets could be represented as Types or as Ensembles.

Since this post relies on homogeneous relations, that strongly limits what the Cartesian product can do for joining two types together; those types must be the same! Instead I decided to write a custom Cartesian product function (cartesian_product) that joins two Ensembles together, where both Ensembles use the same carrier type. However as the notations table describes, a type can be joined with itself to form a relation using true_predicate.

Definition translations

For the following table, let:

$\begin{aligned} X, Y &\subset T \\ U, V &\subset T \times T \\ x &\in X \end{aligned} $

Assume those variables are defined with the following Coq types:

Variable T : Type.
Variable X Y : Ensemble T.
Variable x : T.
Variable U V : binary_relation T.

Set theory notation	Description	Coq syntax	Module
$U=V$	$U$ equals $V$	relation_equivalence U V	Coq.Classes.RelationClasses
		predicate_equivalence U V	Coq.Classes.RelationClasses
		same_relation T U V	Coq.Relations.Relation_Definitions
		same_relation T U V	Coq.Sets.Relations_1
$U \subset V$	$U$ is a subset of $V$	subrelation U V	Coq.Classes.RelationClasses
		predicate_implication U V	Coq.Classes.RelationClasses
		inclusion T U V	Coq.Relations.Relation_Definitions
		contains T U V	Coq.Sets.Relations_1
$U^{-1}$	inverse of $U$	inverse U	Coq.Classes.RelationClasses
		transp T U	Coq.Relations.Relation_Operators
$U^c$	complement of $U$	complement U	Coq.Classes.RelationClasses
		Complement T U	Coq.Sets.Relation_1_Facts
$U \cup V$	union of $U$ and $V$	relation_disjunction U V	Coq.Classes.RelationClasses
		predicate_union U V	Coq.Classes.RelationClasses
		union T U V	Coq.Relations.Relation_Definitions
$U \cap V$	intersection of $U$ and $V$	predicate_intersection U V	Coq.Classes.RelationClasses
		relation_conjunction U V	Coq.Classes.RelationClasses
$T \times T$	full relation of $T$	true_predicate : binary_relation T	Coq.Classes.RelationClasses
$\emptyset$	empty set for $T$	false_predicate : binary_relation T	Coq.Classes.RelationClasses
$X \times Y$	Cartesian product of $X$ and $Y$	cartesian_product X Y	*sets_part3
$U \times V$	Cartesian product of $U$ and $V$	RelProd U V	Coq.Classes.RelationPairs
$U - V$	$U$ minus $V$	relation_minus U V	*sets_part3
$V \circ U$	composition of $V$ and $U$ (Note that $U$ is evaluated first, then $V$)	relation_composition V U	*sets_part3
$U[X]$	image of $X$ under relation $U$	relation_image U X	*sets_part3
$U\{x\}$	image of $x$ under relation $U$	U x
$U \langle X \rangle$		relation_for_all U X	*sets_part3
$U|X$	restriction of $U$ to $X$	relation_restriction U X	*sets_part3
$\triangle$	diagonal of $T$	@eq T
$(X, U)$	relational space	(X,U)
	choice function	choice	Coq.Logic.ClassicalChoice

Extensions to Coq library: sets_part3.v

Exercises

Require Import sets_part3.
Require Import Coq.Sets.Ensembles.
Require Import Coq.Classes.RelationClasses.

Section Lemma_1_38.

Variable T : Type.

Variable U V X Y : Ensemble T.

Lemma Lemma_1_38_i_a :
    relation_equivalence (cartesian_product (Empty_set T) V)
    (cartesian_product U (Empty_set T)).
Proof.
  admit.
Qed.

Lemma Lemma_1_38_i_b :
    relation_equivalence (cartesian_product U (Empty_set T))
    (false_predicate:binary_relation T).
Proof.
  admit.
Qed.

Lemma Lemma_1_38_ii :
    relation_equivalence
    (relation_conjunction (cartesian_product U V) (cartesian_product X Y))
    (cartesian_product (Intersection _ U X) (Intersection _ V Y)).
Proof.
  admit.
Qed.

Lemma Lemma_1_38_iii :
    relation_equivalence
    (cartesian_product X (Union _ V Y))
    (relation_disjunction (cartesian_product X V) (cartesian_product X Y)).
Proof.
  admit.
Qed.

Lemma Lemma_1_38_iv :
    relation_equivalence
    (cartesian_product X (Setminus _ Y V))
    (relation_minus (cartesian_product X Y) (cartesian_product X V)).
Proof.
  admit.
Qed.

End Lemma_1_38.

Section Lemma_1_39.

Variable T : Type.

Variable U : Ensemble T.
Variable V : Ensemble T.
Variable X : Ensemble T.
Variable Y : Ensemble T.

Hypothesis HXInU : Included _ X U.
Hypothesis HYInV : Included _ Y V.

(* This half of Lemma 1.39 can be proven using intuistionistic logic. *)

Lemma Lemma_1_39_constructive :
    subrelation
    (relation_disjunction
      (cartesian_product (Complement _ X) (Complement _ Y))
      (relation_disjunction
        (cartesian_product (Complement _ X) Y)
        (cartesian_product X (Complement _ Y))))
    (complement (cartesian_product X Y)).
Proof.
  admit.
Qed.

(* The other part of Lemma 1.39 requires the excluded middle. *)
Hypothesis classic : forall P:Prop, P \/ ~ P.

Lemma Lemma_1_39 :
    relation_equivalence
    (complement (cartesian_product X Y))
    (relation_disjunction
      (cartesian_product (Complement _ X) (Complement _ Y))
      (relation_disjunction
        (cartesian_product (Complement _ X) Y)
        (cartesian_product X (Complement _ Y)))).
Proof.
  admit.
Qed.

End Lemma_1_39.

Section Lemma_2_6.

Variable T : Type.

Variable X Y Z S : Ensemble T.

Variable U U' V V' W : binary_relation T.

Hypothesis HUSubXY : subrelation U (cartesian_product X Y).
Hypothesis HU'SubU : subrelation U' U.

Hypothesis HVSubYZ : subrelation V (cartesian_product Y Z).
Hypothesis HV'SubV : subrelation V' V.

Hypothesis HWSubZS : subrelation W (cartesian_product Z S).

Lemma Lemma_2_6_i :
    relation_equivalence (inverse (relation_composition V U))
      (relation_composition (inverse U) (inverse V)).
Proof.
  admit.
Qed.

Lemma Lemma_2_6_ii :
    relation_equivalence (relation_composition (relation_composition W V) U)
      (relation_composition W (relation_composition V U)).
Proof.
  admit.
Qed.

Lemma Lemma_2_6_iii :
    subrelation (inverse U') (inverse U).
Proof.
  admit.
Qed.

Lemma Lemma_2_6_iv :
    subrelation (relation_composition V' U)
      (relation_composition V U).
Proof.
  admit.
Qed.

Lemma Lemma_2_6_v :
    subrelation (relation_composition V U')
      (relation_composition V U).
Proof.
  admit.
Qed.

End Lemma_2_6.

Section Lemma_2_7.

Variable T : Type.

Variable X Y Z A : Ensemble T.

Variable U V : binary_relation T.

Hypothesis HUSubXY : subrelation U (cartesian_product X Y).

Hypothesis HVSubYZ : subrelation V (cartesian_product Y Z).

Hypothesis HASubX : Included _ A X.

Lemma Lemma_2_7 :
    relation_image (relation_composition V U) A =
    relation_image V (relation_image U A).
Proof.
  admit.
Qed.

End Lemma_2_7.

Solutions: sets_part3_exercises.v

Learning set theory through Coq (part 2)

This post covers through page 22 (through lemma 1.36).

Power set

In set theory, one use of the power set is used to describe functions take subsets as input parameters or return subsets. For example $f : \mathcal{P}(U) \rightarrow U$ means that function $f$ takes a subset of $U$ and returns an element of $U$. In Coq, this kind of usage of the power set maps to describing the type of the input parameter: Ensemble U.

The rest of the time in set theory, the power set operator is used to build systems (sets of sets) where set operations are performed on the system. For example $Y \subset X \implies Y \in \mathcal{P}(X)$. This type of power set usage maps to Power_set _ X.

Ordered pairs

Set theory defines an ordered pair as a system, specifically $(x,y) = \big\{\{x,y\}, \{x\}\big\}$. However Coq defines an ordered pair using an inductive type without going through the set/Ensemble abstraction.

Coq's ordered pairs have most of the same properties as in set theory, except direct set operations are not allowed. For example, $(1,2) \cup (3,4)$ is defined (but avoided) in set theory, while it is disallowed by Coq's type checker.

Definition translations

For the following table, let $(x~y~z) : U$, $X \subset U$, and $A=(x,y)$.

Set theory notation	Pronunciation	Coq syntax
$\mathcal{P}(U)$	power set of $U$ (as a Type)	Ensemble U
$\mathcal{P}(X)$	power set of $X$ (as an Ensemble)	Power_set U X
$\mathcal{P}(X)$	power set of $X$ (as an Ensemble)	Power_set U X
$\{x\}$	singleton of $x$ 1-tuple of $x$	Singleton U x
$\{x, y\}$	unordered pair of $x$ and $y$ unordered 2-tuple of $x$ and $y$	Couple U x y
$\{x, y, z\}$	unordered triple of $x$, $y$, and $z$ unordered triplet of $x$, $y$, and $z$ unordered 3-tuple of $x$, $y$, and $z$	Triple U x y z
$(x, y)$	ordered pair of $x$ and $y$ ordered 2-tuple of $x$ and $y$	(x, y)
$A_l$	left coordinate of $A$	fst A
$A_r$	right coordinate of $A$	snd A

Exercises

(* Include the extended definitions from the previous post.
   Make sure you downloaded and compiled them. *)
Require Import sets_part1.

(* The exercise in lemma 1.31 does not translate to Coq. *)

Section Lemma_1_34.

Variable U : Type.

Definition US := Ensemble U.

Variable AS BS : Ensemble US.

(* The book's definition of a big intersection requires that the system is
   inhabited. So the exercise says AS and BS are inhabited so that the big
   intersection is defined for them.

   However the Coq definition given in part1 does not require the system to
   be inhabited. For completeness, these hypotheses are included. Uncomment
   them if you choose. They are not necessary to solve the exercises.
*)
(*
Hypothesis AS_inhabited : Inhabited US AS.
Hypothesis BS_inhabited : Inhabited US BS.
*)

Lemma Lemma_1_34_i : Intersection U (Big_union AS) (Big_union BS) =
    Big_union (
      fun x => exists A B,
        x = (Intersection U A B) /\
          In US AS A /\
          In US BS B
    ).
Proof.
  admit.
Qed.

(* Using intuitionistic logic, it is possible to prove that
   ((Big_intersection AS) union (Big_intersection BS)) is a subset of
   (Big_intersection {A union B | A in AS /\ B in BS}), but proving the converse
   requires classical logic.
*)
Lemma Lemma_1_34_ii_constructive :
    Included U (Union U (Big_intersection AS) (Big_intersection BS))
    (Big_intersection (
      fun x => exists A B,
        x = (Union U A B) /\
          In US AS A /\
          In US BS B
    )).
Proof.
  admit.
Qed.

(* The excluded middle is necessary to prove the other case. I found these
   two forms of the excluded middle helpful, but
   Coq.Logic.Classical_Pred_Type could be included instead. *)
Hypothesis not_all_ex_not :
 forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n.

Hypothesis classic : forall P:Prop, P \/ ~ P.

Lemma Lemma_1_34_ii : Union U (Big_intersection AS) (Big_intersection BS) =
    Big_intersection (
      fun x => exists A B,
        x = (Union U A B) /\
          In US AS A /\
          In US BS B
    ).
Proof.
  admit.
Qed.

End Lemma_1_34.

Section Lemma_1_35.

Variable X : Type.

Definition PX := Ensemble X.

Variable AS : Ensemble PX.

(*
Hypothesis AS_inhabited : Inhabited US AS.
*)

Lemma Lemma_1_35_i_constructive : Included X (Big_union (
    fun AC => exists A, In PX AS A /\ AC = Complement X A))
    (Complement X (Big_intersection AS)).
Proof.
  admit.
Qed.


(* The excluded middle is necessary to prove the other case. I found this
   form of the excluded middle helpful, but
   Coq.Logic.Classical_Pred_Type could be included instead. *)
Hypothesis not_all_ex_not :
 forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P n.

Lemma Lemma_1_35_i : Complement X (Big_intersection AS) = Big_union (
    fun AC => exists A, In PX AS A /\ AC = Complement X A).
Proof.
  admit.
Qed.

(* This lemma can be proved constructively. *)
Lemma Lemma_1_35_ii : Complement X (Big_union AS) = Big_intersection (
    fun AC => exists A, In PX AS A /\ AC = Complement X A).
Proof.
  admit.
Qed.

End Lemma_1_35.

Solutions: sets_part2_exercises.v