is_refl

Stream: mathlib4

[Patrick Massot]

Do we have an analogue in Lean4 of docs#is_refl? If no, should it be added to mathlib4?

[Scott Morrison]

init.algebra.classes hasn't been ported so far, but I've bumped into it a few times. When I encountered an is_trans R I just switched to using Trans R R R, and it seemed to work fine. See mathlib4#467.

[Scott Morrison]

In the same PR, I encountered an IsSymmOp, and I just refactored to not use it at all.

[Scott Morrison]

That is, so far I have punted on porting init.algebra.classes. It isn't used a whole lot in mathlib, and maybe it would be nice to be rid of it. On the other hand, it may be easiest to just port it for now.

[Scott Morrison]

Alternatively, we perhaps could ask our mathlib refactoring experts if someone could try remove it as a dependency in mathlib3, to see how it goes.

[Patrick Massot]

I think we can declare that data.prod.basic is fully blocked by this issue since it has 50 lines that are all about those classes from init.algebra.classes.

[Patrick Massot]

I'm ready to port that file if this is what our porting experts recommend. It's no fun at all but I don't expect any fun so low in the import hierarchy (the whole thing blocked now is about lex ordering :zzz: )

[Mario Carneiro]

I would suggest copying over the mathport stuff unmodified (except possibly for style changes), then comment them out and write TODO and link to an issue

[Mario Carneiro]

since presumably we can get away with just not having those theorems. We can revisit if a "real" theorem needs them

[Mario Carneiro]

I wouldn't make this a blocker for being able to mark the file as "done" as long as the theorems are still recorded in the file. Alternatively we can just port it like Scott suggests, or backport remove it

[Mario Carneiro]

Actually backport removing it (or at least investigating what this would sacrifice) seems like the most fruitful approach. This is really just a trivial refactor and there is no need to do it as part of the port

[Scott Morrison]

Actually, looking more closely, init.algebra.classes is used way more than I expected. Why don't we just port it?

[Mario Carneiro]

I think the classes need to be handled case by case

[Scott Morrison]

I tried out porting it as is, it's not too bad. mathlib4#476. I left one section out as a couldn't be bothered repairing notation, and it isn't used.

[Scott Morrison]

I agree this file really needs to be cleaned up and reduced to what we actually use. But ... I don't really want to block other stuff on that.

[Scott Morrison]

What are the alternatives? We could analyse mathlib3 to determine which of these classes are actually used, and only port those?

[Mario Carneiro]

• is_symm_op: unused except for some instances
• is_commutative: used a fair amount via some theorems about folds (also assuming is_associative)
• is_associative: ditto, also used in noncomm_fold
• is_left_id, is_right_id: unused except in the mathlib class is_unital and in mono (which looks like it could use is_unital)
• is_left_null, is_right_null: unused
• is_left_cancel, is_right_cancel: unused except for instances
• is_idempotent: this one is actually used to prove things not directly about is_idempotent
• is_left_distrib, is_right_distrib, is_left_inv, is_right_inv, is_cond_left_inv, is_cond_right_inv: unused
• is_distinct: unused (although we reinvented this one as nontrivial)
• is_irrefl, is_refl, is_symm, is_trans: significant usage
• is_asymm, is_antisymm, is_total, is_strict_order: a lot of uses but all in order theory and it's unclear how much could not be transferred to another typeclass
• is_preorder: unused except for instances (except antisymmetrization, maybe it could be transferred)
• is_total_preorder, is_partial_order: unused except for instances
• is_linear_order: unused except for instances
• is_equiv: unused except for instances (most uses can use equivalence instead)
• is_per: unused
• is_incomp_trans: unused
• is_strict_weak_order: significant usage (most of it on rbmap, could be transferred)
• is_trichotomous: some usage
• is_strict_total_order: looks like the only usage is in rbmap again

[Mario Carneiro]

What I think we could do is to first move as much as possible from lean3 core to mathlib, then remove unused things from mathlib

[Mario Carneiro]

I don't think it will be hard to port this file at all, but it's a bunch of long-unused stuff and we will reimagine most of these classes anyway

[Mario Carneiro]

I think most of the uses are just the result of people grabbing the nearest thing that looks relevant

[Mario Carneiro]

And yes, this isn't port-blocking in any way. Porting everything except stuff that is hard seems like a good approach to get it over and done with

[Scott Morrison]

Mario Carneiro said:

What I think we could do is to first move as much as possible from lean3 core to mathlib, then remove unused things from mathlib

Okay, but aren't the alternatives today:

• Port Init/Algebra/Classes.lean as is (e.g. as in mathlib4#476), and then @Patrick Massot gets on with Data/Prod/Basic.lean, and later someone removes the unused classes from Init/Algebra/Classes.lean (in mathlib4).
• Someone does this move from lean3 core to mathlib, then removes unused things, and then we port to mathlib4.

It seems like the two are mutually exclusive.

[Scott Morrison]

Maybe a good compromise is that we port as is, except I copy and paste your analysis of what is and isn't used into the "Porting notes" section of the doc-string. :-)

[Mario Carneiro]

I don't think they are mutually exclusive. This file is simple enough that I would put it in the category of things that can be modified even after they are "frozen" since the corresponding fixup on the mathlib4 side is easy

[Mario Carneiro]

That is, I suggest we do your first option for now, and if someone is interested to do the backport side then we can update mathlib4 after it lands