Choosing arbitrary element from a nonempty subset of ℕ

Stream: new members

[Gaëtan Serré]

Hello, I was wondering I can construct a function that, given an element e, it returns an arbitrary element of the set {n : ℕ | p(e)}, where I can prove that this set is nonempty for any e. For example:

def f (e : ℕ) := arbitrary_elem {n : ℕ | n <= e}

[Patrick Massot]

docs#Nat.find

[Gaëtan Serré]

Thanks a lot! I was not looking in the right place in the doc…

[Gaëtan Serré]

Ok that's lead to another problem. Here is my context:

E: Set u
h: ∀ e ∈ E, ∃ n, f n = e

The idea is to construct a function g : u → ℕ such that, on E, g e returns an arbitrary (let's says the smallest) n such that f n = e. On the complementary set, I don't care what natural number it returns (let's say 0). The issue is that, in order to use docs#Nat.find, I need the proof that e ∈ E. I looked docs#Set.indicator, docs#Set.piecewise and docs#Pi.single but none seems to "propagate" the proof to the function. Is there a way to do that? Note that the property that e ∈ E is Decidable is not an issue here.

[Gaëtan Serré]

I apologize if it is a dumb question. It is the first time I deal with this kind of issue

[Kyle Miller]

There's also docs#Set.Nonempty.some, which works for all sets (not just sets of natural numbers), and it avoids any Decidable instances.

You could also use sInf of your set to take its infimum. This doesn't itself take a nonemptiness assumption (and it ends up giving 0 if the set is empty), but you need nonemptiness for docs#Nat.sInf_mem

[Kyle Miller]

Instead of sharing contexts, you can usually get better help if you share a #mwe, which is some code that can be pasted into the editor, ideally with the question corresponding to some piece of the code that needs to be filled in.

[Sophie Morel]

variable (u : Type*) (E : Set u) (f : ℕ → E) (h: ∀ e ∈ E, ∃ n, f n = e)
  [∀ (x : u), Decidable (x ∈ E)] [∀ (x : u) (n : ℕ), Decidable (f n = x)]

def g : u → ℕ := fun x ↦ if hx : x ∈ E then Nat.find (h x hx) else 0

?

[Gaëtan Serré]

Kyle Miller said:

There's also docs#Set.Nonempty.some, which works for all sets (not just sets of natural numbers), and it avoids any Decidable instances.

You could also use sInf of your set to take its infimum. This doesn't itself take a nonemptiness assumption (and it ends up giving 0 if the set is empty), but you need nonemptiness for docs#Nat.sInf_mem

Thanks for all the references!

Instead of sharing contexts, you can usually get better help if you share a #mwe, which is some code that can be pasted into the editor, ideally with the question corresponding to some piece of the code that needs to be filled in.

You're totally right, I don't know why I did not provided a mwe this time, sorry for that

[Gaëtan Serré]

Sophie Morel said:

variable (u : Type*) (E : Set u) (f : ℕ → E) (h: ∀ e ∈ E, ∃ n, f n = e)
  [∀ (x : u), Decidable (x ∈ E)] [∀ (x : u) (n : ℕ), Decidable (f n = x)]

def g : u → ℕ := fun x ↦ if hx : x ∈ E then Nat.find (h x hx) else 0

?

Awesome, thanks a lot! I tried something like that earlier but it did not typechecked for some reason...