Zulip Chat Archive

Stream: new members

Topic: an element of set (set unit)


view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (May 10 2020 at 22:42):

dec_trivial should work but doesn't seem to

view this post on Zulip 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.

view this post on Zulip Bhavik Mehta (May 10 2020 at 22:44):

that instance is classical - does that affect things?

view this post on Zulip Kenny Lau (May 10 2020 at 22:44):

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

view this post on Zulip Mario Carneiro (May 10 2020 at 22:44):

You need decidable equality I think?

view this post on Zulip Kevin Buzzard (May 10 2020 at 22:45):

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

view this post on Zulip Mario Carneiro (May 10 2020 at 22:45):

that doesn't sound right though

view this post on Zulip Kenny Lau (May 10 2020 at 22:45):

the statement x = \empty is undecidable

view this post on Zulip Kevin Buzzard (May 10 2020 at 22:45):

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:45):

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

view this post on Zulip Mario Carneiro (May 10 2020 at 22:45):

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

view this post on Zulip Kevin Buzzard (May 10 2020 at 22:46):

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

view this post on Zulip Bhavik Mehta (May 10 2020 at 22:46):

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

view this post on Zulip Kevin Buzzard (May 10 2020 at 22:46):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 10 2020 at 22:47):

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

view this post on Zulip Kenny Lau (May 10 2020 at 22:47):

exactly

view this post on Zulip Mario Carneiro (May 10 2020 at 22:47):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 10 2020 at 22:48):

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

view this post on Zulip Mario Carneiro (May 10 2020 at 22:48):

there is another proof that avoids the assumption

view this post on Zulip Kevin Buzzard (May 10 2020 at 22:54):

Mario's instance above has one too many sets.

view this post on Zulip 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⟩⟩

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 10 2020 at 23:42):

I almost died writing this

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Jalex Stark (May 10 2020 at 23:53):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 11 2020 at 00:02):

If you have both fintype instances then you might have trouble

view this post on Zulip Mario Carneiro (May 11 2020 at 00:02):

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

view this post on Zulip Jalex Stark (May 11 2020 at 00:03):

mm interesting

view this post on Zulip 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