to_ framework

[YaelDillies]

to_additive has had great success in homogenizing lemmas and reducing maintenance burden. It would now be great to extend this principle to other kinds of dualities:

• to_add_op: Turn lemmas about a + b into b + a
• to_mul_op: Turn lemmas about a * b into b * a
• to_dual: Turn lemmas about a ≤ b into b ≤ a. to_additive-like attribute for order_dual #7691

Many lemmas could benefit of several attributes at the same time, generating exponentially many lemmas. To ensure this,

• We should probably hardcode an order in which the to_ attributes should be applied, and each should apply to all the previously generated lemmas. Further, some combinations of attributes have nontrivial relations between them. For example, to_mul_op + to_additive creates the to_add_op lemmas.
• The actual replacement will become significantly more complicated (both in the proof term and lemma name) as the dual of a ≤ b is b ≤ a, not b ≥ a (and similarly for a + b/b + a and a * b/b * a).
• The attribute syntax might need to change, to be @[to [add_op, mul_op, dual]] rather than @[to_add_op, to_mul_op, to_dual], similar to how derive works.
• Adding comments will be more complicated as n attributes need 2^n - 1 comments within the attribute. Luckily, it should rarely happen that a lemma is both interesting enough to deserve a docstring and boring enough to be dualized.

Examples

• mul_le_mul_of_le_of_lt, mul_le_mul_of_lt_of_lt, add_le_add_of_le_of_lt, add_le_add_of_lt_of_lt

Non-examples

• add_le_add. This is a fixed point of both add_op and dual

[alexjbest]

It would be really helpful to collect a bunch of examples here of lemmas that could/should be autogenerated, as examples and test cases for whoever writes this.