## Stream: new members

### Topic: an element of set (set unit)

#### Bhavik Mehta (May 10 2020 at 22:28):

Here's a MWE:

lemma pp1 (x : set (set unit)) : x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {∅, {()}} :=
sorry


Golf away! (This came up in the middle of some category theory which I'm hoping to make into a kata)

#### Kevin Buzzard (May 10 2020 at 22:42):

dec_trivial should work but doesn't seem to

#### Kevin Buzzard (May 10 2020 at 22:42):

import data.fintype.basic

example (X : Type) [fintype X] : fintype (set X) := by apply_instance


doesn't either.

#### Bhavik Mehta (May 10 2020 at 22:44):

that instance is classical - does that affect things?

#### Kenny Lau (May 10 2020 at 22:44):

they don't work because set X doesn't have decidable equality

#### Mario Carneiro (May 10 2020 at 22:44):

You need decidable equality I think?

#### Kevin Buzzard (May 10 2020 at 22:45):

Then why doesn't dec_trivial work for Bhavik's lemma?

#### Mario Carneiro (May 10 2020 at 22:45):

that doesn't sound right though

#### Kenny Lau (May 10 2020 at 22:45):

the statement x = \empty is undecidable

#### Kevin Buzzard (May 10 2020 at 22:45):

example (X : Type) [decidable_eq X] [fintype X] : fintype (set X) := by apply_instance works

#### Kenny Lau (May 10 2020 at 22:45):

because x can be the set of counter-examples to Riemann's hypothesis

#### Mario Carneiro (May 10 2020 at 22:45):

You should not need decidable equality to produce this set, it's just powerset fintype.univ

#### Kevin Buzzard (May 10 2020 at 22:46):

Aah, but maybe it doesn't have decidable equality!

#### Bhavik Mehta (May 10 2020 at 22:46):

I'm totally okay with noncomputable/classical proofs for this, by the way

#### Kevin Buzzard (May 10 2020 at 22:46):

example (X : Type) [decidable_eq X] [fintype X] : decidable_eq (set X) := by apply_instance -- fails

#### Mario Carneiro (May 10 2020 at 22:47):

The only requirement of fintype is that you have a constructible list of elements that are all (classically) provably exhaustive and distinct from each other

#### Kevin Buzzard (May 10 2020 at 22:47):

so set (set unit) might not be a fintype after all :-) in constructiveland

exactly

#### Mario Carneiro (May 10 2020 at 22:47):

An instance of fintype (set (set unit)) is <{univ, empty}, <classical proof>>

#### Bhavik Mehta (May 10 2020 at 22:48):

in data.fintype the instance set.fintype is given:

instance set.fintype [decidable_eq α] [fintype α] : fintype (set α) :=
pi.fintype


#### Mario Carneiro (May 10 2020 at 22:48):

I see, if that's the proof then that explains it

#### Mario Carneiro (May 10 2020 at 22:48):

there is another proof that avoids the assumption

#### Kevin Buzzard (May 10 2020 at 22:54):

Mario's instance above has one too many sets.

#### Mario Carneiro (May 10 2020 at 22:57):

instance set.fintype [fintype α] : fintype (set α) :=
⟨(@finset.univ α _).powerset.map ⟨coe, to_set_injective⟩, λ s,
by classical; simp [subset_univ]; exact ⟨finset.univ.filter s, by simp; refl⟩⟩


#### Mario Carneiro (May 10 2020 at 22:59):

which is at least enough to prove

#eval fintype.card (set (set unit)) -- 4


(which indeed shows that I don't have enough sets in my instance)

#### Jalex Stark (May 10 2020 at 23:28):

I have a solution up to this sorry

example
(x : set (set unit))
(hx : x ⊆ {∅, {()}}) :
x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {∅, {()}} :=
sorry


(I tried using mario's fintype instance to convince dec_trivial to do it but that didn't work)

#### Mario Carneiro (May 10 2020 at 23:29):

You should be able to use the fintype instance to do this, although some rewriting is necessary

#### Kenny Lau (May 10 2020 at 23:42):

import data.fintype.basic data.set.finite

universes u v

noncomputable def finset_equiv_set (α : Type u) [fintype α] : finset α ≃ set α :=
⟨coe, λ x, (set.finite.of_fintype x).to_finset,
λ x, finset.ext' \$ λ y, by rw [set.finite.mem_to_finset, finset.mem_coe],
λ x, set.finite.coe_to_finset _⟩

def finset_congr {α : Type u} {β : Type v} [decidable_eq α] [decidable_eq β] (e : α ≃ β)
: finset α ≃ finset β :=
⟨finset.map e.to_embedding, finset.map e.symm.to_embedding,
λ s, by { simp_rw [finset.map_eq_image, finset.image_image], convert finset.image_id,
ext x, exact e.symm_apply_apply x, apply_instance },
λ s, by { simp_rw [finset.map_eq_image, finset.image_image], convert finset.image_id,
ext x, exact e.apply_symm_apply x, apply_instance }⟩

lemma pp1 (x : set (set unit)) : x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {∅, {()}} :=
begin
haveI := classical.dec_eq (set unit),
rw [set.insert_eq, set.union_comm, ← set.insert_eq],
rw ← (set.finite.of_fintype x).coe_to_finset,
generalize : (set.finite.of_fintype x).to_finset = s,
rcases (finset_congr (finset_equiv_set unit)).bijective.2 s with ⟨s, rfl⟩,
change finset_congr (finset_equiv_set unit) s with finset.map _ s,
simp_rw [← finset.coe_empty, ← finset.coe_singleton, ← finset.coe_insert, finset.coe_inj],
rcases finset.mem_univ s with rfl|rfl|rfl|rfl|H,
{ left, refl },
{ right, left, refl },
{ right, right, left, refl },
{ right, right, right,
erw ← finset.map_singleton (finset_equiv_set unit).to_embedding,
erw ← finset.map_insert (finset_equiv_set unit).to_embedding,
refl },
{ cases H }
end


#### Kenny Lau (May 10 2020 at 23:42):

I almost died writing this

#### Jalex Stark (May 10 2020 at 23:45):

I guess this is obsoleted by kenny's submission, but I just finished and don't want to chuck it in the wastebin

lemma pp0_aux (x : unit) : x = () := begin
exact punit_eq x (),
end

lemma pp0 (x : set unit) : x = ∅ ∨ x = {()} :=
begin
by_cases set.nonempty x,
swap,
{ left, ext, split,
{intro h2, exfalso, revert h, suffices q: set.nonempty x, cc,
exact set.nonempty_of_mem h2},
simp only [set.mem_empty_eq, forall_prop_of_false, not_false_iff],
},
right, ext, rw set.mem_singleton_iff,
split,
{intro, apply pp0_aux,},
intro h, rw h, clear h x_1,
have hy:= h.some_mem,
have key := pp0_aux h.some,
rwa ← key,
end

lemma pp1_aux (x : set (set unit)) (hx : x ⊆ {∅, {()}}) : x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {∅, {()}} := begin
by_cases ∅ ∈ x;
by_cases {()} ∈ x,
right, right, right,
rotate, right, left,
rotate, right, right, left,
rotate, left,
all_goals {ext, split, swap, finish},
all_goals {intro hx_1, rw set.subset_def at hx,
have key := hx x_1 hx_1, clear hx},
all_goals {try {finish}},
end

theorem pp1 (x : set (set unit)) : x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {∅, {()}} :=
begin
have key : x ⊆ {∅, {()}},
{rw set.subset_def, intros a ha,
have key := pp0 a, finish},
apply pp1_aux, exact key,
end


#### Jalex Stark (May 10 2020 at 23:46):

is there a trick to copying long code blocks out of a zulip message? I always find myself fussing with the mouse for like twenty seconds
EDIT: the trick is to press the "view source" button, that gives you a focus window in which you can ctrl+a to select all

#### Mario Carneiro (May 10 2020 at 23:51):

Here's what you can accomplish by abusing defeq given the fintype instance:

import data.fintype.basic

example (x : set (set unit)) :
x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {∅, {()}} :=
begin
have := finset.mem_univ x,
change x = ∅ ∨ x = ↑(finset.singleton ∅) ∨ x = ↑_ ∨ x = ↑_ ∨ false at this,
let c : set unit := ↑(finset.singleton ()),
let a : finset (set unit) := finset.mk (quotient.mk' [c]) _,
let b : finset (set unit) := finset.mk (quotient.mk' [∅, c]) _,
change x = ∅ ∨ x = ↑(finset.singleton ∅) ∨ x = ↑a ∨ x = ↑b ∨ false at this,
end


#### Jalex Stark (May 10 2020 at 23:53):

unkown identifier mem_univ? is it missing open finset or something?

#### Jalex Stark (May 11 2020 at 00:00):

for some reason even this (the second apply_instance) fails for me

instance set.fintype [fintype α] : fintype (set α) :=
⟨(@finset.univ α _).powerset.map ⟨coe, to_set_injective⟩, λ s,
by classical; simp [subset_univ]; exact ⟨finset.univ.filter s, by simp; refl⟩⟩

example (x : set (set unit)) :
x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {∅, {()}} :=
begin
have inst_1 : fintype (set unit) := by apply_instance,
have inst_2 : fintype (set (set unit)) := by apply_instance,
end


#### Mario Carneiro (May 11 2020 at 00:02):

import data.fintype.basic
example (x : set (set unit)) : x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {∅, {()}} :=
begin
have := finset.mem_univ x,
change x = ∅ ∨ x = {∅} ∨ x = {{()}} ∨ x = {{()}, ∅} ∨ false at this,
simpa [singleton, set.insert_comm ∅, or_false]
end


#### Mario Carneiro (May 11 2020 at 00:02):

If you have both fintype instances then you might have trouble

#### Mario Carneiro (May 11 2020 at 00:02):

I modified data.fintype.basic to replace the original instance

mm interesting

#### Mario Carneiro (May 11 2020 at 00:04):

For this trick to work you need to know exactly how everything is defined so that you can get the change line right

Last updated: May 16 2021 at 05:21 UTC