\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Data.Array
\import Function.Meta
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set.Fin

\class Semiring \extends AbMonoid, Monoid {
  | ldistr {x y z : E} : x * (y + z) = x * y + x * z
  | rdistr {x y z : E} : (x + y) * z = x * z + y * z
  | zro_*-left {x : E} : zro * x = zro
  | zro_*-right {x : E} : x * zro = zro

  | natCoef : Nat -> E
  \default natCoef \as natCoefImpl n \with {
    |  => zro
    | suc n => natCoefImpl n + ide
  }
  | natCoefZero : natCoef  = zro
  \default natCoefZero \as natCoefZeroImpl : natCoefImpl  = zro => idp
  | natCoefSuc (n : Nat) : natCoef (suc n) = natCoef n + ide
  \default natCoefSuc \as natCoefSucImpl n : natCoefImpl (suc n) = natCoefImpl n + ide => idp

  \lemma zero-div {x : E} : LDiv x   \cowith
    | inv-right => zro_*-right

  \lemma ldiv=0 {x y : E} (l : LDiv x y) (p : x = ) : y = 
    => Paths.inv l.inv-right *> pmap (`* _) p *> zro_*-left

  \lemma ldiv/=0 {x y : E} (y/=0 : y /= ) (x|y : LDiv x y) : x /= 
    => \lam x=0 => y/=0 (ldiv=0 x|y x=0)

  \func LDiv_+ {a b c : E} (a|b : LDiv a b) (a|c : LDiv a c) : LDiv a (b + c) \cowith
    | inv => a|b.inv + a|c.inv
    | inv-right => ldistr *> pmap2 (+) a|b.inv-right a|c.inv-right

  \func LDiv_BigSum {a : E} {l : Array E} (p : \Pi (j : Fin l.len) -> LDiv a (l j)) : LDiv a (BigSum l) \cowith
    | inv => BigSum (\lam j => LDiv.inv {p j})
    | inv-right => BigSum-ldistr *> pmap BigSum (later $ exts \lam j => LDiv.inv-right {p j})

  \lemma natCoef_+ (n m : Nat) : natCoef (n Nat.+ m) = natCoef n + natCoef m \elim m
    |  => inv (pmap (_ +) natCoefZero *> zro-right)
    | suc m => natCoefSuc _ *> pmap (`+ ) (natCoef_+ n m) *> +-assoc *> inv (pmap (_ +) (natCoefSuc m))

  \lemma BigSum-ldistr {x : E} {l : Array E} : x * BigSum l = BigSum (map (x *) l) \elim l
    | nil => zro_*-right
    | :: a l => ldistr *> pmap (x * a +) BigSum-ldistr

  \lemma FinSum-ldistr {A : FinSet} {x : E} {y : A -> E} : x * FinSum y = FinSum (x * y __)
    => \case FinSum_char y \with {
      | inP p => pmap (x *) p. *> BigSum-ldistr *> inv (FinSum_char2 _ p.)
    }

  \lemma BigSum-rdistr {l : Array E} {z : E} : BigSum l * z = BigSum (\lam i => l i * z) \elim l
    | nil => zro_*-left
    | :: a arr => rdistr *> pmap (_ +) BigSum-rdistr

  \lemma FinSum-rdistr {A : FinSet} {x : E} {y : A -> E} : FinSum y * x = FinSum (y __ * x)
    => \case FinSum_char y \with {
      | inP p => pmap (`* x) p. *> BigSum-rdistr *> inv (FinSum_char2 _ p.)
    }

  \lemma FinSum-distr {A B : FinSet} {x : A -> E} {y : B -> E} : FinSum x * FinSum y = FinSum (\lam (s : \Sigma A B) => x s. * y s.)
    => FinSum-rdistr *> path (\lam i => FinSum (\lam a => FinSum-ldistr {_} {_} {x a} i)) *> FinSum-double

  \lemma BigSum_replicate {x : E} {n : Nat} : BigSum (replicate n x) = natCoef n * x \elim n
    |  => rewrite natCoefZero (inv zro_*-left)
    | suc n => rewrite natCoefSuc $ pmap (x +) BigSum_replicate *> equation

  \lemma BigSum_replicate1 {n : Nat} : BigSum (replicate n ide) = natCoef n
    => BigSum_replicate *> ide-right

  \lemma FinSum_replicate {A : FinSet} {x : E} : FinSum {_} {A} (\lam _ => x) = natCoef A.finCard * x
    => FinSum-const *> BigSum_replicate

  \lemma BigProd_zro {l : Array E} (j : Fin l.len) (p : l j = ) : BigProd l =  \elim l, j
    | a :: l,  => pmap (`* _) p *> zro_*-left
    | a :: l, suc j => pmap (_ *) (BigProd_zro j p) *> zro_*-right

  \lemma trivial (p :  = {E} ) {x y : E} : x = y
    => inv ide-right *> inv (pmap (x *) p) *> zro_*-right *> inv zro_*-right *> pmap (y *) p *> ide-right

  \lemma associates0 {a b : E} (c : associates a b) (p : a = ) : b = 
    => (associates-sym c). *> pmap (_ *) p *> zro_*-right

  \func op : Semiring \cowith
    | AbMonoid => \this
    | Monoid => Monoid.op
    | ldistr => rdistr
    | rdistr => ldistr
    | zro_*-left => zro_*-right
    | zro_*-right => zro_*-left
} \where {
    \open Monoid(LDiv)
  }

\class NonZeroSemiring \extends Semiring {
  | zro/=ide : zro /= ide

  \lemma inv-nonZero {a : E} (i : Monoid.Inv a) : a /= zro
    => \lam a=0 => zro/=ide (inv zro_*-right *> pmap (_ *) (inv a=0) *> i.inv-left)
}

\class CSemiring \extends Semiring, CMonoid {
  \default ldistr => *-comm *> rdistr *> pmap2 (+) *-comm *-comm
  \default rdistr => *-comm *> ldistr *> pmap2 (+) *-comm *-comm
  \default zro_*-left => *-comm *> zro_*-right
  \default zro_*-right => *-comm *> zro_*-left

  \lemma divQuotient_un0 {a : E} (p : in~ a = {DivQuotient \this} in~ ) : a = 
    => \case (DivQuotient.make~ p). \with {
         | inP d => inv (Monoid.LDiv.inv-right {d}) *> zro_*-left
       }
}