Introduce Semiring and refactor finite sums (#1042)

* introduce semiring

* refactor CommSemiring

* Semiring import boilerplate

* more boilerplate

* boilerplate, show that a comm semiring is a semiring

* refactor, use new CommSemiring constructor

* boilerplate: forget structure

* fix name

* Semiring: reexport better names

* another constructor for semiring

* move sum to semiring

* oops

* remove makeCommSemiring

Cubical/Algebra/CommSemiring/Base.agda

@@ -6,6 +6,7 @@ open import Cubical.Foundations.SIP using (TypeWithStr)
 
 open import Cubical.Algebra.CommMonoid
 open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Semiring.Base
 
 private
   variable
@@ -15,22 +16,10 @@ record IsCommSemiring {R : Type ℓ}
                   (0r 1r : R) (_+_ _·_ : R → R → R) : Type ℓ where
 
   field
-    +IsCommMonoid  : IsCommMonoid 0r _+_
-    ·IsCommMonoid  : IsCommMonoid 1r _·_
-    ·LDist+        : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
-    AnnihilL       : (x : R) → 0r · x ≡ 0r
-
-  open IsCommMonoid +IsCommMonoid public
-    renaming
-      ( isSemigroup to +IsSemigroup
-      ; isMonoid    to +IsMonoid)
-
-  open IsCommMonoid ·IsCommMonoid public
-    renaming
-      ( isSemigroup to ·IsSemigroup
-      ; isMonoid    to ·IsMonoid)
-    hiding
-      ( is-set ) -- We only want to export one proof of this
+    isSemiring : IsSemiring 0r 1r _+_ _·_
+    ·Comm : (x y : R) → x · y ≡ y · x
+
+  open IsSemiring isSemiring public
 
 record CommSemiringStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
 
@@ -48,3 +37,28 @@ record CommSemiringStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
 
 CommSemiring : ∀ ℓ → Type (ℓ-suc ℓ)
 CommSemiring ℓ = TypeWithStr ℓ CommSemiringStr
+
+makeIsCommSemiring : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R}
+                 (is-setR : isSet R)
+                 (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
+                 (+IdR : (x : R) → x + 0r ≡ x)
+                 (+Comm : (x y : R) → x + y ≡ y + x)
+                 (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
+                 (·IdR : (x : R) → x · 1r ≡ x)
+                 (·DistR+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
+                 (AnnihilL : (x : R) → 0r · x ≡ 0r)
+                 (·Comm : (x y : R) → x · y ≡ y · x)
+               → IsCommSemiring 0r 1r _+_ _·_
+makeIsCommSemiring {_+_ = _+_} {_·_ = _·_}
+  is-setR +Assoc +IdR +Comm ·Assoc ·IdR ·DistR+ AnnihilL ·Comm = x
+  where x : IsCommSemiring _ _ _ _
+        IsCommSemiring.isSemiring x =
+          makeIsSemiring
+            is-setR +Assoc +IdR +Comm ·Assoc
+            ·IdR (λ x → ·Comm _ x ∙ (·IdR x))
+            ·DistR+ (λ x y z → (x + y) · z       ≡⟨ ·Comm (x + y) z ⟩
+                               z · (x + y)       ≡⟨ ·DistR+ z x y ⟩
+                               (z · x) + (z · y) ≡[ i ]⟨ (·Comm z x i + ·Comm z y i) ⟩
+                               (x · z) + (y · z) ∎ )
+            ( λ x → ·Comm x _ ∙ AnnihilL x) AnnihilL
+        IsCommSemiring.·Comm x = ·Comm

Cubical/Algebra/CommSemiring/Instances/UpperNat.agda

@@ -186,16 +186,25 @@ module ConstructionBounded where
 
 
   asCommSemiring : CommSemiring (ℓ-suc ℓ-zero)
-  fst asCommSemiring = ℕ↑b
-  CommSemiringStr.0r (snd asCommSemiring) = 0↑
-  CommSemiringStr.1r (snd asCommSemiring) = OrderedCommMonoidStr.ε (snd ℕ↑-·b)
-  CommSemiringStr._+_ (snd asCommSemiring) = _+_
-  CommSemiringStr._·_ (snd asCommSemiring) = _·_
-  IsCommSemiring.+IsCommMonoid (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
-    OrderedCommMonoidStr.isCommMonoid (snd ℕ↑-+b)
-  IsCommSemiring.·IsCommMonoid (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
-    OrderedCommMonoidStr.isCommMonoid (snd ℕ↑-·b)
-  IsCommSemiring.·LDist+ (CommSemiringStr.isCommSemiring (snd asCommSemiring)) =
-    λ x y z → Σ≡Prop (λ s → PropCompletion.isPropIsBounded ℓ-zero ℕ≤+ s)
-                     (ConstructionUnbounded.+LDist· (fst x) (fst y) (fst z))
-  IsCommSemiring.AnnihilL (CommSemiringStr.isCommSemiring (snd asCommSemiring)) = AnnihilL
+  asCommSemiring .fst = ℕ↑b
+  asCommSemiring .snd = str
+    where
+      module CS = CommSemiringStr
+      open IsCommMonoid
+      +IsCM = OrderedCommMonoidStr.isCommMonoid (snd ℕ↑-+b)
+      ·IsCM = OrderedCommMonoidStr.isCommMonoid (snd ℕ↑-·b)
+
+      str : CommSemiringStr ℕ↑b
+      CS.0r str = 0↑
+      CS.1r str = OrderedCommMonoidStr.ε (snd ℕ↑-·b)
+      CS._+_ str = _+_
+      CS._·_ str = _·_
+      CS.isCommSemiring str =
+        makeIsCommSemiring
+          (is-set +IsCM)
+          (·Assoc +IsCM) (·IdR +IsCM) (·Comm +IsCM)
+          (·Assoc ·IsCM) (·IdR ·IsCM)
+          (λ x y z → Σ≡Prop (λ s → PropCompletion.isPropIsBounded ℓ-zero ℕ≤+ s)
+                     (ConstructionUnbounded.+LDist· (fst x) (fst y) (fst z)))
+          AnnihilL
+          (·Comm ·IsCM)

Cubical/Algebra/Ring/BigOps.agda

@@ -13,79 +13,24 @@ open import Cubical.Data.Sigma
 open import Cubical.Data.FinData
 
 open import Cubical.Algebra.Monoid.BigOp
+import Cubical.Algebra.Semiring.BigOps as Semiring
 open import Cubical.Algebra.Ring.Base
 open import Cubical.Algebra.Ring.Properties
 
 private
   variable
     ℓ ℓ' : Level
 
-module KroneckerDelta (R' : Ring ℓ) where
- private
-  R = fst R'
- open RingStr (snd R')
-
- δ : {n : ℕ} (i j : Fin n) → R
- δ i j = if i == j then 1r else 0r
-
+module KroneckerDelta (R : Ring ℓ) where
+  δ = Semiring.KroneckerDelta.δ (Ring→Semiring R)
 
+module Sum (R : Ring ℓ) where
+  open Semiring.Sum (Ring→Semiring R) public
+  open RingStr (snd R)
+  open RingTheory R
 
-module Sum (R' : Ring ℓ) where
- private
-  R = fst R'
- open RingStr (snd R')
- open MonoidBigOp (Ring→AddMonoid R')
- open RingTheory R'
- open KroneckerDelta R'
-
- ∑ = bigOp
- ∑Ext = bigOpExt
- ∑0r = bigOpε
- ∑Last = bigOpLast
-
- ∑Split : ∀ {n} → (V W : FinVec R n) → ∑ (λ i → V i + W i) ≡ ∑ V + ∑ W
- ∑Split = bigOpSplit +Comm
-
- ∑Split++ : ∀ {n m : ℕ} (V : FinVec R n) (W : FinVec R m)
-          → ∑ (V ++Fin W) ≡ ∑ V + ∑ W
- ∑Split++ = bigOpSplit++ +Comm
-
- ∑Mulrdist : ∀ {n} → (x : R) → (V : FinVec R n)
-                → x · ∑ V ≡ ∑ λ i → x · V i
- ∑Mulrdist {n = zero}  x _ = 0RightAnnihilates x
- ∑Mulrdist {n = suc n} x V =
-   x · (V zero + ∑ (V ∘ suc))           ≡⟨ ·DistR+ _ _ _ ⟩
-   x · V zero + x · ∑ (V ∘ suc)         ≡⟨ (λ i → x · V zero + ∑Mulrdist x (V ∘ suc) i) ⟩
-   x · V zero + ∑ (λ i → x · V (suc i)) ∎
-
- ∑Mulldist : ∀ {n} → (x : R) → (V : FinVec R n)
-                → (∑ V) · x ≡ ∑ λ i → V i · x
- ∑Mulldist {n = zero}  x _ = 0LeftAnnihilates x
- ∑Mulldist {n = suc n} x V =
-   (V zero + ∑ (V ∘ suc)) · x           ≡⟨ ·DistL+ _ _ _ ⟩
-   V zero · x + (∑ (V ∘ suc)) · x       ≡⟨ (λ i → V zero · x + ∑Mulldist x (V ∘ suc) i) ⟩
-   V zero · x + ∑ (λ i → V (suc i) · x) ∎
-
- ∑Mulr0 : ∀ {n} → (V : FinVec R n) → ∑ (λ i → V i · 0r) ≡ 0r
- ∑Mulr0 V = sym (∑Mulldist 0r V) ∙ 0RightAnnihilates _
-
- ∑Mul0r : ∀ {n} → (V : FinVec R n) → ∑ (λ i → 0r · V i) ≡ 0r
- ∑Mul0r V = sym (∑Mulrdist 0r V) ∙ 0LeftAnnihilates _
-
- ∑Mulr1 : (n : ℕ) (V : FinVec R n) → (j : Fin n) → ∑ (λ i → V i · δ i j) ≡ V j
- ∑Mulr1 (suc n) V zero = (λ k → ·IdR (V zero) k + ∑Mulr0 (V ∘ suc) k) ∙ +IdR (V zero)
- ∑Mulr1 (suc n) V (suc j) =
-    (λ i → 0RightAnnihilates (V zero) i + ∑ (λ x → V (suc x) · δ x j))
-    ∙∙ +IdL _ ∙∙ ∑Mulr1 n (V ∘ suc) j
-
- ∑Mul1r : (n : ℕ) (V : FinVec R n) → (j : Fin n) → ∑ (λ i → (δ j i) · V i) ≡ V j
- ∑Mul1r (suc n) V zero = (λ k → ·IdL (V zero) k + ∑Mul0r (V ∘ suc) k) ∙ +IdR (V zero)
- ∑Mul1r (suc n) V (suc j) =
-   (λ i → 0LeftAnnihilates (V zero) i + ∑ (λ i → (δ j i) · V (suc i)))
-   ∙∙ +IdL _ ∙∙ ∑Mul1r n (V ∘ suc) j
-
- ∑Dist- : ∀ {n : ℕ} (V : FinVec R n) → ∑ (λ i → - V i) ≡ - ∑ V
- ∑Dist- V = ∑Ext (λ i → -IsMult-1 (V i)) ∙ sym (∑Mulrdist _ V) ∙ sym (-IsMult-1 _)
+  ∑Dist- : ∀ {n : ℕ} (V : FinVec (fst R) n) → ∑ (λ i → - V i) ≡ - ∑ V
+  ∑Dist- V = ∑Ext (λ i → -IsMult-1 (V i)) ∙ sym (∑Mulrdist _ V) ∙ sym (-IsMult-1 _)
 
 module SumMap
   (Ar@(A , Astr) : Ring ℓ)

Cubical/Algebra/Ring/Properties.agda

@@ -15,9 +15,11 @@ open import Cubical.Foundations.Path
 open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.CommMonoid
 open import Cubical.Algebra.Ring.Base
 open import Cubical.Algebra.Group
 open import Cubical.Algebra.AbGroup.Base
+open import Cubical.Algebra.Semiring.Base
 
 open import Cubical.HITs.PropositionalTruncation
 
@@ -158,6 +160,15 @@ module RingTheory (R' : Ring ℓ) where
   ·-assoc2 : (x y z w : R) → (x · y) · (z · w) ≡ x · (y · z) · w
   ·-assoc2 x y z w = ·Assoc (x · y) z w ∙ cong (_· w) (sym (·Assoc x y z))
 
+Ring→Semiring : Ring ℓ → Semiring ℓ
+Ring→Semiring R =
+  let open RingStr (snd R)
+      open RingTheory R
+  in SemiringFromMonoids (fst R) 0r 1r _+_ _·_
+       (CommMonoidStr.isCommMonoid (snd (AbGroup→CommMonoid (Ring→AbGroup R))))
+       (MonoidStr.isMonoid (snd (Ring→MultMonoid R)))
+       ·DistR+ ·DistL+
+       0RightAnnihilates 0LeftAnnihilates
 
 module RingHoms where
   open IsRingHom

Cubical/Algebra/Semiring.agda

@@ -0,0 +1,4 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Semiring where
+
+open import Cubical.Algebra.Semiring.Base public

Cubical/Algebra/Semiring/Base.agda

@@ -0,0 +1,124 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.Semiring.Base where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.SIP using (TypeWithStr)
+
+open import Cubical.Algebra.CommMonoid
+open import Cubical.Algebra.Monoid
+
+private
+  variable
+    ℓ ℓ' : Level
+
+record IsSemiring {R : Type ℓ}
+                  (0r 1r : R) (_+_ _·_ : R → R → R) : Type ℓ where
+
+  field
+    +IsCommMonoid  : IsCommMonoid 0r _+_
+    ·IsMonoid      : IsMonoid 1r _·_
+    ·DistR+        : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z)
+    ·DistL+        : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z)
+    AnnihilL       : (x : R) → 0r · x ≡ 0r
+    AnnihilR       : (x : R) → x · 0r ≡ 0r
+
+  open IsCommMonoid +IsCommMonoid public
+    renaming
+      ( isSemigroup to +IsSemigroup
+      ; isMonoid    to +IsMonoid
+      ; ·Comm       to +Comm
+      ; ·Assoc      to +Assoc
+      ; ·IdR        to +IdR
+      ; ·IdL        to +IdL)
+
+  open IsMonoid ·IsMonoid public
+    renaming
+      ( isSemigroup to ·IsSemigroup )
+    hiding
+      ( is-set ) -- We only want to export one proof of this
+
+record SemiringStr (A : Type ℓ) : Type (ℓ-suc ℓ) where
+
+  field
+    0r      : A
+    1r      : A
+    _+_     : A → A → A
+    _·_     : A → A → A
+    isSemiring  : IsSemiring 0r 1r _+_ _·_
+
+  infixl 7 _·_
+  infixl 6 _+_
+
+  open IsSemiring isSemiring public
+
+Semiring : ∀ ℓ → Type (ℓ-suc ℓ)
+Semiring ℓ = TypeWithStr ℓ SemiringStr
+
+makeIsSemiring : {R : Type ℓ} {0r 1r : R} {_+_ _·_ : R → R → R}
+                 (is-setR : isSet R)
+                 (+Assoc : (x y z : R) → x + (y + z) ≡ (x + y) + z)
+                 (+IdR : (x : R) → x + 0r ≡ x)
+                 (+Comm : (x y : R) → x + y ≡ y + x)
+                 (·Assoc : (x y z : R) → x · (y · z) ≡ (x · y) · z)
+                 (·IdR : (x : R) → x · 1r ≡ x)
+                 (·IdL : (x : R) → 1r · x ≡ x)
+                 (·LDist+ : (x y z : R) → x · (y + z) ≡ (x · y) + (x · z))
+                 (·RDist+ : (x y z : R) → (x + y) · z ≡ (x · z) + (y · z))
+                 (AnnihilR : (x : R) → x · 0r ≡ 0r)
+                 (AnnihilL : (x : R) → 0r · x ≡ 0r)
+               → IsSemiring 0r 1r _+_ _·_
+makeIsSemiring is-setR +Assoc +IdR +Comm ·Assoc ·IdR ·IdL ·DistR+ ·DistL+ AnnihilR AnnihilL
+  = isSR
+  where module IS = IsSemiring
+        isSR : IsSemiring _ _ _ _
+        IS.+IsCommMonoid isSR = makeIsCommMonoid is-setR +Assoc +IdR +Comm
+        IS.·IsMonoid isSR = makeIsMonoid is-setR ·Assoc ·IdR ·IdL
+        IS.·DistR+ isSR = ·DistR+
+        IS.·DistL+ isSR = ·DistL+
+        IS.AnnihilL isSR = AnnihilL
+        IS.AnnihilR isSR = AnnihilR
+
+SemiringFromMonoids :
+  (S : Type ℓ)
+  (0r 1r : S) (_+_ _·_ : S → S → S)
+  (+CommMonoid : IsCommMonoid 0r _+_)
+  (·Monoiod : IsMonoid 1r _·_)
+  (·LDist+ : (x y z : S) → x · (y + z) ≡ (x · y) + (x · z))
+  (·RDist+ : (x y z : S) → (x + y) · z ≡ (x · z) + (y · z))
+  (AnnihilR : (x : S) → x · 0r ≡ 0r)
+  (AnnihilL : (x : S) → 0r · x ≡ 0r)
+  → Semiring ℓ
+SemiringFromMonoids
+  S 0r 1r _+_ _·_
+  +CommMonoid ·Monoid
+  ·LDist+ ·RDist+
+  AnnihilR AnnihilL
+  = S , str
+  where module SR = SemiringStr
+        module + = IsCommMonoid +CommMonoid
+        open IsMonoid ·Monoid
+
+        str : SemiringStr S
+        SR.0r str = 0r
+        SR.1r str = 1r
+        SR._+_ str = _+_
+        SR._·_ str = _·_
+        SR.isSemiring str =
+          makeIsSemiring
+            +.is-set +.·Assoc +.·IdR +.·Comm
+            ·Assoc ·IdR ·IdL
+            ·LDist+ ·RDist+
+            AnnihilR AnnihilL
+
+
+Semiring→CommMonoid : Semiring ℓ → CommMonoid ℓ
+Semiring→CommMonoid S .fst = fst S
+Semiring→CommMonoid S .snd = commMonoidStr
+ where
+   open CommMonoidStr
+   +CM = IsSemiring.+IsCommMonoid (SemiringStr.isSemiring (snd S))
+
+   commMonoidStr : CommMonoidStr (fst S)
+   ε commMonoidStr = _
+   _·_ commMonoidStr = _
+   isCommMonoid commMonoidStr = +CM