to_finset_inter

Stream: maths

[Kevin Buzzard]

Does Yury's rule of thumb say that docs#set.to_finset_inter and the other lemmas around there should have a [decidable_eq α] assumption rather than the (equivalent of) open_locale classical here? The issue is that you can't do things like intersections on finsets without decidable equality. I am still trying to get to grips with this rule of thumb. It's one reason I stay away from finsets :-)

[Floris van Doorn]

Yeah, I think that's right.

[Kevin Buzzard]

oh this is annoying, if I remove the classical.prop_decidable and add decidable_eq alpha then the statement of to_finset_inter still doesn't compile:

failed to synthesize type class instance for
α : Type ?,
_inst_1 : fintype α,
_inst_2 : decidable_eq α,
s t : set α
⊢ fintype ↥s

I don't need this for anything, I've just been reading data.set.finite recently and the [priority 1] thing caught my eye,

[Eric Wieser]

You need decidable_pred s too

[Yakov Pechersky]

(deleted)

[Floris van Doorn]

That needs the assumption decidable_pred (\in s): docs#subtype.fintype

[Kevin Buzzard]

So what does the rule of thumb say for this?

[Kevin Buzzard]

I just add decidable_pred s as well as decidable_eq alpha?

[Eric Wieser]

Or perhaps it says add [fintype ↥s] directly?

[Kevin Buzzard]

Can one make a linter to spot these things? The only reason I'm interested was that it burnt Amelia last week.

[Kevin Buzzard]

Which is better out of decidable_pred s and decidable_pred (∈ s)? Both work.

[Eric Wieser]

Whichever one subtype.fintype actually uses

[Kevin Buzzard]

It uses p : alpha -> Prop and not p : set alpha

[Kevin Buzzard]

#6264 -- let's see if it compiles

[Kyle Miller]

Floris van Doorn said:

That needs the assumption decidable_pred (\in s): docs#subtype.fintype

I saw a recent PR that replaced decidable_pred (∈ s) with decidable_pred s, and I know I've been consistently using decidable_pred s myself. The only uses in mathlib of decidable_pred (∈ s) seem to be four lemmas in data.set.basic (mk_preimage_prod_left_eq_if and the rest). Would it be reasonable to add a decidable_set so that there's an obvious choice?

@[reducible]
def decidable_set {α : Type u} (s : set α) :=
decidable_pred (λ a, a ∈ s)

[Bhavik Mehta]

I think the choice is obvious enough as it is - decidable_pred s can be proved from decidable_pred (∈ s) but not inferred from it, and decidable_pred (∈ s) can be inferred from decidable_pred s, so there's no reason to ever write decidable_pred (∈ s)

[Floris van Doorn]

I think having decidable_set is reasonable. The problem with decidable_pred s is that it breaks the abstraction barrier of set (s is not a predicate, it is a set). Is there a reason to ever favor decidable_pred s over decidable_pred (∈ s), assuming the library consistently uses the latter?

[Bhavik Mehta]

Yes, if you give an instance decidable_pred (∈ s) then the typeclass system can't deduce decidable_pred s from it, but not vice versa

[Floris van Doorn]

Why would you ever want to deduce decidable_pred s? That is a statement I would like to see banned from mathlib, since it breaks the abstraction barrier of set.

[Kyle Miller]

@Kevin Buzzard I think I last touched the section in #6264 (adding the lemmas about erase), and I ended up not changing it to use decidable instances because they are more or less fine if you make sure your tactic proofs are purely classical, and making them use decidable in a way that won't cause any problems was more work than I wanted to do at the time -- you need to make sure that typeclass instances in a lemma statement aren't themselves inferred.

For example, this I think is what you need for the first lemma of the bunch:

lemma to_finset_compl {α : Type*} [fintype α] [decidable_eq α] (s : set α) [fintype (sᶜ : set α)] [fintype s] :
  sᶜ.to_finset = (s.to_finset)ᶜ :=
by ext; simp

[Bhavik Mehta]

Floris van Doorn said:

Why would you ever want to deduce decidable_pred s? That is a statement I would like to see banned from mathlib, since it breaks the abstraction barrier of set.

docs#finset.filter, for instance - this assumption is needed loads throughout combinatorics and in particular mathlib graph theory

[Kyle Miller]

@Bhavik Mehta What's an example of finset.filter where this would be a problem? I'm imagining you're saying something like t.filter s where s is a set, and you could write t.filter (∈ s) instead.

[Floris van Doorn]

t.filter s also breaks the abstraction barrier.

[Bhavik Mehta]

Kyle Miller said:

Bhavik Mehta What's an example of finset.filter where this would be a problem? I'm imagining you're saying something like t.filter s where s is a set, and you could write t.filter (∈ s) instead.

See this PR for instance: https://github.com/leanprover-community/mathlib/pull/5938

[Floris van Doorn]

Bhavik Mehta said:

See this PR for instance: https://github.com/leanprover-community/mathlib/pull/5938

What part should I be looking at?

[Kyle Miller]

That's the PR I was referring to earlier (but I was too lazy to include a link), but I'm not sure I understand what this has to do with finset.filter

[Kyle Miller]

Floris van Doorn said:

Is there a reason to ever favor decidable_pred s over decidable_pred (∈ s), assuming the library consistently uses the latter?

But all the parentheses! :smile:

[Bhavik Mehta]

I should have been clearer. There are cases when mem notation for sets can't be used because the has_mem can't infer what's going on (an example is the definition of presieve here: https://github.com/leanprover-community/mathlib/blob/2411d681127e17b7ba96b80c50c9e50f631491da/src/category_theory/sites/sieves.lean#L36, suggested by Reid), specifically when I wanted to filter over a finset of arrows using the property that they're in a presieve, it's not true that I could write t.filter (∈ s) instead of t.filter s

[Floris van Doorn]

@Kyle Miller I am a big fan of reducing the number of parentheses :)

@Bhavik Mehta: presumable you could have written something like t.filter (λ (x : ...), x ∈ s)? I know that would be quite a bit longer than t.filter s, but I think it's important to not break the abstraction barrier. This is the same reason that we ban s x from the library, and favor x ∈ s.
And if you write decidable_pred s or t.filter s, you are doing the same. For example, if you apply docs#finset.mem_filter to t.filter s, you'll get hypotheses/goals with s x or x ∈ λ x, p x. And then you have to rewrite them away, like this:https://github.com/leanprover-community/mathlib/blob/362619ebc74073495414578128b9bcb10879aa57/src/category_theory/sites/pretopology.lean#L167
(though I'm surprised this doesn't happen more often in the library)