feat(tactic/positivity): a tactic for proving positivity/nonnegativity (

#15618)

This is a new tactic, `positivity`, which solves goals of the form `0 ≤ x` and `0 < x`.  The tactic works
recursively according to the syntax of the expression `x`. 

Co-authored-by: Mario Carneiro <di.gama@gmail.com>

src/algebra/order/field.lean

@@ -101,9 +101,13 @@ suffices ∀ a : α, 0 < a → 0 < a⁻¹,
 from ⟨λ h, inv_inv a ▸ this _ h, this a⟩,
 assume a ha, flip lt_of_mul_lt_mul_left ha.le $ by simp [ne_of_gt ha, zero_lt_one]
 
+alias inv_pos ↔ _ inv_pos_of_pos
+
 @[simp] lemma inv_nonneg : 0 ≤ a⁻¹ ↔ 0 ≤ a :=
 by simp only [le_iff_eq_or_lt, inv_pos, zero_eq_inv]
 
+alias inv_nonneg ↔ _ inv_nonneg_of_nonneg
+
 @[simp] lemma inv_lt_zero : a⁻¹ < 0 ↔ a < 0 :=
 by simp only [← not_le, inv_nonneg]
 

src/analysis/normed/group/basic.lean

@@ -216,6 +216,17 @@ by simpa only [dist_add_left, dist_add_right, dist_comm h₂]
 @[simp] lemma norm_nonneg (g : E) : 0 ≤ ∥g∥ :=
 by { rw[←dist_zero_right], exact dist_nonneg }
 
+section
+open tactic tactic.positivity
+
+/-- Extension for the `positivity` tactic: norms are nonnegative. -/
+@[positivity]
+meta def _root_.tactic.positivity_norm : expr → tactic strictness
+| `(∥%%a∥) := nonnegative <$> mk_app ``norm_nonneg [a]
+| _ := failed
+
+end
+
 @[simp] lemma norm_zero : ∥(0 : E)∥ = 0 :=  by rw [← dist_zero_right, dist_self]
 
 lemma ne_zero_of_norm_ne_zero {g : E} : ∥g∥ ≠ 0 → g ≠ 0 := mt $ by { rintro rfl, exact norm_zero }

src/data/real/sqrt.lean

@@ -5,7 +5,7 @@ Authors: Mario Carneiro, Floris van Doorn, Yury Kudryashov
 -/
 import topology.algebra.order.monotone_continuity
 import topology.instances.nnreal
-import tactic.norm_cast
+import tactic.positivity
 
 /-!
 # Square root of a real number
@@ -272,6 +272,24 @@ by rw [← not_le, not_iff_not, sqrt_eq_zero']
 lt_iff_lt_of_le_iff_le (iff.trans
   (by simp [le_antisymm_iff, sqrt_nonneg]) sqrt_eq_zero')
 
+alias sqrt_pos ↔ _ sqrt_pos_of_pos
+
+section
+open tactic tactic.positivity
+
+/-- Extension for the `positivity` tactic: a square root is nonnegative, and is strictly positive if
+its input is. -/
+@[positivity]
+meta def _root_.tactic.positivity_sqrt : expr → tactic strictness
+| `(real.sqrt %%a) := do
+  (do -- if can prove `0 < a`, report positivity
+    positive pa ← core a,
+    positive <$> mk_app ``sqrt_pos_of_pos [pa]) <|>
+  nonnegative <$> mk_app ``sqrt_nonneg [a] -- else report nonnegativity
+| _ := failed
+
+end
+
 @[simp] theorem sqrt_mul (hx : 0 ≤ x) (y : ℝ) : sqrt (x * y) = sqrt x * sqrt y :=
 by simp_rw [sqrt, ← nnreal.coe_mul, nnreal.coe_eq, real.to_nnreal_mul hx, nnreal.sqrt_mul]