Zulip Chat Archive

Stream: maths

Topic: to_finset_inter


view this post on Zulip Kevin Buzzard (Feb 16 2021 at 16:53):

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 :-)

view this post on Zulip Floris van Doorn (Feb 16 2021 at 16:56):

Yeah, I think that's right.

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:07):

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,

view this post on Zulip Eric Wieser (Feb 16 2021 at 17:09):

You need decidable_pred s too

view this post on Zulip Yakov Pechersky (Feb 16 2021 at 17:09):

(deleted)

view this post on Zulip Floris van Doorn (Feb 16 2021 at 17:09):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:10):

So what does the rule of thumb say for this?

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:10):

I just add decidable_pred s as well as decidable_eq alpha?

view this post on Zulip Eric Wieser (Feb 16 2021 at 17:11):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:11):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:12):

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

view this post on Zulip Eric Wieser (Feb 16 2021 at 17:13):

Whichever one subtype.fintype actually uses

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:14):

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

view this post on Zulip Kevin Buzzard (Feb 16 2021 at 17:18):

#6264 -- let's see if it compiles

view this post on Zulip Kyle Miller (Feb 16 2021 at 18:20):

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)

view this post on Zulip Bhavik Mehta (Feb 16 2021 at 18:30):

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)

view this post on Zulip Floris van Doorn (Feb 16 2021 at 18:31):

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?

view this post on Zulip Bhavik Mehta (Feb 16 2021 at 18:33):

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

view this post on Zulip Floris van Doorn (Feb 16 2021 at 18:35):

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.

view this post on Zulip Kyle Miller (Feb 16 2021 at 18:36):

@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

view this post on Zulip Bhavik Mehta (Feb 16 2021 at 18:36):

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

view this post on Zulip Kyle Miller (Feb 16 2021 at 18:39):

@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.

view this post on Zulip Floris van Doorn (Feb 16 2021 at 18:39):

t.filter s also breaks the abstraction barrier.

view this post on Zulip Bhavik Mehta (Feb 16 2021 at 18:40):

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

view this post on Zulip Floris van Doorn (Feb 16 2021 at 18:42):

Bhavik Mehta said:

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

What part should I be looking at?

view this post on Zulip Kyle Miller (Feb 16 2021 at 18:42):

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

view this post on Zulip Kyle Miller (Feb 16 2021 at 18:45):

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:

view this post on Zulip Bhavik Mehta (Feb 16 2021 at 18:55):

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

view this post on Zulip Floris van Doorn (Feb 16 2021 at 19:08):

@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)


Last updated: May 11 2021 at 16:22 UTC