## Stream: maths

### Topic: ordered stuff

#### Damiano Testa (Apr 21 2021 at 19:18):

Dear All,

every once in a while, someone comes along saying that there is something funny about ordered_[something] (typically ordered_semiring).

Given the large quantity of typeclasses for types with one or two operations, with/without zero, with/without one, (non-)commutative, non-unital, cancel, left/right cancel, and so on, I have a proposal.

Do not define ordered_[everything] with the variant linearly_ordered_. Instead, assume the "ring-type" class and the "order-type" class separately and introduce one or two typeclasses for types that have mul and le (possibly slightly more) to bind the two.

Here is a more concrete proposal.

The main extra axioms are monotonicity of add/mul on the left/right. There is also a "contrapositive" version of monotonicity (that is equivalent to monotonicity for linear orderings):

a * b < a * c → b < c


that I would probably add to the classes below for good measure.

Thus, I suggest to introduce

• a mul_left_mono , a ≤ b → c * a ≤ c * b, and contrapositive,
• a mul_right_mono, a ≤ b → a * c ≤ b * c, and contrapositive,
• a mul_mono (extending left and right),
• the to_additive of those, and
• zero_le_one.

Besides giving more flexibility with mixing in the classes, this also allows removing a large number of typeclasses.

What are people's opinion on this? Does it seem worthwile? Reasonable? Are there some unseen issues that I might be missing?

#### Oliver Nash (Apr 21 2021 at 19:59):

IIUC, this is the ordered flavour of the issue that we have to choose between either having an exponential number of type classes or having exponential term sizes.

#### Oliver Nash (Apr 21 2021 at 20:01):

I am reminded of this recent-ish thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/.60.5Bcomm_ring.20R.5D.60.20vs.20.60.5Bring.20R.5D.20.5Bcomm.20R.5D.60/near/231441524

#### Floris van Doorn (Apr 21 2021 at 23:06):

I also think the current method has a problem: we have many ordered_[algebraic_thing], and we don't nearly have all combinations.
On an old branch branch#canonically_ordered_sub I tried to add a sub field to docs#canonically_ordered_add_monoid (since many canonically ordered types have a sub defined for that type specifically, and I wanted to unify these definitions). However, to do it properly, I would have to greatly increase the number of ordered_[algebraic_thing] classes, so it kind-of stalled.

I think making the ordered_[algebraic_thing] classes mixins is a good idea, that will hugely decrease the number of classes we need. However, I don't think we should split up the classes like you propose: we still keep the [ordered_(semi)ring \a] class. However, this time it takes arguments [semiring \a] [partial_order \a]. And then we can change these arguments, but we don't need change the mixin:

• [semiring \a] [partial_order \a] [ordered_ring \a]
• [ring \a] [partial_order \a] [ordered_ring \a]
• [semiring \a] [linear_order \a] [ordered_ring \a]
• [ring \a] [linear_order \a] [ordered_ring \a]
(currently the linearly ordered structures are also assumed to be nontrivial. If that is important, I guess we have to add that as a separate argument as well.)
This is very similar to how we do docs#topological_group.

#### Damiano Testa (Apr 22 2021 at 03:05):

Floris, thanks a lot for your input!

I will try to make a concrete model following your proposal, although I may not have much time today.

Let me try to summarize your idea. We should have separate typeclasses for left/right_ordered_(semi)rings, left/right_ordered_(comm_)monoid(_with...), (+ additive version), each of which takes

• a left/right/both input,
• a preorder/partial order/linear order input
and returns a typeclass that adds monotonicity on the correct side of the corresponding algebraic structure?

Roughly, we should have
(3 for left, right, both) * (3 for monoid, add_monoid, semiring) = 9
typeclasses, right? E.g.

• ordered_left_add_monoid  with input something with has_add and has_le, => addition on the left is monotone, or
• ordered_semiring  with input something with has_add, has_mul and has_le => addition and multiplication are monotone on the left and on the right.

Let me know if this is not what you had in mind!

#### Scott Morrison (Apr 22 2021 at 03:08):

In your bulleted list you've included preorder/partial order/linear order as a varying parameter. Hopefully this should just be handled by mixing, not dependency.

#### Damiano Testa (Apr 22 2021 at 03:11):

Scott, you are right: I did not intend the kind of order to play a role, other than has_le is present! I will remove it!

#### Damiano Testa (Apr 22 2021 at 03:14):

More concretely, the typeclasses will simply add two axioms for each operation + or * specified: monotonicity of left/right/both addition/multiplication and the cancellative/contrapositive version (which is unnecessary but would be assumed in case the order is linear).

#### Damiano Testa (Apr 22 2021 at 04:21):

Here is a first attempt at setting up this proposal:

import tactic.ring

set_option old_structure_cmd true

namespace ordered_proposal

class ordered_left_mul (α : Type*) extends has_mul α, has_le α, has_lt α :=
(mul_le_mul_left       : ∀ (a b c : α), a ≤ b → c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c)

class ordered_right_mul (α : Type*) extends has_mul α, has_le α, has_lt α :=
(mul_le_mul_right       : ∀ (a b c : α), a ≤ b → a * c ≤ b * c)
(lt_of_mul_lt_mul_right : ∀ (a b c : α), a * c < b * c → a < b)

class ordered_mul (α : Type*) extends ordered_left_mul α, ordered_right_mul α

class ordered_left_add (α : Type*) extends has_add α, has_le α, has_lt α :=
(add_le_add_left       : ∀ (a b c : α), a ≤ b → c + a ≤ c + b)
(lt_of_add_lt_add_left : ∀ (a b c : α), a + b < a + c → b < c)

class ordered_right_add (α : Type*) extends has_add α, has_le α, has_lt α :=
(add_le_add_right       : ∀ (a b c : α), a ≤ b → a + c ≤ b + c)
(lt_of_add_lt_add_right : ∀ (a b c : α), a + c < b + c → a < b)

class ordered_left_semiring (α : Type*)
extends ordered_left_add α, ordered_left_mul α, has_zero α, has_one α :=
(zero_le_one : (0 : α) ≤ 1)

class ordered_right_semiring (α : Type*)
extends ordered_right_add α, ordered_right_mul α, has_zero α, has_one α :=
(zero_le_one : (0 : α) ≤ 1)

class ordered_semiring (α : Type*) extends ordered_left_semiring α, ordered_right_semiring α
-- this name already exists for a typeclass that often raised questions.
-- The typeclass proposed here is not equivalent to the current ordered_semiring.

end ordered_proposal


#### Damiano Testa (Apr 22 2021 at 04:49):

I am thinking that I might make the add/mul be an input of a typeclass ordered_left and then there is no need for the to_additive version...

#### Scott Morrison (Apr 22 2021 at 05:34):

Hmm, that last suggestion sounds a bit un-mathlib-y, and will possibly make using to_additive more of a struggle. I would just embrace to_additive. :-)

#### Damiano Testa (Apr 22 2021 at 05:38):

Ok, I am not trying to push the explicit add/mul issue further, but another unification that would have arisen, is that you could dispense with left/right, since you could feed it (+), for the left add version, or function.swap (*), for the right mul version.

#### Damiano Testa (Apr 22 2021 at 05:42):

Anyway, my initial suggestion would be to simply add these typeclasses in a first PR and do nothing else.

I would relegate the removal of the existing typeclasses, replacing them with the ones above to a later PR.

The only issue that I see at the moment with this plan is that the new ordered_semiring would clash with the old one. Would calling the new one ordered_add_mul be a better name?

#### Scott Morrison (Apr 22 2021 at 06:52):

I don't think we would want to add these new typeclasses unless we knew they were actually going to work, so I'm not sure it makes sense to do this in separate PRs.

#### Sebastien Gouezel (Apr 22 2021 at 08:01):

Damiano Testa said:

Here is a first attempt at setting up this proposal:

import tactic.ring

set_option old_structure_cmd true

namespace ordered_proposal

class ordered_left_mul (α : Type*) extends has_mul α, has_le α, has_lt α :=
(mul_le_mul_left       : ∀ (a b c : α), a ≤ b → c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c)


There is a problem with this definition that you are embedding a multiplication in this class. So, if you require [ring α] [linear_order α] [ordered_left_mul α] then you have two unrelated multiplications, which is not what you want. The idea of mixins is rather that they should not contain data, and take the data as typeclass assumptions. I am a little bit wary of

class ordered_left_mul (α : Type*) [has_mul α] [has_le α] [has_lt α] :=
(mul_le_mul_left       : ∀ (a b c : α), a ≤ b → c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c)


because it means that any mention of this class would have a lot of parameters. Maybe one could indeed define these classes to state theorems in the most general version, but for the practical hierarchy I think I'd go directly for things like

class left_ordered_semiring (α : Type*) [semiring α] [partial_order α] :=
(mul_le_mul_left       : ∀ (a b c : α), a ≤ b → c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c)


and then record an instance from this to your general class ordered_left_mul.

#### Damiano Testa (Apr 22 2021 at 13:41):

Sébastien, thank you very much for your comments: I did run exactly into the issue that you mention!

#### Damiano Testa (Apr 22 2021 at 13:42):

I have been playing a bit with this and the code below seems like it would work to do the mix and interact well with to_additive. Do people have any opinion on whether it seems like a good solution?

import tactic.ring

set_option old_structure_cmd true

class my_mix (M N : Type*) (μ : M → N → N) (r : N → N → Prop) (s : N → N → Prop) :=
(direct  :  ∀ (c) {a b}, r a b → r (μ c a) (μ c b))
(inverse :  ∀ (c) {a b}, s (μ c a) (μ c b) → s a b)

namespace my_mix

variables {M : Type*} [has_mul M] [has_le M] [has_lt M]
variables {a b : M} (c : M)

lemma mul_le_mul_left [my_mix M M (*) (≤) (<)] (ab : a ≤ b) :
c * a ≤ c * b :=
direct (<) c ab

lemma mul_le_mul_right [my_mix M M (function.swap (*)) (≤) (<)] (ab : a ≤ b) :
a * c ≤ b * c :=
direct (<) c ab

lemma lt_of_mul_lt_mul_left [my_mix M M (*) (≤) (<)] (ab : c * a < c * b) :
a < b :=
inverse (≤) c ab

lemma lt_of_mul_lt_mul_right [my_mix M M (function.swap (*)) (≤) (<)] (ab : a * c < b * c) :
a < b :=
inverse (≤) c ab

end my_mix


#### Damiano Testa (Apr 26 2021 at 10:00):

Dear All,

here is a current proposal to counterbalance the ordered_algebraic_gadget hierarchy in such a way that the hypotheses on

• the order (preorder, partial_order, linear_order),
• the algebraic operations (mul, add),
• the appropriate left/right monotonicity

can be split. I am planning to make a PR with these changes, but I welcome any comment! Below is a sample of what is going on: the actual code posted below is quite short, but it also contains a lot of doc-strings and comments to help with readability.

import algebra.ring.basic

set_option old_structure_cmd true

section variants

variables {M N : Type*} (μ : M → N → N) (r s : N → N → Prop) (m : M) {a b c : N}

variables (M N)
/-- covariant is useful to formulate succintly statements about the interactions between an
action of a Type on another one and a relation on the acted-upon Type.

See the covariant_class doc-string for its meaning. -/
def covariant     : Prop := ∀ (m) {n₁ n₂}, r n₁ n₂ → r (μ m n₁) (μ m n₂)

/-- contravariant is useful to formulate succintly statements about the interactions between an
action of a Type on another one and a relation on the acted-upon Type.

See the contravariant_class doc-string for its meaning. -/
def contravariant : Prop := ∀ (m) {n₁ n₂}, s (μ m n₁) (μ m n₂) → s n₁ n₂

/--  Given an action μ of a Type M on a Type N and a relation r on N, informally, the
covariant_class says that "the action μ preserves the relation r.

More precisely, the covariant_class is a class taking two Types M N, together with an "action"
μ : M → N → N and a relation r : N → N.  Its unique field covc is the assertion that
for all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair
(n₁, n₂), then, the relation r also holds for the pair (μ m n₁, μ m n₂),
obtained from (n₁, n₂) by "acting upon it by m".

If m : M and h : r n₁ n₂, then covariant_class.covc m h : r (μ m n₁) (μ m n₂).
-/
class covariant_class :=
(covc :  covariant M N μ r)

/--  Given an action μ of a Type M on a Type N and a relation r on N, informally, the
contravariant_class says that "if the result of the action μ on a pair satisfies the
relation r, then the initial pair satisfied the relation r.

More precisely, the contravariant_class is a class taking two Types M N, together with an
"action" μ : M → N → N and a relation r : N → N.  Its unique field covtc is the assertion that
for all m ∈ M and all elements n₁, n₂ ∈ N, if the relation r holds for the pair
(μ m n₁, μ m n₂) obtained from (n₁, n₂) by "acting upon it by m"", then, the relation r
also holds for the pair (n₁, n₂).

If m : M and h : r (μ m n₁) (μ m n₂), then covariant_class.covc m h : r n₁ n₂.
-/
class contravariant_class :=
(covtc : contravariant M N μ s)

namespace sample_application

variables (R : Type*) [comm_ring R] [linear_order R]
variables [covariant_class R R (*) (≤)] [contravariant_class R R (function.swap (+)) (<)]
variables {x y z : R} (hle : y ≤ z)  (hlt : y + x < z + x)

#check (covariant_class.covc x hle : x * y ≤ x * z)
#check (contravariant_class.covtc x hlt : y < z)

-- sample definition
/--  Addition on the left is monotone.  The two fields are defeq to
* add_le_add_left       :  ∀ (a) {b c}, b ≤ c → a + b ≤ a + c,
* lt_of_add_lt_add_left :  ∀ (a) {b c}, a + b ≤ a + c → b < c.
-/

/--  Multiplication on the left is monotone.  The two fields are defeq to
* mul_le_mul_left       :  ∀ (a) {b c}, b ≤ c → a * b ≤ a * c,
* lt_of_mul_lt_mul_left :  ∀ (a) {b c}, a * b ≤ a * c → b < c.
-/
class mul_left_mono (M : Type*) extends has_mul M, has_le M, has_lt M :=
(mul_le_mul_left       :  (covariant M M (*) (≤)))
(lt_of_mul_lt_mul_left :  contravariant M M (*) (<))

-- sample instance
instance mul_left_mono.to_covariant_class [mul_left_mono M] :
covariant_class M M (*) (≤) :=
{ covc := mul_left_mono.mul_le_mul_left }

-- together with these, I also plan to incorporate instances from "well-known" typeclasses,
-- such as ordered_comm_monoid to this hierarchy

end sample_application


#### Damiano Testa (Apr 26 2021 at 10:06):

I should have said, many of the lemmas in algebra/ordered_monoid can be proven by assuming at most two of the covariant contravariant classes + an algebraic class, such as has_mul or mul_one_class + an order class, such as preorder or partial_order.

#### Eric Wieser (Apr 26 2021 at 10:09):

For what it's worth you could also write covariant as ∀ m, (r ⇒ r) (μ m) (μ m), which is defeq and comes with a tiny bit of API.

#### Damiano Testa (Apr 26 2021 at 10:09):

Thanks Eric: I do not even know how to type the arrow symbol, but I can take a look!

#### Eric Wieser (Apr 26 2021 at 10:10):

It's docs#relator.lift_fun and \r=

#### Eric Wieser (Apr 26 2021 at 10:14):

class mul_left_mono (M : Type*) extends has_mul M, has_le M, has_lt M := is not going to work though

#### Eric Wieser (Apr 26 2021 at 10:14):

If you extend has_mul and has_le, then you can't use your class at the same time as ring or partial_order (doing so would pull in two different versions of those operators), which is a massive dealbreaker.

#### Eric Wieser (Apr 26 2021 at 10:15):

class mul_left_mono (M : Type*) [has_mul M] [has_le M] [has_lt M] := would be safe in that regard

#### Damiano Testa (Apr 26 2021 at 10:19):

Ok, I have been mostly using assumptions such as [preorder α] [mul_one_class α] [covariant_class α α has_mul.mul has_le.le]. To be honest, I do not really feel the need to introduce the classes mul_left_mono. I do seem to care about having instances from the "known" classes to the correctly decorated co(ntra)variant class and then prove lemmas assuming co(ntra)variant_class.

This seems in line with what you are saying, right? I may simply ditch the add/mul_left/righ_mono typeclasses altogether.

#### Eric Wieser (Apr 26 2021 at 10:37):

The direction you're exploring for this ordered stuff looks a lot like the direction explored for basic algebra structure with docs#is_commutative and docs#is_left_id etc. Since the latter exploration seems to have been abandoned, it would be good to understand why before attempting to follow in its footsteps

#### Damiano Testa (Apr 26 2021 at 10:41):

Well, at the moment, the change is really minimal and you can split the left/right assumptions, which alone seems worthwhile.

#### Damiano Testa (Apr 26 2021 at 10:42):

If anyone knows of pitfalls or issues with the is_commutative/is_left_id approach mentioned by Eric, please, let me know!

#### Kevin Buzzard (Apr 26 2021 at 10:55):

It looks to me like something which was introduced in core Lean and they figured they'd see if it turned out to be useful, and for some reason it didn't catch on -- perhaps because we were so fixated on old structures that we didn't need it?

#### Damiano Testa (Apr 26 2021 at 10:57):

Ok, I am going to try it, since I do believe that the left/right distinction is important, the actual change is tiny, and the lemmas are much more general now.

#### Mario Carneiro (Apr 26 2021 at 11:37):

The @[algebra] classes were part of a plan for an algebraic normalizer in lean core that was derailed by lean 4

#### Mario Carneiro (Apr 26 2021 at 11:37):

they are basically unfinished code

#### Mario Carneiro (Apr 26 2021 at 11:40):

Importantly, note the section on "The unbundled approach doesn't work with the simplifier as is." That is still true with today's simp

#### Mario Carneiro (Apr 26 2021 at 11:41):

there was a critical second step in the plan that would have made these classes work well, and that part never happened, so now we just have some unbundled typeclasses, which are useful for exactly what they look like but aren't really usable as a replacement for the algebraic hierarchy

#### Eric Wieser (Apr 26 2021 at 12:18):

I added a brief summary in a docstring in https://github.com/leanprover-community/lean/pull/568 - feel free to edit it @Mario Carneiro.

#### Eric Wieser (Apr 26 2021 at 12:18):

Thanks for the insight!

Ok, thank you!

#### Damiano Testa (Apr 26 2021 at 12:42):

As I am viewing it at the moment, I would keep the usual names (the ordered_...) as the "reference classes". However, I would like the theorems to be proven with the co(ntra)variant assumptions, since those are much more flexible. Since "all" the co(tra)variant variants are instances for ordered_comm_monoid and behave well with to_additive, they should automatically work for the rest of the hierarchy.

#### Damiano Testa (Apr 26 2021 at 12:42):

I am experimenting and it seems to work with very few problems.

#### Damiano Testa (Apr 26 2021 at 15:22):

#7371

It is still experimental, but I also want to see how this hierarchy interacts with the other files!

#### Damiano Testa (Apr 27 2021 at 07:44):

I filled in the various extra _ needed in some files and CI is now in the final Lint/Run Test sprint.

If anyone has any comments on this PR (#7371), I would be very very happy to hear them!

#### Damiano Testa (Apr 27 2021 at 07:45):

(Note that it looks massive, but most of the difference is that I moved a substantial chunk of a file into another one.)

#### Damiano Testa (Apr 27 2021 at 08:13):

To help guide with the review:

• the "old" file algebra/ordered_monoid lost a lot of content that was moved to the new file algebra/ordered_monoid_lemmas,
• new stuff in the old file ordered_monoid includes instances to the new typeclasses covariant and contravariant,
• genuinely new stuff in the new file ordered_monoid_lemmas is basically the first 100 lines; after that, it is "old" lemmas with weaker assumptions (and essentially identical proofs),
• the remaining 10 changed files are simply fixes, almost always caused by different numbers of implicit arguments when @ was used in a lemma.

Disclaimer: no lemmas were removed in the making of this PR.

#### Sebastien Gouezel (Apr 27 2021 at 12:53):

I think I like a lot the idea of switching to mixins instead of infinitely many typeclasses with all possible algebraic structures and all possible order structures. I have a question on the design of the PR, though. You formulate assumptions such as [contravariant_class α α (*) (<)] or [covariant_class α α (*) (≤)] and so on. I think it is a very good idea to have a common instance when it makes it possible to factor out proofs, but here I don't really see what it buys compared to having a few classes like mul_le_mul or friends.

It is likely that instance search would be a little bit faster with the more specialized classes that with the generic contravariant_class and covariant_class mechanism, because with the generic classes Lean would try all instances of the class even when they clearly don't make sense (for instance, it would try the instances for addition even if you're asking for something on multiplication). That shouldn't be a performance bottleneck, though, so if you see an advantage to the generic classes then I'm happy to go for it!

#### Damiano Testa (Apr 27 2021 at 12:56):

I do not know about performance, so I will leave that side of the question. I have tried making a typeclass such as what is below

class ordered_left_mul (α : Type*) [has_mul α] [has_le α] [has_lt α] :=
(mul_le_mul_left       : ∀ (a b c : α), a ≤ b → c * a ≤ c * b)
(lt_of_mul_lt_mul_left : ∀ (a b c : α), a * b < a * c → b < c)


but I could not "stack this on top" of a [semiring α] [partial_order α], since the multiplication and order assumed in ordered_left_mul are "new".

#### Damiano Testa (Apr 27 2021 at 12:59):

With the new instances that take the operation and the order as inputs, you can use the "same" operation and order that you are familiar.

Once I got to this stage, I went for creating only two new classes and merged everything in. I have a dream that, together with the to_additive attribute, there might also be a to_right attribute that would change left to right and mul/add to function.swap mul/add and would just do the quadruplication for you for free!

#### Damiano Testa (Apr 27 2021 at 13:02):

I do think that these typeclasses covariant_class and contravariant_class could be useful in different contexts as well. For instance, Kevin mentioned that a specialization of one of them is something called con/add_con.

#### Damiano Testa (Apr 27 2021 at 13:03):

Also, while they look intimidating, they simply say that you can test a property of pairs before or after acting on each element of the pair by some "operation". This is a relatively common concept in maths.

#### Eric Wieser (Apr 27 2021 at 13:08):

Damiano Testa said:

but I could not "stack this on top" of a [semiring α] [partial_order α], since the multiplication and order assumed in ordered_left_mul are "new".

What do you mean by this? Do you mean example [semiring α] [partial_order α] [ordered_left_mul α] : ... := ... does not work (it should)? Or do you mean that something else you tried that you haven't pasted here didn't work?

#### Damiano Testa (Apr 27 2021 at 13:08):

In any case, there are the axioms that seem useful

• mul_le_mul + left/right + add/mul
• mul_lt_mul + left/right + add/mul
• le_of_mul_le_mul + left/right + add/mul
• lt_of_mul_le_mul + left/right + add/mul

#### Damiano Testa (Apr 27 2021 at 13:09):

Eric, let me try to see what did not work: I was typing based on something that I remembered, not something that I had just tried.

#### Damiano Testa (Apr 27 2021 at 13:36):

I cannot reproduce it now. It might have been that I was trying to use the version with the explicit (*). Indeed, this does not work:

class my_class (α : Type*) (m : α → α → Prop) : Prop := true

class new (α : Type*) extends preorder α, my_class α (≤), my_class α (<)
-- invalid object declaration, environment already has an object named 'new.to_my_class'


I understand the issue, but you are right: if you give different names to the fields, for add, mul, left, right, le, lt, direct and inverse, you should be ok!

#### Damiano Testa (Apr 27 2021 at 13:44):

Ok, this might be a list of all the typeclasses that I have come across:

• mul_le_mul_left
• mul_le_mul_right
• add_le_add_left
• add_le_add_right
• le_of_mul_le_mul_left
• le_of_mul_le_mul_right
• le_of_add_le_add_left
• le_of_add_le_add_right
• mul_lt_mul_left
• mul_lt_mul_right
• add_lt_add_left
• add_lt_add_right
• lt_of_mul_lt_mul_left
• lt_of_mul_lt_mul_right
• lt_of_add_lt_add_left
• lt_of_add_lt_add_right

I was hoping that by reducing them to two and making them take inputs, would have made automation easier. If you think that having them displayed out individually is a better option, I can certainly do this.

This might simply involve changing the first two files, since all the files external to ordered_monoid and ordered_monoid_lemmas have no explicit co(ntra)variant_class assumption.

#### Damiano Testa (Apr 27 2021 at 13:48):

As of now, most of these appear "paired": mul_le_mul_leftcomes together with lt_of_mul_lt_mul_left and there is no "real" left/rightdistinction, since they are only applied to commutative monoids/rings.

#### Sebastien Gouezel (Apr 27 2021 at 13:49):

Yes, I meant using those instead of the covariant_class / contravariant_class instances. I think it shouldn't make any difference for the statements (you would only need to state the multiplicative ones as to_additive should take care of the additive versions).

#### Eric Wieser (Apr 27 2021 at 13:50):

While I like the idea of exploring alternatives to to_additive (that is, passing (*) and (+) explicitly), I think doing it at the same time as splitting apart the order classes is perhaps too many changes at once; your list already becomes half the length with to_additive

#### Damiano Testa (Apr 27 2021 at 13:51):

Ok, but the classes need to be defined individually, right? to_additive only kicks in at the level of lemmas/defs, not classes? Or at least I thought so.

#### Eric Wieser (Apr 27 2021 at 13:56):

Yes, that's true I think

#### Damiano Testa (Apr 27 2021 at 13:58):

Note also that, as of now, to_additive is already doubling all the lemmas, so the change is really only at the "setting up level" and in the first couple of lemmas that refer explicitly with the axiom by its class.field_name. So really, this is a very minor change to the current PR.

to_right: I agree that it does not belong to this PR and I would need to learn a lot of programming to figure out how to do it!

#### Eric Wieser (Apr 27 2021 at 14:06):

Damiano Testa said:

Indeed, this does not work:

class my_class (α : Type*) (m : α → α → Prop) : Prop := true

class new (α : Type*) extends preorder α, my_class α (≤), my_class α (<)
-- invalid object declaration, environment already has an object named 'new.to_my_class'


A version of that which does work is:

class my_class (α : Type*) (m : α → α → Prop) : Prop :=
(cond : true)

class new (α : Type*) extends preorder α :=
(my_class_le : my_class α (≤))
(my_class_lt : my_class α (<))

attribute [instance, priority 100] new.my_class_le new.my_class_lt


#### Damiano Testa (Apr 27 2021 at 14:14):

This is the fully expanded list of classes:

@[ancestor has_add has_le]
(add_le_add_left : ∀ (a : α) {b c}, b ≤ c → a + b ≤ a + c)

class mul_le_mul_left_class (α : Type) extends has_mul α, has_le α :=
(mul_le_mul_left : ∀ (a : α) {b c}, b ≤ c → a * b ≤ a * c)

(add_le_add_right : ∀ (a : α) {b c}, b ≤ c → b + a ≤ c + a)

class mul_le_mul_right_class (α : Type) extends has_mul α, has_le α :=
(mul_le_mul_right : ∀ (a : α) {b c}, b ≤ c → b * a ≤ c * a)

(add_lt_add_left : ∀ (a : α) {b c}, b < c → a + b < a + c)

class mul_lt_mul_left_class (α : Type) extends has_mul α, has_lt α :=
(mul_lt_mul_left : ∀ (a : α) {b c}, b < c → a * b < a * c)

(add_lt_add_right : ∀ (a : α) {b c}, b < c → b + a < c + a)

class mul_lt_mul_right_class (α : Type) extends has_mul α, has_lt α :=
(mul_lt_mul_right : ∀ (a : α) {b c}, b < c → b * a < c * a)

(le_of_add_le_add_left : ∀ (a : α) {b c}, a + b ≤ a + c → b ≤ c)

class le_of_mul_le_mul_left_class (α : Type) extends has_mul α, has_le α :=
(le_of_mul_le_mul_left : ∀ (a : α) {b c}, a * b ≤ a * c → b ≤ c)

(le_of_add_le_add_right : ∀ (a : α) {b c}, b + a ≤ c + a → b ≤ c)

class le_of_mul_le_mul_right_class (α : Type) extends has_mul α, has_le α :=
(le_of_mul_le_mul_right : ∀ (a : α) {b c}, b * a ≤ c * a → b ≤ c)

(lt_of_add_lt_add_left : ∀ (a : α) {b c}, a + b < a + c → b < c)

class lt_of_mul_lt_mul_left_class (α : Type) extends has_mul α, has_lt α :=
(lt_of_mul_lt_mul_left : ∀ (a : α) {b c}, a * b < a * c → b < c)

(lt_of_add_lt_add_right : ∀ (a : α) {b c}, b + a < c + a → b < c)

class lt_of_mul_lt_mul_right_class (α : Type) extends has_mul α, has_lt α :=
(lt_of_mul_lt_mul_right : ∀ (a : α) {b c}, b * a < c * a → b < c)


#### Damiano Testa (Apr 27 2021 at 14:15):

Personally, from the point of view of conciseness, I prefer to have only two new ones. If, however, you think that having all of them is better, than I can change the PR.

#### Sebastien Gouezel (Apr 27 2021 at 14:19):

I don't think extending has_mul and has_le or friends is a good idea: the point of mixins is precisely to let the user prescribe how he likes the algebraic structure (through a ring, a comm_ring, a monoid or a whatever instance), and the order structure (through a partial_order, a linear_order, a conditionally_complete_lattice or whatever instance) and then add your mixin to say how the two interact. If you bake the multiplication and the order into your classes like lt_of_mul_lt_mul_right_class, you can't do this and you're back to square 1, no?

#### Sebastien Gouezel (Apr 27 2021 at 14:20):

Instead, taking them as typeclass assumptions as you did in your previous attemps looks like a perfect solution.

#### Damiano Testa (Apr 27 2021 at 14:21):

I might be misunderstanding something, but I need to have * and < for the field to make sense, no? How can I state

(lt_of_mul_lt_mul_right : ∀ (a : α) {b c}, b * a < c * a → b < c)


for a Type that does not already have a multiplication and an order?

#### Damiano Testa (Apr 27 2021 at 14:22):

(I may be missing something very basic, since I have fallen into many traps while preparing the PR, so feel free to state the completely obvious, or assume that I have missed something trivial!)

#### Sebastien Gouezel (Apr 27 2021 at 14:24):

Just like you did in one of your previous messages:

class mul_le_mul_left (α : Type*) [has_mul α] [has_le α] : Prop :=
∀ (a b c : α), a ≤ b → c * a ≤ c * b


#### Yakov Pechersky (Apr 27 2021 at 14:24):

I think the confusion was which of [ ... ] or extends "creates" a new multiplication or just uses the existing one

#### Damiano Testa (Apr 27 2021 at 14:24):

Ah, the issue is extends! I did not realize that this was different then putting square brackets.. sorry.

#### Yakov Pechersky (Apr 27 2021 at 14:25):

And the answer is [ ... ] says, fetch me what already exists. extends means, create new things of what I'm extending, with this other thing on top additionally

#### Damiano Testa (Apr 27 2021 at 14:25):

Sébastien and Yakov, thank you for bringing my attention to this: I knew that things worked or did not work sometimes, but I had not realized what the source of the problem was!

#### Damiano Testa (Apr 27 2021 at 14:26):

I had the opposite mental image: I thought extend referred to "extend the properties of what you had by adding these axioms", whereas the other, I would have thought "create a new class"!

#### Damiano Testa (Apr 27 2021 at 14:28):

So, here is an updated version:

class has_add_le_add_left (α : Type*) [has_add α] [has_le α] : Prop :=
(add_le_add_left : ∀ (a : α) {b c}, b ≤ c → a + b ≤ a + c)

class has_mul_le_mul_left (α : Type*) [has_mul α] [has_le α] : Prop :=
(mul_le_mul_left : ∀ (a : α) {b c}, b ≤ c → a * b ≤ a * c)

(add_le_add_right : ∀ (a : α) {b c}, b ≤ c → b + a ≤ c + a)

class has_mul_le_mul_right (α : Type*) [has_mul α] [has_le α] : Prop :=
(mul_le_mul_right : ∀ (a : α) {b c}, b ≤ c → b * a ≤ c * a)

(add_lt_add_left : ∀ (a : α) {b c}, b < c → a + b < a + c)

class has_mul_lt_mul_left (α : Type*) [has_mul α] [has_lt α] : Prop :=
(mul_lt_mul_left : ∀ (a : α) {b c}, b < c → a * b < a * c)

(add_lt_add_right : ∀ (a : α) {b c}, b < c → b + a < c + a)

class has_mul_lt_mul_right (α : Type*) [has_mul α] [has_lt α] : Prop :=
(mul_lt_mul_right : ∀ (a : α) {b c}, b < c → b * a < c * a)

(le_of_add_le_add_left : ∀ (a : α) {b c}, a + b ≤ a + c → b ≤ c)

class has_le_of_mul_le_mul_left (α : Type*) [has_mul α] [has_le α] : Prop :=
(le_of_mul_le_mul_left : ∀ (a : α) {b c}, a * b ≤ a * c → b ≤ c)

(le_of_add_le_add_right : ∀ (a : α) {b c}, b + a ≤ c + a → b ≤ c)

class has_le_of_mul_le_mul_right (α : Type*) [has_mul α] [has_le α] : Prop :=
(le_of_mul_le_mul_right : ∀ (a : α) {b c}, b * a ≤ c * a → b ≤ c)

(lt_of_add_lt_add_left : ∀ (a : α) {b c}, a + b < a + c → b < c)

class has_lt_of_mul_lt_mul_left (α : Type*) [has_mul α] [has_lt α] : Prop :=
(lt_of_mul_lt_mul_left : ∀ (a : α) {b c}, a * b < a * c → b < c)

(lt_of_add_lt_add_right : ∀ (a : α) {b c}, b + a < c + a → b < c)

class has_lt_of_mul_lt_mul_right (α : Type*) [has_mul α] [has_lt α] : Prop :=
(lt_of_mul_lt_mul_right : ∀ (a : α) {b c}, b * a < c * a → b < c)


#### Eric Wieser (Apr 27 2021 at 14:30):

attr#ancestor is for extends, so those attributes are wrong there and should just be removed.

#### Yakov Pechersky (Apr 27 2021 at 14:31):

In a lemma, saying [group G] postulates all the axioms of groups on the G : Type, and makes the available in the proving of the lemma. But in a definition (class is just a definition made available to the typeclass search), [group G] says, to use this definition, one must prove first that I have a group structure known on G. Of course, once seen in that way, then lemma is just like a definition: "to use this lemma to prove things, you must first prove that the relevant type has a group structure."

#### Damiano Testa (Apr 27 2021 at 14:37):

Eric, I updated the definitions, removing the ancestors. Anything else?

#### Eric Wieser (Apr 27 2021 at 14:38):

They look reasonable, but I do wonder if they have too much granularity; for instance, are there any situations where you'd want to use any of those on something which isn't a preorder?

#### Eric Wieser (Apr 27 2021 at 14:39):

A good test would be "how many lemmas can I create from just this typeclass"

#### Damiano Testa (Apr 27 2021 at 14:40):

I have not tried hard, but in the initial file, almost all lemmas used a combination of two of the typeclasses above and assumed preorder.

#### Eric Wieser (Apr 27 2021 at 14:42):

I'd also be tempted to use the name has_foo instead of foo_class, but that might be worth a wider poll

#### Damiano Testa (Apr 27 2021 at 14:42):

I agree with you, though, I think that preorder is almost always assumed. However, isn't the point of view that you should make definitions apply as generally as possible? What if someone else later needs a version of this that is not necessarily transitive?

#### Sebastien Gouezel (Apr 27 2021 at 14:44):

I agree that putting just has_le or has_lt is enough here.

#### Sebastien Gouezel (Apr 27 2021 at 14:44):

I agree also that has_foo is better than foo_class.

#### Damiano Testa (Apr 27 2021 at 14:44):

Btw, this was the reasoning that led me to replace them with arbitrary relations and create the covariant and contravariant typeclasses...

#### Damiano Testa (Apr 27 2021 at 14:45):

Once you take this onboard, you only need two classes and apply them to the correct operation and relation.

#### Damiano Testa (Apr 27 2021 at 14:45):

Anyway, I will change the names to has_...

#### Sebastien Gouezel (Apr 27 2021 at 14:45):

There is a gotcha that with your definitions they are of type Type, while you want Prop, so you should specify it explicitly. As in

class lt_of_add_lt_add_right_class (α : Type) [has_add α] [has_lt α] : Prop :=
(lt_of_add_lt_add_right : ∀ (a : α) {b c}, b + a < c + a → b < c)


#### Eric Wieser (Apr 27 2021 at 14:46):

I guess we do have docs#smul_comm_class as prior art for the _class suffix

#### Eric Wieser (Apr 27 2021 at 14:47):

Perhaps that should be renamed to has_smul_comm at some point

#### Damiano Testa (Apr 27 2021 at 14:48):

Changed the names in the code above.

#### Damiano Testa (Apr 27 2021 at 14:51):

... and also (α : Type*) (rather than (α : Type)) as well as : Prop, although I do not understand the reason for this!

#### Damiano Testa (Apr 27 2021 at 14:58):

Anyway, while my "minimalistic" side would have preferred to introduce only 2 new typeclasses instead of 16, if it is the opinion of two moderators that 16 is better than 2, then I will go ahead and revise the PR!

#### Damiano Testa (Apr 27 2021 at 15:01):

(also, my initial driving concept was that I would have wanted to decrease the global number of classes, getting rid of the ordered_[...] ones, in favour of using the two new ones. This also made me less open to adding even more typeclasses!)

#### Eric Wieser (Apr 27 2021 at 15:05):

What's the most of these typeclasses that any existing lemma needs , that you've found so far?

#### Damiano Testa (Apr 27 2021 at 15:07):

I think 3 of these new ones, plus an order and a binary operation

#### Damiano Testa (Apr 27 2021 at 15:08):

e.g.

#check @mul_lt_mul_of_le_of_lt
mul_lt_mul_of_le_of_lt :
∀ {α : Type u_2} {a b c d : α}
[_inst_1 : partial_order α]
[_inst_2 : cancel_monoid α]
[_inst_3 : covariant_class α α has_mul.mul has_le.le]
[_inst_4 : contravariant_class α α has_mul.mul has_lt.lt]
[_inst_5 : covariant_class α α (function.swap has_mul.mul) has_le.le],

a ≤ b → c < d → a * c < b * d


#### Damiano Testa (Apr 27 2021 at 15:09):

I have not played with rings, though, only monoids. So it might be 6, when you want to mix orders on addition and multiplication in the same statement.

#### Damiano Testa (Apr 28 2021 at 13:25):

I have collected all these latest comments in the new PR #7369. I went for a PR that only introduces the new typeclasses and will get to using them for the actual lemmas in a later PR. Of course, comments are always more than welcome!

#### Eric Wieser (Apr 28 2021 at 13:43):

I assume you meant #7396?

#### Damiano Testa (Apr 28 2021 at 14:02):

Yes, Eric, thank you for the correction!

Last updated: Jun 17 2021 at 17:28 UTC