feat: assorted positivity extensions (#3907)

Positivity extensions for `NonnegHomClass` (this includes `AbsoluteValue` and `Seminorm`), `IsAbsoluteValue`, norm, the `NNReal`-to-`Real` coercion, factorials, square roots, distance (in a metric space), and diameter.

I tried to do these "properly" using Qq but I hit various errors I couldn't fix -- see 
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Qq.20doesn't.20know.20that.20two.20things.20have.20the.20same.20type
for some examples.

cc @dwrensha 



Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>

Author: hrmacbeth

Mathlib/Algebra/Order/AbsoluteValue.lean

@@ -308,6 +308,14 @@ variable {R : Type _} [Semiring R] (abv : R → S) [IsAbsoluteValue abv]
 lemma abv_nonneg (x) : 0 ≤ abv x := abv_nonneg' x
 #align is_absolute_value.abv_nonneg IsAbsoluteValue.abv_nonneg
 
+open Lean Meta Mathlib Meta Positivity Qq in
+/-- The `positivity` extension which identifies expressions of the form `abv a`. -/
+@[positivity (_ : α)]
+def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα _pα e := do
+  let (.app f a) ← whnfR e | throwError "not abv ·"
+  let pa' ← mkAppM ``abv_nonneg #[f, a]
+  pure (.nonnegative pa')
+
 lemma abv_eq_zero {x} : abv x = 0 ↔ x = 0 := abv_eq_zero'
 #align is_absolute_value.abv_eq_zero IsAbsoluteValue.abv_eq_zero
 

Mathlib/Algebra/Order/Hom/Basic.lean

@@ -10,6 +10,7 @@ Authors: Yaël Dillies
 -/
 
 import Mathlib.Algebra.GroupPower.Order
+import Mathlib.Tactic.Positivity.Basic
 
 /-!
 # Algebraic order homomorphism classes
@@ -154,17 +155,19 @@ theorem le_map_div_add_map_div [Group α] [AddCommSemigroup β] [LE β] [MulLEAd
 #align le_map_div_add_map_div le_map_div_add_map_div
 -- #align le_map_sub_add_map_sub le_map_sub_add_map_sub -- Porting note: TODO: `to_additive` clashes
 
---namespace Mathlib.Meta.Positivity
+namespace Mathlib.Meta.Positivity
 
---Porting note: tactic extension commented as decided in the weekly porting meeting
--- /-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
--- @[positivity _ _]
--- unsafe def positivity_map : expr → tactic strictness
---   | expr.app (quote.1 ⇑(%%f)) (quote.1 (%%ₓa)) => nonnegative <$> mk_app `` map_nonneg [f, a]
---   | _ => failed
--- #align tactic.positivity_map tactic.positivity_map
+open Lean Meta Qq Function
 
---end Mathlib.Meta.Positivity
+/-- Extension for the `positivity` tactic: nonnegative maps take nonnegative values. -/
+@[positivity FunLike.coe _ _]
+def evalMap : PositivityExt where eval {_ β} _ _ e := do
+  let .app (.app _ f) a ← whnfR e
+    | throwError "not ↑f · where f is of NonnegHomClass"
+  let pa ← mkAppOptM ``map_nonneg #[none, none, β, none, none, none, f, a]
+  pure (.nonnegative pa)
+
+end Mathlib.Meta.Positivity
 
 /-! ### Group (semi)norms -/
 

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -344,8 +344,6 @@ theorem WithSeminorms.T1_of_separating (hp : WithSeminorms p)
   rw [← isOpen_compl_iff, hp.isOpen_iff_mem_balls]
   rintro x (hx : x ≠ 0)
   cases' h x hx with i pi_nonzero
-  -- Porting note: the following line shouldn't be needed, but otherwise `positivity` fails later
-  have : p i x ≥ 0 := map_nonneg _ _
   refine' ⟨{i}, p i x, by positivity, subset_compl_singleton_iff.mpr _⟩
   rw [Finset.sup_singleton, mem_ball, zero_sub, map_neg_eq_map, not_lt]
 #align with_seminorms.t1_of_separating WithSeminorms.T1_of_separating

Mathlib/Analysis/Normed/Group/Basic.lean

@@ -490,21 +490,26 @@ theorem norm_nonneg' (a : E) : 0 ≤ ‖a‖ := by
 #align norm_nonneg' norm_nonneg'
 #align norm_nonneg norm_nonneg
 
-/- porting note: meta code, do not port
-section
-
-open Tactic Tactic.Positivity
-
-/-- Extension for the `positivity` tactic: norms are nonnegative. -/
-@[positivity]
-unsafe def _root_.tactic.positivity_norm : expr → tactic strictness
-  | q(‖$(a)‖) =>
-    nonnegative <$> mk_app `` norm_nonneg [a] <|> nonnegative <$> mk_app `` norm_nonneg' [a]
-  | _ => failed
-#align tactic.positivity_norm tactic.positivity_norm
-
-end
--/
+namespace Mathlib.Meta.Positivity
+
+open Lean Meta Qq Function
+
+/-- Extension for the `positivity` tactic: multiplicative norms are nonnegative, via
+`norm_nonneg'`. -/
+@[positivity Norm.norm _]
+def evalMulNorm : PositivityExt where eval {_ _} _zα _pα e := do
+  let .app _ a ← whnfR e | throwError "not ‖ ⬝ ‖"
+  let p ← mkAppM ``norm_nonneg' #[a]
+  pure (.nonnegative p)
+
+/-- Extension for the `positivity` tactic: additive norms are nonnegative, via `norm_nonneg`. -/
+@[positivity Norm.norm _]
+def evalAddNorm : PositivityExt where eval {_ _} _zα _pα e := do
+  let .app _ a ← whnfR e | throwError "not ‖ ⬝ ‖"
+  let p ← mkAppM ``norm_nonneg #[a]
+  pure (.nonnegative p)
+
+end Mathlib.Meta.Positivity
 
 @[to_additive (attr := simp) norm_zero]
 theorem norm_one' : ‖(1 : E)‖ = 0 := by rw [← dist_one_right, dist_self]

Mathlib/Analysis/Normed/Group/Seminorm.lean

@@ -398,7 +398,7 @@ theorem mul_bddBelow_range_add {p q : GroupSeminorm E} {x : E} :
   ⟨0, by
     rintro _ ⟨x, rfl⟩
     dsimp
-    exact add_nonneg (map_nonneg _ _) (map_nonneg _ _)⟩ -- porting note: was `positivity`
+    positivity⟩
 #align group_seminorm.mul_bdd_below_range_add GroupSeminorm.mul_bddBelow_range_add
 #align add_group_seminorm.add_bdd_below_range_add AddGroupSeminorm.add_bddBelow_range_add
 
@@ -608,8 +608,7 @@ theorem add_bddBelow_range_add {p q : NonarchAddGroupSeminorm E} {x : E} :
   ⟨0, by
     rintro _ ⟨x, rfl⟩
     dsimp
-    exact add_nonneg (map_nonneg _ _) (map_nonneg _ _)⟩
-    -- porting note: was `positivity`
+    positivity⟩
 #align nonarch_add_group_seminorm.add_bdd_below_range_add NonarchAddGroupSeminorm.add_bddBelow_range_add
 
 end AddCommGroup

Mathlib/Analysis/Seminorm.lean

@@ -460,8 +460,7 @@ variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {p q : Seminorm 
 theorem bddBelow_range_add : BddBelow (range fun u => p u + q (x - u)) :=
   ⟨0, by
     rintro _ ⟨x, rfl⟩
-    -- Porting note: the following was previously `dsimp; positivity`
-    exact add_nonneg (map_nonneg _ _) (map_nonneg _ _)⟩
+    dsimp ; positivity⟩
 #align seminorm.bdd_below_range_add Seminorm.bddBelow_range_add
 
 noncomputable instance instInf : Inf (Seminorm 𝕜 E) where

Mathlib/Data/Real/NNReal.lean

@@ -1072,27 +1072,23 @@ theorem cast_natAbs_eq_nnabs_cast (n : ℤ) : (n.natAbs : ℝ≥0) = nnabs n :=
 
 end Real
 
-/-
-namespace Tactic
+namespace Mathlib.Meta.Positivity
 
-open Positivity
+open Lean Meta Qq Function
 
 private theorem nnreal_coe_pos {r : ℝ≥0} : 0 < r → 0 < (r : ℝ) :=
   NNReal.coe_pos.2
-#align tactic.nnreal_coe_pos tactic.nnreal_coe_pos
 
 /-- Extension for the `positivity` tactic: cast from `ℝ≥0` to `ℝ`. -/
-@[positivity]
-unsafe def positivity_coe_nnreal_real : expr → tactic strictness
-  | q(@coe _ _ $(inst) $(a)) => do
-    unify inst q(@coeToLift _ _ <| @coeBase _ _ NNReal.Real.hasCoe)
-    let strictness_a ← core a
-    match strictness_a with
-      | positive p => positive <$> mk_app `` nnreal_coe_pos [p]
-      | _ => nonnegative <$> mk_app `` NNReal.coe_nonneg [a]
-  | e =>
-    pp e >>= fail ∘ format.bracket "The expression " " is not of the form `(r : ℝ)` for `r : ℝ≥0`"
-#align tactic.positivity_coe_nnreal_real tactic.positivity_coe_nnreal_real
-
-end Tactic
--/
+@[positivity NNReal.toReal _]
+def evalNNRealtoReal : PositivityExt where eval {_ _} _zα _pα e := do
+  let (.app _ (a : Q(NNReal))) ← whnfR e | throwError "not NNReal.toReal"
+  let zα' ← synthInstanceQ (q(Zero NNReal) : Q(Type))
+  let pα' ← synthInstanceQ (q(PartialOrder NNReal) : Q(Type))
+  let ra ← core zα' pα' a
+  assertInstancesCommute
+  match ra with
+  | .positive pa => pure (.positive (q(nnreal_coe_pos $pa) : Expr))
+  | _ => pure (.nonnegative (q(NNReal.coe_nonneg $a) : Expr))
+
+end Mathlib.Meta.Positivity

Mathlib/Data/Real/Sqrt.lean

@@ -124,6 +124,10 @@ theorem sqrt_div (x y : ℝ≥0) : sqrt (x / y) = sqrt x / sqrt y :=
 theorem continuous_sqrt : Continuous sqrt := sqrt.continuous
 #align nnreal.continuous_sqrt NNReal.continuous_sqrt
 
+@[simp] theorem sqrt_pos : 0 < sqrt x ↔ 0 < x := by simp [pos_iff_ne_zero]
+
+alias sqrt_pos ↔ _ sqrt_pos_of_pos
+
 end NNReal
 
 namespace Real
@@ -350,29 +354,41 @@ theorem sqrt_pos : 0 < sqrt x ↔ 0 < x :=
 alias sqrt_pos ↔ _ sqrt_pos_of_pos
 #align real.sqrt_pos_of_pos Real.sqrt_pos_of_pos
 
-/-
-section
+end Real
 
-Porting note: todo: restore positivity plugin
-open Tactic Tactic.Positivity
+namespace Mathlib.Meta.Positivity
+
+open Lean Meta Qq Function
+
+/-- Extension for the `positivity` tactic: a square root of a strictly positive nonnegative real is
+positive. -/
+@[positivity NNReal.sqrt _]
+def evalNNRealSqrt : PositivityExt where eval {_ _} _zα _pα e := do
+  let (.app _ (a : Q(NNReal))) ← whnfR e | throwError "not NNReal.sqrt"
+  let zα' ← synthInstanceQ (q(Zero NNReal) : Q(Type))
+  let pα' ← synthInstanceQ (q(PartialOrder NNReal) : Q(Type))
+  let ra ← core zα' pα' a
+  assertInstancesCommute
+  match ra with
+  | .positive pa => pure (.positive (q(NNReal.sqrt_pos_of_pos $pa) : Expr))
+  | _ => failure -- this case is dealt with by generic nonnegativity of nnreals
 
 /-- Extension for the `positivity` tactic: a square root is nonnegative, and is strictly positive if
 its input is. -/
-@[positivity]
-unsafe def _root_.tactic.positivity_sqrt : expr → tactic strictness
-  | q(Real.sqrt $(a)) => do
-    (-- if can prove `0 < a`, report positivity
-        do
-          let positive pa ← core a
-          positive <$> mk_app `` sqrt_pos_of_pos [pa]) <|>
-        nonnegative <$> mk_app `` sqrt_nonneg [a]
-  |-- else report nonnegativity
-    _ =>
-    failed
-#align tactic.positivity_sqrt tactic.positivity_sqrt
-
-end
--/
+@[positivity Real.sqrt _]
+def evalSqrt : PositivityExt where eval {_ _} _zα _pα e := do
+  let (.app _ (a : Q(Real))) ← whnfR e | throwError "not Real.sqrt"
+  let zα' ← synthInstanceQ (q(Zero Real) : Q(Type))
+  let pα' ← synthInstanceQ (q(PartialOrder Real) : Q(Type))
+  let ra ← core zα' pα' a
+  assertInstancesCommute
+  match ra with
+  | .positive pa => pure (.positive (q(Real.sqrt_pos_of_pos $pa) : Expr))
+  | _ => pure (.nonnegative (q(Real.sqrt_nonneg $a) : Expr))
+
+end Mathlib.Meta.Positivity
+
+namespace Real
 
 @[simp]
 theorem sqrt_mul (hx : 0 ≤ x) (y : ℝ) : sqrt (x * y) = sqrt x * sqrt y := by

Mathlib/Tactic/Positivity/Basic.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Heather Macbeth, Yaël Dillies
 -/
 import Std.Lean.Parser
 import Mathlib.Data.Int.Order.Basic
+import Mathlib.Data.Nat.Factorial.Basic
 import Mathlib.Tactic.Positivity.Core
 import Mathlib.Algebra.GroupPower.Order
 import Mathlib.Algebra.Order.Field.Basic
@@ -392,3 +393,9 @@ def evalIntCast : PositivityExt where eval {u α} _zα _pα e := do
 def evalNatSucc : PositivityExt where eval {_u _α} _zα _pα e := do
   let (.app _ (a : Q(Nat))) ← withReducible (whnf e) | throwError "not Nat.succ"
   pure (.positive (q(Nat.succ_pos $a) : Expr))
+
+/-- Extension for Nat.factorial. -/
+@[positivity Nat.factorial _]
+def evalFactorial: PositivityExt where eval {_ _} _ _ e := do
+  let .app _ (a : Q(Nat)) ← whnfR e | throwError "not Nat.factorial"
+  pure (.positive (q(Nat.factorial_pos $a) : Expr))

Mathlib/Topology/MetricSpace/Basic.lean

@@ -274,21 +274,20 @@ theorem dist_nonneg {x y : α} : 0 ≤ dist x y :=
   dist_nonneg' dist dist_self dist_comm dist_triangle
 #align dist_nonneg dist_nonneg
 
-/-
-section
+namespace Mathlib.Meta.Positivity
 
-open Tactic Tactic.Positivity
--- porting note: todo: restore `positivity` plugin
+open Lean Meta Qq Function
 
 /-- Extension for the `positivity` tactic: distances are nonnegative. -/
-@[positivity]
-unsafe def _root_.tactic.positivity_dist : expr → tactic strictness
-  | q(dist $(a) $(b)) => nonnegative <$> mk_app `` dist_nonneg [a, b]
-  | _ => failed
-#align tactic.positivity_dist tactic.positivity_dist
+@[positivity Dist.dist _ _]
+def evalDist : PositivityExt where eval {_ _} _zα _pα e := do
+  let .app (.app _ a) b ← whnfR e | throwError "not dist"
+  let p ← mkAppOptM ``dist_nonneg #[none, none, a, b]
+  pure (.nonnegative p)
 
-end
--/
+end Mathlib.Meta.Positivity
+
+example {x y : α} : 0 ≤ dist x y := by positivity
 
 @[simp] theorem abs_dist {a b : α} : |dist a b| = dist a b := abs_of_nonneg dist_nonneg
 #align abs_dist abs_dist
@@ -2777,21 +2776,18 @@ theorem exists_local_min_mem_ball [ProperSpace α] [TopologicalSpace β]
 
 end Metric
 
-/-
-Porting note: restore positivity extension
-namespace Tactic
+namespace Mathlib.Meta.Positivity
 
-open Positivity
+open Lean Meta Qq Function
 
 /-- Extension for the `positivity` tactic: the diameter of a set is always nonnegative. -/
-@[positivity]
-unsafe def positivity_diam : expr → tactic strictness
-  | q(Metric.diam $(s)) => nonnegative <$> mk_app `` Metric.diam_nonneg [s]
-  | e => pp e >>= fail ∘ format.bracket "The expression " " is not of the form `metric.diam s`"
-#align tactic.positivity_diam tactic.positivity_diam
+@[positivity Metric.diam _]
+def evalDiam : PositivityExt where eval {_ _} _zα _pα e := do
+  let .app _ s ← whnfR e | throwError "not Metric.diam"
+  let p ← mkAppOptM ``Metric.diam_nonneg #[none, none, s]
+  pure (.nonnegative p)
 
-end Tactic
--/
+end Mathlib.Meta.Positivity
 
 theorem comap_dist_right_atTop_le_cocompact (x : α) :
     comap (fun y => dist y x) atTop ≤ cocompact α := by