order.filter.basic

Stream: mathlib4

[Johan Commelin]

The amount of data.foobar in https://tqft.net/mathlib4/2022-12-22/order.filter.basic.pdf is quite unappetizing...

[Patrick Massot]

It all comes from data.set.finite which will unlock a lot of things.

[Eric Wieser]

We have to port all of data eventually!

[Yury G. Kudryashov]

All dependencies are ported (1 is pending review). I'm going to start porting Order.Filter.Basic.

[Yury G. Kudryashov]

Do we have tactic.monotonicity?

[Yury G. Kudryashov]

Probably, not yet.

[Yury G. Kudryashov]

:(

[Heather Macbeth]

No, current advice is to comment out any @[mono] and add a porting note. Although I think that with the new tag_attribute functionality we could create a mono "tag attribute" and then at least keep tagging things mono, maybe even make a quickie implementation of mono as apply_rules only using mono.

[Heather Macbeth]

In fact I can try that now.

[Heather Macbeth]

@Yury G. Kudryashov Are the mono turning up in Order.Filter.Basic for attribute-tagging or for proofs?

[Yury G. Kudryashov]

I don't know yet.

[Yury G. Kudryashov]

Even if it's used for proofs, it should be easy to unfold these usages.

[Heather Macbeth]

Heather Macbeth said:

maybe even make a quickie implementation of mono as apply_rules only using mono.

My guess is that this will work for about 75% of mathlib uses of mono.

[Heather Macbeth]

mathlib4#1740 for a (cheap, very partial) mono implementation.

[Yury G. Kudryashov]

I fixed most proofs.

[Yury G. Kudryashov]

Notable exceptions are filter_upwards (probably, can be implemented as a macro; didn't try yet) and category theory stuff.

[Yury G. Kudryashov]

I see that some classes like Functor, Monad, and their Lawful versions changed. It would be nice if someone who understands what's changed and what's wrong with "filter as a monad" (there are some comments about conflicting instances) will have a look.

[Johan Commelin]

@Yury G. Kudryashov Do you already have a PR to track that you are porting this file?

[Johan Commelin]

Because it doesn't show up as WIP on #port-status

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathlib4/pull/1750 How do I update #port-status?

[Johan Commelin]

It should happend automatically

[Johan Commelin]

Can you please merge master into your branch?

[Yury G. Kudryashov]

Done.

[Anatole Dedecker]

I’ll send the version I have of filter_upwards in ~1h

[Anatole Dedecker]

Well or rather I’ll add it directly to the PR

[Yury G. Kudryashov]

@Anatole Dedecker Any progress?

[Anatole Dedecker]

I just pushed, sorry for the delay, I had to make it up to date. I fixed some of the proofs, but some of them give weird errors, I'm looking into it

[Yury G. Kudryashov]

I'll fix the rest.

[Yury G. Kudryashov]

Do we need these spaces in " with", " using"?

[Anatole Dedecker]

No we don't

[Anatole Dedecker]

There were in Mathport/Syntax so I kept them

[Yury G. Kudryashov]

One of the errors is here because we don't have docs#lift_pair

[Anatole Dedecker]

(If that wasn't clear, I'm looking into the failures that are linked to filter_upwards, because they suggest a bad implementation, not the other failures)

[Anatole Dedecker]

I just pushed a fix to the tactic (a missing withMainContext made that the tactic only knew the context of the lemma, not the current context of the goal)

[Yury G. Kudryashov]

Who should I ask about category theory stuff?

[Yury G. Kudryashov]

Do we want filter to be a monad? What are the issues with applicative instance?

[Yury G. Kudryashov]

applicative filter is used for topological_space (list _)

[Yury G. Kudryashov]

I created a few PRs that fix issues I found while porting to Lean 4: #18253, #18254 (on the queue), #18255

[Yury G. Kudryashov]

Ready for review.