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