feat(tactic/positivity): Extension for coe (#16141)

Add:
* a case in the main `positivity` tactic to show that `0 ≤ a` in a `canonically_ordered_add_monoid`
* `positivity_coe`, an  extension to `positivity`, to turn `0 ≤ a`/`0 < a` into `0 ≤ ↑a`/`0 < ↑a` when `a` is of type `ℕ`, `ℤ`, `ℚ`.

src/data/real/ennreal.lean

@@ -211,7 +211,7 @@ lemma coe_mono : monotone (coe : ℝ≥0 → ℝ≥0∞) := λ _ _, coe_le_coe.2
 @[simp, norm_cast] lemma zero_eq_coe : 0 = (↑r : ℝ≥0∞) ↔ 0 = r := coe_eq_coe
 @[simp, norm_cast] lemma coe_eq_one : (↑r : ℝ≥0∞) = 1 ↔ r = 1 := coe_eq_coe
 @[simp, norm_cast] lemma one_eq_coe : 1 = (↑r : ℝ≥0∞) ↔ 1 = r := coe_eq_coe
-@[simp, norm_cast] lemma coe_nonneg : 0 ≤ (↑r : ℝ≥0∞) ↔ 0 ≤ r := coe_le_coe
+@[simp] lemma coe_nonneg : 0 ≤ (↑r : ℝ≥0∞) := coe_le_coe.2 $ zero_le _
 @[simp, norm_cast] lemma coe_pos : 0 < (↑r : ℝ≥0∞) ↔ 0 < r := coe_lt_coe
 lemma coe_ne_zero : (r : ℝ≥0∞) ≠ 0 ↔ r ≠ 0 := not_congr coe_eq_coe
 
@@ -1931,3 +1931,20 @@ by simpa only [image_image] using h.image_real_to_nnreal.image_coe_nnreal_ennrea
 
 end ord_connected
 end set
+
+namespace tactic
+open positivity
+
+private lemma nnreal_coe_pos {r : ℝ≥0} : 0 < r → 0 < (r : ℝ≥0∞) := ennreal.coe_pos.2
+
+/-- Extension for the `positivity` tactic: cast from `ℝ≥0` to `ℝ≥0∞`. -/
+@[positivity]
+meta def positivity_coe_nnreal_ennreal : expr → tactic strictness
+| `(@coe _ _ %%inst %%a) := do
+  unify inst `(@coe_to_lift _ _ $ @coe_base _ _ ennreal.has_coe),
+  positive p ← core a, -- We already know `0 ≤ r` for all `r : ℝ≥0∞`
+  positive <$> mk_app ``nnreal_coe_pos [p]
+| e := pp e >>= fail ∘ format.bracket "The expression "
+         " is not of the form `(r : ℝ≥0∞)` for `r : ℝ≥0`"
+
+end tactic

src/data/real/ereal.lean

@@ -154,7 +154,19 @@ by { apply with_top.coe_lt_coe.2, exact with_bot.bot_lt_coe _ }
 @[simp, norm_cast] lemma coe_add (x y : ℝ) : ((x + y : ℝ) : ereal) = (x : ereal) + (y : ereal) :=
 rfl
 
-@[simp] lemma coe_zero : ((0 : ℝ) : ereal) = 0 := rfl
+@[simp, norm_cast] lemma coe_zero : ((0 : ℝ) : ereal) = 0 := rfl
+
+@[simp, norm_cast] protected lemma coe_nonneg {x : ℝ} : (0 : ereal) ≤ x ↔ 0 ≤ x :=
+ereal.coe_le_coe_iff
+
+@[simp, norm_cast] protected lemma coe_nonpos {x : ℝ} : (x : ereal) ≤ 0 ↔ x ≤ 0 :=
+ereal.coe_le_coe_iff
+
+@[simp, norm_cast] protected lemma coe_pos {x : ℝ} : (0 : ereal) < x ↔ 0 < x :=
+ereal.coe_lt_coe_iff
+
+@[simp, norm_cast] protected lemma coe_neg' {x : ℝ} : (x : ereal) < 0 ↔ x < 0 :=
+ereal.coe_lt_coe_iff
 
 lemma to_real_le_to_real {x y : ereal} (h : x ≤ y) (hx : x ≠ ⊥) (hy : y ≠ ⊤) :
   x.to_real ≤ y.to_real :=
@@ -214,7 +226,8 @@ end
 
 lemma coe_nnreal_eq_coe_real (x : ℝ≥0) : ((x : ℝ≥0∞) : ereal) = (x : ℝ) := rfl
 
-@[simp] lemma coe_ennreal_top : ((⊤ : ℝ≥0∞) : ereal) = ⊤ := rfl
+@[simp, norm_cast] lemma coe_ennreal_zero : ((0 : ℝ≥0∞) : ereal) = 0 := rfl
+@[simp, norm_cast] lemma coe_ennreal_top : ((⊤ : ℝ≥0∞) : ereal) = ⊤ := rfl
 
 @[simp] lemma coe_ennreal_eq_top_iff : ∀ {x : ℝ≥0∞}, (x : ereal) = ⊤ ↔ x = ⊤
 | ⊤ := by simp
@@ -247,6 +260,9 @@ lemma coe_nnreal_ne_top (x : ℝ≥0) : ((x : ℝ≥0∞) : ereal) ≠ ⊤ := de
 lemma coe_ennreal_nonneg (x : ℝ≥0∞) : (0 : ereal) ≤ x :=
 coe_ennreal_le_coe_ennreal_iff.2 (zero_le x)
 
+@[simp, norm_cast] lemma coe_ennreal_pos {x : ℝ≥0∞} : (0 : ereal) < x ↔ 0 < x :=
+by rw [←coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]
+
 @[simp] lemma bot_lt_coe_ennreal (x : ℝ≥0∞) : (⊥ : ereal) < x :=
 (bot_lt_coe 0).trans_le (coe_ennreal_nonneg _)
 
@@ -257,8 +273,6 @@ coe_ennreal_le_coe_ennreal_iff.2 (zero_le x)
 | x ⊤ := by simp
 | (some x) (some y) := rfl
 
-@[simp] lemma coe_ennreal_zero : ((0 : ℝ≥0∞) : ereal) = 0 := rfl
-
 
 /-! ### Order -/
 
@@ -514,3 +528,38 @@ lemma to_real_mul : ∀ {x y : ereal}, to_real (x * y) = to_real x * to_real y
 | ⊥ ⊥ := by simp
 
 end ereal
+
+namespace tactic
+open positivity
+
+private lemma ereal_coe_nonneg {r : ℝ} : 0 ≤ r → 0 ≤ (r : ereal) := ereal.coe_nonneg.2
+private lemma ereal_coe_pos {r : ℝ} : 0 < r → 0 < (r : ereal) := ereal.coe_pos.2
+private lemma ereal_coe_ennreal_pos {r : ℝ≥0∞} : 0 < r → 0 < (r : ereal) := ereal.coe_ennreal_pos.2
+
+/-- Extension for the `positivity` tactic: cast from `ℝ` to `ereal`. -/
+@[positivity]
+meta def positivity_coe_real_ereal : expr → tactic strictness
+| `(@coe _ _ %%inst %%a) := do
+  unify inst `(@coe_to_lift _ _ $ @coe_base _ _ ereal.has_coe),
+  strictness_a ← core a,
+  match strictness_a with
+  | positive p := positive <$> mk_app ``ereal_coe_pos [p]
+  | nonnegative p := nonnegative <$> mk_mapp ``ereal_coe_nonneg [a, p]
+  end
+| e := pp e >>= fail ∘ format.bracket "The expression "
+         " is not of the form `(r : ereal)` for `r : ℝ`"
+
+/-- Extension for the `positivity` tactic: cast from `ℝ≥0∞` to `ereal`. -/
+@[positivity]
+meta def positivity_coe_ennreal_ereal : expr → tactic strictness
+| `(@coe _ _ %%inst %%a) := do
+  unify inst `(@coe_to_lift _ _ $ @coe_base _ _ ereal.has_coe_ennreal),
+  strictness_a ← core a,
+  match strictness_a with
+  | positive p := positive <$> mk_app ``ereal_coe_ennreal_pos [p]
+  | nonnegative _ := nonnegative <$> mk_mapp `ereal.coe_ennreal_nonneg [a]
+  end
+| e := pp e >>= fail ∘ format.bracket "The expression "
+         " is not of the form `(r : ereal)` for `r : ℝ≥0∞`"
+
+end tactic

src/data/real/hyperreal.lean

@@ -42,9 +42,9 @@ germ.const_inj
 @[simp, norm_cast] lemma coe_sub (x y : ℝ) : ↑(x - y) = (x - y : ℝ*) := rfl
 
 @[simp, norm_cast] lemma coe_lt_coe {x y : ℝ} : (x : ℝ*) < y ↔ x < y := germ.const_lt
-@[simp, norm_cast] lemma coe_pos {x : ℝ} : 0 < (x : ℝ*) ↔ 0 < x :=
-coe_lt_coe
+@[simp, norm_cast] lemma coe_pos {x : ℝ} : 0 < (x : ℝ*) ↔ 0 < x := coe_lt_coe
 @[simp, norm_cast] lemma coe_le_coe {x y : ℝ} : (x : ℝ*) ≤ y ↔ x ≤ y := germ.const_le_iff
+@[simp, norm_cast] lemma coe_nonneg {x : ℝ} : 0 ≤ (x : ℝ*) ↔ 0 ≤ x := coe_le_coe
 @[simp, norm_cast] lemma coe_abs (x : ℝ) : ((|x| : ℝ) : ℝ*) = |x| :=
 begin
   convert const_abs x,
@@ -789,3 +789,23 @@ lemma infinite_mul_infinite {x y : ℝ*} : infinite x → infinite y → infinit
 λ hx hy, infinite_mul_of_infinite_not_infinitesimal hx (not_infinitesimal_of_infinite hy)
 
 end hyperreal
+
+namespace tactic
+open positivity
+
+private lemma hyperreal_coe_nonneg {r : ℝ} : 0 ≤ r → 0 ≤ (r : ℝ*) := hyperreal.coe_nonneg.2
+private lemma hyperreal_coe_pos {r : ℝ} : 0 < r → 0 < (r : ℝ*) := hyperreal.coe_pos.2
+
+/-- Extension for the `positivity` tactic: cast from `ℝ` to `ℝ*`. -/
+@[positivity]
+meta def positivity_coe_real_hyperreal : expr → tactic strictness
+| `(@coe _ _ %%inst %%a) := do
+  unify inst `(@coe_to_lift _ _ hyperreal.has_coe_t),
+  strictness_a ← core a,
+  match strictness_a with
+  | positive p := positive <$> mk_app ``hyperreal_coe_pos [p]
+  | nonnegative p := nonnegative <$> mk_app ``hyperreal_coe_nonneg [p]
+  end
+| e := pp e >>= fail ∘ format.bracket "The expression " " is not of the form `(r : ℝ*)` for `r : ℝ`"
+
+end tactic

src/data/real/nnreal.lean

@@ -3,12 +3,10 @@ Copyright (c) 2018 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-import algebra.big_operators.ring
-import data.real.pointwise
-import algebra.indicator_function
 import algebra.algebra.basic
-import algebra.order.module
 import algebra.order.nonneg
+import data.real.pointwise
+import tactic.positivity
 
 /-!
 # Nonnegative real numbers
@@ -840,3 +838,23 @@ lemma cast_nat_abs_eq_nnabs_cast (n : ℤ) :
 by { ext, rw [nnreal.coe_nat_cast, int.cast_nat_abs, real.coe_nnabs] }
 
 end real
+
+namespace tactic
+open positivity
+
+private lemma nnreal_coe_pos {r : ℝ≥0} : 0 < r → 0 < (r : ℝ) := nnreal.coe_pos.2
+
+/-- Extension for the `positivity` tactic: cast from `ℝ≥0` to `ℝ`. -/
+@[positivity]
+meta def positivity_coe_nnreal_real : expr → tactic strictness
+| `(@coe _ _ %%inst %%a) := do
+  unify inst `(@coe_to_lift _ _ $ @coe_base _ _ nnreal.real.has_coe),
+  strictness_a ← core a,
+  match strictness_a with
+  | positive p := positive <$> mk_app ``nnreal_coe_pos [p]
+  | nonnegative _ := nonnegative <$> mk_app ``nnreal.coe_nonneg [a]
+  end
+| e := pp e >>= fail ∘ format.bracket "The expression "
+         " is not of the form `(r : ℝ)` for `r : ℝ≥0`"
+
+end tactic

src/measure_theory/function/lp_space.lean

@@ -1816,8 +1816,8 @@ lemma snorm_ess_sup_indicator_const_le (s : set α) (c : G) :
   snorm_ess_sup (s.indicator (λ x : α , c)) μ ≤ ∥c∥₊ :=
 begin
   by_cases hμ0 : μ = 0,
-  { rw [hμ0, snorm_ess_sup_measure_zero, ennreal.coe_nonneg],
-    exact zero_le', },
+  { rw [hμ0, snorm_ess_sup_measure_zero],
+    exact ennreal.coe_nonneg },
   { exact (snorm_ess_sup_indicator_le s (λ x, c)).trans (snorm_ess_sup_const c hμ0).le, },
 end
 

src/tactic/positivity.lean

@@ -49,9 +49,7 @@ introduce these operations.
 
 ## TODO
 
-Implement extensions for other operations (raising to non-numeral powers, `exp`, `log`, coercions
-from `ℕ` and `ℝ≥0`).
-
+Implement extensions for other operations (raising to non-numeral powers, `log`).
 -/
 
 namespace tactic
@@ -84,6 +82,11 @@ meta def norm_num.positivity (e : expr) : tactic strictness := do
     pure (nonnegative p')
   else failed
 
+/-- Second base case of the `positivity` tactic: Any element of a canonically ordered additive
+monoid is nonnegative. -/
+meta def positivity_canon : expr → tactic strictness
+| `(%%a) := nonnegative <$> mk_app ``zero_le [a]
+
 namespace positivity
 
 /-- Given two tactics whose result is `strictness`, report a `strictness`:
@@ -102,7 +105,7 @@ meta def orelse' (tac1 tac2 : tactic strictness) : tactic strictness := do
 
 /-! ### Core logic of the `positivity` tactic -/
 
-/-- Second base case of the `positivity` tactic.  Prove an expression `e` is positive/nonnegative by
+/-- Third base case of the `positivity` tactic.  Prove an expression `e` is positive/nonnegative by
 finding a hypothesis of the form `a < e` or `a ≤ e` in which `a` can be proved positive/nonnegative
 by `norm_num`. -/
 meta def compare_hyp (e p₂ : expr) : tactic strictness := do
@@ -140,9 +143,10 @@ meta def attr : user_attribute (expr → tactic strictness) unit :=
         (λ _, failed),
       pure $ λ e, orelse'
         (t e) $ orelse' -- run all the extensions on `e`
-          (norm_num.positivity e) $ -- directly try `norm_num` on `e`
-          -- loop over hypotheses and try to compare with `e`
-          local_context >>= list.foldl (λ tac h, orelse' tac (compare_hyp e h)) failed  },
+          (norm_num.positivity e) $ orelse' -- directly try `norm_num` on `e`
+            (positivity_canon e) $ -- try showing nonnegativity from canonicity of the order
+            -- loop over hypotheses and try to compare with `e`
+            local_context >>= list.foldl (λ tac h, orelse' tac (compare_hyp e h)) failed },
     dependencies := [] } }
 
 /-- Look for a proof of positivity/nonnegativity of an expression `e`; if found, return the proof
@@ -200,7 +204,7 @@ add_tactic_doc
 
 end interactive
 
-variables {R : Type*}
+variables {α R : Type*}
 
 /-! ### `positivity` extensions for particular arithmetic operations -/
 
@@ -390,4 +394,48 @@ meta def positivity_abs : expr → tactic strictness
   nonnegative <$> mk_app ``abs_nonneg [a] -- else report nonnegativity
 | _ := failed
 
+private lemma nat_cast_pos [ordered_semiring α] [nontrivial α] {n : ℕ} : 0 < n → 0 < (n : α) :=
+nat.cast_pos.2
+
+private lemma int_coe_nat_nonneg (n : ℕ) : 0 ≤ (n : ℤ) := n.cast_nonneg
+private lemma int_coe_nat_pos {n : ℕ} : 0 < n → 0 < (n : ℤ) := nat.cast_pos.2
+
+private lemma int_cast_nonneg [ordered_ring α] {n : ℤ} (hn : 0 ≤ n) : 0 ≤ (n : α) :=
+by { rw ←int.cast_zero, exact int.cast_mono hn }
+private lemma int_cast_pos [ordered_ring α] [nontrivial α] {n : ℤ} : 0 < n → 0 < (n : α) :=
+int.cast_pos.2
+
+private lemma rat_cast_nonneg [linear_ordered_field α] {q : ℚ} : 0 ≤ q → 0 ≤ (q : α) :=
+rat.cast_nonneg.2
+private lemma rat_cast_pos [linear_ordered_field α] {q : ℚ} : 0 < q → 0 < (q : α) := rat.cast_pos.2
+
+/-- Extension for the `positivity` tactic: casts from `ℕ`, `ℤ`, `ℚ`. -/
+@[positivity]
+meta def positivity_coe : expr → tactic strictness
+| `(@coe _ %%typ %%inst %%a) := do
+  -- TODO: Using `match` here might turn out too strict since we really want the instance to *unify*
+  -- with one of the instances below rather than being equal on the nose.
+  -- If this turns out to indeed be a problem, we should figure out the right way to pattern match
+  -- up to defeq rather than equality of expressions.
+  -- See also "Reflexive tactics for algebra, revisited" by Kazuhiko Sakaguchi at ITP 2022.
+  match inst with
+  | `(@coe_to_lift _ _ %%inst) := do
+    strictness_a ← core a,
+    match inst, strictness_a with -- `mk_mapp` is necessary in some places. Why?
+    | `(nat.cast_coe), positive p := positive <$> mk_app ``nat_cast_pos [p]
+    | `(nat.cast_coe), _ := nonnegative <$> mk_mapp ``nat.cast_nonneg [typ, none, a]
+    | `(int.cast_coe), positive p := positive <$> mk_mapp ``int_cast_pos [typ, none, none, none, p]
+    | `(int.cast_coe), nonnegative p := nonnegative <$>
+                                          mk_mapp ``int_cast_nonneg [typ, none, none, p]
+    | `(rat.cast_coe), positive p := positive <$> mk_mapp ``rat_cast_pos [typ, none, none, p]
+    | `(rat.cast_coe), nonnegative p := nonnegative <$>
+                                          mk_mapp ``rat_cast_nonneg [typ, none, none, p]
+    | `(@coe_base _ _ int.has_coe), positive p := positive <$> mk_app ``int_coe_nat_pos [p]
+    | `(@coe_base _ _ int.has_coe), _ := nonnegative <$> mk_app ``int_coe_nat_nonneg [a]
+    | _, _ := failed
+    end
+  | _  := failed
+  end
+| _ := failed
+
 end tactic

test/positivity.lean

@@ -1,6 +1,9 @@
 import algebra.order.smul
 import analysis.normed.group.basic
 import data.complex.exponential
+import data.rat.nnrat
+import data.real.ereal
+import data.real.hyperreal
 import data.real.sqrt
 import tactic.positivity
 
@@ -9,6 +12,8 @@ import tactic.positivity
 This tactic proves goals of the form `0 ≤ a` and `0 < a`.
 -/
 
+open_locale ennreal nnrat nnreal
+
 /- ## Numeric goals -/
 
 example : 0 ≤ 0 := by positivity
@@ -106,6 +111,37 @@ example {X : Type*} [metric_space X] (x y : X) : 0 ≤ dist x y := by positivity
 example {E : Type*} [add_group E] {p : add_group_seminorm E} {x : E} : 0 ≤ p x := by positivity
 example {E : Type*} [group E] {p : group_seminorm E} {x : E} : 0 ≤ p x := by positivity
 
+/- ### Canonical orders -/
+
+example {a : ℕ} : 0 ≤ a := by positivity
+example {a : ℚ≥0} : 0 ≤ a := by positivity
+example {a : ℝ≥0} : 0 ≤ a := by positivity
+example {a : ℝ≥0∞} : 0 ≤ a := by positivity
+
+/- ### Coercions -/
+
+example {a : ℕ} : (0 : ℤ) ≤ a := by positivity
+example {a : ℕ} (ha : 0 < a) : (0 : ℤ) < a := by positivity
+example {a : ℤ} (ha : 0 ≤ a) : (0 : ℚ) ≤ a := by positivity
+example {a : ℤ} (ha : 0 < a) : (0 : ℚ) < a := by positivity
+example {a : ℚ} (ha : 0 ≤ a) : (0 : ℝ) ≤ a := by positivity
+example {a : ℚ} (ha : 0 < a) : (0 : ℝ) < a := by positivity
+example {r : ℝ≥0} : (0 : ℝ) ≤ r := by positivity
+example {r : ℝ≥0} (hr : 0 < r) : (0 : ℝ) < r := by positivity
+example {r : ℝ≥0} (hr : 0 < r) : (0 : ℝ≥0∞) < r := by positivity
+-- example {r : ℝ≥0} : (0 : ereal) ≤ r := by positivity -- TODO: Handle `coe_trans`
+-- example {r : ℝ≥0} (hr : 0 < r) : (0 : ereal) < r := by positivity
+example {r : ℝ} (hr : 0 ≤ r) : (0 : ereal) ≤ r := by positivity
+example {r : ℝ} (hr : 0 < r) : (0 : ereal) < r := by positivity
+example {r : ℝ} (hr : 0 ≤ r) : (0 : hyperreal) ≤ r := by positivity
+example {r : ℝ} (hr : 0 < r) : (0 : hyperreal) < r := by positivity
+example {r : ℝ≥0∞} : (0 : ereal) ≤ r := by positivity
+example {r : ℝ≥0∞} (hr : 0 < r) : (0 : ereal) < r := by positivity
+
+example {α : Type*} [ordered_ring α] {n : ℤ} : 0 ≤ ((n ^ 2 : ℤ) : α) := by positivity
+example {r : ℝ≥0} : 0 ≤ ((r : ℝ) : ereal) := by positivity
+example {r : ℝ≥0} : 0 < ((r + 1 : ℝ) : ereal) := by positivity
+
 /- ## Tests that the tactic is agnostic on reversed inequalities -/
 
 example {a : ℤ} (ha : a > 0) : 0 ≤ a := by positivity