Stream: new members

Topic: Obtain function from exists_unique

Marc Masdeu (Oct 07 2020 at 17:50):

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 (Oct 07 2020 at 17:52):

(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 (Oct 07 2020 at 17:55):

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 (Oct 07 2020 at 17:58):

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

Julian Berman (Oct 07 2020 at 17:58):

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

Julian Berman (Oct 07 2020 at 18:00):

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

Marc Masdeu (Oct 07 2020 at 18:00):

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

Kevin Buzzard (Oct 07 2020 at 21:37):

"cases only eliminates into Prop"

Kevin Buzzard (Oct 07 2020 at 21:40):

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 (Oct 07 2020 at 21:42):

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

Kevin Buzzard (Oct 07 2020 at 21:42):

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

Eric Wieser (Oct 07 2020 at 21:47):

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

Last updated: May 15 2021 at 00:39 UTC