Stream: general

Topic: mul_le_mul

Johan Commelin (May 27 2020 at 11:04):

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 (May 27 2020 at 11:05):

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

Mario Carneiro (May 27 2020 at 11:05):

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

Mario Carneiro (May 27 2020 at 11:06):

do we actually have any examples of multiplicative ordered_comm_monoids?

Mario Carneiro (May 27 2020 at 11:06):

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

Reid Barton (May 27 2020 at 11:07):

nat?

Kevin Buzzard (May 27 2020 at 11:07):

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 (May 27 2020 at 11:07):

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

Mario Carneiro (May 27 2020 at 11:08):

in particular zero_le

Kevin Buzzard (May 27 2020 at 11:08):

The multiplication isn't canonically ordered

Mario Carneiro (May 27 2020 at 11:08):

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

Mario Carneiro (May 27 2020 at 11:09):

same for enat, nnreal and ennreal

Mario Carneiro (May 27 2020 at 11:09):

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

Mario Carneiro (May 27 2020 at 11:09):

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

Johan Commelin (May 27 2020 at 11:12):

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

I really should

Mario Carneiro (May 27 2020 at 11:13):

but I think that ship sailed before I even started leaning

Johan Commelin (May 27 2020 at 11:14):

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

Mario Carneiro (May 27 2020 at 11:15):

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 (May 27 2020 at 11:17):

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

Mario Carneiro (May 27 2020 at 11:18):

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

Mario Carneiro (May 27 2020 at 11:19):

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

Kevin Buzzard (May 27 2020 at 11:19):

We work with group_with_zero s I guess

Mario Carneiro (May 27 2020 at 11:20):

Is there an ordered_group_with_zero?

Johan Commelin (May 27 2020 at 11:20):

@Mario Carneiro In the end it will be linearly_ordered_comm_group_with_zero

Johan Commelin (May 27 2020 at 11:20):

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

Johan Commelin (May 27 2020 at 11:21):

But they depend on actual_ordered_comm_monoids

Johan Commelin (May 27 2020 at 11:21):

I'm trying to get rid of the actual_

Mario Carneiro (May 27 2020 at 11:21):

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

Mario Carneiro (May 27 2020 at 11:22):

what are actual_ordered_comm_monoids used for?

Johan Commelin (May 27 2020 at 11:22):

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 (May 27 2020 at 11:23):

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

Mario Carneiro (May 27 2020 at 11:24):

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 (May 27 2020 at 11:25):

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

Johan Commelin (May 27 2020 at 11:27):

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 (May 27 2020 at 11:28):

Also, I would still get the mul_le_mul name conflict

Johan Commelin (May 27 2020 at 11:29):

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

Mario Carneiro (May 27 2020 at 11:31):

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 (May 27 2020 at 11:32):

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

or primes

Johan Commelin (May 27 2020 at 11:33):

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

Last updated: May 17 2021 at 21:12 UTC