binomial lemmas for *-commuting elements in a Semiring

CHANGELOG.md

@@ -1685,6 +1685,15 @@ Other minor changes
   middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x)
   semimedial : Semimedial _∙_
   ```
+* Added new proof to `Algebra.Properties.Monoid.Mult`:
+  ```agda
+  ×-congˡ : ∀ {x} → (_× x) Preserves _≡_ ⟶ _≈_
+  ```
+
+* Added new proof to `Algebra.Properties.Monoid.Sum`:
+  ```agda
+  sum-init-last : ∀ {n} (t : Vector _ (suc n)) → sum t ≈ sum (init t) + last t
+  ```
 
 * Added new proofs to `Algebra.Properties.Semigroup`:
   ```agda
@@ -1694,6 +1703,19 @@ Other minor changes
   flexible : Flexible _∙_
   ```
 
+* Added new proofs to `Algebra.Properties.Semiring.Exp`:
+  ```agda
+  ^-congʳ               : (x ^_) Preserves _≡_ ⟶ _≈_
+  y*x^m*y^n≈x^m*y^[n+1] : (x * y ≈ y * x) → y * (x ^ m * y ^ n) ≈ x ^ m * y ^ suc n
+  ```
+
+* Added new proofs to `Algebra.Properties.Semiring.Mult`:
+  ```agda
+  1×-identityʳ : 1 × x ≈ x
+  ×-comm-*    : x * (n × y) ≈ n × (x * y)
+  ×-assoc-*   : (n × x) * y ≈ n × (x * y)
+  ```
+
 * Added new proofs to `Algebra.Properties.Ring`:
   ```agda
   -1*x≈-x : ∀ x → - 1# * x ≈ - x

src/Algebra/Properties/Monoid/Mult.agda

@@ -46,6 +46,9 @@ open import Algebra.Definitions.RawMonoid rawMonoid public
 ×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
 ×-cong {n} P.refl x≈x′ = ×-congʳ n x≈x′
 
+×-congˡ : ∀ {x} → (_× x) Preserves _≡_ ⟶ _≈_
+×-congˡ m≡n = ×-cong m≡n refl
+
 -- _×_ is homomorphic with respect to _ℕ+_/_+_.
 
 ×-homo-+ : ∀ x m n → (m ℕ.+ n) × x ≈ m × x + n × x

src/Algebra/Properties/Monoid/Sum.agda

@@ -31,6 +31,7 @@ open Monoid M
 open import Data.Vec.Functional.Relation.Binary.Equality.Setoid setoid
 open import Algebra.Properties.Monoid.Mult M
 open import Algebra.Definitions _≈_
+open import Relation.Binary.Reasoning.Setoid setoid
 
 ------------------------------------------------------------------------
 -- Definition
@@ -70,3 +71,20 @@ sum-replicate-idem idem n = trans (sum-replicate n) (×-idem idem n)
 sum-replicate-zero : ∀ n → sum {n} (replicate 0#) ≈ 0#
 sum-replicate-zero zero    = refl
 sum-replicate-zero (suc n) = sum-replicate-idem (+-identityˡ 0#) (suc n)
+
+-- When summing over a `Vector`, we can pull out last element
+
+sum-init-last : ∀ {n} (t : Vector Carrier (suc n)) → sum t ≈ sum (init t) + last t
+sum-init-last {zero} t  = begin
+  t₀ + 0# ≈⟨ +-identityʳ t₀ ⟩
+  t₀      ≈˘⟨ +-identityˡ t₀ ⟩
+  0# + t₀ ∎ where t₀ = t zero
+sum-init-last {suc n} t = begin
+  t₀ + ∑t             ≈⟨ +-congˡ (sum-init-last (tail t)) ⟩
+  t₀ + (∑t′ + tₗ)     ≈˘⟨ +-assoc _ _ _ ⟩
+  (t₀ + ∑t′) + tₗ     ∎
+  where
+    t₀ = head t
+    tₗ = last t
+    ∑t = sum (tail t)
+    ∑t′ = sum (tail (init t))

src/Algebra/Properties/Semiring/Exp.agda

@@ -15,7 +15,7 @@ import Data.Nat.Properties as ℕ
 module Algebra.Properties.Semiring.Exp
   {a ℓ} (S : Semiring a ℓ) where
 
-open Semiring S renaming (zero to *-zero)
+open Semiring S
 open import Relation.Binary.Reasoning.Setoid setoid
 import Algebra.Properties.Monoid.Mult *-monoid as Mult
 
@@ -34,10 +34,39 @@ open import Algebra.Definitions.RawSemiring rawSemiring public
 ^-cong : _^_ Preserves₂ _≈_ ⟶ _≡_ ⟶ _≈_
 ^-cong x≈y u≡v = Mult.×-cong u≡v x≈y
 
+^-congʳ : ∀ x → (x ^_) Preserves _≡_ ⟶ _≈_
+^-congʳ x = Mult.×-congˡ
+
 -- xᵐ⁺ⁿ ≈ xᵐxⁿ
 ^-homo-* : ∀ x m n → x ^ (m ℕ.+ n) ≈ (x ^ m) * (x ^ n)
 ^-homo-* = Mult.×-homo-+
 
 -- (xᵐ)ⁿ≈xᵐ*ⁿ
 ^-assocʳ : ∀ x m n → (x ^ m) ^ n ≈ x ^ (m ℕ.* n)
 ^-assocʳ x m n rewrite ℕ.*-comm m n = Mult.×-assocˡ x n m
+
+------------------------------------------------------------------------
+-- A lemma using commutativity, needed for the Binomial Theorem
+
+y*x^m*y^n≈x^m*y^[n+1] : ∀ {x} {y} (x*y≈y*x : x * y ≈ y * x) →
+                        ∀ m n → y * (x ^ m * y ^ n) ≈ x ^ m * y ^ suc n
+y*x^m*y^n≈x^m*y^[n+1] {x} {y} x*y≈y*x = helper
+  where
+    helper : ∀ m n → y * (x ^ m * y ^ n) ≈ x ^ m * y ^ suc n
+    helper zero    n = begin
+      y * (x ^ ℕ.zero * y ^ n)  ≡⟨⟩
+      y * (1# * y ^ n)          ≈⟨ *-congˡ (*-identityˡ (y ^ n)) ⟩
+      y * (y ^ n)               ≡⟨⟩
+      y ^ (suc n)               ≈˘⟨ *-identityˡ (y ^ suc n) ⟩
+      1# * y ^ (suc n)          ≡⟨⟩
+      x ^ ℕ.zero * y ^ (suc n)  ∎
+    helper (suc m) n = begin
+      y * (x ^ suc m * y ^ n)    ≡⟨⟩
+      y * ((x * x ^ m) * y ^ n)  ≈⟨ *-congˡ (*-assoc x (x ^ m) (y ^ n)) ⟩
+      y * (x * (x ^ m * y ^ n))  ≈˘⟨ *-assoc y x (x ^ m * y ^ n) ⟩
+      y * x * (x ^ m * y ^ n)    ≈˘⟨ *-congʳ x*y≈y*x ⟩
+      x * y * (x ^ m * y ^ n)    ≈⟨ *-assoc x y _ ⟩
+      x * (y * (x ^ m * y ^ n))  ≈⟨ *-congˡ (helper m n) ⟩
+      x * (x ^ m * y ^ suc n)    ≈˘⟨ *-assoc x (x ^ m) (y ^ suc n) ⟩
+      (x * x ^ m) * y ^ suc n    ≡⟨⟩
+      x ^ suc m * y ^ suc n      ∎

src/Algebra/Properties/Semiring/Mult.agda

@@ -33,3 +33,30 @@ open import Algebra.Properties.Monoid.Mult +-monoid public
   n × 1# + (m × 1#) * (n × 1#)        ≈˘⟨ +-congʳ (*-identityˡ _) ⟩
   1# * (n × 1#) + (m × 1#) * (n × 1#) ≈˘⟨ distribʳ (n × 1#) 1# (m × 1#) ⟩
   (1# + m × 1#) * (n × 1#)            ∎
+
+-- (1 ×_) is the identity
+
+1×-identityʳ : ∀ x → 1 × x ≈ x
+1×-identityʳ = +-identityʳ
+
+-- (n ×_) commutes with _*_
+
+×-comm-* : ∀ n x y → x * (n × y) ≈ n × (x * y)
+×-comm-* zero    x y = zeroʳ x
+×-comm-* (suc n) x y = begin
+  x * (suc n × y)       ≡⟨⟩
+  x * (y + n × y)       ≈⟨ distribˡ _ _ _ ⟩
+  x * y + x * (n × y)   ≈⟨ +-congˡ (×-comm-* n _ _) ⟩
+  x * y + n × (x * y)   ≡⟨⟩
+  suc n × (x * y)       ∎
+
+-- (n ×_) associates with _*_
+
+×-assoc-* : ∀ n x y → (n × x) * y ≈ n × (x * y)
+×-assoc-* zero x y = zeroˡ y
+×-assoc-* (suc n) x y = begin
+  (suc n × x) * y       ≡⟨⟩
+  (x + n × x) * y       ≈⟨ distribʳ _ _ _ ⟩
+  x * y + (n × x) * y   ≈⟨ +-congˡ (×-assoc-* n _ _) ⟩
+  x * y + n × (x * y)   ≡⟨⟩
+  suc n × (x * y)       ∎