docs#ordered_smul

Stream: maths

[Yaël Dillies]

What is the motivation for ordered_smul? It seems to me like it's quite restrictive due to the ∀ {a b : M} {c : R}, c • a < c • b → 0 < c → a < b axiom.

And indeed structural instances (docs#pi.ordered_smul and docs#prod.ordered_smul) are only true under strong assumptions on the scalars (namely docs#linear_ordered_field), and the only non-structural instances that we have is docs#linear_ordered_semiring.to_ordered_smul that proves ordered_smul R R.

In particular, I was expecting to find instances for ordered_smul ℕ α, ordered_smul ℤ α, ordered_smul ℚ α each under reasonable assumptions for α. But they may still be true?

[Oliver Nash]

Ages ago I thought I wanted ordered_smul ℕ R for something or other. I have some horrible code that I wrote before I realised I didn't need it after all which shows that linear_ordered_cancel_add_comm_monoid suffices:

import algebra.order.smul

variables {R : Type*} [linear_ordered_cancel_add_comm_monoid R]

lemma foo (a b : R) (n : ℕ) (hab : a < b) (hn : 0 < n) :
  n • a < n • b :=
begin
  suffices : ∀ (m : ℕ), m.succ • a < m.succ • b,
  { rw ← nat.succ_pred_eq_of_pos hn,
    apply this, },
  intros m,
  induction m with m ih,
  { simp only [one_nsmul, hab], },
  { simp only [succ_nsmul _ m.succ, add_lt_add hab ih], },
end

instance ordered_nsmul : ordered_smul ℕ R :=
{ smul_lt_smul_of_pos := λ a b n hab hn,
  begin
    suffices : ∀ (m : ℕ), m.succ • a < m.succ • b,
    { rw ← nat.succ_pred_eq_of_pos hn,
      apply this, },
    intros m,
    induction m with m ih,
    { simp only [one_nsmul, hab], },
    { simp only [succ_nsmul _ m.succ, add_lt_add hab ih], },
  end,
  lt_of_smul_lt_smul_of_pos := λ a b n hab hn,
  begin
    -- TODO Generalise this approach: should have `ordered_smul` constructor with single proof
    -- obligation for any linearly-ordered scalars?
    rcases lt_trichotomy a b with h | rfl | h,
    { assumption, },
    { simp only [lt_self_iff_false] at hab, contradiction, },
    { simpa using hab.trans (foo b a n h hn), },
  end }

[Yaël Dillies]

Isn't your TODO docs#ordered_smul.mk'? Or do you want something intermediate?

[Oliver Nash]

Oh, it looks like it is. That snippet is from months ago, I barely remember writing it. Oh except I note that docs#ordered_smul.mk' demands a field.

[Oliver Nash]

I just wanted to demonstrate that linear_ordered_cancel_add_comm_monoid was sufficient.

[Yaël Dillies]

It really looks like ordered_smul, as currently designed, is only useful over linear orders.

[Yaël Dillies]

#16247