finset.drop_none

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have a definition equivalent to

def finset.drop_none (s : finset (option α)) : finset α :=
s.bUnion (λ o, o.to_finset)

but without the need for [decidable_eq α]? If not, what is the best way to define it? Go all the way from list? Use some existing defs?

[Yakov Pechersky]

docs#finset.filter

[Yakov Pechersky]

Filter for ne none? That might be decidable regardless of decidability of base type

[Eric Wieser]

Perhaps something like this?

lemma option.eq_of_mem : ∀ {a₁ a₂ : option α} {b} (ha₁ : b ∈ a₁) (ha₂ : b ∈ a₂), a₁ = a₂
| (some _) (some _) _ rfl rfl := rfl

def finset.drop_none (s : finset (option α)) : finset α :=
⟨s.1.filter_map id, multiset.nodup_filter_map _ (λ a₁ a₂ b, option.eq_of_mem) s.nodup⟩

[Eric Wieser]

removed the sorry above.

[Floris van Doorn]

@Yakov Pechersky you then still need to map from option α to α, which is annoying (docs#finset.map wouldn't work).

[Yury G. Kudryashov]

I came up with

def unoption (s : finset (option α)) : finset α :=
(s.subtype $ λ o : option α, o.is_some).map (equiv.option_is_some_equiv α).to_embedding

It uses existing operations, so I can prove API lemmas by simp [unoption].

[Eric Wieser]

I would have though you could prove lemmas about my version by coercing to multiset with ext or similar

[Eric Wieser]

Are they defeq?

[Yakov Pechersky]

(deleted)

[Yakov Pechersky]

docs#finset.pmap

[Yakov Pechersky]

That's too bad that that doesn't exist

[Yury G. Kudryashov]

#9630