[Merged by Bors] - feat(data/finset/basic): Add decidable_nonempty for finsets.

[linesthatinterlace]

Also remove some redundant decidable instances in multiset and list.

---

Note: as we have the nonempty predicate, we can define a decidable instance for it without worrying about diamond issues. This is always possible, even if there is no decidable equality on the underlying type.

[linesthatinterlace]

Not sure if this failure is related to the commit or not.

[eric-wieser]

The failure is caused by this application of tauto:

mathlib/src/algebra/big_operators/basic.lean

Line 1189 in 05a33f9

have y = x ∨ y = g x hx, by simp [hy] at hy₁; tauto,

Replacing it with sorry makes the error go away.

[eric-wieser]

This seems like a better proof to me:

instance _root_.multiset.decidable_exists_mem {P : α → Prop} [decidable_pred P] (m : multiset α) :
  decidable (∃ a ∈ m, P a) :=
quotient.rec_on_subsingleton m list.decidable_exists_mem

instance decidable_exists_mem {P : α → Prop} [decidable_pred P] (s : finset α) :
  decidable (∃ a ∈ s, P a) :=
s.val.decidable_exists_mem

instance decidable_nonempty {s : finset α} : decidable (s.nonempty) :=
decidable_of_iff (∃ a ∈ s, true) $ by simp_rw [exists_prop, and_true, finset.nonempty]

where obviously the multiset instance belongs in another file.

[linesthatinterlace]

I also added decidable_forall_mem for both of these as list has it.

I could also add nonempty lemmas for list. Also, the forall and exists lemmas for list are in a very odd place - so I could move them somewhere more appropriate.

What do you think?

[eric-wieser]

Since you were able to put the new lemmas in the right place without any import trouble, I don't think moving the list lemmas is worth the effort.

This looks good now - can you update the PR description?

[linesthatinterlace]

Description updated.

[eric-wieser]

PR title also doesn't match the commit guidelines (it's missing the prefix)

[linesthatinterlace]

Oh bother. Should it be feat(data/finset/basic) (despite the multiset lemmas?)

[linesthatinterlace]

Shall I remove these duplicate instances and just push decidable_nonempty?

[eric-wieser]

@linesthatinterlace: Please do; removing the existing list instance would be good too.

[linesthatinterlace]

Done; let's see if removing those causes any build issues...

[linesthatinterlace]

Yes: counter to what @YaelDillies said, the list versions do appear to be used. Do we have the dependent list versions?

[linesthatinterlace]

We have list.all₂.decidable_pred, which appears to be... another version of one of the non-dependent versions? But I think it uses the existing decidable_forall_mem instances also? This is a mess.

[YaelDillies]

The dependent multiset version uses the non-dependent one, and this looks like it causes a direct non-defeq diamond (but someone should check). Maybe the non-dependent one should not be an instance, then?

[linesthatinterlace]

No, I think they might use decidable_ball and decidable_bexists. These are core instances of the non-dependable ones for list. It seems like decidable_forall_mem and decidable_exists_mem just duplicate them.

[linesthatinterlace]

Current state:
list

• decidable_ball and decidable_bexists. Non-dependent list instances that are in core, not mathlib.
• decidable_forall_mem and decidable_exists_mem. Non-dependent list instances that are in mathlib. They duplicate the above.
• all₂.decidable_pred. Equivalent to decidable_ball but specifically using the all₂ definition (not defeq).

multiset

• Have decidable_forall_multiset, decidable_dforall_multiset, decidable_eq_pi_multiset, decidable_exists_multiset, and decidable_dexists_multiset, where decidable_forall_multiset and decidable_exists_multiset are essentially the non-dependent versions. One of these currently uses decidable_exists_mem but it doesn't have to.

finset

• Have decidable_dforall_finset, decidable_eq_pi_finset, and decidable_dexists_finset. Do not have the non-dependent versions at all as far as I can see.

I am, if I am honest, unsure what we "should" have for each of these, and what they should be called. Do we want decidable_dforall_list, decidable_eq_pi_list, and decidable_dexists_list, say? That might mean we don't need the non-dependent versions for multiset either.

[linesthatinterlace]

Note that my last comment should really wait for another PR. This one is now ready to go, I think - the total changes just remove the list instances we don't need and adds decidable_nonempty. @eric-wieser, are you now happy?

[kmill]

Looks good to me, thanks. Please remove the parentheses, then feel free to merge.

bors d+

[bors]

✌️ linesthatinterlace can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[linesthatinterlace]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests