function definition by uniqueness

Stream: new members

[Cuong Tran]

I'm sorry for being naive. If we have a theorem: forall x, y exists uniquely z such that p(x, y, z), how can we define a function base on this theorem?

I guess this question has been asked many times but sorry I tried to search but got lost here. Thanks!

[Anne Baanen]

You can use docs#Exists.some, which doesn't even need uniqueness! (Although you have no idea which witness you'll get.)

[Anne Baanen]

For example (tested):

import logic.basic

noncomputable def choose {p : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∃! (k : ℕ), p n k) : ℕ → ℕ :=
λ n, (h n).exists.some

lemma choose_spec {p : ℕ → ℕ → Prop} (h : ∀ (n : ℕ), ∃! (k : ℕ), p n k) (n : ℕ) :
  p n (choose h n) :=
λ n, (h n).exists.some_spec

[Anne Baanen]

Although you might find it easier instead of using exists_unique, to define a function that returns the witness + a lemma stating this is the unique witness satisfying p(x, y, z).

[Cuong Tran]

Thank you @Anne Baanen for your keywords. Thank to them, I found this article as well and now have a better insight about Lean non-computable.