.. _tac_choose:

choose
======

Summary
-------

The ``choose`` tactic is a relatively straightforward way to go from a proof of a proposition of the form ``∀ x, ∃ y, P(x,y)`` (where ``P(x,y)`` is some true-false statement depend on ``x`` and ``y``), to an actual *function* which inputs an ``x`` and outputs a ``y`` such that ``P(x,y)`` is true.


Basic usage
-----------

The simplest situation where you find yourself wanting to use ``choose`` is if you have a function ``f : X → Y`` which you know is surjective, and you want to write down a one-sided inverse ``g : Y → X``, i.e., such that ``f(g(y))=y`` for all ``y : Y``. Here's the set-up:

.. code-block::

   import tactic

   example (X Y : Type) (f : X → Y) (hf : ∀ y, ∃ x, f x = y) : ∃ g : Y → X, ∀ y, f (g y) = y :=
   begin
     sorry
   end

The difficulty here is that you don't have ``g`` to hand, you're going to have to make it on the fly in the middle of this proof, so you can't do anything like ``definition g := ...`` (which you could do outside the proof), because ``definition`` isn't a tactic. Here's the proof:

.. code-block::
   
   begin
     choose g hg using hf,
     use g,
     exact hg,
   end

The ``choose`` tactic creates both the function ``g`` and the proof ``hg`` that it does what you want it to do.

Example usage in analysis
-------------------------

Sometimes in analysis you have a proof that for all :math:`\epsilon>0` there's some ``x`` (depending on :math:`\epsilon`) with some property (which depends on ``x`` and :math:`\epsilon` and possibly some other things). And from this you want to get a sequence :math:`x_1,x_2,x_3,\ldots` which satisfy the condition for smaller and smaller :math:`\epsilon`. Typically in a lecture one would say "let :math:`x_n` be any ``x`` satisfying the property for :math:`\epsilon=1/n` and this sequence clearly works". Here's how one might construct that sequence in Lean.

.. code-block::
   
   import tactic
   import data.real.basic

   example (X : Type) (P : X → ℝ → Prop) -- `X` is an abstract type and `P` is an abstract true-false
                                         -- statement depending on an element of `X` and a real number.
    (h : ∀ ε > 0, ∃ x, P x ε)            -- `h` is the hypothesis that given some `ε > 0` you can find
                                         -- an `x` such that the proposition is true for `x` and `ε`
    :                                    -- Conclusion:
    ∃ u : ℕ → X, ∀ n, P (u n) (1/(n+1))  -- there's a sequence of elements of `X` satisfying the
                                         -- condition for smaller and smaller ε
    :=  
   begin
     choose g hg using h,
     /-
     g : Π (ε : ℝ), ε > 0 → X
     hg : ∀ (ε : ℝ) (H : ε > 0), P (g ε H) ε
     -/
     let u : ℕ → X := λ n, g (1/(n+1)) (begin
       -- need to prove 1/(n+1)>0 (this is why I chose 1/(n+1) not 1/n, as 1/0=0 in Lean!)
       show (0 : ℝ) < 1/(n+1),
       rw one_div_pos, -- `linarith` can't deal with `/`
       norm_cast, -- or `↑`; it knows `n ≥ 0` but doesn't know `↑n ≥ 0`
       linarith,
     end),
     use u, -- `u` works
     intro n,
     apply hg,
   end