cleaning up algebra.order.ring and dependencies

Stream: PR reviews

[Scott Morrison]

I've just piled up a bunch of PRs cleaning up algebra.order.ring and its dependencies, mostly just splitting files and postponing unneeded imports.

I think each of the following are (mostly) independent, and I'd love to get them moving:

[Scott Morrison]

#16863

[Scott Morrison]

#16864

[Scott Morrison]

#16865

[Scott Morrison]

#16866

[Scott Morrison]

#16869

[Scott Morrison]

Then there's also #16861 and #16869, but these are stacked up behind Yael's #16172 (which bors is working on), so are harder to review for now.

[Ruben Van de Velde]

Scott Morrison said:

#16863

@Johan Commelin note that bors rejected the merge because of the awaiting-ci label

[Johan Commelin]

Thanks for letting me know, d+d

[Yaël Dillies]

@Scott Morrison, you still haven't answered me what your goal was.

[Yaël Dillies]

Do you have specific pairs of declarations that you think should not import each other?

[Scott Morrison]

Minimize the number of files (and their sizes) that need to be imported to get to ordered_ring and its basic lemmas. Essentially I am looking at leanproject import-graph --to algebra.order.ring, and identifying spurious things in the graph.

[Scott Morrison]

And the xy is that I am porting linarith, and trying to get a balance between only porting the mathlib development that is needed, and not making life harder for the eventual complete port. Having smaller simpler files makes porting more manageable.

[Kevin Buzzard]

I feel like linarith is one of the last big obstacles to getting mathlib ported.

[Patrick Massot]

I definitely vote for letting Scott change whatever he wants in mathlib if it helps him porting linarith.

[Kevin Buzzard]

@Mario Carneiro how wildly off is my linarith claim/hope?

[Scott Morrison]

There's a bunch still to port, don't worry. :-)

[Scott Morrison]

The category theory library is still going to be broken from the first file for lack of tidy. That shouldn't be too hard to implement, but it's lower priority for now as we want to get the prerequisites for Rob's and Heather's courses next year done asap.

[Scott Morrison]

It's encouraging that it is actually possible to do complete ports of some of the low-down-the-hierarchy files now. Maybe we can resume a conversation about how the "flag day" vs "gradual transition" question will work out. It may not be too long before we want to start marking some very basic files in mathlib as "no changes accepted unless you make the corresponding changes in mathlib4".

[Scott Morrison]

I'm still not sure how much work linarith will be. I've got the Fourier-Motzkin elimination part "working" (i.e. compiling, who knows if it actually works) locally in lean4, but there is a lot of frontend still to do.

[Scott Morrison]

#16861 is hopefully ready for review (CI not complete, I'll promise not to merge until it does if someone wants to delegate. :-)