## Stream: new members

### Topic: instance of decidable_set_is_empty

#### Ciprian Teodorov (May 02 2020 at 15:52):

Hi all,
is it possible to create an instance of decidable if a set is empty ?

instance decidable_is_empty
(α : Type)
[H₀: decidable_eq α]
[H₁: fintype α]
: Π (S : set α), decidable (S = ∅) := sorry


#### Reid Barton (May 02 2020 at 15:54):

Assuming you want to do it constructively, you also need to assume decidable_pred S.

#### Ciprian Teodorov (May 02 2020 at 16:05):

Reid Barton said:

Assuming you want to do it constructively, you also need to assume decidable_pred S.

ok, but still I have no idea where to start, after intros I get one goal that I don't know how to tackle

1 goal
H₀ : decidable_eq α,
H₁ : fintype α,
S : set α,
H₂ : decidable_pred S
⊢ decidable (S = ∅)


#### Jalex Stark (May 02 2020 at 18:01):

a #mwe is a lot better than a tactic state

#### Ciprian Teodorov (May 02 2020 at 18:06):

@Jalex Stark the exemple is in my first post

#### Jalex Stark (May 02 2020 at 18:08):

Oh thanks, I should read harder

#### Ciprian Teodorov (May 02 2020 at 18:09):

Basically I'm blocked after intros, i've tried to lookup similar code online, but did not find my inspiration

#### Kevin Buzzard (May 02 2020 at 18:20):

import data.fintype.basic

instance decidable_is_empty (α : Type*) [decidable_eq α] [fintype α]
(S : set α) [decidable_pred S] : decidable (S = ∅) :=
begin
by_cases h : ∃ x : α, x ∈ S,
{ apply is_false,
intro hS,
cases h with a ha,
rw hS at ha,
cases ha
},
{ apply is_true,
push_neg at h,
refine eq_bot_iff.mpr h, -- crazy library_search answer
}
end

#print axioms decidable_is_empty
/-
propext
quot.sound
-/


I don't know anything about constructivism, I don't know whether the list of axioms is acceptable.

#### Kevin Buzzard (May 02 2020 at 18:23):

import data.fintype.basic

open_locale classical

noncomputable instance decidable_is_empty (α : Type*) (S : set α) : decidable (S = ∅) :=
by apply_instance


That's how I'd do it, but presumably that's not what you're looking for

No no!

oh I see

#### Reid Barton (May 02 2020 at 18:24):

Still, I think you are supposed to use decidable_of_iff for this

#### Kevin Buzzard (May 02 2020 at 18:25):

How are my axioms (when I was pretending not to be a mathematician)?

#### Reid Barton (May 02 2020 at 18:26):

Your axioms are fine for constructivity, but it's still possible to write decidable instances with bad reduction behavior without extra axioms, I think

#### Reid Barton (May 02 2020 at 18:26):

I can't tell easily whether your definition is good.

#### Reid Barton (May 02 2020 at 18:26):

Actually, it is fine. But decidable_of_iff is clearer

#### Kevin Buzzard (May 02 2020 at 18:27):

my lovely tactic mode proof isn't clear??

#### Reid Barton (May 02 2020 at 18:27):

This is a construction, not a proof

#### Kevin Buzzard (May 02 2020 at 18:28):

well the computer scientists call it a construction...

#### Kevin Buzzard (May 02 2020 at 18:28):

my noncomputable construction may as well be a proof :-)

#### Reid Barton (May 02 2020 at 18:28):

Yes, a proof of true.

#### Reid Barton (May 02 2020 at 18:30):

Or as the "computer scientists" call it, p ∨ ¬ p

same thing!

#### Kevin Buzzard (May 02 2020 at 18:31):

I think sarcasm should be an axiom.

#### Kevin Buzzard (May 02 2020 at 18:32):

wow, so decidable is a type. I guess I shouldn't have used tactic mode after all :-/

#### Kevin Buzzard (May 02 2020 at 18:32):

I've never really even looked at the definition of stuff like decidable_pred.

#### Kevin Buzzard (May 02 2020 at 18:34):

I was surprised by apply_instance didn't do the original question automatically. That's some computer science people missing a trick, right? @Chris Hughes is the kind of person that can make this magically happen.

#### Kevin Buzzard (May 02 2020 at 18:34):

I thought proofs were equal to programs or something.

#### Chris Hughes (May 02 2020 at 18:35):

I guess you could make an instance that if fintype A and decidable_pred s and decidable_pred t, then decidable (s = t). But I don't think this is going to be that well used, since you should probably be using finsets for this anyway.

#### Bryan Gin-ge Chen (May 02 2020 at 18:49):

Here's a decidable_of_iff proof:

instance decidable_is_empty' (α : Type*) [decidable_eq α] [fintype α]
(S : set α) [decidable_pred S] : decidable (S = ∅) :=
begin
apply decidable_of_iff (∀ x : α, x ∉ S),
split,
{ intro h, ext, simp [h], },
{ intro h, simp [h], },
end


I was hoping that simp would do it earlier but I ended up having to split and ext first.

#### Ciprian Teodorov (May 03 2020 at 10:50):

Thanks alot guys. The classical proof is nice, sadly noncomputable. The one based on decidable_off_iff worked for me. As for the first one @Kevin Buzzard my lean setup does not have the eq_bot_iff.mpr (I guess I should check my install)

#### Kevin Buzzard (May 03 2020 at 11:15):

Try leanproject up?

#### Kevin Buzzard (May 03 2020 at 11:16):

Either you should or I should :-)

#### Ciprian Teodorov (May 04 2020 at 07:47):

leanproject up worked, thanks again

Last updated: Dec 20 2023 at 11:08 UTC