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:

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:

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 \(\epsilon>0\) there’s some x (depending on \(\epsilon\)) with some property (which depends on x and \(\epsilon\) and possibly some other things). And from this you want to get a sequence \(x_1,x_2,x_3,\ldots\) which satisfy the condition for smaller and smaller \(\epsilon\). Typically in a lecture one would say “let \(x_n\) be any x satisfying the property for \(\epsilon=1/n\) and this sequence clearly works”. Here’s how one might construct that sequence in Lean.

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