Zulip Chat Archive

Stream: general

Topic: ordered with pos


Damiano Testa (Jun 08 2021 at 12:44):

Dear All,

I am about to start preparing a PR to push the ordered refactor across types with add and mul. This essentially involves asserting that multiplication by strictly positive elements be monotone (on top of what is already there for monotonicity of addition). While this is relatively easy to implement, there are two possible approaches that I have played with. I think that, in the long run, maybe we should implement both, but, for the moment, I would start with one. Below are the two approaches that I have in mind: let me know if you have a preference for either one of them or if you see problems/benefits with one or the other!

Thanks!

Approach 1: monotone multiplication. Simply introduce new typeclasses asserting

 (a : N) {b c : N}, (0 < a)  (b  c)  (a * b  a * c)

with various layers according to whether the inequality is strict or not, or whether multiplication is on the left or on the right. This is relatively straightforward. The main drawback is that it uses homogeneous multiplication. Thus, it may cause problems when trying to multiply a (unit nnreal) by an ennreal.

Approach 2: monotone action. Introduce a more general typeclass allowing an action of a Type M on a second Type N and asserting

 (m : M) {n₁ n₂ : N}, (n₁  n₂)  (m  n₁  m  n₂)

This approach of course allows for more general statements, and would work better developing some API for "positive subtypes" of types with an order. In the first instance, this can be quite short, only introducing a "Type of positive elements" whenever a type has_zero and has_lt.

My preference is for Approach 2. This works well in abstract Types, but also in concrete cases where you might want to multiply a positive rational number by an ennreal and know that multiplication is monotone.

What are people's opinions on this? Should I create a poll?

Gabriel Ebner (Jun 08 2021 at 12:51):

Damiano Testa said:

Thus, it may cause problems when trying to multiply a (unit nnreal) by an ennreal.

Can you maybe give another example? You can multiply a units nnreal and an ennreal just fine (the unit will just coerce to an ennreal).

Damiano Testa (Jun 08 2021 at 13:22):

At the moment, I am actually failing to identify an example where there may not be a coercion saving the day. Maybe there is no need for the extra generality of the "proper action" and all can be resolved using coercions+multiplication?

I can only think of the following "dynamical-systems-like" example.
Suppose that you have a Type X with a self-map f : X → X. This determines an action of on X by iterating f. You can then act on set X elementwise via f^[n] ''. On set X there is an addition (taking unions) and a (taking subsets) and the -action is monotone. At this level, there is no coercion from to set X that would work, I think.

Does this count? The answer could well be: "this is too contrived, so we do not need the greater generality"!

Damiano Testa (Jun 08 2021 at 13:27):

I guess that the main take-away from the example is that you do not need a multiplication on N to have a monotonicity of something acting on it. I feel like I should know a good example of this, but I am not managing to bring it to my conscience!

Eric Wieser (Jun 08 2021 at 14:55):

Your approach 2 looks like a weaker version of docs#smul_lt_smul_of_pos

Eric Wieser (Jun 08 2021 at 14:57):

Gabriel Ebner said:

You can multiply a units nnreal and an ennreal just fine (the unit will just coerce to an ennreal).

It's not really the point of this thread, but I think there should be a algebra nnreal ennreal instance somewhere, from which we'd get has_scalar (units nnreal) ennreal automatically.

Johan Commelin (Jun 08 2021 at 14:58):

algebra R A assumes that A is a semiring, right? But ennreal isn't.

Damiano Testa (Jun 08 2021 at 15:14):

Eric, thank you for digging out something that would likely be an application of Approach 2, (should Approach 2 become part of mathlib)!

While it is possible that most applications of the ordered refactor could be solved by instances, I still think that it might be worthwhile to pursue both Approach 1 and Approach 2, although not in the same PR. I am now going to propose a poll, to see with which one to begin!

Damiano Testa (Jun 08 2021 at 15:16):

/poll mul_pos_monotone
Approach 1: monotone multiplication ∀ (a : N) {b c : N}, (0 < a) → (b ≤ c) → (a * b ≤ a * c)
Approach 2: monotone action ∀ (m : M) {n₁ n₂ : N}, (n₁ ≤ n₂) → (m • n₁ ≤ m • n₂)

Eric Wieser (Jun 08 2021 at 15:17):

Oh, I totally missed that. Then I guess I mean there should be a mul_action nnreal ennreal?

Eric Wieser (Jun 08 2021 at 15:19):

Damiano, is the idea behind approach 2 to use a subtype M for the 0 < a condition?

Damiano Testa (Jun 08 2021 at 15:22):

Eric, yes, I would use the subtype that you mention to apply it, but only if approach 1 is not also developed.

Eric Wieser (Jun 08 2021 at 15:22):

Johan Commelin said:

algebra R A assumes that A is a semiring, right? But ennreal isn't.

docs#ennreal.canonically_ordered_comm_semiring suggests to me that ennreal is a semiring

Damiano Testa (Jun 08 2021 at 15:23):

(I do not view the two approaches as opposing: sometimes the "unbundled" approach 1 is better, other times the "bundled" approach 2 is better. it is not difficult to go from one to the other, though having direct paths both ways may be convenient)

Floris van Doorn (Jun 08 2021 at 15:25):

In approach 2 you are adding the assumption 0 < m right?

Damiano Testa (Jun 08 2021 at 15:25):

In approach 2 you do not need to add the assumption 0 < m, since you would only get an instance of that type if multiplication is monotone.

Johan Commelin (Jun 08 2021 at 15:25):

@Eric Wieser you're right. my bad

Damiano Testa (Jun 08 2021 at 15:26):

In other words, if multiplication of a type on another is monotone, likely the action of the first type is by positive elements.

Damiano Testa (Jun 08 2021 at 15:26):

But you need not have even an order relation on the acting type in order to get monotonicity of the action: the inequalities are all on the target type N.

Floris van Doorn (Jun 08 2021 at 15:28):

Ah, I see.

Damiano Testa (Jun 08 2021 at 15:28):

Thus, Approach 2 is outsourcing to the typeclass system to make sure that you have a proof that the elements of the Type M actually do have the correct monotonicity.

Floris van Doorn (Jun 08 2021 at 15:28):

One advantage of approach 2 is that it generalizes both approach 1 and the current covariant_class, right?

Damiano Testa (Jun 08 2021 at 15:29):

Yes, indeed, covariant_class would be applying approach 2 with twice the same type (i.e. M = N).
and the "positive multiplication" would be using approach 2 with the "type of positive elements" acting on the actual type.

Damiano Testa (Jun 08 2021 at 15:34):

Mathematically, there is little difference. In Lean, instead of multiplying by the elements of a Type N that happen to be positive, you allow yourself to act on N with the elements of another type M.

The use case is of course the one where M is the subtype of the positive elements of N, though this would not be required by the definitions.

Floris van Doorn (Jun 08 2021 at 15:36):

I think approach 2 is worth trying.

Eric Wieser (Jun 08 2021 at 15:42):

How about a third appoach:

class is_monotone (f : A  B) :=
(out : monotone f)

which you can then write approach 2 as using [∀ m : M, is_monotone ((•) m : N → N)]

Damiano Testa (Jun 08 2021 at 15:45):

Eric, I like your suggestion, although I would also want to allow the freedom of having strict_mono. In other words, I was thinking of leaving the (order) relation as an input of the class, like for covariant.

Damiano Testa (Jun 08 2021 at 15:46):

So, I could sometimes assume that multiplication is monotone and sometimes strictly monotone.

Floris van Doorn (Jun 08 2021 at 16:10):

Wait, covariant_class can be used to do approach 2, right? covariant_class {x : M // 0 < x} M (•) (≤)

Eric Wieser (Jun 08 2021 at 16:19):

Damiano Testa said:

Eric, I like your suggestion, although I would also want to allow the freedom of having strict_mono. In other words, I was thinking of leaving the (order) relation as an input of the class, like for covariant.

my experiments in #7834 suggest that typeclasses with lots of (dependent) inputs as you're suggesting might be a bad idea - but it's also possible my problem is something else

Eric Wieser (Jun 08 2021 at 16:35):

Johan Commelin said:

Eric Wieser you're right. my bad

#7846

Damiano Testa (Jun 08 2021 at 16:39):

Eric, some similar comments on times had been raised before the introduction of covariant_class though some timings performed by Jannis Limperg suggested that the covariant approach was (very marginally) faster than the current one with ordered_...`. In any case, I will try to see how it works and then we can decide what is best. This will likely be tomorrow, though!

Damiano Testa (Jun 08 2021 at 16:40):

Floris, I think that I had tried to recycle covariant_class, but had failed. I will try again and see how it works!

Damiano Testa (Jun 08 2021 at 16:40):

In any case, thank you all for the support!

Eric Wieser (Jun 08 2021 at 17:00):

My concern is not so much about speed, but about whether typeclass search will get stuck on the resulting dependent types.

Eric Wieser (Jun 08 2021 at 17:01):

Eric Wieser said:

I think there should be a algebra nnreal ennreal instance somewhere, from which we'd get has_scalar (units nnreal) ennreal automatically.

#7846 now provides distrib_mul_action (units ℝ≥0) ℝ≥0∞

Damiano Testa (Jun 09 2021 at 13:29):

Dear All,

here is a follow up, based on the discussion that we were having yesterday. Below is a beginning of code to convert lemmas about ordered_semirings into lemmas about covariant_class M N (some_action) (<).

[Floris, this seems to work: I think that I had something more general in mind that would require three types, instead of two.]

Main question. Can I make the final proof of mul_lt_mul_of_pos_left"simpler"?

Side question. How would you improve the code?

Thanks!

import algebra.ordered_ring

/--  The positive elements of a type. -/
def posi (α : Type*) [has_zero α] [has_lt α] : Type* := { a : α // 0 < a }

namespace posi

/--  An element of `posi α` can be coerced into `α`. -/
instance (α : Type*) [has_zero α] [has_lt α] : has_coe (posi α) α :=
{ coe := λ a, a.1 }

/--  A positive element of `α` can be lifted into `posi α`. -/
instance (α : Type*) [has_zero α] [has_lt α] : can_lift α (posi α) :=
{ coe  := coe,
  cond := λ a, 0 < a,
  prf  := λ a ha, Exists.intro a, ha rfl }

/--  An ordered semiring automatically inherits a covariant_class for strictly monotone
multiplication by positive elements. -/
instance ordered_semiring.to_covariant_class_posi_left (α : Type*) [ordered_semiring α] :
  covariant_class (posi α) α (λ a b, a * b) (<) :=
{ covc := λ a b c bc, mul_lt_mul_of_pos_left bc a.2 }

/-  The lemma in general. -/
lemma mul_lt_mul_of_pos {M N : Type*} (μ : M  N  N) [has_lt N] [covariant_class M N μ (<)]
  {m : M} {n o : N} (h₁ : n < o) : μ m n < μ m o :=
covariant_class.covc _ h₁

/-  If possible, I would like this proof to be simply an application of the general lemma. -/
lemma mul_lt_mul_of_pos_left {α : Type*} [ordered_semiring α] {a b c : α}
  (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b :=
by {  lift c to (posi α) using h₂,
      convert posi.mul_lt_mul_of_pos (λ (x : posi α) (y : α), x * y) h₁ }

end posi

Damiano Testa (Jun 09 2021 at 13:42):

(also, I do not mind if a few initial lemmas have some awkwardness, but I would like to simply be able to apply most of the general lemmas in the ordered_semiring context, without having to juggle around type-theoretic assumptions all the time.)

Kevin Buzzard (Jun 09 2021 at 15:03):

instance (α : Type*) [has_zero α] [has_lt α] : can_lift α (posi α) :=
{ coe  := coe,
  cond := λ a, 0 < a,
  prf  := λ a ha, ⟨⟨a, ha⟩, rfl }

Damiano Testa (Jun 09 2021 at 15:08):

Thanks Kevin! I edited the code above, to implement your suggestion!

Kevin Buzzard (Jun 09 2021 at 15:20):

local attribute [elab_simple] mul_lt_mul_of_pos

lemma mul_lt_mul_of_pos_left' {α : Type*} [ordered_semiring α] {a b c : α}
  (h₁ : a < b) (h₂ : 0 < c) : ((⟨c, h₂ : posi α) : α) * a < c * b :=
mul_lt_mul_of_pos (λ x y, x * y : posi α  α  α) h₁

lemma mul_lt_mul_of_pos_left {α : Type*} [ordered_semiring α] {a b c : α}
  (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b :=
mul_lt_mul_of_pos_left' h₁ h₂

Kevin Buzzard (Jun 09 2021 at 15:21):

not sure if that's the answer you wanted!

Damiano Testa (Jun 09 2021 at 15:22):

I need to digest it, but it might be close to what I had in mind!

Damiano Testa (Jun 09 2021 at 15:23):

The idea would be that "under the hood" you prove the lemmas with the ' in that style, but then you are allowed to use them in the familiar context with the "explicit" positivity assumption, rather than the one implicit in the subtype?

Damiano Testa (Jun 09 2021 at 15:25):

(I am also toying around with introducing a smul between posi α and α, but that is also a little heavy: having the explicit 0 < c or 0 \le c assumption in context is convenient, certainly for thinking about these lemmas.)

Kevin Buzzard (Jun 09 2021 at 15:37):

I'm not sure I know the idea, I was just trying to solve the puzzle you set :-)

Damiano Testa (Jun 09 2021 at 15:41):

Yes, that is a great start: thank you so much for your help!

Floris van Doorn (Jun 09 2021 at 18:05):

If you make the m in mul_lt_mul_of_pos explicit (which it should be), then the following also works:

lemma mul_lt_mul_of_pos_left {α : Type*} [ordered_semiring α] {a b c : α}
  (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b :=
(posi.mul_lt_mul_of_pos (λ (x : posi α) (y : α), x * y) c, h₂ h₁ : _)

Kevin Buzzard (Jun 09 2021 at 19:11):

Aah, this is the correct solution. I knew you shouldn't be messing with the elaboration strategies but I've realised recently that I still don't properly understand the rules for which inputs should be explicit.

Damiano Testa (Jun 09 2021 at 19:24):

Floris, thank you so much! I had the correct argument explicit in the definition of covariant_class but got lazy here: I will be more careful!

Reid Barton (Jun 09 2021 at 22:30):

Is there a reason to (at least in Approach 1) only require multiplication by positive elements to be monotone? It seems better mathematically to include the case 0 = a. For example, the product of two types satisfying the condition with 0 < a won't necessarily also satisfy it, because 0 < (a, a') doesn't imply 0 < a.

Is this a historical artifact perhaps? I seem to recall the Lean core library's definition of an ordered ring being odd, involving strict inequalities where <= would be more natural.

Reid Barton (Jun 09 2021 at 22:34):

Of course in any sensible context it shouldn't matter since when 0 = a we have 0 * b = 0 = 0 * c.

Damiano Testa (Jun 10 2021 at 04:26):

Dear Reid,

you are completely right, of course!

The reason I chose specifically strict monotonicity was simply because I still want the existing lemmas in mathlib to "just work". In fact, the whole ordered refactor started because I felt that the existing system was not designed to deal with order relations interacting with general algebraic operations, not necessarily commutative, for instance. Thus, I plan to prove lemmas for strict and non-strict monotonicity, but I certainly want to preserve the existing lemmas.

Reid Barton (Jun 10 2021 at 15:10):

OK, I don't know what order of refactors is best, but the eventually desired state should be one in which ordered_ring has only mul_nonneg as an axiom and not mul_pos.

Ruben Van de Velde (Jun 10 2021 at 15:32):

order of refactors, huh

Damiano Testa (Jun 10 2021 at 15:55):

Reid, at the moment, I am simply introducing typeclasses for proving statements with more flexible (typeclass) assumptions. I am not thinking of changing the definition of ordered_ring. At least, not yet!


Last updated: Dec 20 2023 at 11:08 UTC