ordered stuff

Stream: maths

[Damiano Testa]

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]

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]

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]

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]

Oliver, thanks for your comment: I had not thought about the lengthening of proof terms!

[Damiano Testa]

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 ring/monoid/add_monoid typeclass, and
• 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]

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]

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]

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]

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_add (α : Type*) extends ordered_left_add α, ordered_right_add α

attribute [to_additive] ordered_left_mul
attribute [to_additive] ordered_right_mul
attribute [to_additive] ordered_mul

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]

Any comments are really welcome!

[Damiano Testa]

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]

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]

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]

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]

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]

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)
(add_le_add ...) : add the right axiom you want to put here

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

[Damiano Testa]

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

[Damiano Testa]

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)

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

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

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

@[to_additive]
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]

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`.
-/
@[ancestor has_add has_le has_lt]
class add_left_mono extends has_add M, has_le M, has_lt M :=
(add_le_add_left       :  covariant M M (+) (≤))
(lt_of_add_lt_add_left :  contravariant M M (+) (<))

/--  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`.
-/
@[ancestor has_mul has_le has_lt, to_additive]
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
@[to_additive]
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]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

they are basically unfinished code

[Mario Carneiro]

see https://github.com/leanprover/lean/wiki/Refactoring-structures#encoding-the-algebraic-hierarchy-1

[Mario Carneiro]

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]

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]

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]

Thanks for the insight!

[Damiano Testa]

Ok, thank you!

[Damiano Testa]

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]

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

[Damiano Testa]

#7371

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

[Damiano Testa]

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]

(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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

Yes, that's true I think

[Damiano Testa]

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]

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]

Eric, I like your suggestion!

This is the fully expanded list of classes:

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

@[ancestor has_mul has_le, to_additive]
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)

@[ancestor has_add has_le]
class add_le_add_right_class (α : Type) extends has_add α, has_le α :=
(add_le_add_right : ∀ (a : α) {b c}, b ≤ c → b + a ≤ c + a)

@[ancestor has_mul has_le, to_additive]
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)

@[ancestor has_add has_lt]
class add_lt_add_left_class (α : Type) extends has_add α, has_lt α :=
(add_lt_add_left : ∀ (a : α) {b c}, b < c → a + b < a + c)

@[ancestor has_mul has_lt, to_additive]
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)

@[ancestor has_add has_lt]
class add_lt_add_right_class (α : Type) extends has_add α, has_lt α :=
(add_lt_add_right : ∀ (a : α) {b c}, b < c → b + a < c + a)

@[ancestor has_mul has_lt, to_additive]
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)

@[ancestor has_add has_le]
class le_of_add_le_add_left_class (α : Type) extends has_add α, has_le α :=
(le_of_add_le_add_left : ∀ (a : α) {b c}, a + b ≤ a + c → b ≤ c)

@[ancestor has_mul has_le, to_additive]
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)

@[ancestor has_add has_le]
class le_of_add_le_add_right_class (α : Type) extends has_add α, has_le α :=
(le_of_add_le_add_right : ∀ (a : α) {b c}, b + a ≤ c + a → b ≤ c)

@[ancestor has_mul has_le, to_additive]
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)

@[ancestor has_add has_lt]
class lt_of_add_lt_add_left_class (α : Type) extends has_add α, has_lt α :=
(lt_of_add_lt_add_left : ∀ (a : α) {b c}, a + b < a + c → b < c)

@[ancestor has_mul has_lt, to_additive]
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)

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

@[ancestor has_mul has_lt, to_additive]
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]

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]

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]

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

[Damiano Testa]

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]

(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]

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]

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

[Damiano Testa]

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

[Yakov Pechersky]

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]

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]

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]

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)

@[to_additive]
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)

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

@[to_additive]
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)

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

@[to_additive]
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)

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

@[to_additive]
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)

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

@[to_additive]
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)

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

@[to_additive]
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)

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

@[to_additive]
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)

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

@[to_additive]
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]

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

[Yakov Pechersky]

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]

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

[Eric Wieser]

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]

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

[Damiano Testa]

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]

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]

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]

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

[Sebastien Gouezel]

I agree also that has_foo is better than foo_class.

[Damiano Testa]

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

[Damiano Testa]

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

[Damiano Testa]

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

[Sebastien Gouezel]

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]

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

[Eric Wieser]

Perhaps that should be renamed to has_smul_comm at some point

[Damiano Testa]

Changed the names in the code above.

[Damiano Testa]

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

[Damiano Testa]

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]

(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]

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

[Damiano Testa]

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

[Damiano Testa]

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]

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]

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]

I assume you meant #7396?

[Damiano Testa]

Yes, Eric, thank you for the correction!