[ re #1752 ] add properties of ordered structures for Nat.

CHANGELOG.md

@@ -18,7 +18,6 @@ Highlights
 
 * Improved the `solve` tactic in `Tactic.RingSolver` to work in a much
   wider range of situations.
-
 Bug-fixes
 ---------
 
@@ -1269,6 +1268,22 @@ Other minor changes
 
   anyUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∃ λ n → n < v × P n)
   allUpTo? : ∀ (P? : U.Decidable P) (v : ℕ) → Dec (∀ {n} → n < v → P n)
+
+  +-isPomagma               : IsPomagma _+_
+  +-isPosemigroup           : IsPosemigroup _+_
+  +-0-isPomonoid            : IsPomonoid _+_ 0
+  +-0-isCommutativePomonoid : IsCommutativePomonoid _+_ 0
+
+  +-0-commutativePomonoid   : CommutativePomonoid 0ℓ 0ℓ 0ℓ
+
+  *-isPomagma               : IsPomagma _≤_ _*_
+  *-isPosemigroup           : IsPosemigroup _≤_ _*_
+  *-1-isPomonoid            : IsPomonoid _≤_ _*_ 1
+  *-1-isCommutativePomonoid : IsCommutativePomonoid _*_ 1
+  +-*-isPosemiring          : IsPosemiring _+_ _*_ 0 1
+
+  *-1-commutativePomonoid   : CommutativePomonoid 0ℓ 0ℓ 0ℓ
+  +-*-posemiring            : Posemiring 0ℓ 0ℓ 0ℓ
   ```
 
 * Added new functions in `Data.Nat`:

src/Algebra/Ordered/Structures.agda

@@ -13,9 +13,9 @@
 open import Relation.Binary.Core using (Rel; _⇒_)
 
 module Algebra.Ordered.Structures
-  {a ℓ₁ ℓ₂} {A : Set a}  -- The underlying set
-  (_≈_ : Rel A ℓ₁)       -- The underlying equality relation
-  (_≤_ : Rel A ℓ₂)       -- The order
+  {a}  {A : Set a}     -- The underlying set
+  {ℓ₁} (_≈_ : Rel A ℓ₁) -- The underlying equality relation
+  {ℓ₂} (_≤_ : Rel A ℓ₂) -- The order
   where
 
 open import Algebra.Core

src/Data/Nat/Properties.agda

@@ -19,6 +19,7 @@ open import Algebra.Construct.NaturalChoice.Base
 import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp
 import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp
 import Algebra.Properties.CommutativeSemigroup as CommSemigroupProperties
+open import Algebra.Ordered.Bundles
 open import Data.Bool.Base using (Bool; false; true; T)
 open import Data.Bool.Properties using (T?)
 open import Data.Empty using (⊥)
@@ -44,6 +45,7 @@ open import Algebra.Definitions {A = ℕ} _≡_
 open import Algebra.Definitions
   using (LeftCancellative; RightCancellative; Cancellative)
 open import Algebra.Structures {A = ℕ} _≡_
+open import Algebra.Ordered.Structures {A = ℕ} _≡_
 
 ------------------------------------------------------------------------
 -- Properties of NonZero
@@ -614,10 +616,6 @@ open ≤-Reasoning
   { isCommutativeMonoid = +-0-isCommutativeMonoid
   }
 
-∸-magma : Magma 0ℓ 0ℓ
-∸-magma = magma _∸_
-
-
 ------------------------------------------------------------------------
 -- Other properties of _+_ and _≡_
 
@@ -732,6 +730,41 @@ m+n≮n (suc m) (suc n) (s<s m+n<n) = m+n≮n m (suc n) (<-step m+n<n)
 m+n≮m : ∀ m n → m + n ≮ m
 m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m)
 
+------------------------------------------------------------------------
+-- Ordered structures for _+_ and _≤_
+
++-isPomagma : IsPomagma _≤_ _+_
++-isPomagma = record
+  { isPartialOrder = ≤-isPartialOrder
+  ; mono           = +-mono-≤
+  }
+
++-isPosemigroup : IsPosemigroup _≤_ _+_
++-isPosemigroup = record
+  { isPomagma = +-isPomagma
+  ; assoc     = +-assoc
+  }
+
++-0-isPomonoid : IsPomonoid _≤_ _+_ 0
++-0-isPomonoid = record
+  { isPosemigroup = +-isPosemigroup
+  ; identity      = +-identity
+  }
+
++-0-isCommutativePomonoid : IsCommutativePomonoid _≤_ _+_ 0
++-0-isCommutativePomonoid = record
+  { isPomonoid = +-0-isPomonoid
+  ; comm       = +-comm
+  }
+
+------------------------------------------------------------------------
+-- Ordered bundles for _+_ and _≤_
+
++-0-commutativePomonoid : CommutativePomonoid 0ℓ 0ℓ 0ℓ
++-0-commutativePomonoid = record
+  { isCommutativePomonoid = +-0-isCommutativePomonoid
+  }
+
 ------------------------------------------------------------------------
 -- Properties of _*_
 ------------------------------------------------------------------------
@@ -1009,6 +1042,56 @@ m<m*n m@(suc m-1) n@(suc (suc n-2)) (s≤s (s≤s _)) = begin-strict
 *-cancel-< : Cancellative _<_ _*_
 *-cancel-< = *-cancelˡ-< , *-cancelʳ-<
 
+------------------------------------------------------------------------
+-- Ordered structures for _*_ and _≤_
+
+*-isPomagma : IsPomagma _≤_ _*_
+*-isPomagma = record
+  { isPartialOrder = ≤-isPartialOrder
+  ; mono           = *-mono-≤
+  }
+
+*-isPosemigroup : IsPosemigroup _≤_ _*_
+*-isPosemigroup = record
+  { isPomagma = *-isPomagma
+  ; assoc     = *-assoc
+  }
+
+*-1-isPomonoid : IsPomonoid _≤_ _*_ 1
+*-1-isPomonoid = record
+  { isPosemigroup = *-isPosemigroup
+  ; identity      = *-identity
+  }
+
+*-1-isCommutativePomonoid : IsCommutativePomonoid _≤_ _*_ 1
+*-1-isCommutativePomonoid = record
+  { isPomonoid = *-1-isPomonoid
+  ; comm       = *-comm
+  }
+
++-*-isPosemiring : IsPosemiring _≤_ _+_ _*_ 0 1
++-*-isPosemiring = record
+  { +-isCommutativePomonoid = +-0-isCommutativePomonoid
+  ; *-mono                  = *-mono-≤
+  ; *-assoc                 = *-assoc
+  ; *-identity              = *-identity
+  ; distrib                 = *-distrib-+
+  ; zero                    = *-zero
+  }
+
+------------------------------------------------------------------------
+-- Ordered bundles for _*_ and _≤_
+
+*-1-commutativePomonoid : CommutativePomonoid 0ℓ 0ℓ 0ℓ
+*-1-commutativePomonoid = record
+  { isCommutativePomonoid = *-1-isCommutativePomonoid
+  }
+
++-*-posemiring : Posemiring 0ℓ 0ℓ 0ℓ
++-*-posemiring = record
+  { isPosemiring = +-*-isPosemiring
+  }
+
 ------------------------------------------------------------------------
 -- Properties of _^_
 ------------------------------------------------------------------------
@@ -1448,6 +1531,9 @@ n∸n≡0 : ∀ n → n ∸ n ≡ 0
 n∸n≡0 zero    = refl
 n∸n≡0 (suc n) = n∸n≡0 n
 
+∸-magma : Magma 0ℓ 0ℓ
+∸-magma = magma _∸_
+
 ------------------------------------------------------------------------
 -- Properties of _∸_ and pred