Zulip Chat Archive

Stream: new members

Topic: Obtain function from exists_unique


view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 07 2020 at 17:58):

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

view this post on Zulip Julian Berman (Oct 07 2020 at 17:58):

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

view this post on Zulip 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?

view this post on Zulip Marc Masdeu (Oct 07 2020 at 18:00):

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

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 21:37):

"cases only eliminates into Prop"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 07 2020 at 21:42):

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

view this post on Zulip 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