refactor: turn posPart into a notation class again (#17426)

Author: j-loreaux

Mathlib.lean

@@ -543,6 +543,7 @@ import Mathlib.Algebra.MvPolynomial.Rename
 import Mathlib.Algebra.MvPolynomial.Supported
 import Mathlib.Algebra.MvPolynomial.Variables
 import Mathlib.Algebra.NeZero
+import Mathlib.Algebra.Notation
 import Mathlib.Algebra.Opposites
 import Mathlib.Algebra.Order.AbsoluteValue
 import Mathlib.Algebra.Order.AddGroupWithTop

Mathlib/Algebra/Notation.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2024 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+import Mathlib.Tactic.ToAdditive
+
+/-!
+# Notations for operations involving order and algebraic structure
+
+## Notations
+
+* `a⁺ᵐ = a ⊔ 1`: *Positive component* of an element `a` of a multiplicative lattice ordered group
+* `a⁻ᵐ = a⁻¹ ⊔ 1`: *Negative component* of an element `a` of a multiplicative lattice ordered group
+* `a⁺ = a ⊔ 0`: *Positive component* of an element `a` of a lattice ordered group
+* `a⁻ = (-a) ⊔ 0`: *Negative component* of an element `a` of a lattice ordered group
+-/
+
+/-- A notation class for the *positive part* function: `a⁺`. -/
+class PosPart (α : Type*) where
+  /-- The *positive part* of an element `a`. -/
+  posPart : α → α
+
+/-- A notation class for the *positive part* function (multiplicative version): `a⁺ᵐ`. -/
+@[to_additive]
+class OneLePart (α : Type*) where
+  /-- The *positive part* of an element `a`. -/
+  oneLePart : α → α
+
+/-- A notation class for the *negative part* function: `a⁻`. -/
+class NegPart (α : Type*) where
+  /-- The *negative part* of an element `a`. -/
+  negPart : α → α
+
+/-- A notation class for the *negative part* function (multiplicative version): `a⁻ᵐ`. -/
+@[to_additive]
+class LeOnePart (α : Type*) where
+  /-- The *negative part* of an element `a`. -/
+  leOnePart : α → α
+
+export OneLePart (oneLePart)
+export LeOnePart (leOnePart)
+export PosPart (posPart)
+export NegPart (negPart)
+
+@[inherit_doc] postfix:max "⁺ᵐ " => OneLePart.oneLePart
+@[inherit_doc] postfix:max "⁻ᵐ" => LeOnePart.leOnePart
+@[inherit_doc] postfix:max "⁺" => PosPart.posPart
+@[inherit_doc] postfix:max "⁻" => NegPart.negPart

Mathlib/Algebra/Order/Group/PosPart.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin, Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Group.Unbundled.Abs
+import Mathlib.Algebra.Notation
 
 /-!
 # Positive & negative parts
@@ -12,22 +13,15 @@ Mathematical structures possessing an absolute value often also possess a unique
 elements into "positive" and "negative" parts which are in some sense "disjoint" (e.g. the Jordan
 decomposition of a measure).
 
-This file defines `posPart` and `negPart`, the positive and negative parts of an element in a
-lattice ordered group.
+This file provides instances of `PosPart` and `NegPart`, the positive and negative parts of an
+element in a lattice ordered group.
 
 ## Main statements
 
 * `posPart_sub_negPart`: Every element `a` can be decomposed into `a⁺ - a⁻`, the difference of its
   positive and negative parts.
 * `posPart_inf_negPart_eq_zero`: The positive and negative parts are coprime.
 
-## Notations
-
-* `a⁺ᵐ = a ⊔ 1`: *Positive component* of an element `a` of a multiplicative lattice ordered group
-* `a⁻ᵐ = a⁻¹ ⊔ 1`: *Negative component* of an element `a` of a multiplicative lattice ordered group
-* `a⁺ = a ⊔ 0`: *Positive component* of an element `a` of a lattice ordered group
-* `a⁻ = (-a) ⊔ 0`: *Negative component* of an element `a` of a lattice ordered group
-
 ## References
 
 * [Birkhoff, Lattice-ordered Groups][birkhoff1942]
@@ -54,20 +48,21 @@ variable [Group α] {a b : α}
 /-- The *positive part* of an element `a` in a lattice ordered group is `a ⊔ 1`, denoted `a⁺ᵐ`. -/
 @[to_additive
 "The *positive part* of an element `a` in a lattice ordered group is `a ⊔ 0`, denoted `a⁺`."]
-def oneLePart (a : α) : α := a ⊔ 1
+instance instOneLePart : OneLePart α where
+  oneLePart a := a ⊔ 1
 
 /-- The *negative part* of an element `a` in a lattice ordered group is `a⁻¹ ⊔ 1`, denoted `a⁻ᵐ `.
 -/
 @[to_additive
 "The *negative part* of an element `a` in a lattice ordered group is `(-a) ⊔ 0`, denoted `a⁻`."]
-def leOnePart (a : α) : α := a⁻¹ ⊔ 1
+instance instLeOnePart : LeOnePart α where
+  leOnePart a := a⁻¹ ⊔ 1
+
+@[to_additive] lemma leOnePart_def (a : α) : a⁻ᵐ = a⁻¹ ⊔ 1 := rfl
 
-@[inherit_doc] postfix:max "⁺ᵐ " => oneLePart
-@[inherit_doc] postfix:max "⁻ᵐ" => leOnePart
-@[inherit_doc] postfix:max "⁺" => posPart
-@[inherit_doc] postfix:max "⁻" => negPart
+@[to_additive] lemma oneLePart_def (a : α) : a⁺ᵐ = a ⊔ 1 := rfl
 
-@[to_additive] lemma oneLePart_mono : Monotone (oneLePart : α → α) :=
+@[to_additive] lemma oneLePart_mono : Monotone (·⁺ᵐ : α → α) :=
   fun _a _b hab ↦ sup_le_sup_right hab _
 
 @[to_additive (attr := simp)] lemma oneLePart_one : (1 : α)⁺ᵐ = 1 := sup_idem _
@@ -124,8 +119,8 @@ lemma leOnePart_eq_one : a⁻ᵐ = 1 ↔ 1 ≤ a := by simp [leOnePart_eq_one']
 
 -- Bourbaki A.VI.12 Prop 9 a)
 @[to_additive (attr := simp)] lemma oneLePart_div_leOnePart (a : α) : a⁺ᵐ / a⁻ᵐ = a := by
-  rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart, mul_sup, mul_one, mul_inv_cancel, sup_comm,
-    oneLePart]
+  rw [div_eq_mul_inv, mul_inv_eq_iff_eq_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel,
+    sup_comm, oneLePart_def]
 
 @[to_additive (attr := simp)] lemma leOnePart_div_oneLePart (a : α) : a⁻ᵐ / a⁺ᵐ = a⁻¹ := by
   rw [← inv_div, oneLePart_div_leOnePart]
@@ -148,16 +143,16 @@ variable [CovariantClass α α (swap (· * ·)) (· ≤ ·)]
 
 @[to_additive]
 lemma leOnePart_eq_inv_inf_one (a : α) : a⁻ᵐ = (a ⊓ 1)⁻¹ := by
-  rw [leOnePart, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
+  rw [leOnePart_def, ← inv_inj, inv_sup, inv_inv, inv_inv, inv_one]
 
 -- Bourbaki A.VI.12 Prop 9 d)
 @[to_additive] lemma oneLePart_mul_leOnePart (a : α) : a⁺ᵐ * a⁻ᵐ = |a|ₘ := by
-  rw [oneLePart, sup_mul, one_mul, leOnePart, mul_sup, mul_one, mul_inv_cancel, sup_assoc,
+  rw [oneLePart_def, sup_mul, one_mul, leOnePart_def, mul_sup, mul_one, mul_inv_cancel, sup_assoc,
     ← sup_assoc a, sup_eq_right.2 le_sup_right]
   exact sup_eq_left.2 <| one_le_mabs a
 
 @[to_additive] lemma leOnePart_mul_oneLePart (a : α) : a⁻ᵐ * a⁺ᵐ = |a|ₘ := by
-  rw [oneLePart, mul_sup, mul_one, leOnePart, sup_mul, one_mul, inv_mul_cancel, sup_assoc,
+  rw [oneLePart_def, mul_sup, mul_one, leOnePart_def, sup_mul, one_mul, inv_mul_cancel, sup_assoc,
     ← @sup_assoc _ _ a, sup_eq_right.2 le_sup_right]
   exact sup_eq_left.2 <| one_le_mabs a
 
@@ -213,22 +208,22 @@ section LinearOrder
 variable [LinearOrder α] [Group α] {a b : α}
 
 @[to_additive] lemma oneLePart_eq_ite : a⁺ᵐ = if 1 ≤ a then a else 1 := by
-  rw [oneLePart, ← maxDefault, ← sup_eq_maxDefault]; simp_rw [sup_comm]
+  rw [oneLePart_def, ← maxDefault, ← sup_eq_maxDefault]; simp_rw [sup_comm]
 
 @[to_additive (attr := simp) posPart_pos_iff] lemma one_lt_oneLePart_iff : 1 < a⁺ᵐ ↔ 1 < a :=
   lt_iff_lt_of_le_iff_le <| (one_le_oneLePart _).le_iff_eq.trans oneLePart_eq_one
 
 @[to_additive posPart_eq_of_posPart_pos]
 lemma oneLePart_of_one_lt_oneLePart (ha : 1 < a⁺ᵐ) : a⁺ᵐ = a := by
-  rw [oneLePart, right_lt_sup, not_le] at ha; exact oneLePart_eq_self.2 ha.le
+  rw [oneLePart_def, right_lt_sup, not_le] at ha; exact oneLePart_eq_self.2 ha.le
 
 @[to_additive (attr := simp)] lemma oneLePart_lt : a⁺ᵐ < b ↔ a < b ∧ 1 < b := sup_lt_iff
 
 section covariantmul
 variable [CovariantClass α α (· * ·) (· ≤ ·)]
 
 @[to_additive] lemma leOnePart_eq_ite : a⁻ᵐ = if a ≤ 1 then a⁻¹ else 1 := by
-  simp_rw [← one_le_inv']; rw [leOnePart, ← maxDefault, ← sup_eq_maxDefault]; simp_rw [sup_comm]
+  simp_rw [← one_le_inv']; rw [leOnePart_def, ← maxDefault, ← sup_eq_maxDefault]; simp_rw [sup_comm]
 
 @[to_additive (attr := simp) negPart_pos_iff] lemma one_lt_ltOnePart_iff : 1 < a⁻ᵐ ↔ a < 1 :=
   lt_iff_lt_of_le_iff_le <| (one_le_leOnePart _).le_iff_eq.trans leOnePart_eq_one

Mathlib/Tactic/Positivity/Basic.lean

@@ -500,9 +500,11 @@ def evalRatDen : PositivityExt where eval {u α} _ _ e := do
 
 /-- Extension for `posPart`. `a⁺` is always nonegative, and positive if `a` is. -/
 @[positivity _⁺]
-def evalPosPart : PositivityExt where eval zα pα e := do
+def evalPosPart : PositivityExt where eval {u α} zα pα e := do
   match e with
-  | ~q(@posPart _ $instαlat $instαgrp $a) =>
+  | ~q(@posPart _ $instαpospart $a) =>
+    let _instαlat ← synthInstanceQ q(Lattice $α)
+    let _instαgrp ← synthInstanceQ q(AddGroup $α)
     assertInstancesCommute
     -- FIXME: There seems to be a bug in `Positivity.core` that makes it fail (instead of returning
     -- `.none`) here sometimes. See eg the first test for `posPart`. This is why we need `catchNone`
@@ -513,9 +515,11 @@ def evalPosPart : PositivityExt where eval zα pα e := do
 
 /-- Extension for `negPart`. `a⁻` is always nonegative. -/
 @[positivity _⁻]
-def evalNegPart : PositivityExt where eval _ _ e := do
+def evalNegPart : PositivityExt where eval {u α} _ _ e := do
   match e with
-  | ~q(@negPart _ $instαlat $instαgrp $a) =>
+  | ~q(@negPart _ $instαnegpart $a) =>
+    let _instαlat ← synthInstanceQ q(Lattice $α)
+    let _instαgrp ← synthInstanceQ q(AddGroup $α)
     assertInstancesCommute
     return .nonnegative q(negPart_nonneg $a)
   | _ => throwError "not `negPart`"

Mathlib/Tactic/ToAdditive/Frontend.lean

@@ -1048,6 +1048,8 @@ def fixAbbreviation : List String → List String
                                       => "function" :: "_" :: "semiconj" :: fixAbbreviation s
   | "function" :: "_" :: "add" :: "Commute" :: s
                                       => "function" :: "_" :: "commute" :: fixAbbreviation s
+  | "Zero" :: "Le" :: "Part" :: s         => "PosPart" :: fixAbbreviation s
+  | "Le" :: "Zero" :: "Part" :: s         => "NegPart" :: fixAbbreviation s
   | "zero" :: "Le" :: "Part" :: s         => "posPart" :: fixAbbreviation s
   | "le" :: "Zero" :: "Part" :: s         => "negPart" :: fixAbbreviation s
   | "Division" :: "Add" :: "Monoid" :: s => "SubtractionMonoid" :: fixAbbreviation s