linarith over NNReal

Stream: new members

[Li Xuanji]

I find linarith very useful for inequalities in ℝ (I know when it will/won't work), and I miss a tactic like it in NNReal, and I'm wondering how people work with inequalities in NNReal. I think I understand why linarith doesn't work (Fourier-Motzkin elimination (FME) won't work with saturating subtraction). One way I saw to prove inequalities is to transfer to ℝ:

import Mathlib

example (a b c d: NNReal) (h1 : a < b) (h2 : c ≤ d) : a + c < b + d := by
    rw [←NNReal.coe_lt_coe, ←NNReal.coe_le_coe] at *
    push_cast
    -- now h1, h2, ⊢ are statements about ℝ, so linarith works
    linarith

This is less convenient as it modifies all the assumptions by default, and I also need to manually rewrite inequalities to < or ≤

import Mathlib

example (a b c d: NNReal) (h1 : b > a) (h2 : c ≤ d) : a + c < b + d := by
    have h1' : a < b := h1  -- necessary otherwise the next line fails to modify h1
    rw [←NNReal.coe_lt_coe, ←NNReal.coe_le_coe] at *
    push_cast
    linarith

And it needs help to prove that specific subtractions don't saturate:

import Mathlib

example (a b c d: NNReal) (h1 : a < b) : 0 < b - a := by
    sorry -- I don't actually know how to prove this, haven't needed to learn yet

Some concrete questions:

1. Is there some algorithm like FME in informal math that proves linear inequalities with "saturating" subtraction?
2. Is there a uniform way to prove the first two examples? E.g. a tactic to rewrite all inequalities to < / ≤. Even better if it handles all 3 examples.

[Yaël Dillies]

Do you know about rify?

[Yaël Dillies]

Li Xuanji said:

a tactic to rewrite all inequalities to < / ≤

The mathlib philosophy here is to have all inequalities in the form < / ≤ in the first place. Who handed you those shady >/≥?

[Li Xuanji]

Do you know about rify?

Not really - I use zify so I have some idea of what this kind of tactic does, but the rify docstring doesn't mention NNReal (only ℕ, ℤ or ℚ)

Who handed you those shady >/≥?

Some informal math proof which has steps like (some complicated expression) > (a simpler expression) > (a very simple expression). I try to rewrite stuff in < / ≤ but when working with ℝ I'm used to being able to switch to the other form (for short sections at least) and having linarith deal with it

[Yaël Dillies]

Li Xuanji said:

the rify docstring doesn't mention NNReal (only ℕ, ℤ or ℚ)

Ah! If it doesn't handle ℝ≥0, we definitely should change it so that it does :smile:

[Kevin Buzzard]

Yes, given that we have zify to go to Int from Nat, we should make rify work from NNreal to Real, presumably following what zify does.