Moved properties from Data.Integer.Addition.Properties and `Data.In…

…teger.Multiplication.Properties` to `Data.Integer.Properties` and deprivatised `Data.Integer.Properties`

CHANGELOG.md

@@ -44,9 +44,8 @@ Non-backwards compatible changes
 * Changed the implementation of `All₂` in `Data.Vec.All` to a native datatype
   which allows better pattern matching.
 
-  The new version (and the associated
-  proofs in `Data.Vec.All.Properties`) are also more generic with respect to
-  types and levels.
+  The new version (and the associated proofs in `Data.Vec.All.Properties`)
+  are also more generic with respect to types and levels.
 
 * Changed the implementation of `downFrom` in `Data.List` to a native
   (pattern-matching) definition.
@@ -64,19 +63,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.
 
@@ -205,7 +216,29 @@ Backwards compatible changes
   ∩⇔×       : x ∈ p ∩ q ⇔ (x ∈ p × x ∈ q)
   ```
 
-* Added additional proofs to `Data.Nat.Properties`:
+* Added proofs to `Data.Integer.Properties`
+  ```agda
+  +◃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.-
+
+  +-identity            : Identity (+ 0) _+_
+  +-0-isMonoid          : IsMonoid _≡_ _+_ (+ 0)
+  +-0-isGroup           : IsGroup _≡_ _+_ (+ 0) (-_)
+
+  *-identityʳ           : RightIdentity (+ 1) _*_
+  *-identity            : Identity (+ 1) _*_
+  *-1-isMonoid          : IsMonoid _≡_ _*_ (+ 1)
+
+  +-*-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 = ℕ})
@@ -358,6 +391,17 @@ 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 + _*_
+  cancel-*-left  : LeftCancellative _*_
+  *-cancellative : Cancellative _*_
+  ```
+
 * Added proofs to `Data.Vec.All.Properties`
   ```agda
   All-++⁺      : All P xs → All P ys → All P (xs ++ ys)

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/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
+  )

src/Data/Integer/Properties.agda

@@ -12,50 +12,49 @@ import Algebra.Morphism as Morphism
 import Algebra.Properties.AbelianGroup
 open import Algebra.Structures
 open import Data.Integer hiding (suc; _≤?_)
-import Data.Integer.Addition.Properties as Add
-import Data.Integer.Multiplication.Properties as Mul
 open import Data.Nat
-  using (ℕ; suc; zero; _∸_; _≤?_; _<_; _≥_; _≱_; s≤s; z≤n; ≤-pred)
+  using (ℕ; suc; zero; _∸_; _≤?_; _<_; _≥_; _≰_; s≤s; z≤n; ≤-pred)
   hiding (module ℕ)
   renaming (_+_ to _ℕ+_; _*_ to _ℕ*_)
-open import Data.Nat.Properties as ℕ using (_*-mono_; ≤-refl)
+open import Data.Nat.Properties as ℕ using (≤-refl)
 open import Data.Product using (proj₁; proj₂; _,_)
-open import Data.Sign as Sign using () renaming (_*_ to _S*_)
-import Data.Sign.Properties as SignProp
+open import Data.Sign as Sign using () renaming (_*_ to _𝕊*_)
+import Data.Sign.Properties as 𝕊
 open import Function using (_∘_; _$_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality
 open import Relation.Nullary using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 
 open Algebra.FunctionProperties (_≡_ {A = ℤ})
-open CommutativeMonoid Add.commutativeMonoid
-  using ()
-  renaming ( assoc to +-assoc; comm to +-comm; identity to +-identity
-           ; isCommutativeMonoid to +-isCommutativeMonoid
-           ; isMonoid to +-isMonoid
-           )
-open CommutativeMonoid Mul.commutativeMonoid
-  using ()
-  renaming ( assoc to *-assoc; comm to *-comm; identity to *-identity
-           ; isCommutativeMonoid to *-isCommutativeMonoid
-           ; isMonoid to *-isMonoid
-           )
-open CommutativeSemiring ℕ.commutativeSemiring
-  using () renaming (zero to *-zero; distrib to *-distrib)
 open Morphism.Definitions ℤ ℕ _≡_
 open ℕ.SemiringSolver
 open ≡-Reasoning
 
 ------------------------------------------------------------------------
--- Miscellaneous properties
+-- Properties of sign and _◃_
 
--- Some properties relating sign and ∣_∣ to _◃_.
++◃n≡+n : ∀ n → Sign.+ ◃ n ≡ + n
++◃n≡+n zero    = refl
++◃n≡+n (suc _) = refl
+
+-◃n≡-n : ∀ n → Sign.- ◃ n ≡ - + n
+-◃n≡-n zero    = refl
+-◃n≡-n (suc _) = refl
 
 sign-◃ : ∀ s n → sign (s ◃ suc n) ≡ s
 sign-◃ Sign.- _ = refl
 sign-◃ Sign.+ _ = refl
 
+abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n
+abs-◃ _      zero    = refl
+abs-◃ Sign.- (suc n) = refl
+abs-◃ Sign.+ (suc n) = refl
+
+signₙ◃∣n∣≡n : ∀ n → sign n ◃ ∣ n ∣ ≡ n
+signₙ◃∣n∣≡n (+ n)      = +◃n≡+n n
+signₙ◃∣n∣≡n (-[1+ n ]) = refl
+
 sign-cong : ∀ {s₁ s₂ n₁ n₂} →
             s₁ ◃ suc n₁ ≡ s₂ ◃ suc n₂ → s₁ ≡ s₂
 sign-cong {s₁} {s₂} {n₁} {n₂} eq = begin
@@ -64,11 +63,6 @@ sign-cong {s₁} {s₂} {n₁} {n₂} eq = begin
   sign (s₂ ◃ suc n₂)  ≡⟨ sign-◃ s₂ n₂ ⟩
   s₂                  ∎
 
-abs-◃ : ∀ s n → ∣ s ◃ n ∣ ≡ n
-abs-◃ _      zero    = refl
-abs-◃ Sign.- (suc n) = refl
-abs-◃ Sign.+ (suc n) = refl
-
 abs-cong : ∀ {s₁ s₂ n₁ n₂} →
            s₁ ◃ n₁ ≡ s₂ ◃ n₂ → n₁ ≡ n₂
 abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin
@@ -77,25 +71,13 @@ abs-cong {s₁} {s₂} {n₁} {n₂} eq = begin
   ∣ s₂ ◃ n₂ ∣  ≡⟨ abs-◃ s₂ n₂ ⟩
   n₂           ∎
 
--- ∣_∣ commutes with multiplication.
-
-abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_
-abs-*-commute i j = abs-◃ _ _
-
--- Subtraction properties
+------------------------------------------------------------------------
+-- Properties of _⊖_
 
 n⊖n≡0 : ∀ n → n ⊖ n ≡ + 0
 n⊖n≡0 zero    = refl
 n⊖n≡0 (suc n) = n⊖n≡0 n
 
-sign-⊖-< : ∀ {m n} → m < n → sign (m ⊖ n) ≡ Sign.-
-sign-⊖-< {zero}  (s≤s z≤n) = refl
-sign-⊖-< {suc n} (s≤s m<n) = sign-⊖-< m<n
-
-+-⊖-left-cancel : ∀ a b c → (a ℕ+ b) ⊖ (a ℕ+ c) ≡ b ⊖ c
-+-⊖-left-cancel zero    b c = refl
-+-⊖-left-cancel (suc a) b c = +-⊖-left-cancel a b c
-
 ⊖-swap : ∀ a b → a ⊖ b ≡ - (b ⊖ a)
 ⊖-swap zero    zero    = refl
 ⊖-swap (suc _) zero    = refl
@@ -110,15 +92,102 @@ sign-⊖-< {suc n} (s≤s m<n) = sign-⊖-< m<n
 ⊖-< {zero}  (s≤s z≤n) = refl
 ⊖-< {suc m} (s≤s m<n) = ⊖-< m<n
 
+⊖-≰ : ∀ {m n} → n ≰ m → m ⊖ n ≡ - + (n ∸ m)
+⊖-≰ = ⊖-< ∘ ℕ.≰⇒>
+
 ∣⊖∣-< : ∀ {m n} → m < n → ∣ m ⊖ n ∣ ≡ n ∸ m
 ∣⊖∣-< {zero}  (s≤s z≤n) = refl
 ∣⊖∣-< {suc n} (s≤s m<n) = ∣⊖∣-< m<n
 
+∣⊖∣-≰ : ∀ {m n} → n ≰ m → ∣ m ⊖ n ∣ ≡ n ∸ m
+∣⊖∣-≰ = ∣⊖∣-< ∘ ℕ.≰⇒>
+
+sign-⊖-< : ∀ {m n} → m < n → sign (m ⊖ n) ≡ Sign.-
+sign-⊖-< {zero}  (s≤s z≤n) = refl
+sign-⊖-< {suc n} (s≤s m<n) = sign-⊖-< m<n
+
+sign-⊖-≰ : ∀ {m n} → n ≰ m → sign (m ⊖ n) ≡ Sign.-
+sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒>
+
++-⊖-left-cancel : ∀ a b c → (a ℕ+ b) ⊖ (a ℕ+ c) ≡ b ⊖ c
++-⊖-left-cancel zero    b c = refl
++-⊖-left-cancel (suc a) b c = +-⊖-left-cancel a b c
 
 ------------------------------------------------------------------------
--- The integers form a commutative ring
+-- Properties of _+_
+
++-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
+
++-identity : Identity (+ 0) _+_
++-identity = +-identityˡ , +-identityʳ
+
+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
 
--- Additive abelian group.
++-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
 
 inverseˡ : LeftInverse (+ 0) -_ _+_
 inverseˡ -[1+ n ]  = n⊖n≡0 n
@@ -131,46 +200,140 @@ inverseʳ i = begin
   - i + i  ≡⟨ inverseˡ i ⟩
   + 0      ∎
 
++-isSemigroup : IsSemigroup _≡_ _+_
++-isSemigroup = record
+  { isEquivalence = isEquivalence
+  ; assoc         = +-assoc
+  ; ∙-cong        = cong₂ _+_
+  }
+
++-0-isMonoid : IsMonoid _≡_ _+_ (+ 0)
++-0-isMonoid = record
+  { isSemigroup = +-isSemigroup
+  ; identity    = +-identity
+  }
+
++-0-isCommutativeMonoid : IsCommutativeMonoid _≡_ _+_ (+ 0)
++-0-isCommutativeMonoid = record
+  { isSemigroup = +-isSemigroup
+  ; identityˡ   = +-identityˡ
+  ; comm        = +-comm
+  }
+
++-0-commutativeMonoid : CommutativeMonoid _ _
++-0-commutativeMonoid = record
+  { Carrier             = ℤ
+  ; _≈_                 = _≡_
+  ; _∙_                 = _+_
+  ; ε                   = + 0
+  ; isCommutativeMonoid = +-0-isCommutativeMonoid
+  }
+
++-0-isGroup : IsGroup _≡_ _+_ (+ 0) (-_)
++-0-isGroup = record
+  { isMonoid = +-0-isMonoid
+  ; inverse  = inverseˡ , inverseʳ
+  ; ⁻¹-cong  = cong (-_)
+  }
+
 +-isAbelianGroup : IsAbelianGroup _≡_ _+_ (+ 0) (-_)
 +-isAbelianGroup = record
-  { isGroup = record
-    { isMonoid = +-isMonoid
-    ; inverse  = inverseˡ , inverseʳ
-    ; ⁻¹-cong  = cong (-_)
-    }
-  ; comm = +-comm
+  { isGroup = +-0-isGroup
+  ; comm    = +-comm
   }
 
 open Algebra.Properties.AbelianGroup
        (record { isAbelianGroup = +-isAbelianGroup })
   using () renaming (⁻¹-involutive to -‿involutive)
 
+------------------------------------------------------------------------
+-- Properties of _*_
 
--- Distributivity
+*-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
+
+*-identityˡ : LeftIdentity (+ 1) _*_
+*-identityˡ (+ zero ) = refl
+*-identityˡ -[1+  n ] rewrite ℕ.+-right-identity n = refl
+*-identityˡ (+ suc n) rewrite ℕ.+-right-identity n = refl
+
+*-identityʳ : RightIdentity (+ 1) _*_
+*-identityʳ x rewrite
+    𝕊.*-identityʳ (sign x)
+  | ℕ.*-right-identity ∣ x ∣
+  | signₙ◃∣n∣≡n x
+  = refl
+
+*-identity : Identity (+ 1) _*_
+*-identity = *-identityˡ , *-identityʳ
 
 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
+
+*-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 𝕊* 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₂ _*_
+  }
 
-  -- Various lemmas used to prove distributivity.
+*-1-isMonoid : IsMonoid _≡_ _*_ (+ 1)
+*-1-isMonoid = record
+  { isSemigroup = *-isSemigroup
+  ; identity    = *-identity
+  }
 
-  sign-⊖-≱ : ∀ {m n} → m ≱ n → sign (m ⊖ n) ≡ Sign.-
-  sign-⊖-≱ = sign-⊖-< ∘ ℕ.≰⇒>
+*-1-isCommutativeMonoid : IsCommutativeMonoid _≡_ _*_ (+ 1)
+*-1-isCommutativeMonoid = record
+  { isSemigroup = *-isSemigroup
+  ; identityˡ   = *-identityˡ
+  ; comm        = *-comm
+  }
 
-  ∣⊖∣-≱ : ∀ {m n} → m ≱ n → ∣ m ⊖ n ∣ ≡ n ∸ m
-  ∣⊖∣-≱ = ∣⊖∣-< ∘ ℕ.≰⇒>
+*-1-commutativeMonoid : CommutativeMonoid _ _
+*-1-commutativeMonoid = record
+  { Carrier             = ℤ
+  ; _≈_                 = _≡_
+  ; _∙_                 = _*_
+  ; ε                   = + 1
+  ; isCommutativeMonoid = *-1-isCommutativeMonoid
+  }
 
-  ⊖-≱ : ∀ {m n} → m ≱ n → m ⊖ n ≡ - + (n ∸ m)
-  ⊖-≱ = ⊖-< ∘ ℕ.≰⇒>
+------------------------------------------------------------------------
+-- The integers form a commutative ring
 
-  -- Lemmas working around the fact that _◃_ pattern matches on its
-  -- second argument before its first.
+-- Distributivity
 
-  +‿◃ : ∀ n → Sign.+ ◃ n ≡ + n
-  +‿◃ zero    = refl
-  +‿◃ (suc _) = refl
+private
 
-  -‿◃ : ∀ n → Sign.- ◃ n ≡ - + n
-  -‿◃ zero    = refl
-  -‿◃ (suc _) = refl
+  -- lemma used to prove distributivity.
 
   distrib-lemma :
     ∀ a b c → (c ⊖ b) * -[1+ a ] ≡ a ℕ+ b ℕ* suc a ⊖ (a ℕ+ c ℕ* suc a)
@@ -180,35 +343,35 @@ private
     with b ≤? c
   ... | yes b≤c
     rewrite ⊖-≥ b≤c
-          | ⊖-≥ (b≤c *-mono (≤-refl {x = suc a}))
-          | -‿◃ ((c ∸ b) ℕ* suc a)
+          | ⊖-≥ (ℕ.*-mono-≤ b≤c (≤-refl {x = suc a}))
+          | -◃n≡-n ((c ∸ b) ℕ* suc a)
           | ℕ.*-distrib-∸ʳ (suc a) c b
           = refl
   ... | no b≰c
-    rewrite sign-⊖-≱ b≰c
-          | ∣⊖∣-≱ b≰c
-          | +‿◃ ((b ∸ c) ℕ* suc a)
-          | ⊖-≱ (b≰c ∘ ℕ.cancel-*-right-≤ b c a)
+    rewrite sign-⊖-≰ b≰c
+          | ∣⊖∣-≰ b≰c
+          | +◃n≡+n ((b ∸ c) ℕ* suc a)
+          | ⊖-≰ (b≰c ∘ ℕ.cancel-*-right-≤ b c a)
           | -‿involutive (+ (b ℕ* suc a ∸ c ℕ* suc a))
           | ℕ.*-distrib-∸ʳ (suc a) b c
           = refl
 
 distribʳ : _*_ DistributesOverʳ _+_
 
 distribʳ (+ zero) y z
-  rewrite proj₂ *-zero ∣ y ∣
-        | proj₂ *-zero ∣ z ∣
-        | proj₂ *-zero ∣ y + z ∣
+  rewrite ℕ.*-right-zero ∣ y ∣
+        | ℕ.*-right-zero ∣ z ∣
+        | ℕ.*-right-zero ∣ y + z ∣
         = refl
 
 distribʳ x (+ zero) z
-  rewrite proj₁ +-identity z
-        | proj₁ +-identity (sign z S* sign x ◃ ∣ z ∣ ℕ* ∣ x ∣)
+  rewrite +-identityˡ z
+        | +-identityˡ (sign z 𝕊* sign x ◃ ∣ z ∣ ℕ* ∣ x ∣)
         = refl
 
 distribʳ x y (+ zero)
-  rewrite proj₂ +-identity y
-        | proj₂ +-identity (sign y S* sign x ◃ ∣ y ∣ ℕ* ∣ x ∣)
+  rewrite +-identityʳ y
+        | +-identityʳ (sign y 𝕊* sign x ◃ ∣ y ∣ ℕ* ∣ x ∣)
         = refl
 
 distribʳ -[1+ a ] -[1+ b ] -[1+ c ] = cong (+_) $
@@ -245,15 +408,15 @@ distribʳ (+ suc a) -[1+ b ] (+ suc c)
 ... | yes b≤c
   rewrite ⊖-≥ b≤c
         | +-comm (- (+ (a ℕ+ b ℕ* suc a))) (+ (a ℕ+ c ℕ* suc a))
-        | ⊖-≥ (b≤c *-mono ≤-refl {x = suc a})
+        | ⊖-≥ (ℕ.*-mono-≤ b≤c (≤-refl {x = suc a}))
         | ℕ.*-distrib-∸ʳ (suc a) c b
-        | +‿◃ (c ℕ* suc a ∸ b ℕ* suc a)
+        | +◃n≡+n (c ℕ* suc a ∸ b ℕ* suc a)
         = refl
 ... | no b≰c
-  rewrite sign-⊖-≱ b≰c
-        | ∣⊖∣-≱ b≰c
-        | -‿◃ ((b ∸ c) ℕ* suc a)
-        | ⊖-≱ (b≰c ∘ ℕ.cancel-*-right-≤ b c a)
+  rewrite sign-⊖-≰ b≰c
+        | ∣⊖∣-≰ b≰c
+        | -◃n≡-n ((b ∸ c) ℕ* suc a)
+        | ⊖-≰ (b≰c ∘ ℕ.cancel-*-right-≤ b c a)
         | ℕ.*-distrib-∸ʳ (suc a) b c
         = refl
 
@@ -262,29 +425,40 @@ distribʳ (+ suc c) (+ suc a) -[1+ b ]
   with b ≤? a
 ... | yes b≤a
   rewrite ⊖-≥ b≤a
-        | ⊖-≥ (b≤a *-mono ≤-refl {x = suc c})
-        | +‿◃ ((a ∸ b) ℕ* suc c)
+        | ⊖-≥ (ℕ.*-mono-≤ b≤a (≤-refl {x = suc c}))
+        | +◃n≡+n ((a ∸ b) ℕ* suc c)
         | ℕ.*-distrib-∸ʳ (suc c) a b
         = refl
 ... | no b≰a
-  rewrite sign-⊖-≱ b≰a
-        | ∣⊖∣-≱ b≰a
-        | ⊖-≱ (b≰a ∘ ℕ.cancel-*-right-≤ b a c)
-        | -‿◃ ((b ∸ a) ℕ* suc c)
+  rewrite sign-⊖-≰ b≰a
+        | ∣⊖∣-≰ b≰a
+        | ⊖-≰ (b≰a ∘ ℕ.cancel-*-right-≤ b a c)
+        | -◃n≡-n ((b ∸ a) ℕ* suc c)
         | ℕ.*-distrib-∸ʳ (suc c) b a
         = refl
 
--- The IsCommutativeSemiring module contains a proof of
--- distributivity which is used below.
-
 isCommutativeSemiring : IsCommutativeSemiring _≡_ _+_ _*_ (+ 0) (+ 1)
 isCommutativeSemiring = record
-  { +-isCommutativeMonoid = +-isCommutativeMonoid
-  ; *-isCommutativeMonoid = *-isCommutativeMonoid
+  { +-isCommutativeMonoid = +-0-isCommutativeMonoid
+  ; *-isCommutativeMonoid = *-1-isCommutativeMonoid
   ; distribʳ              = distribʳ
   ; zeroˡ                 = λ _ → refl
   }
 
++-*-isRing : IsRing _≡_ _+_ _*_ -_ (+ 0) (+ 1)
++-*-isRing = record
+  { +-isAbelianGroup = +-isAbelianGroup
+  ; *-isMonoid       = *-1-isMonoid
+  ; distrib          = IsCommutativeSemiring.distrib
+                         isCommutativeSemiring
+  }
+
++-*-isCommutativeRing : IsCommutativeRing _≡_ _+_ _*_ -_ (+ 0) (+ 1)
++-*-isCommutativeRing = record
+  { isRing = +-*-isRing
+  ; *-comm = *-comm
+  }
+
 commutativeRing : CommutativeRing _ _
 commutativeRing = record
   { Carrier           = ℤ
@@ -294,15 +468,7 @@ commutativeRing = record
   ; -_                = -_
   ; 0#                = + 0
   ; 1#                = + 1
-  ; isCommutativeRing = record
-    { isRing = record
-      { +-isAbelianGroup = +-isAbelianGroup
-      ; *-isMonoid       = *-isMonoid
-      ; distrib          = IsCommutativeSemiring.distrib
-                             isCommutativeSemiring
-      }
-    ; *-comm = *-comm
-    }
+  ; isCommutativeRing = +-*-isCommutativeRing
   }
 
 import Algebra.RingSolver.Simple as Solver
@@ -313,10 +479,14 @@ module RingSolver =
 ------------------------------------------------------------------------
 -- More properties
 
+-- ∣_∣ commutes with multiplication.
+
+abs-*-commute : Homomorphic₂ ∣_∣ _*_ _ℕ*_
+abs-*-commute i j = abs-◃ _ _
+
 -- Multiplication is right cancellative for non-zero integers.
 
-cancel-*-right : ∀ i j k →
-                 k ≢ + 0 → i * k ≡ j * k → i ≡ j
+cancel-*-right : ∀ i j k → k ≢ + 0 → i * k ≡ j * k → i ≡ j
 cancel-*-right i j k            ≢0 eq with signAbs k
 cancel-*-right i j .(+ 0)       ≢0 eq | s ◂ zero  = contradiction refl ≢0
 cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n
@@ -326,28 +496,28 @@ cancel-*-right i j .(s ◃ suc n) ≢0 eq | s ◂ suc n
          ℕ.cancel-*-right ∣ i ∣ ∣ j ∣ $ abs-cong eq
   where
   sign-i≡sign-j : ∀ i j →
-                  sign i S* s ◃ ∣ i ∣ ℕ* suc n ≡
-                  sign j S* s ◃ ∣ j ∣ ℕ* suc n →
+                  sign i 𝕊* s ◃ ∣ i ∣ ℕ* suc n ≡
+                  sign j 𝕊* s ◃ ∣ j ∣ ℕ* suc n →
                   sign i ≡ sign j
   sign-i≡sign-j i              j              eq with signAbs i | signAbs j
   sign-i≡sign-j .(+ 0)         .(+ 0)         eq | s₁ ◂ zero   | s₂ ◂ zero   = refl
   sign-i≡sign-j .(+ 0)         .(s₂ ◃ suc n₂) eq | s₁ ◂ zero   | s₂ ◂ suc n₂
     with ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂)
   ... | .(suc n₂) | refl
-    with abs-cong {s₁} {sign (s₂ ◃ suc n₂) S* s} {0} {suc n₂ ℕ* suc n} eq
+    with abs-cong {s₁} {sign (s₂ ◃ suc n₂) 𝕊* s} {0} {suc n₂ ℕ* suc n} eq
   ...   | ()
   sign-i≡sign-j .(s₁ ◃ suc n₁) .(+ 0)         eq | s₁ ◂ suc n₁ | s₂ ◂ zero
     with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁)
   ... | .(suc n₁) | refl
-    with abs-cong {sign (s₁ ◃ suc n₁) S* s} {s₁} {suc n₁ ℕ* suc n} {0} eq
+    with abs-cong {sign (s₁ ◃ suc n₁) 𝕊* s} {s₁} {suc n₁ ℕ* suc n} {0} eq
   ...   | ()
   sign-i≡sign-j .(s₁ ◃ suc n₁) .(s₂ ◃ suc n₂) eq | s₁ ◂ suc n₁ | s₂ ◂ suc n₂
     with ∣ s₁ ◃ suc n₁ ∣ | abs-◃ s₁ (suc n₁)
        | sign (s₁ ◃ suc n₁) | sign-◃ s₁ n₁
        | ∣ s₂ ◃ suc n₂ ∣ | abs-◃ s₂ (suc n₂)
        | sign (s₂ ◃ suc n₂) | sign-◃ s₂ n₂
   ... | .(suc n₁) | refl | .s₁ | refl | .(suc n₂) | refl | .s₂ | refl =
-    SignProp.cancel-*-right s₁ s₂ (sign-cong eq)
+    𝕊.cancel-*-right s₁ s₂ (sign-cong eq)
 
 -- Multiplication with a positive number is right cancellative (for
 -- _≤_).
@@ -370,9 +540,9 @@ cancel-*-+-right-≤ (+ suc m)  (+ suc n)  o (+≤+ m≤n) =
 *-+-right-mono _ (-≤+             {n = 0})         = -≤+
 *-+-right-mono _ (-≤+             {n = suc _})     = -≤+
 *-+-right-mono x (-≤-                         n≤m) =
-  -≤- (≤-pred (s≤s n≤m *-mono ≤-refl {x = suc x}))
+  -≤- (≤-pred (ℕ.*-mono-≤ (s≤s n≤m) (≤-refl {x = suc x})))
 *-+-right-mono _ (+≤+ {m = 0}     {n = 0}     m≤n) = +≤+ m≤n
 *-+-right-mono _ (+≤+ {m = 0}     {n = suc _} m≤n) = +≤+ z≤n
 *-+-right-mono _ (+≤+ {m = suc _} {n = 0}     ())
 *-+-right-mono x (+≤+ {m = suc _} {n = suc _} m≤n) =
-  +≤+ (m≤n *-mono ≤-refl {x = suc x})
+  +≤+ ((ℕ.*-mono-≤ m≤n (≤-refl {x = suc x})))

src/Data/Sign/Properties.agda

@@ -9,18 +9,44 @@ module Data.Sign.Properties where
 open import Data.Empty
 open import Function
 open import Data.Sign
+open import Data.Product using (_,_)
 open import Relation.Binary.PropositionalEquality
+open import Algebra.FunctionProperties (_≡_ {A = Sign})
 
 -- The opposite of a sign is not equal to the sign.
 
 opposite-not-equal : ∀ s → s ≢ opposite s
 opposite-not-equal - ()
 opposite-not-equal + ()
 
--- Sign multiplication is right cancellative.
+opposite-cong : ∀ {s t} → opposite s ≡ opposite t → s ≡ t
+opposite-cong { - } { - } refl = refl
+opposite-cong { - } { + } ()
+opposite-cong { + } { - } ()
+opposite-cong { + } { + } refl = refl
 
-cancel-*-right : ∀ s₁ s₂ {s} → s₁ * s ≡ s₂ * s → s₁ ≡ s₂
+------------------------------------------------------------------------
+-- _*_
+
+*-identityˡ : LeftIdentity + _*_
+*-identityˡ _ = refl
+
+*-identityʳ : RightIdentity + _*_
+*-identityʳ - = refl
+*-identityʳ + = refl
+
+*-identity : Identity + _*_
+*-identity = *-identityˡ  , *-identityʳ
+
+cancel-*-right : RightCancellative _*_
 cancel-*-right - - _  = refl
 cancel-*-right - + eq = ⊥-elim (opposite-not-equal _ $ sym eq)
 cancel-*-right + - eq = ⊥-elim (opposite-not-equal _ eq)
 cancel-*-right + + _  = refl
+
+cancel-*-left : LeftCancellative _*_
+cancel-*-left - eq = opposite-cong eq
+cancel-*-left + eq = eq
+
+*-cancellative : Cancellative _*_
+*-cancellative = cancel-*-left , cancel-*-right