feat(tactic/positivity): Extension for function.const (#17126)

Positivity extension for `function.const`

src/algebra/group/pi.lean

@@ -16,6 +16,7 @@ This file defines instances for group, monoid, semigroup and related structures
 -/
 
 universes u v w
+variables {ι α : Type*}
 variable {I : Type u}     -- The indexing type
 variable {f : I → Type v} -- The family of types already equipped with instances
 variables (x y : Π i, f i) (i : I)
@@ -392,6 +393,11 @@ lemma update_div [Π i, has_div (f i)] [decidable_eq I]
   update (f₁ / f₂) i (x₁ / x₂) = update f₁ i x₁ / update f₂ i x₂ :=
 funext $ λ j, (apply_update₂ (λ i, (/)) f₁ f₂ i x₁ x₂ j).symm
 
+variables [has_one α] [nonempty ι] {a : α}
+
+@[simp, to_additive] lemma const_eq_one : const ι a = 1 ↔ a = 1 := @const_inj _ _ _ _ 1
+@[to_additive] lemma const_ne_one : const ι a ≠ 1 ↔ a ≠ 1 := const_eq_one.not
+
 end function
 
 section piecewise
@@ -418,7 +424,7 @@ end piecewise
 
 section extend
 
-variables {ι : Type u} {η : Type v} (R : Type w) (s : ι → η)
+variables {η : Type v} (R : Type w) (s : ι → η)
 
 /-- `function.extend s f 1` as a bundled hom. -/
 @[to_additive function.extend_by_zero.hom "`function.extend s f 0` as a bundled hom.", simps]

src/algebra/order/pi.lean

@@ -5,6 +5,7 @@ Authors: Simon Hudon, Patrick Massot
 -/
 import algebra.order.ring
 import algebra.ring.pi
+import tactic.positivity
 
 /-!
 # Pi instances for ordered groups and monoids
@@ -13,6 +14,7 @@ This file defines instances for ordered group, monoid, and related structures on
 -/
 
 universes u v w
+variables {ι α β : Type*}
 variable {I : Type u}     -- The indexing type
 variable {f : I → Type v} -- The family of types already equipped with instances
 variables (x y : Π i, f i) (i : I)
@@ -74,3 +76,50 @@ instance [Π i, ordered_comm_ring (f i)] : ordered_comm_ring (Π i, f i) :=
 { ..pi.comm_ring, ..pi.ordered_ring }
 
 end pi
+
+namespace function
+variables (β) [has_one α] [preorder α] {a : α}
+
+@[to_additive const_nonneg_of_nonneg]
+lemma one_le_const_of_one_le (ha : 1 ≤ a) : 1 ≤ const β a := λ _, ha
+
+@[to_additive] lemma const_le_one_of_le_one (ha : a ≤ 1) : const β a ≤ 1 := λ _, ha
+
+variables {β} [nonempty β]
+
+@[simp, to_additive const_nonneg]
+lemma one_le_const : 1 ≤ const β a ↔ 1 ≤ a := @const_le_const _ _ _ _ 1 _
+@[simp, to_additive const_pos]
+lemma one_lt_const : 1 < const β a ↔ 1 < a := @const_lt_const _ _ _ _ 1 a
+@[simp, to_additive] lemma const_le_one : const β a ≤ 1 ↔ a ≤ 1 := @const_le_const _ _ _ _ _ 1
+@[simp, to_additive] lemma const_lt_one : const β a < 1 ↔ a < 1 := @const_lt_const _ _ _ _ _ 1
+
+end function
+
+namespace tactic
+open function positivity
+variables (ι) [has_zero α] {a : α}
+
+private lemma function_const_nonneg_of_pos [preorder α] (ha : 0 < a) : 0 ≤ const ι a :=
+const_nonneg_of_nonneg _ ha.le
+
+variables [nonempty ι]
+
+private lemma function_const_ne_zero : a ≠ 0 → const ι a ≠ 0 := const_ne_zero.2
+private lemma function_const_pos [preorder α] : 0 < a → 0 < const ι a := const_pos.2
+
+/-- Extension for the `positivity` tactic: `function.const` is positive/nonnegative/nonzero if its
+input is. -/
+@[positivity]
+meta def positivity_const : expr → tactic strictness
+| `(function.const %%ι %%a) := do
+    strict_a ← core a,
+    match strict_a with
+    | positive p := positive <$> to_expr ``(function_const_pos %%ι %%p)
+        <|> nonnegative <$> to_expr ``(function_const_nonneg_of_pos %%ι %%p)
+    | nonnegative p := nonnegative <$> to_expr ``(const_nonneg_of_nonneg %%ι %%p)
+    | nonzero p := nonzero <$> to_expr ``(function_const_ne_zero %%ι %%p)
+    end
+| e := pp e >>= fail ∘ format.bracket "The expression `" "` is not of the form `function.const ι a`"
+
+end tactic

src/order/basic.lean

@@ -526,6 +526,14 @@ lemma pi.sdiff_def {ι : Type u} {α : ι → Type v} [∀ i, has_sdiff (α i)]
 lemma pi.sdiff_apply {ι : Type u} {α : ι → Type v} [∀ i, has_sdiff (α i)] (x y : Π i, α i) (i : ι) :
   (x \ y) i = x i \ y i := rfl
 
+namespace function
+variables [preorder α] [nonempty β] {a b : α}
+
+@[simp] lemma const_le_const : const β a ≤ const β b ↔ a ≤ b := by simp [pi.le_def]
+@[simp] lemma const_lt_const : const β a < const β b ↔ a < b := by simpa [pi.lt_def] using le_of_lt
+
+end function
+
 /-! ### `min`/`max` recursors -/
 
 section min_max_rec

src/order/monotone.lean

@@ -843,3 +843,11 @@ lemma strict_anti.prod_map (hf : strict_anti f) (hg : strict_anti g) : strict_an
   exact or.imp (and.imp hf.imp hg.antitone.imp) (and.imp hf.antitone.imp hg.imp) }
 
 end partial_order
+
+namespace function
+variables [preorder α]
+
+lemma const_mono : monotone (const β : α → β → α) := λ a b h i, h
+lemma const_strict_mono [nonempty β] : strict_mono (const β : α → β → α) := λ a b, const_lt_const.2
+
+end function

src/tactic/positivity.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro, Heather Macbeth, Yaël Dillies
 import tactic.norm_num
 
 /-! # `positivity` tactic
-αᵒᵈ βᵒᵈ
+
 The `positivity` tactic in this file solves goals of the form `0 ≤ x`, `0 < x` and `x ≠ 0`.  The
 tactic works recursively according to the syntax of the expression `x`.  For example, a goal of the
 form `0 ≤ 3 * a ^ 2 + b * c` can be solved either
@@ -345,7 +345,7 @@ add_tactic_doc
 
 end interactive
 
-variables {α R : Type*}
+variables {ι α R : Type*}
 
 /-! ### `positivity` extensions for particular arithmetic operations -/
 

test/positivity.lean

@@ -14,10 +14,11 @@ import tactic.positivity
 This tactic proves goals of the form `0 ≤ a` and `0 < a`.
 -/
 
+open function
 open_locale ennreal nat nnrat nnreal
 
 universe u
-variables {α β : Type*}
+variables {ι α β : Type*}
 
 /- ## Numeric goals -/
 
@@ -73,6 +74,11 @@ example {a : ℤ} (hlt : 0 ≤ a) (hne : a ≠ 0) : 0 < a := by positivity
 
 /- ## Tests of the @[positivity] plugin tactics (addition, multiplication, division) -/
 
+example [nonempty ι] [has_zero α] {a : α} (ha : a ≠ 0) : const ι a ≠ 0 := by positivity
+example [has_zero α] [preorder α] {a : α} (ha : 0 < a) : 0 ≤ const ι a := by positivity
+example [has_zero α] [preorder α] {a : α} (ha : 0 ≤ a) : 0 ≤ const ι a := by positivity
+example [nonempty ι] [has_zero α] [preorder α] {a : α} (ha : 0 < a) : 0 < const ι a := by positivity
+
 example {a b : ℚ} (ha : 0 < a) (hb : 0 < b) : 0 < min a b := by positivity
 example {a b : ℚ} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ min a b := by positivity
 example {a b : ℚ} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ min a b := by positivity