Zulip Chat Archive

Stream: general

Topic: ordered refactor resurrected


Damiano Testa (Jan 30 2022 at 12:20):

Dear All,

after a long pause, I am picking this up again. Here is now where the real test of the covariant_classes starts! What do people think of this prototype?

import algebra.order.ring

universe u
variable {α : Type u}

/-  For reference, the definition of an `ordered_semiring`:
An `ordered_semiring α` is a semiring `α` with a partial order such that
addition is monotone and multiplication by a positive number is strictly monotone.
@[protect_proj]
class ordered_semiring (α : Type u) extends semiring α, ordered_cancel_add_comm_monoid α :=
(zero_le_one : 0 ≤ (1 : α))
(mul_lt_mul_of_pos_left :  ∀ a b c : α, a < b → 0 < c → c * a < c * b)
(mul_lt_mul_of_pos_right : ∀ a b c : α, a < b → 0 < c → a * c < b * c)
-/

section cov_con
variables [semiring α] [partial_order α]
instance semiring_has_scalar_pos : has_scalar {x : α // 0 < x} α :=
{ smul := λ x y, x * y }

variables [covariant_class {x : α // 0 < x} α () ()] {a b c : α}

/-  A sample lemma.  Most of the subsequent ones will not need to juggle with `let` and `show`. -/
lemma pre (ab : a  b) (c0 : 0  c) : c * a  c * b :=
begin
  by_cases cz : c = 0, { simp [cz] },
  let c₀ : {x : α // 0 < x} := c, c0.lt_of_ne (ne.symm cz)⟩,
  show c₀  a  c₀  b, from covariant_class.elim c₀ ab
end

/-  For instance, this one does not need it. -/
lemma mul_nonneg_1 (a0 : 0  a) (b0 : 0  b) : 0  a * b :=
(mul_zero a).ge.trans (pre b0 a0)

end cov_con

section ordered_semiring
variables [ordered_semiring α] {a b c d : α}

/-  There will be several instances like this one. -/
instance : covariant_class {x : α // 0 < x} α () (<) :=
{ elim := λ c a b ab, ordered_semiring.mul_lt_mul_of_pos_left a b c ab c.2 }

end ordered_semiring

--... etc

Damiano Testa (Feb 02 2022 at 17:47):

I would be very happy to hear comments and ideas!

Thank you!

Johan Commelin (Feb 02 2022 at 18:13):

Great to see you back on track! Thanks a lot for doing this

Alex J. Best (Feb 02 2022 at 18:42):

What is the motivation for the notation, did you try any alternatives like or (or even + or >0!), I personally find some of these a bit more intuitive, but of course they may not work technically due to clashes with other notations.

Damiano Testa (Feb 02 2022 at 18:54):

The main reason is that typing \+ feels like the right symbol!

There was a discussion about notation, and I seem to remember that >0 did not please Mario.

I am not sure that I tried + alone, but either that or something similar confused lean with the actual + sign of has_add.add

Damiano Testa (Feb 02 2022 at 18:56):

Anyway, I was not set on the notation and am happy to try out different things. My expectation is that the notation will only be used inside the typeclasses, but not elsewhere.

Alex J. Best (Feb 02 2022 at 19:04):

Oh okay, I was thinking this was a first step towards having a way of getting pnat from nat and lemmas coming from TC, to allow preal prat etc also and that these types would be referred to by the notation. But if the notation is just for the file its not worth worrying about too much of course.

Damiano Testa (Feb 02 2022 at 19:10):

I will try out your suggestions extensively tomorrow, though.

Thanks for your comments!

Damiano Testa (Feb 02 2022 at 19:10):

Hmm, I had not thought about pnat, since I was focused on the fields of an ordered_semiring. I need to think a bit about whether I can get pnat to work as well, though!

Damiano Testa (Feb 02 2022 at 19:10):

In this case, good notation would definitely be more important!

Damiano Testa (Feb 02 2022 at 21:02):

Alex, I've been thinking about this and I suspect that the following might work.

The coercion from ˋpnatˋ to ˋℕˋ is injective, monotone and preserves multiplication. From this, it should be possible to prove that ˋpnatˋ satisfies several ˋco(ntra)_variant_classˋes.

Thus, you should get access to many lemmas about interactions between multiplication and order on ˋpnatˋ.

Addition should follow in a similar way, although then it becomes important that no additive identity is required by the typeclass assumptions. I think that I have been careful about this and only climbed the typeclass ladder progressively, starting from ˋhas_mulˋ to lush ˋgroupˋ only when really required, but I would need to check this again.

Yaël Dillies (Feb 02 2022 at 21:06):

Importantly, pnat is an add_monoid.

Damiano Testa (Feb 02 2022 at 21:06):

add_monoid or add_semigroup? I always get the two confused...

Yaël Dillies (Feb 02 2022 at 21:07):

Oh, uh, add_semigroup actually...

Damiano Testa (Feb 02 2022 at 21:07):

Anyways, the one without an additive identity!

Yaël Dillies (Feb 02 2022 at 21:07):

docs#pnat.add_comm_semigroup

Damiano Testa (Feb 02 2022 at 21:08):

Regardless of terminology, I have actually proved many lemmas only assuming ˋ@[to_additive] has_mulˋ, so most of the pieces at least should be there.

Damiano Testa (Feb 03 2022 at 08:16):

I attempted this and it might be a success! Here is what works in my file:

section pos_notation
variables {α : Type*} [has_zero α] [has_lt α]

notation α`⊹`:1025 := {x : α // 0 < x}

end pos_notation

section pnat_like
-- start with a reasonable type
variables {α : Type*} [mul_zero_class α] [preorder α] [covariant_class α α sx (<)]

-- e.g. `ℕ` satisfies them by introducing
instance : covariant_class   sx (<)  :=
{ elim := by { rintros a, a0 b c bc, exact (mul_lt_mul_left a0).mpr bc } }

--  get multiplication on `α⊹`; order properties seem to be automatically deduced by subtypes
instance pos.has_mul : has_mul α :=
{ mul := λ a, a0 b, b0⟩, _, (mul_zero (a : α)).symm.le.trans_lt (mul_lt_mul_left' b0 a0)⟩ }

--  get the appropriate monotonicity type-class on `α⊹`
instance pos.to_covariant_class : covariant_class α α (*) (<) :=
{ elim := by { rintros a, a0 b, b0 c, c0 bc, exact mul_lt_mul_left' bc a0 } }

-- both of these now work!  I put `_root_` just to make sure that I was not using a specialized
-- lemma from one of my current imports.
current imports.
lemma attempt_1 {b c : α} (bc : b < c) (a : α) :
  a * b < a * c :=
_root_.mul_lt_mul_left' bc a

-- of course, this should not be surprising, given the above, but it feels good!
lemma attempt_2 {b c : } (bc : b < c) (a : ) :
  a * b < a * c :=
_root_.mul_lt_mul_left' bc a

end pnat_like

Damiano Testa (Feb 03 2022 at 08:25):

So, if this is really where the PR is going, it may be a good idea to think carefully about the notation α⊹ for the subtype of positive elements of a type (with zero and lt). This would then probably be in a separate file, where all the relevant typeclasses would also be added.

Damiano Testa (Feb 03 2022 at 08:25):

I am tempted to finish this PR as is, possibly changing only the notation. I would leave the"reaping out the goodies" from this refactor to subsequence ones.

Yaël Dillies (Feb 03 2022 at 08:30):

What you really want is an analog of docs#nonneg

Damiano Testa (Feb 03 2022 at 08:45):

Ok, I would then be even more inclined to introduce a simple (possible better) notation for this file and leave the full API of pos to a separate PR.

Damiano Testa (Feb 03 2022 at 08:46):

I really would like to get ahead with the lemmas in ordered_semiring using co(ntra)variant_classes, before embarking on this other journey!

Damiano Testa (Feb 03 2022 at 08:46):

And, if someone else feels that the want to do pos, do go for it! It will take me some time to do the ordered_semiring lemmas!

Yaël Dillies (Feb 03 2022 at 08:53):

Btw, pos is canonically ordered, but not in the sense of docs#canonically_ordered_add_monoid

Yaël Dillies (Feb 03 2022 at 08:54):

One must replace le_iff_exists_add (a b : α) : a ≤ b ↔ ∃ c, b = a + c by lt_iff_exists_add (a b : α) : a < b ↔ ∃ c, b = a + c

Damiano Testa (Feb 03 2022 at 13:13):

Is there a list of available symbols that can be used, for instance, in notations?

Yaël Dillies (Feb 03 2022 at 13:18):

Have you had a look through the VScode extension abbreviation list?

Damiano Testa (Feb 03 2022 at 13:22):

I had not: I did not know it existed! Thanks!

Damiano Testa (Feb 04 2022 at 16:59):

After a few comments and the discussion about notation, I opened a PR: #11833.

More lemmas like these will follow, but I prefer to get the process started, before producing a long PR with lemmas that all look very similar to one another!

Oliver Nash (Apr 29 2022 at 12:39):

Is #13376 part of this effort? It looks fine to me but I confess I never followed the ordered refactor in detail (despite being very grateful to @Damiano Testa and others for their work) so I'd appreciate some additional context.

Damiano Testa (Apr 29 2022 at 12:52):

Oliver, thank you for bringing my attention back to this!

This is indeed part of the order refactor and I am happy with the proposed changes!

Damiano Testa (Apr 29 2022 at 12:54):

The refactor is now in its final stages: the lemmas and instances take care of using monotonicity of multiplication when the multiplying element is positive. These are the final steps, in order to start being able to place instances on ordered_semirings and the "explicit" types.

Oliver Nash (Apr 29 2022 at 12:59):

OK great, thanks for the context! As I said it looks good to me too so I've sent it to bors.

Scott Morrison (May 07 2022 at 08:09):

Related to this topic, hopefully, if someone interested in lemmas about orders could have a look at #13296, that would be great. It has been sitting near the top of the #queue for a while.

Damiano Testa (May 07 2022 at 08:27):

Scott, thanks for bringing my attention back to this: I had not given my approval, just because I forgot.

FR (Jun 17 2022 at 17:01):

Most of the basic lemmas have been prepared. In the following PRs, I will try to replace some lemmas in algebra/order/ring.

All these lemmas put the assumptions for comparison with 0 in the last now, but I guess it's better to put them before others. Hoping to get some guidelines.

Yuyang Zhao (Sep 09 2022 at 22:54):

zero_lt lemmas encountered the similar problems that happened on group_with_zero lemmas. Their names conflict with the names of plain covariant_class lemmas. Adding a suffix like _of_nonneg often makes the name too long and sometimes there are both 0 < and 0 ≤ assumptions. How about letting some of the zero_lt lemmas also have the suffix ?

Yuyang Zhao (Sep 10 2022 at 00:14):

Unfortunately there is something like docs#mul_lt_mul_of_lt_of_le₀. I will check if these can be replaced by covariant_class lemmas.

Yuyang Zhao (Sep 10 2022 at 01:32):

Seems we can't do that. It would be nice if the suffix could be used...

Yuyang Zhao (Sep 10 2022 at 01:50):

Then I would use which means positive.


Last updated: Dec 20 2023 at 11:08 UTC