A ring or linarith tactic for ENNReal numbers

Stream: new members

[Arshak Parsa]

ring or linarith work fine for real numbers. Is there any similar tactic for ENNReal?
I don't know why it's so hard to prove the following theorem :/

theorem ENNReal.add_sub_cancel_left2 {a b : ENNReal}  (ha : a ≠ ∞) (hb : b ≠ ∞): a + (b - a) = b := by
  -- linarith
  -- ring
  -- lift a to ℝ using ha
  #check ENNReal.add_sub_cancel_left
  sorry

[Etienne Marion]

This is not true. 1 + (0 - 1) = 1 + 0 = 1 ≠ 0

[Arshak Parsa]

@Etienne Marion
You are right.

[Etienne Marion]

This works though:

import Mathlib

theorem ENNReal.add_sub_cancel_left2 {a b : ENNReal} (hab : a ≤ b): a + (b - a) = b := by
  simp only [add_tsub_cancel_of_le, hab]

[Arshak Parsa]

Is there any tactic like ring or linarith for ENNReal?

[Etienne Marion]

I don't think so, but not 100% sure

[Jireh Loreaux]

No, primarily because it would have very bad properties due to ∞ and truncated subtraction. If you really want access to something like that, you would need to first deal with the ∞ case, express everything as a coercion from ℝ≥0, apply norm_cast to remove the coercions, then coerce to ℝ, and in the latter step you'll still need to deal with truncated subtraction. All of that is considerable work. For now, I recommend just using the API for ℝ≥0∞ as suggested by Etienne.

[Eric Wieser]

norm_num still can't handle division in ℝ≥0, though I have a stale PR that makes progress on this