From e339d96dc9f7cb532934275e6545aaf8b6342e53 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 22 Sep 2022 21:26:30 +0000 Subject: [PATCH] feat(analysis/special_functions/pow, set_theory/*): `positivity` extension for powers (#16462) Add the following `positivity` extensions to handle powers: * `positivity_rpow` for real powers * `positivity_opow` for ordinal powers * `positivity_cardinal_pow` for cardinal powers --- src/analysis/special_functions/pow.lean | 56 +++++++++++++++++++++++++ src/set_theory/cardinal/basic.lean | 19 +++++++++ src/set_theory/ordinal/arithmetic.lean | 17 ++++++++ src/tactic/positivity.lean | 51 +++++++++++++++------- test/positivity.lean | 29 +++++++++++-- 5 files changed, 153 insertions(+), 19 deletions(-) diff --git a/src/analysis/special_functions/pow.lean b/src/analysis/special_functions/pow.lean index 4ee23bb0f116e..2302dbe222696 100644 --- a/src/analysis/special_functions/pow.lean +++ b/src/analysis/special_functions/pow.lean @@ -2103,3 +2103,59 @@ prove_rpow' ``ennrpow_pos ``ennrpow_neg ``ennreal.rpow_zero `(ℝ≥0∞) `(ℝ) | _ := tactic.failed end norm_num + +namespace tactic +namespace positivity + +/-- Auxiliary definition for the `positivity` tactic to handle real powers of reals. -/ +meta def prove_rpow (a b : expr) : tactic strictness := +do + strictness_a ← core a, + match strictness_a with + | nonnegative p := nonnegative <$> mk_app ``real.rpow_nonneg_of_nonneg [p, b] + | positive p := positive <$> mk_app ``real.rpow_pos_of_pos [p, b] + end + +private lemma nnrpow_pos {a : ℝ≥0} (ha : 0 < a) (b : ℝ) : 0 < a ^ b := nnreal.rpow_pos ha + +/-- Auxiliary definition for the `positivity` tactic to handle real powers of nonnegative reals. -/ +meta def prove_nnrpow (a b : expr) : tactic strictness := +do + strictness_a ← core a, + match strictness_a with + | positive p := positive <$> mk_app ``nnrpow_pos [p, b] + | _ := failed -- We already know `0 ≤ x` for all `x : ℝ≥0` + end + +private lemma ennrpow_pos {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < a ^ b := +ennreal.rpow_pos_of_nonneg ha hb.le + +/-- Auxiliary definition for the `positivity` tactic to handle real powers of extended nonnegative +reals. -/ +meta def prove_ennrpow (a b : expr) : tactic strictness := +do + strictness_a ← core a, + strictness_b ← core b, + match strictness_a, strictness_b with + | positive pa, positive pb := positive <$> mk_app ``ennrpow_pos [pa, pb] + | positive pa, nonnegative pb := positive <$> mk_app ``ennreal.rpow_pos_of_nonneg [pa, pb] + | _, _ := failed -- We already know `0 ≤ x` for all `x : ℝ≥0∞` + end + +end positivity + +open positivity + +/-- Extension for the `positivity` tactic: exponentiation by a real number is nonnegative when the +base is nonnegative and positive when the base is positive. -/ +@[positivity] +meta def positivity_rpow : expr → tactic strictness +| `(@has_pow.pow _ _ real.has_pow %%a %%b) := prove_rpow a b +| `(real.rpow %%a %%b) := prove_rpow a b +| `(@has_pow.pow _ _ nnreal.real.has_pow %%a %%b) := prove_nnrpow a b +| `(nnreal.rpow %%a %%b) := prove_nnrpow a b +| `(@has_pow.pow _ _ ennreal.real.has_pow %%a %%b) := prove_ennrpow a b +| `(ennreal.rpow %%a %%b) := prove_ennrpow a b +| _ := failed + +end tactic diff --git a/src/set_theory/cardinal/basic.lean b/src/set_theory/cardinal/basic.lean index e7b7eefa30b7c..6585a0ed2a0f7 100644 --- a/src/set_theory/cardinal/basic.lean +++ b/src/set_theory/cardinal/basic.lean @@ -11,6 +11,7 @@ import logic.small import order.conditionally_complete_lattice import order.succ_pred.basic import set_theory.cardinal.schroeder_bernstein +import tactic.positivity /-! # Cardinal Numbers @@ -518,6 +519,8 @@ end theorem power_le_power_right {a b c : cardinal} : a ≤ b → a ^ c ≤ b ^ c := induction_on₃ a b c $ λ α β γ ⟨e⟩, ⟨embedding.arrow_congr_right e⟩ +theorem power_pos {a : cardinal} (b) (ha : 0 < a) : 0 < a ^ b := (power_ne_zero _ ha.ne').bot_lt + end order_properties protected theorem lt_wf : @well_founded cardinal.{u} (<) := @@ -1580,3 +1583,19 @@ begin end end cardinal + +namespace tactic +open cardinal positivity + +/-- Extension for the `positivity` tactic: The cardinal power of a positive cardinal is positive. -/ +@[positivity] +meta def positivity_cardinal_pow : expr → tactic strictness +| `(@has_pow.pow _ _ %%inst %%a %%b) := do + strictness_a ← core a, + match strictness_a with + | positive p := positive <$> mk_app ``power_pos [b, p] + | _ := failed -- We already know that `0 ≤ x` for all `x : cardinal` + end +| _ := failed + +end tactic diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean index 4a49974afe067..cde5a7d017013 100644 --- a/src/set_theory/ordinal/arithmetic.lean +++ b/src/set_theory/ordinal/arithmetic.lean @@ -2363,3 +2363,20 @@ begin end end ordinal + +namespace tactic +open ordinal positivity + +/-- Extension for the `positivity` tactic: `ordinal.opow` takes positive values on positive inputs. +-/ +@[positivity] +meta def positivity_opow : expr → tactic strictness +| `(@has_pow.pow _ _ %%inst %%a %%b) := do + strictness_a ← core a, + match strictness_a with + | positive p := positive <$> mk_app ``opow_pos [b, p] + | _ := failed -- We already know that `0 ≤ x` for all `x : ordinal` + end +| _ := failed + +end tactic diff --git a/src/tactic/positivity.lean b/src/tactic/positivity.lean index 7bc39befbdf9e..1827ade0ca6de 100644 --- a/src/tactic/positivity.lean +++ b/src/tactic/positivity.lean @@ -358,29 +358,48 @@ meta def positivity_inv : expr → tactic strictness private lemma pow_zero_pos [ordered_semiring R] [nontrivial R] (a : R) : 0 < a ^ 0 := zero_lt_one.trans_le (pow_zero a).ge -/-- Extension for the `positivity` tactic: raising a number `a` to a natural number power `n` is -known to be positive if `n = 0` (since `a ^ 0 = 1`) or if `0 < a`, and is known to be nonnegative if -`n = 2` (squares are nonnegative) or if `0 ≤ a`. -/ +private lemma zpow_zero_pos [linear_ordered_semifield R] (a : R) : 0 < a ^ (0 : ℤ) := +zero_lt_one.trans_le (zpow_zero a).ge + +/-- Extension for the `positivity` tactic: raising a number `a` to a natural/integer power `n` is +positive if `n = 0` (since `a ^ 0 = 1`) or if `0 < a`, and is nonnegative if `n` is even (squares +are nonnegative) or if `0 ≤ a`. -/ @[positivity] meta def positivity_pow : expr → tactic strictness | `(%%a ^ %%n) := do - n_typ ← infer_type n, - match n_typ with - | `(ℕ) := do + typ ← infer_type n, + (do + unify typ `(ℕ), if n = `(0) then positive <$> mk_app ``pow_zero_pos [a] - else tactic.positivity.orelse' - -- squares are nonnegative (TODO: similar for any `bit0` exponent?) - (nonnegative <$> mk_app ``sq_nonneg [a]) - -- moreover `a ^ n` is positive if `a` is and nonnegative if `a` is - (do + else positivity.orelse' + (do -- even powers are nonnegative + match n with -- TODO: Decision procedure for parity + | `(bit0 %% n) := nonnegative <$> mk_app ``pow_bit0_nonneg [a, n] + | _ := failed + end) $ + do -- `a ^ n` is positive if `a` is, and nonnegative if `a` is strictness_a ← core a, match strictness_a with - | (positive pa) := positive <$> mk_app ``pow_pos [pa, n] - | (nonnegative pa) := nonnegative <$> mk_app ``pow_nonneg [pa, n] - end) - | _ := failed -- TODO handle integer powers, maybe even real powers - end + | positive p := positive <$> mk_app ``pow_pos [p, n] + | nonnegative p := nonnegative <$> mk_app `pow_nonneg [p, n] + end) <|> + (do + unify typ `(ℤ), + if n = `(0 : ℤ) then + positive <$> mk_app ``zpow_zero_pos [a] + else positivity.orelse' + (do -- even powers are nonnegative + match n with -- TODO: Decision procedure for parity + | `(bit0 %% n) := nonnegative <$> mk_app ``zpow_bit0_nonneg [a, n] + | _ := failed + end) $ + do -- `a ^ n` is positive if `a` is, and nonnegative if `a` is + strictness_a ← core a, + match strictness_a with + | positive p := positive <$> mk_app ``zpow_pos_of_pos [p, n] + | nonnegative p := nonnegative <$> mk_app ``zpow_nonneg [p, n] + end) | _ := failed /-- Extension for the `positivity` tactic: an absolute value is nonnegative, and is strictly diff --git a/test/positivity.lean b/test/positivity.lean index 804b2de9adab0..fa89a779f1927 100644 --- a/test/positivity.lean +++ b/test/positivity.lean @@ -1,5 +1,6 @@ import algebra.order.smul import analysis.normed.group.basic +import analysis.special_functions.pow import data.complex.exponential import data.rat.nnrat import data.real.ereal @@ -12,7 +13,10 @@ import tactic.positivity This tactic proves goals of the form `0 ≤ a` and `0 < a`. -/ -open_locale ennreal nnrat nnreal +open_locale ennreal nnreal + +universe u +variables {α β : Type*} /- ## Numeric goals -/ @@ -56,7 +60,26 @@ example {a b : ℤ} (ha : 3 < a) (hb : 4 ≤ b) : 0 < 3 + a * b / 7 + b + 7 + 14 example {a : ℤ} (ha : 0 < a) : 0 < a / a := by positivity -example {a : ℕ} : 0 < a ^ 0 := by positivity +/-! ### Exponentiation -/ + +example [ordered_semiring α] [nontrivial α] (a : α) : 0 < a ^ 0 := by positivity +example [linear_ordered_ring α] (a : α) (n : ℕ) : 0 ≤ a ^ (bit0 n) := by positivity +example [ordered_semiring α] {a : α} {n : ℕ} (ha : 0 ≤ a) : 0 ≤ a ^ n := by positivity +example [ordered_semiring α] {a : α} {n : ℕ} (ha : 0 < a) : 0 < a ^ n := by positivity + +example [linear_ordered_semifield α] (a : α) : 0 < a ^ (0 : ℤ) := by positivity +example [linear_ordered_field α] (a : α) (n : ℤ) : 0 ≤ a ^ (bit0 n) := by positivity +example [linear_ordered_semifield α] {a : α} {n : ℤ} (ha : 0 ≤ a) : 0 ≤ a ^ n := by positivity +example [linear_ordered_semifield α] {a : α} {n : ℤ} (ha : 0 < a) : 0 < a ^ n := by positivity + +example {a b : cardinal.{u}} (ha : 0 < a) : 0 < a ^ b := by positivity +example {a b : ordinal.{u}} (ha : 0 < a) : 0 < a ^ b := by positivity + +example {a b : ℝ} (ha : 0 ≤ a) : 0 ≤ a ^ b := by positivity +example {a b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity +example {a : ℝ≥0} {b : ℝ} (ha : 0 < a) : 0 < a ^ b := by positivity +example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a ^ b := by positivity +example {a : ℝ≥0∞} {b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < a ^ b := by positivity example {a : ℤ} (ha : 3 < a) : 0 ≤ a ^ 2 + a := by positivity @@ -99,7 +122,7 @@ example : 0 ≤ max (0:ℤ) (-3) := by positivity example : 0 ≤ max (-3 : ℤ) 5 := by positivity -example {α β : Type*} [ordered_semiring α] [ordered_add_comm_monoid β] [smul_with_zero α β] +example [ordered_semiring α] [ordered_add_comm_monoid β] [smul_with_zero α β] [ordered_smul α β] {a : α} (ha : 0 < a) {b : β} (hb : 0 < b) : 0 ≤ a • b := by positivity example {r : ℝ} : 0 < real.exp r := by positivity