instance of decidable_set_is_empty

Stream: new members

[Ciprian Teodorov]

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]

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

[Ciprian Teodorov]

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]

a #mwe is a lot better than a tactic state

[Ciprian Teodorov]

@Jalex Stark the exemple is in my first post

[Jalex Stark]

Oh thanks, I should read harder

[Ciprian Teodorov]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

No no!

[Reid Barton]

oh I see

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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]

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

[Reid Barton]

Actually, it is fine. But decidable_of_iff is clearer

[Kevin Buzzard]

my lovely tactic mode proof isn't clear??

[Reid Barton]

This is a construction, not a proof

[Kevin Buzzard]

well the computer scientists call it a construction...

[Kevin Buzzard]

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

[Reid Barton]

Yes, a proof of true.

[Reid Barton]

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

[Kevin Buzzard]

same thing!

[Kevin Buzzard]

I think sarcasm should be an axiom.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I thought proofs were equal to programs or something.

[Chris Hughes]

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]

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]

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]

Try leanproject up?

[Kevin Buzzard]

Either you should or I should :-)

[Ciprian Teodorov]

leanproject up worked, thanks again