linarith max

Stream: mathlib4

[Gareth Ma]

Is it possible to make linarith solve this?

example {a b : ℝ} : a ≤ max a b := by linarith

[Scott Morrison]

Rewrite with the definition of max and then split ifs? This is outside the scope of linarith, although if we put a bit more effort into nice configuration of pre-processors there's not reason you couldn't have a preprocessor for this.

[Gareth Ma]

Yeah, what I meant was to patch linarith to solve it directly. It seems that it fails to find a contradiction in a > max a b, but that sounds feasible if as you said, you unfold the definition and the and.

[Gareth Ma]

But if you said it's out of scope for the tactic, then nevermind :)

[Scott Morrison]

If you look at the code for linarith, you'll see that the core code tries to do something very simple: just inequalities over a linearly ordered field. Anything beyond that is a "pre-processor". You could add one that unfolds and splits max and min, I think.

[Joël Riou]

It would not be useful here, but you may help linarith by providing some extras facts it can use, like linarith [le_max_left a b]: this would help getting more intricate inequalities for which we need to know a ≤ max a b.

[Gareth Ma]

Yep I know that, thanks though!