Refactor interval succ/pred order?

Stream: mathlib4

[Bernhard Reinke]

In a question related to the equational theories project, I wanted to use docs#Set.Iic_pred_eq_Iio_of_not_isMin on a PartialOrder instead of a LinearOrder, motivating me to create #23810, where the interval lemmas for succ/pred orders are generalized to PartialOrders if possible. The PR hasn't been reviewed yet but recently got a merge conflict, which got me thinking about this again.

A thing which is a bit tricky for this PR is that at the moment Mathlib/Order/Interval/Set/SuccPred.lean is structured via nested sections with the outer one assuming LinearOrder. My approach has been to double the outer section and creating a new one with only PartialOrder as an assumption. This made it easy to create via copy paste, but probably not easy to review. Here are some alternative ways one could proceed:

One way would be to "fold" the sections first, getting rid of most variable statements by including all type class assumptions into the statements of the lemmas, and adjusting the LinearOrder assumption to PartialOrder when possible. Here we can also easily generalize the lemmas to PreOrder if we want to.

Or just have one outer PartialOrder section with PartialOrder as a hypothesis, and add LinearOrder assumption in the lemmas if they need it. Here I think we would change the ordering of the type class assumptions, and maybe we want to omit PartialOrder as an assumption if we have LinearOrder.

Please let me know what you think, in particular, @Yaël Dillies , would you mind sharing your opinion on this?

[Yaël Dillies]

Oh sorry, this is really a bad time to do this refactor. I am currently spending a lot of time rewriting these files from scratch

[Yaël Dillies]

In particular, I am not done writing those files. They are in a temporary state and are not ready to be used

[Yaël Dillies]

Why do you need those results for partial orders? I was explicitly writing these files specialised to linear orders because non-linear orders should be basically irrelevant

[Bernhard Reinke]

It is not really a high priority, see this question for the short answer. Here comes the large answer:

In one of the infinite magma constructions of the equational theories project, we use a partial order on a free group N given by x <= y if x is on the geodesic from the identity to y in the Cayley graph (or, and this is how we define it, the reduced word representing x is a suffix of the reduced word for y).

This partial order is very naturally a PredOrder (and in the rest of the construction, we use the predecessor quite lot). In the rest of the construction we also needed to do an inductive construction over <. For me it seemed natural to show the LocallyFiniteOrderBot instance of the order: we have that Iic g = (List.map (FreeGroup.mk) g.toWord.tails).toFinset. For the inductive construction @Aaron Hill had to prove again that < is actually well-founded. From my perspective PartialOrder + PredOrder + LocallyFiniteOrderBot should already imply that the strict order well-founded, even ranked, with rank of g being the cardinality of Iio g.