Going from "exists unique" to a function

Stream: general

[Martin C. Martin]

In math, we often prove "for all x, there exists y such that ...", then prove that y is unique, then define a function mapping x to y. For example, a common group axiom is "For each a in G, there exists an element b in G such that a ⋅ b = e and b ⋅ a = e, where e is the identity element." (Taken from Wikipedia.) We then prove that the inverse is unique, which lets us declare a function taking an element to its inverse.

How is this done in Lean? I found a CMU master's thesis on formalizing group theory in Lean, but it starts with the inverse function, not a proposition on the existence of the inverse. https://www.andrew.cmu.edu/user/avigad/Students/zipperer_ms_thesis.pdf

The book "Logic and Proof" chapter 16 "Functions in Lean" mentions this, including iota notation, but doesn't say how to render this in Lean. 16.4 "Defining the inverse classically" gets close, but talks about the case where you HAVEN'T proven uniqueness, and therefore you need to invoke the axiom of choice. As I understand it, in the case of exists UNIQUE, you don't need to invoke AoC, and a constructive proof of "for all x exists y," which provides a witness for y, essentially gives you a way to compute y from x.

So, is iota notation common in Lean? For example, is it used for inverse in group, or the square root function on real numbers?

[Adam Topaz]

docs#classical.some gives a choice, once and for all, for every existential statement in the system, while docs#classical.some_spec gives the proof that this choice satisfies the proposition in the existential.

[Adam Topaz]

as far as I know, even if you have a proof of unique existence, this classical.some is still the only way to "produce" a function

[Yakov Pechersky]

In mathlib, we have ∃! notation. And one can define a noncomputable function that extracts an element from an exists proposition. If you postulate that ∃!, then the proof that the term the function produces is unique is true by definition, because you postulated it to be so. For finite types, one can even do this computably.

[Jeremy Avigad]

NB Andrew's thesis is pretty outdated...

As far as using some:

noncomputable theory

theorem exists_even : ∃ x : nat, even x :=
⟨2, ⟨1, by norm_num⟩⟩

def my_even := classical.some exists_even

theorem even_my_even : even my_even :=
classical.some_spec _

If you have have unique existence, you can prove moreover that anything meeting the specification is equal to the value returned by some.

[Yakov Pechersky]

docs#finset.choose and docs#fintype.choose are the computable way of eliminating a unique existence, over a finite set or type.

[Johan Commelin]

There's also tactic#choose

[Alistair Tucker]

As I understand it ... a constructive proof of "for all x exists y," which provides a witness for y, essentially gives you a way to compute y from x.

If your proof is genuinely constructive then you needn't touch Prop at all.. That is, instead of using it to prove (∀ x, ∃ y, r x y : Prop), use it to define (Π x, {y // r x y} : Type).

[Kevin Buzzard]

My understanding is that in set theory, if you know there's a unique y such that R x y then you can define a function sending x to y, but in Lean's type theory you still need choice in general.

[Eric Wieser]

docs#fintype.choose does not use choice

[Adam Topaz]

Eric Wieser said:

docs#fintype.choose does not use choice

Right, it all comes down to docs#list.choose_x

[Yakov Pechersky]

The lisp guys were right, it's S expressions all the way down...