an element of set (set unit)

Stream: new members

[Bhavik Mehta]

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]

dec_trivial should work but doesn't seem to

[Kevin Buzzard]

import data.fintype.basic

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

doesn't either.

[Bhavik Mehta]

that instance is classical - does that affect things?

[Kenny Lau]

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

[Mario Carneiro]

You need decidable equality I think?

[Kevin Buzzard]

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

[Mario Carneiro]

that doesn't sound right though

[Kenny Lau]

the statement x = \empty is undecidable

[Kevin Buzzard]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Bhavik Mehta]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

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

[Kenny Lau]

exactly

[Mario Carneiro]

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

[Bhavik Mehta]

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

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

[Mario Carneiro]

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

[Mario Carneiro]

there is another proof that avoids the assumption

[Kevin Buzzard]

Mario's instance above has one too many sets.

[Mario Carneiro]

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]

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]

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]

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

[Kenny Lau]

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]

I almost died writing this

[Jalex Stark]

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]

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]

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]

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

[Jalex Stark]

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]

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]

If you have both fintype instances then you might have trouble

[Mario Carneiro]

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

[Jalex Stark]

mm interesting

[Mario Carneiro]

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