Escaping Prop

Stream: new members

[Marcus Rossel]

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]

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]

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]

Do we have docs#set.subsingleton ?

[Kevin Buzzard]

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

[Adam Topaz]

docs#set.subsingleton.induction_on

[Kevin Buzzard]

Yes but that's only to Prop

[Adam Topaz]

Ah

[Adam Topaz]

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]

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

[Marcus Rossel]

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]

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

[Kevin Buzzard]

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

[Ruben Van de Velde]

docs#finset.card_eq_one

[Marcus Rossel]

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]

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

[Marcus Rossel]

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]

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

[Marcus Rossel]

No, non-constructively is perfectly fine.

[Ruben Van de Velde]

Is this for a definition or in a proof?

[Marcus Rossel]

for a definition

[Ruben Van de Velde]

Then docs#classical.some could help

[Marcus Rossel]

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.

[Eric Rodriguez]

docs#finset.card_le_one_iff_subset_singleton?

[Marcus Rossel]

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

[Marcus Rossel]

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

[Yakov Pechersky]

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