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_class
es 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):
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_class
es, 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_semiring
s 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