Zulip Chat Archive

Stream: general

Topic: mul_le_mul


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 27 2020 at 11:05):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:05):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:06):

do we actually have any examples of multiplicative ordered_comm_monoids?

view this post on Zulip 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

view this post on Zulip Reid Barton (May 27 2020 at 11:07):

nat?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:07):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:08):

in particular zero_le

view this post on Zulip Kevin Buzzard (May 27 2020 at 11:08):

The multiplication isn't canonically ordered

view this post on Zulip Mario Carneiro (May 27 2020 at 11:08):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:09):

same for enat, nnreal and ennreal

view this post on Zulip Mario Carneiro (May 27 2020 at 11:09):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 11:13):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:13):

I really should

view this post on Zulip Mario Carneiro (May 27 2020 at 11:13):

but I think that ship sailed before I even started leaning

view this post on Zulip Johan Commelin (May 27 2020 at 11:14):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:18):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:19):

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

view this post on Zulip Kevin Buzzard (May 27 2020 at 11:19):

We work with group_with_zero s I guess

view this post on Zulip Mario Carneiro (May 27 2020 at 11:20):

Is there an ordered_group_with_zero?

view this post on Zulip Johan Commelin (May 27 2020 at 11:20):

@Mario Carneiro In the end it will be linearly_ordered_comm_group_with_zero

view this post on Zulip Johan Commelin (May 27 2020 at 11:20):

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

view this post on Zulip Johan Commelin (May 27 2020 at 11:21):

But they depend on actual_ordered_comm_monoids

view this post on Zulip Johan Commelin (May 27 2020 at 11:21):

I'm trying to get rid of the actual_

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:22):

what are actual_ordered_comm_monoids used for?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:23):

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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 27 2020 at 11:28):

Also, I would still get the mul_le_mul name conflict

view this post on Zulip Johan Commelin (May 27 2020 at 11:29):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:32):

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

view this post on Zulip Mario Carneiro (May 27 2020 at 11:32):

or primes

view this post on Zulip 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