Cleaning up Data.Integer.Properties (#146)

* Moved properties from `Data.Integer.Addition.Properties` and `Data.Integer.Multiplication.Properties` to `Data.Integer.Properties` and deprivatised `Data.Integer.Properties`

* Added some additional properties from mechvel to Data.Integer.Properties

* Added Sergei Meshveliani to README.agda

Author: MatthewDaggitt

CHANGELOG.md

@@ -80,19 +80,31 @@ but they may be removed in some future release of the library.
   have been deprecated in favour of `+-mono-≤` and `*-mono-≤` which better
   follow the library's naming conventions.
 
+* The module `Data.Nat.Properties.Simple` is now deprecated. All proofs
+  have been moved to `Data.Nat.Properties` where they should be used directly.
+  The `Simple` file still exists for backwards compatability reasons and
+  re-exports the proofs from `Data.Nat.Properties` but will be removed in some
+  future release.
+
+* The module `Data.Integer.Addition.Properties` is now deprecated. All proofs
+  have been moved to `Data.Integer.Properties` where they should be used
+  directly. The `Addition.Properties` file still exists for backwards
+  compatability reasons and re-exports the proofs from `Data.Integer.Properties`
+  but will be removed in some future release.
+
+* The module `Data.Integer.Multiplication.Properties` is now deprecated. All
+  proofs have been moved to `Data.Integer.Properties` where they should be used
+  directly. The `Multiplication.Properties` file still exists for backwards
+  compatability reasons and re-exports the proofs from `Data.Integer.Properties`
+  but will be removed in some future release.
+
 Backwards compatible changes
 ----------------------------
 
 * Added support for GHC 8.0.2.
 
 * Added `Category.Functor.Morphism` and module `Category.Functor.Identity`.
 
-* The module `Data.Nat.Properties.Simple` is now deprecated. All proofs
-  have been moved to `Data.Nat.Properties` where they should be used directly.
-  The `Simple` file still exists for backwards compatability reasons and
-  re-exports the proofs from `Data.Nat.Properties` but will be removed in some
-  future release.
-
 * `Data.Container` and `Data.Container.Indexed` now allow for different
   levels in the container and in the data it contains.
 
@@ -221,7 +233,46 @@ Backwards compatible changes
   ∩⇔×       : x ∈ p ∩ q ⇔ (x ∈ p × x ∈ q)
   ```
 
-* Added additional proofs to `Data.Nat.Properties`:
+* Added proofs to `Data.Integer.Properties`
+  ```agda
+  +-injective           : + m ≡ + n → m ≡ n
+  -[1+-injective        : -[1+ m ] ≡ -[1+ n ] → m ≡ n
+
+  doubleNeg             : - - n ≡ n
+  neg-injective         : - m ≡ - n → m ≡ n
+
+  ∣n∣≡0⇒n≡0             : ∀ {n} → ∣ n ∣ ≡ 0 → n ≡ + 0
+  ∣-n∣≡∣n∣              : ∀ n → ∣ - n ∣ ≡ ∣ n ∣
+
+  +◃n≡+n                : Sign.+ ◃ n ≡ + n
+  -◃n≡-n                : Sign.- ◃ n ≡ - + n
+  signₙ◃∣n∣≡n           : sign n ◃ ∣ n ∣ ≡ n
+
+  ⊖-≰                   : n ≰ m → m ⊖ n ≡ - + (n ∸ m)
+  ∣⊖∣-≰                 : n ≰ m → ∣ m ⊖ n ∣ ≡ n ∸ m
+  sign-⊖-≰              : n ≰ m → sign (m ⊖ n) ≡ Sign.-
+  -[n⊖m]≡-m+n           : - (m ⊖ n) ≡ (- (+ m)) + (+ n)
+
+  +-identity            : Identity (+ 0) _+_
+  +-inverse             : Inverse (+ 0) -_ _+_
+  +-0-isMonoid          : IsMonoid _≡_ _+_ (+ 0)
+  +-0-isGroup           : IsGroup _≡_ _+_ (+ 0) (-_)
+  neg-distrib-+         : - (m + n) ≡ (- m) + (- n)
+  ◃-distrib-+           : s ◃ (m + n) ≡ (s ◃ m) + (s ◃ n)
+
+  *-identityʳ           : RightIdentity (+ 1) _*_
+  *-identity            : Identity (+ 1) _*_
+  *-zeroˡ               : LeftZero (+ 0) _*_
+  *-zeroʳ               : RightZero (+ 0) _*_
+  *-zero                : Zero (+ 0) _*_
+  *-1-isMonoid          : IsMonoid _≡_ _*_ (+ 1)
+  -1*n≡-n               : -[1+ 0 ] * n ≡ - n
+
+  +-*-isRing            : IsRing _≡_ _+_ _*_ -_ (+ 0) (+ 1)
+  +-*-isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (+ 0) (+ 1)
+  ```
+
+* Added proofs to `Data.Nat.Properties`:
   ```agda
   suc-injective        : suc m ≡ suc n → m ≡ n
   ≡-isDecEquivalence   : IsDecEquivalence (_≡_ {A = ℕ})
@@ -374,6 +425,20 @@ Backwards compatible changes
   zipWith-map₂            : zipWith _⊕_ xs (map f ys) ≡ zipWith (λ x y → x ⊕ f y) xs ys
   ```
 
+* Added proofs to `Data.Sign.Properties`:
+  ```agda
+  opposite-cong  : opposite s ≡ opposite t → s ≡ t
+
+  *-identityˡ    : LeftIdentity + _*_
+  *-identityʳ    : RightIdentity + _*_
+  *-identity     : Identity + _*_
+  *-comm         : Commutative _*_
+  *-assoc        : Associative _*_
+  cancel-*-left  : LeftCancellative _*_
+  *-cancellative : Cancellative _*_
+  s*s≡+          : s * s ≡ +
+  ```
+
 * Added proofs to `Data.Vec.All.Properties`
   ```agda
   All-++⁺      : All P xs → All P ys → All P (xs ++ ys)

README.agda

@@ -8,10 +8,10 @@ module README where
 -- Joachim Breitner, Samuel Bronson, Daniel Brown, James Chapman,
 -- Liang-Ting Chen, Matthew Daggitt, Dominique Devriese, Dan Doel,
 -- Érdi Gergő, Helmut Grohne, Simon Foster, Liyang Hu, Patrik Jansson,
--- Alan Jeffrey, Pepijn Kokke, Evgeny Kotelnikov, Eric Mertens, Darin
--- Morrison, Guilhem Moulin, Shin-Cheng Mu, Ulf Norell, Noriyuki
--- OHKAWA, Nicolas Pouillard, Andrés Sicard-Ramírez, Noam Zeilberger
--- and some anonymous contributors.
+-- Alan Jeffrey, Pepijn Kokke, Evgeny Kotelnikov, Sergei Meshveliani
+-- Eric Mertens, Darin Morrison, Guilhem Moulin, Shin-Cheng Mu,
+-- Ulf Norell, Noriyuki OHKAWA, Nicolas Pouillard, Andrés Sicard-Ramírez,
+-- Noam Zeilberger and some anonymous contributors.
 -- ----------------------------------------------------------------------
 
 -- The development version of the library often requires the latest

src/Data/Integer/Addition/Properties.agda

@@ -2,110 +2,26 @@
 -- The Agda standard library
 --
 -- Properties related to addition of integers
+--
+-- This module is DEPRECATED. Please use the corresponding properties in
+-- Data.Integer.Properties directly.
 ------------------------------------------------------------------------
 
 module Data.Integer.Addition.Properties where
 
-open import Algebra
-open import Algebra.Structures
-open import Data.Integer hiding (suc)
-open import Data.Nat.Base using (suc; zero) renaming (_+_ to _ℕ+_)
-import Data.Nat.Properties as ℕ
-open import Relation.Binary.PropositionalEquality
-open import Algebra.FunctionProperties (_≡_ {A = ℤ})
-
-------------------------------------------------------------------------
--- Addition and zero form a commutative monoid
-
-comm : Commutative _+_
-comm -[1+ a ] -[1+ b ] rewrite ℕ.+-comm a b = refl
-comm (+   a ) (+   b ) rewrite ℕ.+-comm a b = refl
-comm -[1+ _ ] (+   _ ) = refl
-comm (+   _ ) -[1+ _ ] = refl
-
-identityˡ : LeftIdentity (+ 0) _+_
-identityˡ -[1+ _ ] = refl
-identityˡ (+   _ ) = refl
-
-identityʳ : RightIdentity (+ 0) _+_
-identityʳ x rewrite comm x (+ 0) = identityˡ x
-
-distribˡ-⊖-+-neg : ∀ a b c → b ⊖ c + -[1+ a ] ≡ b ⊖ (suc c ℕ+ a)
-distribˡ-⊖-+-neg _ zero    zero    = refl
-distribˡ-⊖-+-neg _ zero    (suc _) = refl
-distribˡ-⊖-+-neg _ (suc _) zero    = refl
-distribˡ-⊖-+-neg a (suc b) (suc c) = distribˡ-⊖-+-neg a b c
-
-distribʳ-⊖-+-neg : ∀ a b c → -[1+ a ] + (b ⊖ c) ≡ b ⊖ (suc a ℕ+ c)
-distribʳ-⊖-+-neg a b c
-  rewrite comm -[1+ a ] (b ⊖ c)
-        | distribˡ-⊖-+-neg a b c
-        | ℕ.+-comm a c
-        = refl
-
-distribˡ-⊖-+-pos : ∀ a b c → b ⊖ c + + a ≡ b ℕ+ a ⊖ c
-distribˡ-⊖-+-pos _ zero    zero    = refl
-distribˡ-⊖-+-pos _ zero    (suc _) = refl
-distribˡ-⊖-+-pos _ (suc _) zero    = refl
-distribˡ-⊖-+-pos a (suc b) (suc c) = distribˡ-⊖-+-pos a b c
-
-distribʳ-⊖-+-pos : ∀ a b c → + a + (b ⊖ c) ≡ a ℕ+ b ⊖ c
-distribʳ-⊖-+-pos a b c
-  rewrite comm (+ a) (b ⊖ c)
-        | distribˡ-⊖-+-pos a b c
-        | ℕ.+-comm a b
-        = refl
-
-assoc : Associative _+_
-assoc (+ zero) y z rewrite identityˡ      y  | identityˡ (y + z) = refl
-assoc x (+ zero) z rewrite identityʳ  x      | identityˡ      z  = refl
-assoc x y (+ zero) rewrite identityʳ (x + y) | identityʳ  y      = refl
-assoc -[1+ a ]  -[1+ b ]  (+ suc c) = sym (distribʳ-⊖-+-neg a c b)
-assoc -[1+ a ]  (+ suc b) (+ suc c) = distribˡ-⊖-+-pos (suc c) b a
-assoc (+ suc a) -[1+ b ]  -[1+ c ]  = distribˡ-⊖-+-neg c a b
-assoc (+ suc a) -[1+ b ] (+ suc c)
-  rewrite distribˡ-⊖-+-pos (suc c) a b
-        | distribʳ-⊖-+-pos (suc a) c b
-        | sym (ℕ.+-assoc a 1 c)
-        | ℕ.+-comm a 1
-        = refl
-assoc (+ suc a) (+ suc b) -[1+ c ]
-  rewrite distribʳ-⊖-+-pos (suc a) b c
-        | sym (ℕ.+-assoc a 1 b)
-        | ℕ.+-comm a 1
-        = refl
-assoc -[1+ a ] -[1+ b ] -[1+ c ]
-  rewrite sym (ℕ.+-assoc a 1 (b ℕ+ c))
-        | ℕ.+-comm a 1
-        | ℕ.+-assoc a b c
-        = refl
-assoc -[1+ a ] (+ suc b) -[1+ c ]
-  rewrite distribʳ-⊖-+-neg a b c
-        | distribˡ-⊖-+-neg c b a
-        = refl
-assoc (+ suc a) (+ suc b) (+ suc c)
-  rewrite ℕ.+-assoc (suc a) (suc b) (suc c)
-        = refl
-
-isSemigroup : IsSemigroup _≡_ _+_
-isSemigroup = record
-  { isEquivalence = isEquivalence
-  ; assoc         = assoc
-  ; ∙-cong        = cong₂ _+_
-  }
-
-isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ 0)
-isCommutativeMonoid = record
-  { isSemigroup = isSemigroup
-  ; identityˡ   = identityˡ
-  ; comm        = comm
-  }
-
-commutativeMonoid : CommutativeMonoid _ _
-commutativeMonoid = record
-  { Carrier             = ℤ
-  ; _≈_                 = _≡_
-  ; _∙_                 = _+_
-  ; ε                   = + 0
-  ; isCommutativeMonoid = isCommutativeMonoid
-  }
+open import Data.Integer.Properties public
+  using
+  ( distribˡ-⊖-+-neg
+  ; distribʳ-⊖-+-neg
+  ; distribˡ-⊖-+-pos
+  ; distribʳ-⊖-+-pos
+  )
+  renaming
+  ( +-comm                  to comm
+  ; +-identityˡ              to identityˡ
+  ; +-identityʳ              to identityʳ
+  ; +-assoc                 to assoc
+  ; +-isSemigroup           to isSemigroup
+  ; +-0-isCommutativeMonoid to isCommutativeMonoid
+  ; +-0-commutativeMonoid   to commutativeMonoid
+  )

src/Data/Integer/Base.agda

@@ -146,8 +146,8 @@ _⊓_ : ℤ → ℤ → ℤ
 
 data _≤_ : ℤ → ℤ → Set where
   -≤+ : ∀ {m n} → -[1+ m ] ≤ + n
-  -≤- : ∀ {m n} → (n≤m : ℕ._≤_ n m) → -[1+ m ] ≤ -[1+ n ]
-  +≤+ : ∀ {m n} → (m≤n : ℕ._≤_ m n) → + m ≤ + n
+  -≤- : ∀ {m n} → (n≤m : n ℕ.≤ m) → -[1+ m ] ≤ -[1+ n ]
+  +≤+ : ∀ {m n} → (m≤n : m ℕ.≤ n) → + m ≤ + n
 
 drop‿+≤+ : ∀ {m n} → + m ≤ + n → ℕ._≤_ m n
 drop‿+≤+ (+≤+ m≤n) = m≤n

src/Data/Integer/Multiplication/Properties.agda

@@ -2,86 +2,20 @@
 -- The Agda standard library
 --
 -- Properties related to multiplication of integers
+--
+-- This module is DEPRECATED. Please use the corresponding properties in
+-- Data.Integer.Properties directly.
 ------------------------------------------------------------------------
 
 module Data.Integer.Multiplication.Properties where
 
-open import Algebra using (CommutativeMonoid)
-open import Algebra.Structures using (IsSemigroup; IsCommutativeMonoid)
-open import Data.Integer
-   using (ℤ; -[1+_]; +_; ∣_∣; sign; _◃_) renaming (_*_ to ℤ*)
-open import Data.Nat
-  using (suc; zero) renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
-open import Data.Product using (proj₂)
-import Data.Nat.Properties as ℕ
-open import Data.Sign using () renaming (_*_ to _S*_)
-open import Function using (_∘_)
-open import Relation.Binary.PropositionalEquality
-   using (_≡_; refl; cong; cong₂; isEquivalence)
-
-open import Algebra.FunctionProperties (_≡_ {A = ℤ})
-
-------------------------------------------------------------------------
--- Multiplication and one form a commutative monoid
-
-private
-  lemma : ∀ a b c → c ℕ+ (b ℕ+ a ℕ* suc b) ℕ* suc c
-                  ≡ c ℕ+ b ℕ* suc c ℕ+ a ℕ* suc (c ℕ+ b ℕ* suc c)
-  lemma =
-    solve 3 (λ a b c → c :+ (b :+ a :* (con 1 :+ b)) :* (con 1 :+ c)
-                    := c :+ b :* (con 1 :+ c) :+
-                       a :* (con 1 :+ (c :+ b :* (con 1 :+ c))))
-            refl
-    where open ℕ.SemiringSolver
-
-
-identityˡ : LeftIdentity (+ 1) ℤ*
-identityˡ (+ zero ) = refl
-identityˡ -[1+  n ] rewrite ℕ.+-right-identity n = refl
-identityˡ (+ suc n) rewrite ℕ.+-right-identity n = refl
-
-comm : Commutative ℤ*
-comm -[1+ a ] -[1+ b ] rewrite ℕ.*-comm (suc a) (suc b) = refl
-comm -[1+ a ] (+   b ) rewrite ℕ.*-comm (suc a) b       = refl
-comm (+   a ) -[1+ b ] rewrite ℕ.*-comm a       (suc b) = refl
-comm (+   a ) (+   b ) rewrite ℕ.*-comm a       b       = refl
-
-assoc : Associative ℤ*
-assoc (+ zero) _ _ = refl
-assoc x (+ zero) _ rewrite ℕ.*-right-zero ∣ x ∣ = refl
-assoc x y (+ zero) rewrite
-    ℕ.*-right-zero ∣ y ∣
-  | ℕ.*-right-zero ∣ x ∣
-  | ℕ.*-right-zero ∣ sign x S* sign y ◃ ∣ x ∣ ℕ* ∣ y ∣ ∣
-  = refl
-assoc -[1+ a  ] -[1+ b  ] (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
-assoc -[1+ a  ] (+ suc b) -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
-assoc (+ suc a) (+ suc b) (+ suc c) = cong (+_ ∘ suc) (lemma a b c)
-assoc (+ suc a) -[1+ b  ] -[1+ c  ] = cong (+_ ∘ suc) (lemma a b c)
-assoc -[1+ a  ] -[1+ b  ] -[1+ c  ] = cong -[1+_]     (lemma a b c)
-assoc -[1+ a  ] (+ suc b) (+ suc c) = cong -[1+_]     (lemma a b c)
-assoc (+ suc a) -[1+ b  ] (+ suc c) = cong -[1+_]     (lemma a b c)
-assoc (+ suc a) (+ suc b) -[1+ c  ] = cong -[1+_]     (lemma a b c)
-
-isSemigroup : IsSemigroup _ _
-isSemigroup = record
-    { isEquivalence = isEquivalence
-    ; assoc         = assoc
-    ; ∙-cong        = cong₂ ℤ*
-    }
-
-isCommutativeMonoid : IsCommutativeMonoid _≡_ ℤ* (+ 1)
-isCommutativeMonoid = record
-  { isSemigroup = isSemigroup
-  ; identityˡ   = identityˡ
-  ; comm        = comm
-  }
-
-commutativeMonoid : CommutativeMonoid _ _
-commutativeMonoid = record
-  { Carrier             = ℤ
-  ; _≈_                 = _≡_
-  ; _∙_                 = ℤ*
-  ; ε                   = + 1
-  ; isCommutativeMonoid = isCommutativeMonoid
-  }
+open import Data.Integer.Properties public
+  using ()
+  renaming
+  ( *-comm                  to comm
+  ; *-identityˡ              to identityˡ
+  ; *-assoc                 to assoc
+  ; *-isSemigroup           to isSemigroup
+  ; *-1-isCommutativeMonoid to isCommutativeMonoid
+  ; *-1-commutativeMonoid   to commutativeMonoid
+  )