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