refactor: introduce Properties module

CHANGELOG.md

@@ -29,22 +29,22 @@ Deprecated names
 
 * In `Data.List.Properties`:
   ```agda
-  sum-++       ↦  Data.Nat.ListAction.sum-++
-  ∈⇒∣product   ↦  Data.Nat.ListAction.∈⇒∣product
-  product≢0    ↦  Data.Nat.ListAction.product≢0
-  ∈⇒≤product   ↦  Data.Nat.ListAction.∈⇒≤product
+  sum-++       ↦  Data.Nat.ListAction.Properties.sum-++
+  ∈⇒∣product   ↦  Data.Nat.ListAction.Properties.∈⇒∣product
+  product≢0    ↦  Data.Nat.ListAction.Properties.product≢0
+  ∈⇒≤product   ↦  Data.Nat.ListAction.Properties.∈⇒≤product
   ```
 
 * In `Data.List.Relation.Binary.Permutation.Propositional.Properties`:
   ```agda
-  sum-↭       ↦  Data.Nat.ListAction.sum-↭
-  product-↭   ↦  Data.Nat.ListAction.product-↭
+  sum-↭       ↦  Data.Nat.ListAction.Properties.sum-↭
+  product-↭   ↦  Data.Nat.ListAction.Properties.product-↭
   ```
 
 New modules
 -----------
 
-* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction`.
+* `Data.List.Base.{sum|product}` and their properties have been lifted out into `Data.Nat.ListAction` and `Data.Nat.ListAction.Properties`.
 
 Additions to existing modules
 -----------------------------

src/Data/List/Base.agda

@@ -590,4 +590,3 @@ product = foldr ℕ._*_ 1
 "Warning: product was deprecated in v2.3.
 Please use Data.Nat.ListAction.product instead."
 #-}
-

src/Data/List/Properties.agda

@@ -1633,12 +1633,12 @@ sum-++ (x ∷ xs) ys = begin
   (x + sum xs) + sum ys  ∎
 {-# WARNING_ON_USAGE sum-++
 "Warning: sum-++ was deprecated in v2.3.
-Please use Data.Nat.SumAndProperties.sum-++ instead."
+Please use Data.Nat.ListAction.Properties.sum-++ instead."
 #-}
 sum-++-commute = sum-++
 {-# WARNING_ON_USAGE sum-++-commute
 "Warning: sum-++-commute was deprecated in v2.0.
-Please use Data.Nat.SumAndProperties.sum-++ instead."
+Please use Data.Nat.ListAction.Properties.sum-++ instead."
 #-}
 
 open import Data.List.Membership.Propositional using (_∈_)
@@ -1649,15 +1649,15 @@ open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
 ∈⇒∣product {ns = m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
 {-# WARNING_ON_USAGE ∈⇒∣product
 "Warning: ∈⇒∣product was deprecated in v2.3.
-Please use Data.Nat.SumAndProperties.∈⇒∣product instead."
+Please use Data.Nat.ListAction.Properties.∈⇒∣product instead."
 #-}
 
 product≢0 : ∀ {ns} → All NonZero ns → NonZero (product ns)
 product≢0 [] = _
 product≢0 {n ∷ ns} (n≢0 ∷ ns≢0) = m*n≢0 n (product ns) {{n≢0}} {{product≢0 ns≢0}}
 {-# WARNING_ON_USAGE product≢0
 "Warning: product≢0 was deprecated in v2.3.
-Please use Data.Nat.SumAndProperties.product≢0 instead."
+Please use Data.Nat.ListAction.Properties.product≢0 instead."
 #-}
 
 ∈⇒≤product : ∀ {n ns} → All NonZero ns → n ∈ ns → n ≤ product ns
@@ -1667,5 +1667,5 @@ Please use Data.Nat.SumAndProperties.product≢0 instead."
   m≤n⇒m≤o*n n {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
 {-# WARNING_ON_USAGE ∈⇒≤product
 "Warning: ∈⇒≤product was deprecated in v2.3.
-Please use Data.Nat.SumAndProperties.∈⇒≤product instead."
+Please use Data.Nat.ListAction.Properties.∈⇒≤product instead."
 #-}

src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda

@@ -400,7 +400,7 @@ mapMaybe-↭ f = catMaybes-↭ ∘ map⁺ f
 
 -- Version 2.3
 
-import Data.Nat.ListAction as ℕ
+import Data.Nat.ListAction.Properties as ℕ
 
 sum-↭ = ℕ.sum-↭
 {-# WARNING_ON_USAGE sum-↭

src/Data/Nat/ListAction.agda

@@ -11,29 +11,8 @@
 
 module Data.Nat.ListAction where
 
-open import Algebra.Bundles using (CommutativeMonoid)
 open import Data.List.Base using (List; []; _∷_; _++_; foldr)
-open import Data.List.Membership.Propositional using (_∈_)
-open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ)
-open import Data.List.Relation.Binary.Permutation.Setoid.Properties
-  using (foldr-commMonoid)
-open import Data.List.Relation.Unary.All using (All; []; _∷_)
-open import Data.List.Relation.Unary.Any using (here; there)
-open import Data.Nat.Base using (ℕ; _+_; _*_; NonZero; _≤_)
-open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
-open import Data.Nat.Properties
-  using (+-assoc; *-assoc; *-identityˡ; m*n≢0; m≤m*n; m≤n⇒m≤o*n;
-         +-0-commutativeMonoid; *-1-commutativeMonoid)
-open import Relation.Binary.Core using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; sym; cong)
-open import Relation.Binary.PropositionalEquality.Properties
-  using (module ≡-Reasoning)
-
-private
-  variable
-    m n : ℕ
-    ms ns : List ℕ
+open import Data.Nat.Base using (ℕ; _+_; _*_)
 
 
 ------------------------------------------------------------------------
@@ -44,47 +23,3 @@ sum = foldr _+_ 0
 
 product : List ℕ → ℕ
 product = foldr _*_ 1
-
-------------------------------------------------------------------------
--- Properties
-
--- sum
-
-sum-++ : ∀ ms ns → sum (ms ++ ns) ≡ sum ms + sum ns
-sum-++ []       ns = refl
-sum-++ (m ∷ ms) ns = begin
-  m + sum (ms ++ ns)     ≡⟨ cong (m +_) (sum-++ ms ns) ⟩
-  m + (sum ms + sum ns)  ≡⟨ +-assoc m _ _ ⟨
-  (m + sum ms) + sum ns  ∎
-  where open ≡-Reasoning
-
-sum-↭ : sum Preserves _↭_ ⟶ _≡_
-sum-↭ p = foldr-commMonoid ℕ-+-0.setoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p)
-  where module ℕ-+-0 = CommutativeMonoid +-0-commutativeMonoid
-
-
--- product
-
-product-++ : ∀ ms ns → product (ms ++ ns) ≡ product ms * product ns
-product-++ []       ns = sym (*-identityˡ _)
-product-++ (m ∷ ms) ns = begin
-  m * product (ms ++ ns)         ≡⟨ cong (m *_) (product-++ ms ns) ⟩
-  m * (product ms * product ns)  ≡⟨ *-assoc m _ _ ⟨
-  (m * product ms) * product ns  ∎
-  where open ≡-Reasoning
-
-∈⇒∣product : n ∈ ns → n ∣ product ns
-∈⇒∣product {ns = n ∷ ns} (here  refl) = m∣m*n (product ns)
-∈⇒∣product {ns = m ∷ ns} (there n∈ns) = ∣n⇒∣m*n m (∈⇒∣product n∈ns)
-
-product≢0 : All NonZero ns → NonZero (product ns)
-product≢0 []           = _
-product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}}
-
-∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
-∈⇒≤product (n≢0 ∷ ns≢0) (here refl)  = m≤m*n _ _ {{product≢0 ns≢0}}
-∈⇒≤product (n≢0 ∷ ns≢0) (there n∈ns) = m≤n⇒m≤o*n _ {{n≢0}} (∈⇒≤product ns≢0 n∈ns)
-
-product-↭ : product Preserves _↭_ ⟶ _≡_
-product-↭ p = foldr-commMonoid ℕ-*-1.setoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
-  where module ℕ-*-1 = CommutativeMonoid *-1-commutativeMonoid

src/Data/Nat/Primality.agda

@@ -13,8 +13,9 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
 open import Data.Nat.GCD using (module GCD; module Bézout)
+open import Data.Nat.ListAction using (product)
+open import Data.Nat.ListAction.Properties using (product≢0)
 open import Data.Nat.Properties
-open import Data.Nat.ListAction using (product; product≢0)
 open import Data.Product.Base using (∃-syntax; _×_; map₂; _,_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (flip; _∘_; _∘′_)

src/Data/Nat/Primality/Factorisation.agda

@@ -14,10 +14,11 @@ open import Data.Nat.Divisibility
         divides)
 open import Data.Nat.Properties
 open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
+open import Data.Nat.ListAction using (product)
+open import Data.Nat.ListAction.Properties using (product-↭)
 open import Data.Nat.Primality
   using (Prime; _Rough_; rough∧square>⇒prime; ∤⇒rough-suc; rough∧∣⇒rough; rough∧∣⇒prime;
          2-rough; euclidsLemma; prime⇒irreducible; ¬prime[1]; productOfPrimes≥1; prime⇒nonZero)
-open import Data.Nat.ListAction using (product; product-↭)
 open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
 open import Data.List.Base using (List; []; _∷_; _++_)
 open import Data.List.Membership.Propositional using (_∈_)