Zulip Chat Archive

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

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

No no!

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

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

Kevin Buzzard (May 02 2020 at 18:30):

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