The axiom of choice
===================

The axiom of choice was something I found quite complicated as an undergraduate; it was summarised as "you can make infinitely many choices at the same time" but because I didn't really know much about set theory it took me a while before this description made any sense.

In Lean's type theory, the situation is much simpler (at least in my mind). There are two universes in Lean (at least for the purposes of this course) -- ``Prop`` and ``Type``. The ``Prop`` universe is for proofs, and the ``Type`` universe is for data. The axiom of choice is a route from the ``Prop`` universe to the ``Type`` universe. In other words, it is a way of getting data from a proof.

nonempty X
----------

If ``X : Type`` then ``nonempty X : Prop`` is the true-false statement asserting that ``X`` is nonempty, or equivalently, that there's a term of type ``X``. For example here's part of the API for ``nonempty``:

.. code-block::
   
   import tactic

   example (X : Type) : (∃ x : X, true) ↔ nonempty X :=
   begin
     exact exists_true_iff_nonempty
   end

This example shows that given a term of type ``nonempty X``, you can get a term of type ``∃ x : X, true`` (i.e., "there exists an element of ``X`` such that a true statement is true"). We would now like to go from this to actually *get* a term of type ``X``! In constructive mathematics this is impossible: because ``h`` lives in the ``Prop`` universe, Lean forgot how it was proved. However in classical mathematics we can pass from the ``Prop`` universe to the ``Type`` universe with ``classical.choice h``, a term of type `X`. This gives us a "noncomputable" term of type ``X``, magically constructed only from the proof ``h`` that ``X`` was nonempty. Mathematically, "noncomputable" means "it exists, but we don't actually have an algorithm or a formula for it". This is a subtlety which is often not explicitly talked about in mathematics courses, probably because it is often not relevant in a mathematical argument.

You might wonder what the code for this ``classical.choice`` function looks like, but in fact there isn't any code for it; Lean simply declares that ``classical.choice`` is an ``axiom``, just like how in set theory the axiom of choice is declared to be an axiom.

When I first saw this axiom, it felt to me like it was way weaker than the set theory axiom of choice; in set theory you can make infinitely many choices of elements of nonempty sets all at once, whereas in Lean we're just making one choice. But later on I realised that in fact you could think of it as much *stronger* than the set theory axiom of choice, because you can interpret ``classical.choice`` as a function which makes, once and for all, a choice of an element of *every single nonempty type*, so it easily implies the usual set-theoretic axiom of choice.

classical.some
--------------

In my experience, the way people want to use the axiom of choice when doing mathematics in Lean is to get an element of X not from a hypothesis ``∃ x : X, true``, but from a hypothesis like ``∃ x : X, x^2 = 2`` or more generally ``∃ x : X, p x`` where ``p : X → Prop`` is a predicate on ``X``. The way to do this is as follows: you run ``classical.some`` on ``h : ∃ x : X, p x`` to get the element of ``X``, and the proof that this element satisfies ``p`` is ``classical.some_spec h``. Here's a worked example.

.. code-block::

   import analysis.complex.polynomial -- import proof of fundamental theorem of algebra
   
   open_locale polynomial -- so I can use notation ℂ[X] for polynomial rings
   
   open polynomial -- so I can write `X` and not `polynomial.X`
   
   noncomputable theory -- we are not supplying algorithms for being able
   -- to compute what is about to happen
   
   def f : ℂ[X] := X^5 + X + 37 -- a random polynomial
   
   theorem f_has_a_root : ∃ (z : ℂ), f.is_root z :=
   begin
     apply complex.exists_root, -- the fundamental theorem of algebra
     -- it remains to show that f has degree > 0
     sorry -- proof omitted (more annoying than you would think!)
   end
   
   -- let z be a root of f
   def z : ℂ := classical.some f_has_a_root
   
   -- proof that z is a root of f
   theorem z_is_a_root_of_f : f.is_root z :=
   begin
     exact classical.some_spec f_has_a_root,
   end