Fix #1844 by renaming abelian group proof for integers and moving raw bundles (#1862)

Author: jamesmckinna

CHANGELOG.md

@@ -968,6 +968,8 @@ Deprecated names
   pos-distrib-* ↦ pos-*
   pos-+-commute ↦ pos-+
   abs-*-commute ↦ abs-*
+  
+  +-isAbelianGroup ↦ +-0-isAbelianGroup
   ```
 
 * In `Data.List.Properties`:

src/Data/Integer/Base.agda

@@ -11,6 +11,8 @@
 
 module Data.Integer.Base where
 
+open import Algebra.Bundles.Raw
+  using (RawMagma; RawMonoid; RawNearSemiring; RawSemiring; RawRing)
 open import Data.Bool.Base using (Bool; T; true; false)
 open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s)
 open import Data.Sign.Base as Sign using (Sign)
@@ -293,3 +295,49 @@ _%ℕ_ : (dividend : ℤ) (divisor : ℕ) .{{_ : ℕ.NonZero divisor}} → ℕ
 
 _%_ : (dividend divisor : ℤ) .{{_ : NonZero divisor}} → ℕ
 i % j = i %ℕ ∣ j ∣
+
+------------------------------------------------------------------------
+-- Bundles
+
++-rawMagma : RawMagma 0ℓ 0ℓ
++-rawMagma = record { _≈_ = _≡_ ; _∙_ = _+_ }
+
++-0-rawMonoid : RawMonoid 0ℓ 0ℓ
++-0-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _+_ ; ε = 0ℤ }
+
+*-rawMagma : RawMagma 0ℓ 0ℓ
+*-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ }
+
+*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
+*-1-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1ℤ }
+
++-*-rawNearSemiring : RawNearSemiring 0ℓ 0ℓ
++-*-rawNearSemiring = record
+  { Carrier = _
+  ; _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; 0# = 0ℤ
+  }
+
++-*-rawSemiring : RawSemiring 0ℓ 0ℓ
++-*-rawSemiring = record
+  { Carrier = _
+  ; _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; 0# = 0ℤ
+  ; 1# = 1ℤ
+  }
+
++-*-rawRing : RawRing 0ℓ 0ℓ
++-*-rawRing = record
+  { Carrier = _
+  ; _≈_ = _≡_
+  ; _+_ = _+_
+  ; _*_ = _*_
+  ; -_ = -_
+  ; 0# = 0ℤ
+  ; 1# = 1ℤ
+  }
+

src/Data/Integer/Properties.agda

@@ -944,8 +944,8 @@ distribʳ-⊖-+-neg m n o = begin
   ; ⁻¹-cong  = cong (-_)
   }
 
-+-isAbelianGroup : IsAbelianGroup _+_ +0 (-_)
-+-isAbelianGroup = record
++-0-isAbelianGroup : IsAbelianGroup _+_ +0 (-_)
++-0-isAbelianGroup = record
   { isGroup = +-0-isGroup
   ; comm    = +-comm
   }
@@ -980,7 +980,7 @@ distribʳ-⊖-+-neg m n o = begin
 
 +-0-abelianGroup : AbelianGroup 0ℓ 0ℓ
 +-0-abelianGroup = record
-  { isAbelianGroup = +-isAbelianGroup
+  { isAbelianGroup = +-0-isAbelianGroup
   }
 
 ------------------------------------------------------------------------
@@ -1522,7 +1522,7 @@ private
 
 +-*-isRing : IsRing _+_ _*_ -_ 0ℤ 1ℤ
 +-*-isRing = record
-  { +-isAbelianGroup = +-isAbelianGroup
+  { +-isAbelianGroup = +-0-isAbelianGroup
   ; *-cong           = cong₂ _*_
   ; *-assoc          = *-assoc
   ; *-identity       = *-identity
@@ -1539,12 +1539,6 @@ private
 ------------------------------------------------------------------------
 -- Bundles
 
-*-rawMagma : RawMagma 0ℓ 0ℓ
-*-rawMagma = record { _≈_ = _≡_ ; _∙_ = _*_ }
-
-*-1-rawMonoid : RawMonoid 0ℓ 0ℓ
-*-1-rawMonoid = record { _≈_ = _≡_ ; _∙_ = _*_ ; ε = 1ℤ }
-
 *-magma : Magma 0ℓ 0ℓ
 *-magma = record
   { isMagma = *-isMagma
@@ -2387,3 +2381,11 @@ pos-distrib-* m n = sym (pos-* m n)
 "Warning: pos-distrib-* was deprecated in v2.0
 Please use pos-* instead."
 #-}
++-isAbelianGroup = +-0-isAbelianGroup
+{-# WARNING_ON_USAGE +-isAbelianGroup
+"Warning: +-isAbelianGroup was deprecated in v2.0
+Please use +-0-isAbelianGroup instead."
+#-}
+{- issue1844/issue1755: raw bundles have moved to `Data.X.Base` -}
+open Data.Integer.Base public
+  using (*-rawMagma; *-1-rawMonoid)