{-# OPTIONS --safe #-}
module Cubical.Algebra.Semiring.BigOps where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Function

open import Cubical.Data.Nat using (; zero; suc)
open import Cubical.Data.FinData
open import Cubical.Data.Bool using (if_then_else_)

open import Cubical.Algebra.Semiring.Base
open import Cubical.Algebra.CommMonoid
open import Cubical.Algebra.Monoid
open import Cubical.Algebra.Monoid.BigOp

private variable
   ℓ' : Level


module KroneckerDelta (S : Semiring ) where
  open SemiringStr (snd S)

  δ : {n : } (i j : Fin n)  fst S
  δ i j = if i == j then 1r else 0r


module Sum (S : Semiring ) where
  open MonoidBigOp (CommMonoid→Monoid (Semiring→CommMonoid S))
  open SemiringStr (snd S)
  open KroneckerDelta S

   : {n : }  FinVec (fst S) n  (fst S)
   = bigOp

  ∑Ext = bigOpExt
  ∑0r = bigOpε
  ∑Last = bigOpLast

  ∑Split :  {n}  (V W : FinVec (fst S) n)    i  V i + W i)   V +  W
  ∑Split = bigOpSplit +Comm

  ∑Split++ :  {n m : } (V : FinVec (fst S) n) (W : FinVec (fst S) m)
            (V ++Fin W)   V +  W
  ∑Split++ = bigOpSplit++

  ∑Mulrdist :  {n}  (x : fst S)  (V : FinVec (fst S) n)
                  x ·  V   λ i  x · V i
  ∑Mulrdist {n = zero}  x _ = AnnihilR 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 : (fst S))  (V : FinVec (fst S) n)
                  ( V) · x   λ i  V i · x
  ∑Mulldist {n = zero}  x _ = AnnihilL 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 (fst S) n)    i  V i · 0r)  0r
  ∑Mulr0 V = sym (∑Mulldist 0r V)  AnnihilR _

  ∑Mul0r :  {n}  (V : FinVec (fst S) n)    i  0r · V i)  0r
  ∑Mul0r V = sym (∑Mulrdist 0r V)  AnnihilL _

  ∑Mulr1 : (n : ) (V : FinVec (fst S) 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  AnnihilR (V zero) i +   x  V (suc x) · δ x j))
     ∙∙ +IdL _ ∙∙ ∑Mulr1 n (V  suc) j

  ∑Mul1r : (n : ) (V : FinVec (fst S) 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  AnnihilL (V zero) i +   i  (δ j i) · V (suc i)))
    ∙∙ +IdL _ ∙∙ ∑Mul1r n (V  suc) j