Linearly ordered vector spaces: spelling and linarith

Stream: Is there code for X?

[Terence Tao]

I'm interested in developing some API for linearly ordered vector spaces, in order to easily handle manipulations of asymptotic orders of magnitude (such as $O(N^2 \log^3 N)$) which can be viewed as belonging to such spaces (with the "logarithmic scale" interpretation of multiplication as addition, and exponentiation as scalar multiplication, while addition becomes "max" in the obvious ordering). For this I would like the ability to use a linarith type tool to immediately settle implications such as the following:

import Mathlib

example (R: Type*) [AddCommMonoid R] [Module ℝ R] [LinearOrder R] [OrderedSMul ℝ R] (x y z: R) (h1: x ≤ (2:ℝ) • y) (h2: y < z) : x < (2:ℝ) • z := calc
    _ ≤ (2:ℝ) • y := h1
    _ < _ := OrderedSMul.smul_lt_smul_of_pos h2 (by norm_num)

I have two questions:

1. Is there a better spelling for linearly ordered vector spaces than this? docs#OrderedSMul has very minimal API and states "This file is now mostly useless. We should try deleting OrderedSMul", but it is not clear what the replacement would be. There is docs#ConvexCone , which has more API, but does not have much in the way of identifying this cone with the order structure.
2. How difficult would it be to extend linarith to be able to cover these sorts of use cases?

[Yaël Dillies]

Oh apologies, the TODO should say that the replacement is the definitions in Mathlib.Algebra.Order.Module.Defs, ie docs#PosSMulMono and friends

[Terence Tao]

Amusingly, docs#PosSMulMono states "You should usually not use this very granular typeclass directly, but rather a typeclass like OrderedSMul."

[Yaël Dillies]

Time has passed :-)

[Terence Tao]

Wait, so is the recommendation to continue using OrderedSMul, but look to docs#PosSMulMono and friends for all the actual API?

[Yaël Dillies]

No, the recommendation is to avoid using OrderedSMul as much as possible, although it is currently the most convenient option. The history is that:

1. I encountered some use case which OrderedSMul didn't cover
2. I added PosSMulMono and friends, with the docstring that probably you should use OrderedSMul instead
3. I noticed that actually all OrderedSMul could do, PosSMulMono and friends could do better
4. I generalised the OrderedSMul API to PosSMulMono and friends, and added that TODO to delete OrderedSMul
5. The uses of OrderedSMul outside its immediate API still survive to this day, and you get confused by reading a confusing set of docstrings

[Yaël Dillies]

Of course, step 5 should have been "OrderedSMul is fully deprecated", but we all know how long my TODO list is :see_no_evil:

[Ruben Van de Velde]

Step 4.5: update the docs

[Kim Morrison]

grind can now prove some results about linearly ordered vector space (and give counterexamples).

open Lean.Grind

variable (R : Type) [IntModule R] [LinearOrder R] [IntModule.IsOrdered R]

example (x y z : R) (h1 : x ≤ 2 * y) (h2 : y < z) : x < 2 * z := by
  grind -- 🎉

We'll be hooking this up to Mathlib's typeclasses in the next few weeks.