ordered_module on nat and int

Stream: maths

[Eric Wieser]

Is this true? We don't have the instance for it if so.

instance {M : Type*} [ordered_add_comm_monoid M] : ordered_module ℕ M := sorry

@Damiano Testa, you might have some insight here.

[Damiano Testa]

I have not played yet with ordered_modules, so I am not able to help, sorry...

[Kevin Buzzard]

It looks true to me but I ran into this when I tried:

import tactic
import algebra.module.ordered

instance foo {M : Type*} [ordered_add_comm_monoid M] : ordered_module ℕ M :=
{ smul_lt_smul_of_pos := begin
    intros a b c hab hcpos,
    cases c, cases hcpos, clear hcpos,
    induction c,
    { rwa [one_nsmul, one_nsmul] },
    { rw [succ_nsmul, succ_nsmul b],
      apply add_lt_add,
      /-
      invalid apply tactic, failed to synthesize type class instance for
      covariant_class M M has_add.add has_lt.lt
      state:
      case nat.succ
      M : Type ?,
      _inst_1 : ordered_add_comm_monoid M,
     -/
      sorry }
  end,
  lt_of_smul_lt_smul_of_pos := sorry }

Am I doing something wrong? I want a<b and c<d implies a+c<b+d in an ordered_add_comm_monoid.

[Eric Wieser]

docs#add_lt_add doesn't give any clues

[Eric Wieser]

Does refine fare any better

[Adam Topaz]

Isnt {0,1} with the idempotent addition and 0<1 an additive commutative ordered monoid?

[Damiano Testa]

Adam, I was not able to get your example to work, but a slight modification seems to work: in {0,1,at_least_two} with addition defined by setting everything bigger than 1 equal to at_least_two, the inequality 1 < at_least_two does not imply the inequality 1+1 < at_least_two + at_least_two = at_least_two, since the two sides are equal. This in particular explains why Lean does not find the covariant_class instance that is stopping Kevin's proof: if that instance were there, then add_lt_add would hold.

[Damiano Testa]

I forgot to mention: of course, also 1 < at_least_two does not imply 2 • 1 < 2 • at_least_two, again since the two sides are equal. This should contradict the smul_lt_smul_of_pos field of ordered_module.

[Adam Topaz]

Oh yeah, of course. But yes, this is essentially the counterexample I had in mind.

[Adam Topaz]

Anyway, it seems to me that these examples are sufficiently natural that they should fit into the framework. Perhaps the axioms should be relaxed a bit?

[Damiano Testa]

Yes, I agree and this is partly why I embarked in the order refactor.

[Damiano Testa]

I am not sure that eventually the definition of ordered_[...] will change, but it will be easy to assume what you want of your ordered_[...] and have access to the correct lemmas.

[Damiano Testa]

covariant_class and contravariant_class simply mean some monotonicity of some operation and you have complete freedom of which operation, on which side you act and on whether the inequality is strict or not.

[Adam Topaz]

Wouldn't all these issues disappear if we enforce only non-strict inequalities?

[Damiano Testa]

They probably would, but the strict inequality holds (and is useful) in other cases, for instance for linear ordered groups. It is convenient to get these assumptions by typeclasses

[Damiano Testa]

(For instance, it would be awkward to state add_lt_add, but that is a lemma that you definitely want to use sometimes.)

[Adam Topaz]

That would work in an ordered additive monoid with cancellative addition, so we could use the typeclass system for this as well

[Damiano Testa]

True, but with covariant_class you assume even less than cancellative_....

[Reid Barton]

I think it's more reasonable to impose these conditions involving < only when we are in the totally ordered case.
I found https://www.math.lsu.edu/~madden/tomonoids.pdf which seems relevant, see the paragraph on page 5 containing the equation (TI). There, $S$ is a commutative monoid.

[Damiano Testa]

In fact, the final reason why I started the refactor was that getting lemmas to work for nnreal was always a bit tricky.

[Adam Topaz]

Oh, what I'm suggesting is for add_lt_add to use the following classes:
[covariant_class A A has_add.add has_le.le] and [cancellative A] (I don't know if [cancellative] is thing)

[Reid Barton]

In general, a partially ordered whatever should only have conditions saying that the whatever structure preserves <= in a reasonable sense

[Damiano Testa]

Adam, Reid, I think that the origin of the strict inequalities in Lean for ordered arises from negatingcontraposing the implication a \le b -> a*c \le b*c and then formally replacing the \not \le with < and assuming that instead. So, yes, for linear orders, they are "correct". Otherwise, they are weird.

[Damiano Testa]

Also, Adam, add_lt_add holds with the assumptions

[preorder α]
[_inst_2 : has_add α]
[covariant_class α α has_add.add has_lt.lt]
[covariant_class α α (function.swap has_add.add) has_le.le]

and the two covariant assumptions are there, just because there is no need to assume commutativity of addition: they are equivalent under the commutativity assumption.