mul_le_mul

Stream: general

[Johan Commelin]

My refactor leads to a conflict: mul_le_mul is now a lemma about ordered_cancel_comm_monoid, but it was already a lemma for ordered_semirings:

-- TODO: there are four variations, depending on which variables we assume to be nonneg
lemma mul_le_mul (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d :=
calc
  a * b ≤ c * b : mul_le_mul_of_nonneg_right hac nn_b
    ... ≤ c * d : mul_le_mul_of_nonneg_left hbd nn_c

What is the preferred way to resolve this conflict?

[Mario Carneiro]

I should have asked this before: why are you doing this refactor?

[Mario Carneiro]

I hope it's not only for uniformity's sake

[Mario Carneiro]

do we actually have any examples of multiplicative ordered_comm_monoids?

[Mario Carneiro]

the fact that the new mul_le_mul_left has no nonnegativity assumptions on the multiplicand looks very weird to me

[Reid Barton]

nat?

[Kevin Buzzard]

The perfectoid project sets up a very general theory of valuations into ordered comm monoids, and work like Rob's on p-adic numbers has a valuation into the non-negative reals, and maybe things can be unified somehow

[Mario Carneiro]

Sure, but that's a canonically_ordered_monoid which gives it more structure

[Mario Carneiro]

in particular zero_le

[Kevin Buzzard]

The multiplication isn't canonically ordered

[Mario Carneiro]

no but it's a semiring, it's got both

[Mario Carneiro]

same for enat, nnreal and ennreal

[Mario Carneiro]

so I'm not sure where this class will be used

[Mario Carneiro]

and I would certainly hate to displace an actually useful lemma for one with no known applications

[Johan Commelin]

Mario Carneiro said:

so I'm not sure where this class will be used

The valuations take values in an arbitrary such monoid. Not all of them are ordered semirings

[Johan Commelin]

You could argue that we should use additive valuations instead... but...

[Mario Carneiro]

I really should

[Mario Carneiro]

but I think that ship sailed before I even started leaning

[Johan Commelin]

Also... it means that valuations can't take values in nnreal

[Mario Carneiro]

Johan Commelin said:

The valuations take values in an arbitrary such monoid. Not all of them are ordered semirings

Fair enough. But I'm guessing that you don't need to do that much as far as algebraic manipulations in these types though, so perhaps you can make do with namespacing everything

[Mario Carneiro]

I think you might have use for something a bit more than an ordered_comm_monoid for your valuations though

[Mario Carneiro]

Don't you want to add a zero to the type?

[Mario Carneiro]

and then you will have zero_le which isn't true in an ordered_comm_monoid

[Kevin Buzzard]

We work with group_with_zero s I guess

[Mario Carneiro]

Is there an ordered_group_with_zero?

[Johan Commelin]

@Mario Carneiro In the end it will be linearly_ordered_comm_group_with_zero

[Johan Commelin]

And we have files with lots of basic lemmas about these guys in the perfectoid project

[Johan Commelin]

But they depend on actual_ordered_comm_monoids

[Johan Commelin]

I'm trying to get rid of the actual_

[Mario Carneiro]

I think you should start with the minimum number of classes necessary to say what you need

[Mario Carneiro]

what are actual_ordered_comm_monoids used for?

[Johan Commelin]

They are only there currently to prove a bunch of lemmas that are true more generally than just for linearly_ordered_comm_group_with_zeros

[Mario Carneiro]

yeah, that qualifies as a non-use from my point of view

[Mario Carneiro]

you can just put those theorems in a section and say "Note: these hold more generally, make sure to migrate these if/when we need the generality"

[Mario Carneiro]

but there is a reason you won't find theorems like mul_inv_cancel stated over quasigroups

[Johan Commelin]

Hmmmzz... I thought we tried to do things in "the right generality" because you never know if someone will show up with a sudden orthogonal application.

[Johan Commelin]

Also, I would still get the mul_le_mul name conflict

[Johan Commelin]

Whatever method I use then to solve the name conflict, could also be applied here.

[Mario Carneiro]

you never know if someone will show up with a sudden orthogonal application

Don't try to anticipate applications you don't understand. You will be sufficiently wrong sufficiently often as to make the extra effort worthless. Instead, plan for the applications you are aware of, and try to design things so that it is otherwise generally maintainable and refactorable, and let future-you or future-someone else deal with future applications

[Mario Carneiro]

As for the name conflict, the usual technique works here: use a namespace

[Mario Carneiro]

or primes

[Johan Commelin]

Ok, I'll just make sure that none of the existing names in mathlib changes.