feat(Tactic): linarith and rify for NNReal (leanprover-community#35155)

Co-authored-by: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>

Author: DavidLedvinka

Mathlib.lean

@@ -6805,6 +6805,7 @@ public import Mathlib.Tactic.Linarith
 public import Mathlib.Tactic.Linarith.Datatypes
 public import Mathlib.Tactic.Linarith.Frontend
 public import Mathlib.Tactic.Linarith.Lemmas
+public import Mathlib.Tactic.Linarith.NNRealPreprocessor
 public import Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
 public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
 public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes

Mathlib/Data/NNReal/Basic.lean

@@ -140,6 +140,12 @@ typeclass. For lemmas about subtraction and addition see lemmas about `OrderedSu
 theorem sub_div (a b c : ℝ≥0) : (a - b) / c = a / c - b / c :=
   tsub_div _ _ _
 
+/-- This lemma is needed for the `norm_cast` simp set. Outside of this use case `Nat.coe_sub`
+should be used. -/
+@[norm_cast]
+protected theorem coe_sub_of_lt {a b : ℝ≥0} (h : a < b) :
+    ((b - a : ℝ≥0) : ℝ) = b - a := NNReal.coe_sub h.le
+
 end Sub
 
 section Csupr
@@ -210,6 +216,18 @@ set_option backward.isDefEq.respectTransparency false in
 
 end Csupr
 
+section rify
+
+@[rify_simps] lemma toReal_eq (a b : ℝ≥0) : a = b ↔ (a : ℝ) = (b : ℝ) := by simp
+
+@[rify_simps] lemma toReal_le (a b : ℝ≥0) : a ≤ b ↔ (a : ℝ) ≤ (b : ℝ) := by simp
+
+@[rify_simps] lemma toReal_lt (a b : ℝ≥0) : a < b ↔ (a : ℝ) < (b : ℝ) := by simp
+
+@[rify_simps] lemma toReal_ne (a b : ℝ≥0) : a ≠ b ↔ (a : ℝ) ≠ (b : ℝ) := by simp
+
+end rify
+
 @[simp]
 theorem range_coe : range toReal = Ici 0 := Subtype.range_coe
 

Mathlib/Tactic.lean

@@ -138,6 +138,7 @@ public import Mathlib.Tactic.Linarith
 public import Mathlib.Tactic.Linarith.Datatypes
 public import Mathlib.Tactic.Linarith.Frontend
 public import Mathlib.Tactic.Linarith.Lemmas
+public import Mathlib.Tactic.Linarith.NNRealPreprocessor
 public import Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
 public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
 public import Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes

Mathlib/Tactic/Linarith/NNRealPreprocessor.lean

@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2026 David Ledvinka. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Ledvinka
+-/
+module
+
+public meta import Mathlib.Tactic.Linarith
+public meta import Mathlib.Tactic.Rify
+public import Mathlib.Data.NNReal.Basic
+
+/-!
+# NNReal linarith preprocessing
+
+This file contains a `linarith` preprocessor for converting (in)equalities in `ℝ≥0` to `ℝ`.
+
+By overriding the behaviour of the placeholder preprocessor `nnrealToReal` (which does nothing
+unless this file is imported) `linarith` can still be used without importing `NNReal`.
+-/
+
+public meta section
+
+namespace Mathlib.Tactic.Linarith
+
+open Lean Meta
+
+/--
+`isNNRealProp tp` is true iff `tp` is an inequality or equality between nonnegative real numbers
+or the negation thereof.
+-/
+partial def isNNRealProp (e : Expr) : MetaM Bool := succeeds do
+  let (_, _, .const ``NNReal _, _, _) ← e.ineqOrNotIneq? | failure
+
+/-- If `e` is of the form `((x : ℝ≥0) : ℝ)`, `NNReal.toReal e` returns `x`. -/
+def isNNRealtoReal (e : Expr) : Option Expr :=
+  match e with
+  | .app (.const ``NNReal.toReal _) n => some n
+  | _ => none
+
+/--
+`getNNRealComparisons e` returns a list of all subexpressions of `e` of the form `(x : ℝ)`.
+-/
+partial def getNNRealCoes (e : Expr) : List Expr :=
+  match isNNRealtoReal e with
+  | some x => [x]
+  | none => match e.getAppFnArgs with
+    | (``HAdd.hAdd, #[_, _, _, _, a, b]) => getNNRealCoes a ++ getNNRealCoes b
+    | (``HMul.hMul, #[_, _, _, _, a, b]) => getNNRealCoes a ++ getNNRealCoes b
+    | (``HSub.hSub, #[_, _, _, _, a, b]) => getNNRealCoes a ++ getNNRealCoes b
+    | (``HDiv.hDiv, #[_, _, _, _, a, _]) => getNNRealCoes a
+    | (``Neg.neg, #[_, _, a]) => getNNRealCoes a
+    | _ => []
+
+/-- If `e : ℝ≥0`, returns a proof of `0 ≤ (e : ℝ)`. -/
+def mk_toReal_nonneg_prf (e : Expr) : MetaM (Option Expr) :=
+  try commitIfNoEx (mkAppM ``NNReal.coe_nonneg #[e])
+  catch e => do
+    trace[linarith] "Got exception when using `coe_nonneg` {e.toMessageData}"
+    return none
+
+initialize nnrealToRealTransform.set fun l => do
+  let l ← l.mapM fun e => do
+    let t ← whnfR (← instantiateMVars (← inferType e))
+    if ← isNNRealProp t then
+      return (← Rify.rifyProof e t).1
+    else
+      return e
+  let atoms : List Expr ← withNewMCtxDepth <| AtomM.run .reducible do
+    for e in l do
+      let (_, _, a, b) ← (← inferType e).ineq?
+      discard <| (getNNRealCoes a).mapM AtomM.addAtom
+      discard <| (getNNRealCoes b).mapM AtomM.addAtom
+    return (← get).atoms.toList
+  let nonneg_pfs : List Expr ← atoms.filterMapM mk_toReal_nonneg_prf
+  return nonneg_pfs ++ l
+
+end  Mathlib.Tactic.Linarith

Mathlib/Tactic/Linarith/Preprocessing.lean

@@ -389,12 +389,23 @@ def removeNe : GlobalBranchingPreprocessor where
   transform := removeNe_aux
 end removeNe
 
+/-- Definition overidden in `Mathlib.Tactic.Linarith.NNRealPreprocessor`. -/
+initialize nnrealToRealTransform : IO.Ref (List Expr → MetaM (List Expr)) ← IO.mkRef pure
+
+/--
+If `h` is an equality or inequality between NNReals, `nnrealToReal` lifts this inequality to the
+Reals. It also adds the facts that the reals involved are nonnegative. To avoid adding the same
+nonnegativity facts many times, it is a global preprocessor. This preprocessor does nothing unless
+`Mathlib.Tactic.Linarith.NNRealPreprocessor` is imported -/
+def nnrealToReal : GlobalPreprocessor where
+  description := "move nnreals to reals"
+  transform l := do (← nnrealToRealTransform.get) l
 
 /--
 The default list of preprocessors, in the order they should typically run.
 -/
 def defaultPreprocessors : List GlobalBranchingPreprocessor :=
-  [filterComparisons, removeNegations, natToInt, strengthenStrictInt,
+  [filterComparisons, removeNegations, nnrealToReal, natToInt, strengthenStrictInt,
     compWithZero, cancelDenoms]
 
 /--

Mathlib/Tactic/Rify.lean

@@ -7,12 +7,13 @@ module
 
 public import Mathlib.Data.Rat.Cast.Order
 public import Mathlib.Data.Real.Basic
+public import Mathlib.Tactic.Zify
 public import Mathlib.Tactic.Qify -- shake: keep (for `@[qify_simps]`)
 
 /-!
 # `rify` tactic
 
-The `rify` tactic is used to shift propositions from `ℕ`, `ℤ` or `ℚ` to `ℝ`.
+The `rify` tactic is used to shift propositions from `ℕ`, `ℤ`, `ℚ` or `ℝ≥0` to `ℝ`.
 
 Although less useful than its cousins `zify` and `qify`, it can be useful when your
 goal or context already involves real numbers.
@@ -78,11 +79,32 @@ macro_rules
     simp -decide only [zify_simps, qify_simps, rify_simps, push_cast, $args,*]
       $[at $location]?)
 
+/-- The `Simp.Context` generated by `rify` (with no optional arguments or local context). -/
+def mkRifyContext : MetaM Simp.Context := do
+  let result ← #[`zify_simps, `qify_simps, `rify_simps, `push_cast].mapM fun ext ↦ do
+    let some ext ← getSimpExtension? ext | failure
+    ext.getTheorems
+  Simp.mkContext {failIfUnchanged := false} (simpTheorems := result)
+
+/-- Translate a proof and the proposition into rified form. -/
+def rifyProof (proof : Expr) (prop : Expr) : MetaM (Expr × Expr) := do
+  let (r, _) ← simp prop (← mkRifyContext)
+  Zify.applySimpResultToProp' proof prop r
+
 @[rify_simps] lemma ratCast_eq (a b : ℚ) : a = b ↔ (a : ℝ) = (b : ℝ) := by simp
 @[rify_simps] lemma ratCast_le (a b : ℚ) : a ≤ b ↔ (a : ℝ) ≤ (b : ℝ) := by simp
 @[rify_simps] lemma ratCast_lt (a b : ℚ) : a < b ↔ (a : ℝ) < (b : ℝ) := by simp
 @[rify_simps] lemma ratCast_ne (a b : ℚ) : a ≠ b ↔ (a : ℝ) ≠ (b : ℝ) := by simp
 
+/- The following lemmas are included in `Mathlib.Data.NNReal.Basic` (so that they
+don't need to be imported when using this tactic for `ℕ, ℤ`, or `ℚ`)
+
+`@[rify_simps] lemma toReal_eq (a b : ℝ≥0) : a = b ↔ (a : ℝ) = (b : ℝ) := by simp`
+`@[rify_simps] lemma toReal_le (a b : ℝ≥0) : a ≤ b ↔ (a : ℝ) ≤ (b : ℝ) := by simp`
+`@[rify_simps] lemma toReal_lt (a b : ℝ≥0) : a < b ↔ (a : ℝ) < (b : ℝ) := by simp`
+`@[rify_simps] lemma toReal_ne (a b : ℝ≥0) : a ≠ b ↔ (a : ℝ) ≠ (b : ℝ) := by simp`
+-/
+
 @[rify_simps] lemma ofNat_rat_real (a : ℕ) [a.AtLeastTwo] :
     ((ofNat(a) : ℚ) : ℝ) = (ofNat(a) : ℝ) := rfl
 

MathlibTest/linarith.lean MathlibTest/Linarith/Basic.leanMathlibTest/linarith.lean renamed to MathlibTest/Linarith/Basic.lean

@@ -0,0 +1,26 @@
+import Mathlib.Tactic.Linarith.NNRealPreprocessor
+import Mathlib.Data.ENNReal.Operations
+import Mathlib.Data.ENNReal.Inv
+
+open NNReal
+
+example {a b c : ℝ≥0} (h1 : 2 * a < b + 1) (h2 : b ≤ c) : a < (c + 1) / 2 := by
+  linarith
+
+example {a b c d : ℝ≥0} (h1 : 3 * a + 2 * b ≤ 5 * c + 7) (h2 : c ≤ d) : a ≤ (5 * d + 7) / 3 := by
+  linarith
+
+example {a b c d e : ℝ≥0} (h1 : (a + b) / 2 + c ≤ d) (h2 : d ≤ e) : a ≤ 2 * e := by
+  linarith
+
+example {a b c d : ℝ≥0} (h1 : (a + 3 * b) / 4 < c + 1) (h2 : c ≤ d) : a < 4 * (d + 1) := by
+  linarith
+
+example {a b c d : ℝ≥0} (h1 : 2 * a + b ≤ 3 * c) (h2 : c < d + 5) : a < (3 * (d + 5)) / 2 := by
+  linarith
+
+example {a b c d : ℝ≥0} (h1 : a + b ≤ c) (h2 : c ≤ d / 2) : a ≤ d / 2 := by
+  linarith
+
+example {a b c d : ℝ≥0} (h1 : a + b ≤ 2 * c + 3) (h2 : c ≤ d) : a ≤ 2 * d + 3 := by
+  linarith

MathlibTest/Linarith/NNReal.lean

@@ -1,5 +1,6 @@
 import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.Rify
+import Mathlib.Data.NNReal.Basic
 
 set_option linter.unusedVariables false
 
@@ -36,3 +37,34 @@ example {n k : ℕ} (h₁ : 8 ≤ n) (h₂ : 2 * k > n) (h₃ : k + 1 < n) :
   have f₂ : n - (k + 1) ≤ n := by rify [f₁]; linarith
   rify [f₁, f₂] at *
   linarith
+
+/- ℝ≥0 Tests -/
+
+open NNReal
+
+example {a : ℝ≥0} {b : ℝ} (ha : 8 ≤ a) (hb : 2 * b ≤ a + 2) :
+    (0 : ℝ) < a - b - 1 := by
+  rify at ha hb
+  linarith
+
+example {a : ℝ≥0} {b : ℝ} (ha : 8 ≤ a) (hb : (2 : ℚ) * b ≤ b + 2) :
+    (0 : ℝ) < a - b - 1 := by
+  rify at ha hb
+  linarith
+
+example (a b c : ℝ≥0) (h : a - b < c) (hab : b ≤ a) : a < b + c := by
+  rify [hab] at h ⊢
+  linarith
+
+example {a : ℝ≥0} (h : 8 ≤ a) : (0 : ℝ) < a - 1 := by
+  rify at h
+  linarith
+
+example {a b : ℝ≥0} (h : 2 * b ≤ a + 2) (h' : 8 ≤ a) : (0 : ℝ) ≤ 3 * a - 4 - 4 * b := by
+  rify at *
+  linarith
+
+example {a b : ℝ≥0} (h₁ : 8 ≤ a) (h₂ : 2 * b > a) (h₃ : b + 1 < a) :
+    a - (b + 1) + 3 ≤ a := by
+  rify [h₃] at *
+  linarith