Zulip Chat Archive

Stream: new members

Topic: decidable disjoint


view this post on Zulip Bhavik Mehta (Dec 11 2019 at 13:13):

When I write:

import data.finset
import data.fintype

open fintype
open finset

variable {n : }
local notation `X` := fin n

variable {𝒜 : finset (finset X)}

def compress (U V : finset X) (A : finset X) :=
if (disjoint U A)  (V  A)
  then (A  U) \ V
  else A

I get an error saying "failed to synthesize type class instance" for "decidable (disjoint U A ∧ V ⊆ A)", but if I rewrite the condition with U ∩ A = ∅, it's fine... I'd like to keep the definition with disjoint though, since every time I use this definition I found myself converting the empty intersection to disjointness. How could I get around this?

view this post on Zulip Bhavik Mehta (Dec 11 2019 at 14:10):

I proved disjoint U V is decidable instead... Is there a reason this isn't already in data/finset.lean?

view this post on Zulip Simon Hudon (Dec 12 2019 at 01:39):

There's no reason not to have it in mathlib. People tend to add what they use so that might just never have come up before

view this post on Zulip Bhavik Mehta (Dec 12 2019 at 13:20):

Okay! Is there an issue with typeclass resolution, since this is saying disjoint on finsets is decidable, but might not be in other cases?

view this post on Zulip Simon Hudon (Dec 12 2019 at 19:38):

With decidable equality on α, disjointness on finset should always be decidable.


Last updated: May 14 2021 at 00:42 UTC