## Stream: new members

### Topic: Escaping Prop

#### Marcus Rossel (May 15 2021 at 17:11):

Say we have the following function:

def f (s : set ℕ) (h : (s = ∅) ∨ (∃! n, s = {n})) : option ℕ :=
sorry


What this function is supposed to do is:

* if s = ∅, return none
* if s = {n}, return n

We know that one of these conditions holds, by virtue of h.
How can this behaviour be expressed in Lean?

My first attempt was to do this by elimination on h, but that only allows me to return Props.
I feel like classical must play a role in order to extract n from h, but I don't know how.

#### Floris van Doorn (May 15 2021 at 17:15):

The way to do what you ask is to use docs#classical.some for a well-chosen predicate p (basically the predicate you wrote in words).

If you care about computability/constructivity at all, you will want to reformulate the type of f.

#### Johan Commelin (May 15 2021 at 17:19):

Unrelated, but I would just ask for exists n, s = {n} instead of asking for the uniqueness as well. Because uniqueness is automatic, so it will quickly become boring to prove it every time you need to provide h.

#### Kevin Buzzard (May 15 2021 at 19:00):

Do we have docs#set.subsingleton ?

#### Kevin Buzzard (May 15 2021 at 19:03):

Apparently we do, so perhaps we should have set.subsingleton.rec_on?

#### Adam Topaz (May 15 2021 at 19:04):

docs#set.subsingleton.induction_on

#### Kevin Buzzard (May 15 2021 at 19:04):

Yes but that's only to Prop

Ah

#### Adam Topaz (May 15 2021 at 19:13):

Here's some code for the original question, in case it helps:

import data.set.basic

open_locale classical

noncomputable def f {α} {S : set α} (h : S.subsingleton) : option α :=
h.eq_empty_or_singleton.by_cases (λ _, none) (λ hh, some \$ classical.some hh)


#### Kevin Buzzard (May 15 2021 at 21:46):

Oh so it seems we do have the recursor :-)

#### Marcus Rossel (May 28 2021 at 08:58):

Does something like subsingleton exist for finset, too?
I'm using .card ≤ 1 right now, but that doesn't come with .eq_empty_or_singleton.

#### Marcus Rossel (May 28 2021 at 09:07):

In other words, is there a way to get the unique element out of a finset with .card ≤ 1?

#### Kevin Buzzard (May 28 2021 at 09:19):

You mean card = 1, right? The answer will be yes because surely this is the point of finsets.

#### Ruben Van de Velde (May 28 2021 at 09:20):

docs#finset.card_eq_one

#### Marcus Rossel (May 28 2021 at 09:20):

No, I mean.card ≤ 1.
For a finset X with .card ≤ 1 I would like to get an instance of option X.

#### Ruben Van de Velde (May 28 2021 at 09:21):

Also docs#finset.card_le_one and docs#finset.card_le_one_iff exist (and they're both iffs)

#### Marcus Rossel (May 28 2021 at 09:22):

Ruben Van de Velde said:

Also docs#finset.card_le_one and docs#finset.card_le_one_iff exist (and they're both iffs)

The problem is that I don't understand how to use these to actually get the instance out of the finset.
I feel like I would need a theorem that contains ∃.

#### Kevin Buzzard (May 28 2021 at 09:24):

You want to do this constructively, presumably? Classically you can just use classical.some

#### Marcus Rossel (May 28 2021 at 09:25):

No, non-constructively is perfectly fine.

#### Ruben Van de Velde (May 28 2021 at 09:26):

Is this for a definition or in a proof?

for a definition

#### Ruben Van de Velde (May 28 2021 at 09:27):

Then docs#classical.some could help

#### Marcus Rossel (May 28 2021 at 09:29):

For that I need an ∃-proof though.
And f.card ≤ 1 is equivalent to f = ∅ ∨ (∃! x, {x} = f), but I guess mathlib doesn't have a lemma for that.

#### Marcus Rossel (May 28 2021 at 09:33):

Cool! Now I just need to figure out how to convert f ⊆ {x} into f = ∅ ∨ (∃! x, {x} = f).

#### Marcus Rossel (May 28 2021 at 09:35):

Which should be possible with docs#set.subsingleton.mono, docs#set.subsingleton_singleton and docs#set.subsingleton.eq_empty_or_singleton

#### Yakov Pechersky (May 28 2021 at 13:15):

You can use finset.find (can't remember the exact name atm) , which is computable

Last updated: Dec 20 2023 at 11:08 UTC