decidable on finset

Stream: new members

[Iocta]

import data.setoid.partition
import data.finset

inductive thing : Type
| a : thing
| b : thing
| c : thing


def a_b_connected (p: set (set thing)) (hp: setoid.is_partition p)
[decidable (∃ (s : set thing) (H : s ∈ p), thing.a ∈ s ∧ thing.b ∈ s)]:
bool :=
∃ s ∈ p, thing.a ∈ s ∧ thing.b ∈ s

Can I use https://leanprover-community.github.io/mathlib_docs/data/finset/basic.html#finset.decidable_dexists_finset instead of [decidable (∃ (s : set thing) (H : s ∈ p), thing.a ∈ s ∧ thing.b ∈ s)] somehow?

[Kenny Lau]

Just use Prop instead of bool so that you don't need decidable

[Kenny Lau]

#xy

[Iocta]

When am I supposed to use bool?

[Kenny Lau]

next to never

[Iocta]

$ rg '\bbool\b' mathlib | wc -l
484

that's a pretty good-sized never :)

[Kenny Lau]

and what about Prop?

[Iocta]

2335

[Kenny Lau]

well those numbers tell you nothing

[Kenny Lau]

what I meant was that you don't use bool to state propositions

[Kenny Lau]

if you look into the actual use cases of bool you will find them being used as a fixed type with two elements or in tactics (metaprogramming)

[Iocta]

I'm not sure which one I mean here, but starting with Prop seems like a good bet. Thanks