More distributivity properties for nats (#2833)

* More distributivity properties for nats

* Simplify proof using existing lemma

* Use lemma instead of refl

In principle this lets us translate more easily to an arbitrary semiring

Author: Taneb

CHANGELOG.md

@@ -72,10 +72,18 @@ Additions to existing modules
   ≟-≢          : (i≢j : i ≢ j) → (i ≟ j) ≡ no i≢j
   ```
 
+* In `Data.Nat.ListAction.Properties`
+  ```agda
+  *-distribˡ-sum : ∀ m ns → m * sum ns ≡ sum (map (m *_) ns)
+  *-distribʳ-sum : ∀ m ns → sum ns * m ≡ sum (map (_* m) ns)
+  ^-distribʳ-product : ∀ m ns → product ns ^ m ≡ product (map (_^ m) ns)
+  ```
+
 * In `Data.Nat.Properties`:
   ```agda
   ≟-≢   : (m≢n : m ≢ n) → (m ≟ n) ≡ no m≢n
   ∸-suc : m ≤ n → suc n ∸ m ≡ suc (n ∸ m)
+  ^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m
   ```
 
 * In `Data.Vec.Properties`:

src/Data/Nat/ListAction/Properties.agda

@@ -12,23 +12,25 @@
 module Data.Nat.ListAction.Properties where
 
 open import Algebra.Bundles using (CommutativeMonoid)
-open import Data.List.Base using (List; []; _∷_; _++_)
+open import Data.List.Base using (List; []; _∷_; _++_; map)
 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.Base using (ℕ; _+_; _*_; _^_; NonZero; _≤_)
 open import Data.Nat.Divisibility using (_∣_; m∣m*n; ∣n⇒∣m*n)
 open import Data.Nat.ListAction using (sum; product)
 open import Data.Nat.Properties
   using (+-assoc; *-assoc; *-identityˡ; m*n≢0; m≤m*n; m≤n⇒m≤o*n
-        ; +-0-commutativeMonoid; *-1-commutativeMonoid)
+        ; +-0-commutativeMonoid; *-1-commutativeMonoid
+        ; *-zeroˡ; *-zeroʳ; *-distribˡ-+; *-distribʳ-+
+        ; ^-zeroˡ; ^-distribʳ-*)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; refl; sym; cong)
+  using (_≡_; refl; sym; trans; cong)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 
@@ -51,6 +53,14 @@ sum-++ (m ∷ ms) ns = begin
   (m + sum ms) + sum ns  ∎
   where open ≡-Reasoning
 
+*-distribˡ-sum : ∀ m ns → m * sum ns ≡ sum (map (m *_) ns)
+*-distribˡ-sum m [] = *-zeroʳ m
+*-distribˡ-sum m (n ∷ ns) = trans (*-distribˡ-+ m n (sum ns)) (cong (m * n +_) (*-distribˡ-sum m ns))
+
+*-distribʳ-sum : ∀ m ns → sum ns * m ≡ sum (map (_* m) ns)
+*-distribʳ-sum m [] = *-zeroˡ m
+*-distribʳ-sum m (n ∷ ns) = trans (*-distribʳ-+ m n (sum ns)) (cong (n * m +_) (*-distribʳ-sum m ns))
+
 sum-↭ : sum Preserves _↭_ ⟶ _≡_
 sum-↭ p = foldr-commMonoid ℕ-+-0.setoid ℕ-+-0.isCommutativeMonoid (↭⇒↭ₛ p)
   where module ℕ-+-0 = CommutativeMonoid +-0-commutativeMonoid
@@ -78,6 +88,10 @@ product≢0 (n≢0 ∷ ns≢0) = m*n≢0 _ _ {{n≢0}} {{product≢0 ns≢0}}
 ∈⇒≤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)
 
+^-distribʳ-product : ∀ m ns → product ns ^ m ≡ product (map (_^ m) ns)
+^-distribʳ-product m [] = ^-zeroˡ m
+^-distribʳ-product m (n ∷ ns) = trans (^-distribʳ-* m n (product ns)) (cong (n ^ m *_) (^-distribʳ-product m ns))
+
 product-↭ : product Preserves _↭_ ⟶ _≡_
 product-↭ p = foldr-commMonoid ℕ-*-1.setoid ℕ-*-1.isCommutativeMonoid (↭⇒↭ₛ p)
   where module ℕ-*-1 = CommutativeMonoid *-1-commutativeMonoid

src/Data/Nat/Properties.agda

@@ -1067,6 +1067,13 @@ m<n⇒m<o*n = m≤n⇒m≤o*n
   m * ((m ^ n) * (m ^ o)) ≡⟨ sym (*-assoc m _ _) ⟩
   (m * (m ^ n)) * (m ^ o) ∎
 
+^-distribʳ-* : ∀ m n o → (n * o) ^ m ≡ n ^ m * o ^ m
+^-distribʳ-* zero n o = sym (*-identityˡ 1)
+^-distribʳ-* (suc m) n o = begin-equality
+  (n * o) * (n * o) ^ m     ≡⟨ cong (n * o *_) (^-distribʳ-* m n o) ⟩
+  (n * o) * (n ^ m * o ^ m) ≡⟨ [m*n]*[o*p]≡[m*o]*[n*p] n o (n ^ m) (o ^ m) ⟩
+  n ^ suc m * o ^ suc m     ∎
+
 ^-semigroup-morphism : ∀ {n} → (n ^_) Is +-semigroup -Semigroup⟶ *-semigroup
 ^-semigroup-morphism = record
   { ⟦⟧-cong = cong (_ ^_)