From e90e0a6119d01e3ef1703b3038b555785a998285 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Fri, 28 Jul 2023 07:23:47 +0000
Subject: [PATCH] feat(tactic/positivity): Extension for `ite` (#17650)

Add `positivity_ite`, an extension for `ite`.



Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
---
 src/tactic/positivity.lean | 46 ++++++++++++++++++++++++++++++++++++++
 test/positivity.lean       | 12 ++++++++++
 2 files changed, 58 insertions(+)

diff --git a/src/tactic/positivity.lean b/src/tactic/positivity.lean
index 6544387973144..bec4bfd4a8cb8 100644
--- a/src/tactic/positivity.lean
+++ b/src/tactic/positivity.lean
@@ -352,6 +352,52 @@ variables {ι α R : Type*}
 
 /-! ### `positivity` extensions for particular arithmetic operations -/
 
+section ite
+variables [has_zero α] {p : Prop} [decidable p] {a b : α}
+
+private lemma ite_pos [has_lt α] (ha : 0 < a) (hb : 0 < b) : 0 < ite p a b :=
+by by_cases p; simp [*]
+
+private lemma ite_nonneg [has_le α] (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ ite p a b :=
+by by_cases p; simp [*]
+
+private lemma ite_nonneg_of_pos_of_nonneg [preorder α] (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ ite p a b :=
+ite_nonneg ha.le hb
+
+private lemma ite_nonneg_of_nonneg_of_pos [preorder α] (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ ite p a b :=
+ite_nonneg ha hb.le
+
+private lemma ite_ne_zero (ha : a ≠ 0) (hb : b ≠ 0) : ite p a b ≠ 0 := by by_cases p; simp [*]
+
+private lemma ite_ne_zero_of_pos_of_ne_zero [preorder α] (ha : 0 < a) (hb : b ≠ 0) :
+  ite p a b ≠ 0 :=
+ite_ne_zero ha.ne' hb
+
+private lemma ite_ne_zero_of_ne_zero_of_pos [preorder α] (ha : a ≠ 0) (hb : 0 < b) :
+  ite p a b ≠ 0 :=
+ite_ne_zero ha hb.ne'
+
+end ite
+
+/-- Extension for the `positivity` tactic: the `if then else` of two numbers is
+positive/nonnegative/nonzero if both are. -/
+@[positivity]
+meta def positivity_ite : expr → tactic strictness
+| e@`(@ite %%typ %%p %%hp %%a %%b) := do
+  strictness_a ← core a,
+  strictness_b ← core b,
+  match strictness_a, strictness_b with
+  | positive pa, positive pb := positive <$> mk_app ``ite_pos [pa, pb]
+  | positive pa, nonnegative pb := nonnegative <$> mk_app ``ite_nonneg_of_pos_of_nonneg [pa, pb]
+  | nonnegative pa, positive pb := nonnegative <$> mk_app ``ite_nonneg_of_nonneg_of_pos [pa, pb]
+  | nonnegative pa, nonnegative pb := nonnegative <$> mk_app ``ite_nonneg [pa, pb]
+  | positive pa, nonzero pb := nonzero <$> to_expr ``(ite_ne_zero_of_pos_of_ne_zero %%pa %%pb)
+  | nonzero pa, positive pb := nonzero <$> to_expr ``(ite_ne_zero_of_ne_zero_of_pos %%pa %%pb)
+  | nonzero pa, nonzero pb := nonzero <$> to_expr ``(ite_ne_zero %%pa %%pb)
+  | sa@_, sb@ _ := positivity_fail e a b sa sb
+  end
+| e := pp e >>= fail ∘ format.bracket "The expression `" "` isn't of the form `ite p a b`"
+
 section linear_order
 variables [linear_order R] {a b c : R}
 
diff --git a/test/positivity.lean b/test/positivity.lean
index f4dc7425036ef..007d449a37bf3 100644
--- a/test/positivity.lean
+++ b/test/positivity.lean
@@ -80,6 +80,18 @@ example [has_zero α] [preorder α] {a : α} (ha : 0 < a) : 0 ≤ const ι a :=
 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
 
+section ite
+variables {p : Prop} [decidable p] {a b : ℤ}
+
+example (ha : 0 < a) (hb : 0 < b) : 0 < ite p a b := by positivity
+example (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ ite p a b := by positivity
+example (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ ite p a b := by positivity
+example (ha : 0 < a) (hb : b ≠ 0) : ite p a b ≠ 0 := by positivity
+example (ha : a ≠ 0) (hb : 0 < b) : ite p a b ≠ 0 := by positivity
+example (ha : a ≠ 0) (hb : b ≠ 0) : ite p a b ≠ 0 := by positivity
+
+end ite
+
 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