.. _set_exercises:

Sets
====

What we will learn here.
------------------------

Let :math:`\mathbb{R}` denote the real numbers. We're going to talk about subsets of the reals here. We could use any type - we use the real numbers initially because they're not so scary.

In Lean, ``X : set ℝ`` means that ``X`` is a set of real numbers (or equivalently, ``X`` is a subset of ``ℝ``). If ``a`` is a real number, then ``a ∈ X`` means that ``a`` is an element of ``X``. In this chapter, we will learn how to work with unions ``X ∪ Y``, intersections ``X ∩ Y`` and inclusions ``X ⊆ Y`` of sets, and how to prove basic facts about these things in Lean. The key trick is that ``X : set ℝ`` is internally represented as a map ``ℝ → Prop``. 

Introduction
------------

Let ``X`` be a set of real numbers. For any real number ``a`` we can ask if ``a`` is an element of ``X``. The notation for this is ``a ∈ X``, and of course it is a true/false statement, that is, a proposition. So given a set ``X`` we get a map ``ℝ → Prop``, sending a real number ``a`` to the true/false statement ``a ∈ X``. For example, if ``X`` is just the set ``{6}`` containng one element ``6``, then the associated map ``ℝ → Prop`` sends a real number ``a`` to the true/false statement ``a = 6``. To give another example -- if ``X`` is the set of positive real numbers, the associated map ``ℝ → Prop`` sends ``a`` to the true/false statement ``a > 0``.

Conversely, if ``p : ℝ → Prop`` is a function sending real numbers to true/false statements, then ``p`` divides the real numbers into two parts, namely the real numbers ``a`` such that ``p a`` is true, and those such that ``p a`` is false. So we could define a set ``X`` associated to ``p``, by letting ``X`` be exactly the real numbers for which ``p a`` is true. For example if ``p : ℝ → Prop`` is the function sending a real number ``a`` to the statement ``a ^ 2 = 4``, the corresponding subset ``X`` of real numbers is the real numbers ``a`` whose square equals ``4``, so ``X = {2, -2}``.

Hence what we have here is two different ways of thinking about the same concept. Given a subset of the real numbers, we get a map ``ℝ → Prop``, and conversely given such a map we can recover the subset as the real numbers being sent to the propositions which are true.

Inclusions
----------

Let ``X`` and ``Y`` be subsets of the real numbers, with corresponding functions ``pX`` and ``pY : ℝ → Prop``. We say that ``X`` is a *subset* of ``Y``, and write ``X ⊆ Y``, if every element of ``X`` is also an element of ``Y``. We could write this as "for all real numbers ``a``, ``a ∈ X → a ∈ Y``. So in fact the subset symbol ``⊆`` is just a disguised version of an implication of the form ``P → Q``, and we have seen how to prove such things in Lean. Let's prove that every set ``X`` of reals is a subset of itself by just treating ``⊆`` as what it really means.

.. code-block:: lean

   import data.real.basic

   example (X : set ℝ) : X ⊆ X :=
   begin
     -- remember the goal is just an elaborate notation
     -- for the proposition ∀ x : ℝ, x ∈ X → x ∈ X
     intro x,
     intro Hx,
     exact Hx,
   end

[It's probably worth mentioning that such fundamental facts like this are already in Lean and can be hence proved directly in one line. The result is known as "reflexivity of the subset relation" and a shorter proof looks like this:

.. code-block:: lean

   import data.real.basic

   example (X : set ℝ) : X ⊆ X := set.subset.refl X


]

Let's do a more complicated example. Let's start with two real numbers ``s`` and ``t``, with ``s<t``. If ``r`` is another real number, with ``r<s``, then of course ``r<t``. How do we know this? As mathematicians we are well aware that the statements `r<s` and `s<t` imply that `r<t`. This basic fact has a name -- "transitivity of the ``<`` relation". Lean just calls it ``lt_trans``.

.. code-block:: lean

   import data.real.basic

   example (r s t : ℝ) (Hrs : r < s) (Hst : s < t) : r < t :=
   begin
     exact lt_trans Hrs Hst
   end		

Let's stay with our fixed real numbers ``s`` and ``t`` with ``s < t``, and let's introduce some sets. We let :math:`X=\{x\in\mathbb{R}\,\mid\,x<s\}` and :math:`Y=\{x\in\mathbb{R}\,\mid\,x<t\}`.

		DRAW A PICTURE

We see :math:`X\subseteq Y` from the picture. Let's prove it in Lean.

.. code-block:: lean

   import data.real.basic

   example (s t : ℝ) (Hst : s < t) : {x : ℝ | x < s} ⊆ {x : ℝ | x < t} :=
   begin
     intro a,
     intro Ha,
     change a < s at Ha,
     show a < t,
     exact lt_trans Ha Hst,
   end

The ``change`` and ``show`` commands do the same thing and I don't really know why they have different names; ``change`` works on a hypothesis and ``show`` on the goal. Both of them can be used to simplify a proposition to something which is *by definition* the same. For example the proposition ``a ∈ {x : ℝ | x < s}`` literally means by definition that ``x < s`` is true when you let ``x = a``, so it literally means ``a < s``.
		
   
Intersections ``∩`` of sets
----------------------------

The *intersection* of two subsets ``X`` and ``Y`` of the real numbers is simply the real numbers which are in both ``X`` and ``Y``. The notation is ``X ∩ Y`` and you get the intersection symbol in Lean by typing ``\cap``.

Remember that a subset of the real numbers is just the same as a map R->prop. Let's translate the idea of intersection into this language. The statement ``a ∈ X ∩ Y`` means exactly that ``a`` is in both ``X`` and ``Y``. Let's set ``Z = X ∩ Y``. If ``pX`` is the map ``ℝ → Prop`` corresponding to ``X``, and ``pY`` and ``pZ`` are defined similarly, then we see that ``pZ x``, a.k.a. ``x ∈ Z``, is equivalent to ``x ∈ X ∧ x ∈ Y``, or in other words to ``pZ x ∧ pZ y``.

We have already learnt techniques for proving goals like ``P ∧ Q → P`` and we can use these techniques to prove basic facts about sets such as ``A ∩ B \subseteq A``.

.. code-block:: lean

   import data.real.basic

   example (X : set ℝ) (Y : set ℝ) : X ∩ Y ⊆ X :=
   begin
     -- recall that ⊆ is really a → in disguise, so we can use intro.
     intro a,
     intro Ha,
     -- Ha is really an "and" statement in disguise, so we can use cases.
     cases Ha with Hx Hy,
     exact Hx
   end

Exercise (symmetry of intersection)
-----------------------------------

Two sets are equal if and only if they have the same elements. Computer scientists call this "set extensionality" and in Lean the tactic for it is called ``ext``. Run the code below in Lean, see what the line ``ext a`` does to the goal, and then use the usual suspects like ``split`` and ``cases`` to solve the goal.

.. code-block:: lean

   import data.real.basic

   example (X : set ℝ) (Y : set ℝ) : X ∩ Y = Y ∩ X :=
   begin
     ext a
     sorry
   end

Exercise (this has nothing to do with the real numbers)
-------------------------------------------------------

Prove the same thing but for subsets of a general "Type". I would encourage the use of cut and paste.

.. code-block:: lean

   example (Ω : Type) (X : set Ω) (Y : set Ω) : X ∩ Y = Y ∩ X := sorry

Unions of sets.
===============

If ``X`` and ``Y`` are subsets of the real numbers (or of any type), their union ``X ∪ Y`` is defined to be the elements of the type which are in either ``X`` or ``Y`` or both. You get the notation ``∪`` in Lean by typing `\cup`. Just like ``∩`` is a disguised ``∧``, we have that ``∪`` is a disguised ``∨``. Let's prove symmetry of ``∪`` using the things we know about propositions.

.. code-block:: lean
		
   example (Ω : Type) (X : set Ω) (Y : set Ω) : X ∪ Y = Y ∪ X :=
   begin
     ext a,
     split,
     { intro Ha,
       cases Ha,
         -- a in X
         right,assumption,
         -- a in Y
         left,assumption
     },
     { intro Ha,
       cases Ha,
         -- a in Y
         right,assumption,
         -- a in X
         left,assumption
     },
   end

Exercise (set.subset_union_left)
--------------------------------

.. code-block:: lean
		
   example (Ω : Type) (X : set Ω) (Y : set Ω) : X ⊆ X ∪ Y :=
   begin
     sorry
   end

Exercise (logic and union)
--------------------------

.. code-block:: lean

   example (Ω : Type) (A B C : set Ω) (x : Ω) (HC : x ∈ C)
     (HA : x ∉ A) (HB : x ∉ B) : ¬ (C ⊆ A ∪ B) :=
   begin
     sorry
   end