Obtain function from exists_unique

Stream: new members

[Marc Masdeu]

If the conclusion of a lemma is that there exists a unique object, I'd like to have a function that gives me that object:

import tactic
import data.real.basic

noncomputable theory
open_locale classical

lemma my_lemma (x : ℝ): ∃! (m : ℤ), (m : ℝ) ≤ x ∧ x < m + 1 :=
begin
    sorry
end

def my_floor : ℝ → ℤ :=
begin
    sorry -- want to use my_lemma, not a an explicit construction of the floor function!
end

How would I do that? Thanks!

[Marc Masdeu]

(Ideally, my_floor would spit out not only an integer, but a pair of an integer and a proof of the two inequalities)

[Patrick Massot]

import tactic
import data.real.basic

noncomputable theory
open_locale classical

lemma my_lemma (x : ℝ): ∃! (m : ℤ), (m : ℝ) ≤ x ∧ x < m + 1 :=
begin
    sorry
end

def my_floor : ℝ → ℤ := λ x, classical.some (my_lemma x)

lemma my_floor_spec : ∀ x, (my_floor x : ℝ) ≤ x ∧ x < my_floor x + 1 :=
λ x : ℝ, (classical.some_spec (my_lemma x)).1

lemma my_floor_unique : ∀ x, ∀ y : ℤ, (y : ℝ) ≤ x ∧ x < y + 1 → y = my_floor x:=
λ x : ℝ, (classical.some_spec (my_lemma x)).2

[Julian Berman]

How come using obtain on my_lemma doesn't work for this

[Julian Berman]

(I see it doesn't, but I expected it to I guess)

[Julian Berman]

Oh it's saying you can't do that if my_floor is to return an integer and not a proposition?

[Marc Masdeu]

Thanks @Patrick Massot , I think this is what I want...

[Kevin Buzzard]

"cases only eliminates into Prop"

[Kevin Buzzard]

If you have a proof of "exists x, ..." and you want an x, then if your goal is a prop you can have it using cases, but if your goal is a type eg if you're building a function, then the virtual machine can't get data from the proposition because it can't cross from the prop universe into the type universe. You can extract it but you have to use a classical axiom. The easiest way in tactic mode is using the choose tactic -- this is what I usually direct beginners to rather than all this classical.some stuff

[Kevin Buzzard]

Basically you're using the axiom of choice in an essential way so obtain can't do it because obtain is constructive

[Kevin Buzzard]

The CS axiom of choice that is -- getting from Prop to Type.

[Eric Wieser]

Is there an analogy for the CS axiom of choice between other universe levels?