Filter (set) vs filter (poset)

Stream: general

[Mathieu Guay-Paquet]

I'm running into a naming problem, where should definitions and lemmas about filters (on a partially ordered set) go in mathlib? The natural place seemed like src/order/filter/, but that's already taken up by the notationally conflicting notion of filters (on a set). The notion I want is dual to order ideals, which live in src/order/ideal.lean.

(What mathlib calls filter α, some others would call filter (set α), an unfortunate clash as noted on Wikipedia.)

I just noticed that the code in src/order/ideal.lean lives in a namespace order, whereas the code in src/order/filter/ is outside of namespace order. Is this discrepancy between the directory structure and the namespaces normal? Maybe src/order/filter/ should move up to src/filter/?

For now I can just be gross and put stuff in a new file src/order/filter.lean and have its contents in namespace order, so it won't technically clash with the existing filter stuff.

[Johan Commelin]

@Mario Carneiro has an almost finished refactor of filters from set to ordered structures...
...

[Mario Carneiro]

Filters are used everywhere so even if it's a fairly straightforward change it's a really big refactoring project

[Mathieu Guay-Paquet]

Is that almost-finished-refactor available anywhere? Searching the github issues and pull requests for 'filter' didn't turn up anything

[Mathieu Guay-Paquet]

Ah, looks like it's in the pfilter branch, maybe

[Mathieu Guay-Paquet]

For the record, I wasn't proposing _changing_ mathlib's notion of filter, just _adding_ a new notion in parallel (with later refactors for synergy, if applicable). But if it's better to wait until the refactor is done that's what I'll do.

[Mathieu Guay-Paquet]

Oh, the pfilter branch is marked as stale because it's 2 years old, maybe you're talking about a different refactor.

[Eric Wieser]

For the lazy (like me): branch#pfilter

[Johan Commelin]

Mathieu Guay-Paquet said:

Oh, the pfilter branch is marked as stale because it's 2 years old, maybe you're talking about a different refactor.

Unfortunately, I don't think I'm talking about a different one...

[Mathieu Guay-Paquet]

Is there some sort of statute of limitations? I don't think 3000 lines of change in a 2 year old commit is likely to be finished/reviewed/merged any time soon

[Johan Commelin]

Unless Mario finishes it, I would consider it dead code.

[Johan Commelin]

Mario is probably the only one from whom we would accept a 3000 lines patch, without worrying about it (-;

[Johan Commelin]

But I'm not sure if usability of current filter will get worse if it is refactored into filter (set X). If so, then there will probably be a lot of pushback.
In that case, just adding a new def'n is probably better.

[Mario Carneiro]

It will need to be redone by hand, probably using the original as inspiration but not much more. An actual merge is far too likely to accidentally delete theorems

[Mario Carneiro]

IIRC in the refactor filter A was defined as pfilter (set A), but the filter theorems were still there basically as is

[Eric Wieser]

I was going to say, shouldn't it be possible to redefine filter = pfilter (set A) with a relatively small blast radius?

[Mathieu Guay-Paquet]

It looks like the current filter (for sets) is in the global namespace, whereas preorder ideals (which are dual to the preorder filters) currently live atorder.ideal. Which naming option do you prefer:

1. Keep filter for sets, add order.filter dual to order.ideal for preorders, for the nice name;
2. Keep filter for sets, add order.pfilter dual to order.ideal for preorders, for less confusion;
3. Something else (please specify).

[Johan Commelin]

I guess pfilter in the root namespace would also be fine

[Johan Commelin]

With ideal you want to distinguish from ideals of rings. But with pfilter there is no such risk.

[Aaron Anderson]

There is also finset.filter, but presumably we’ve already found ways of avoiding that naming confusion

[Mathieu Guay-Paquet]

Ah, if finset.filter already exists along with the global filter, I'm tempted to go for order.filter

[Mathieu Guay-Paquet]

Oh wait no, that's the computer science filter, which keeps or discards elements from a container-like object

[Mathieu Guay-Paquet]

As per the contribution guidelines, could I get write access to non-master branches of the mathlib repository? My github username is mguaypaq. I'd like to start a first PR towards adding preorder filters

[Rob Lewis]

Mathieu Guay-Paquet said:

As per the contribution guidelines, could I get write access to non-master branches of the mathlib repository? My github username is mguaypaq. I'd like to start a first PR towards adding preorder filters

Sent!

[Mathieu Guay-Paquet]

Great, thanks!

[Patrick Massot]

Johan already wrote it but I think we should emphasize: before embarking for this adventure, you need to know that if a refactor makes actual filters even very very slightly less convenient to use then it simply won't be merged.

[Mathieu Guay-Paquet]

Thanks for the emphasis. I am totally on board with that approach

[Mario Carneiro]

Should we rename finset.filter to finset.sep in keeping with the set-like name?

[Mathieu Guay-Paquet]

Alright, just moving the order/filter/* files and fixing the imports is now a pull request, #5900. However, I'm getting a CI failure about lint style, with no details (just: Error: ), where would I get more information about that?

[Yakov Pechersky]

src/data/set/filter/filter_product.lean : line 14 : ERR_LIN : Line has more than 100 characters

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib/runs/1771058560

[Mathieu Guay-Paquet]

Ah, the error message appeared empty because of my adblocker, thanks

[Johan Commelin]

@Mathieu Guay-Paquet I think it would be good to first settle on the name pfilter vs order.filter.
Because if we choose pfilter, then stuff can just go in order/pfilter/*.

[Mathieu Guay-Paquet]

I'm leaning towards pfilter, because there's already more than one thing called filter, and we might want to relate both notions sometimes. For example, relating filter α and pfilter (set α); or talking about pfilter (finset α), where finset.filter already exists (and is the computer science filter-a-list operation)

[Mathieu Guay-Paquet]

I'm fine closing the PR, it's almost just a proof of concept that moving the files wouldn't be hard in practice

[Johan Commelin]

In that case I would suggest just putting new things in order/pfilter/*.

[Johan Commelin]

Right, but I think it's better to keep them where they are. We don't care too much about backwards compatibility, or completely breaking api's and putting them up in new places. But usually there will be some specific problem leading to such a refactor. In the case of #5900, I don't think there is an urgent need of moving the files to a different place.

[Mathieu Guay-Paquet]

I'll note that a more contentful PR is currently at #5909, currently just awaiting bors merge. I plan on defining pfilters as ideals on the dual preorder, so it makes sense to prove more things about ideals, to get facts about pfilters almost for free