\import Algebra.Algebra
\import Algebra.Group
\import Algebra.Group.Category
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Pointed
\import Algebra.Pointed.Category
\import Algebra.Ring
\import Algebra.Ring.Category
\import Algebra.Ring.RingHom
\import Algebra.Ring.Poly
\import Algebra.Semiring
\import Category
\import Data.Array
\import Data.Bool
\import Function.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence \hiding (~)
\open EPerm
\open Transitive(Closure,cin,ctrans)

\type MonoidSet (M : \Set) (R : AddMonoid) => Quotient {Array (\Sigma R M)} (~)
  \where {
    \data \infix  ~ {M : \Set} {R : AddMonoid} (l l' : Array (\Sigma R M))
      | ~-perm (EPerm l l')
      | ~-sym (l' ~ l)
      | ~-zro {m : M} (l = (,m) :: l')
      | ~-+ {l'' : Array (\Sigma R M)} (m : M) {a b : R} (l = (a + b, m) :: l'') (l' = (a,m) :: (b,m) :: l'')

    \func inMS~ {M : \Set} {R : AddMonoid} (l : Array (\Sigma R M)) : Quotient (~) => in~ l

    \func inMS {M : \Set} {R : AddMonoid} (l : Array (\Sigma R M)) : MonoidSet M R => in~ l

    \func ~_++-left {M : \Set} {R : AddMonoid} {l1 l2 l : Array (\Sigma R M)} (e : l1 ~ l2) : (l1 ++ l) ~ (l2 ++ l) \elim e
      | ~-perm e => ~-perm (eperm-++-left e)
      | ~-sym e => ~-sym (~_++-left e)
      | ~-zro p => ~-zro (pmap (`++ l) p)
      | ~-+ m p q => ~-+ m (pmap (`++ l) p) (pmap (`++ l) q)

    \func ~_++-right {M : \Set} {R : AddMonoid} {l l1 l2 : Array (\Sigma R M)} (e : Closure (~) l1 l2) : Closure (~) (l ++ l1) (l ++ l2) \elim e
      | cin e => cin (~-perm eperm-++-comm) `ctrans` cin (~_++-left e) `ctrans` cin (~-perm eperm-++-comm)
      | ctrans e1 e2 => ~_++-right e1 `ctrans` ~_++-right e2

    \func ~_++ {M : \Set} {R : AddMonoid} {l1 l2 l1' l2' : Array (\Sigma R M)} (e1 : Closure (~) l1 l1') (e2 : Closure (~) l2 l2') : Closure (~) (l1 ++ l2) (l1' ++ l2') \elim e1
      | cin e1 => cin (~_++-left e1) `ctrans` ~_++-right e2
      | ctrans r1 r2 => ~_++ r1 e2 `ctrans` ~_++ r2 (cin (~-perm eperm-refl))

    \func ~_map {M M' : \Set} (f : AddMonoidHom) (g : M -> M') {l l' : Array (\Sigma f.Dom M)} (e : l ~ l') : map (\lam s => (f s., g s.)) l ~ map (\lam s => (f s., g s.)) l' \elim e
      | ~-perm e => ~-perm (EPerm_map (\lam s => (f s., g s.)) e)
      | ~-sym e => ~-sym (~_map f g e)
      | ~-zro {m} idp => ~-zro $ pmap (\lam x => (x, g m) :: map (\lam s => (f s., g s.)) l') f.func-zro
      | ~-+ {l''} m idp idp => ~-+ (g m) (pmap (\lam x => (x, g m) :: map (\lam s => (f s., g s.)) l'') f.func-+) idp

    \lemma toClosure {M : \Set} {R : AddMonoid} {l l' : Array (\Sigma R M)} (c : inMS l = inMS l') : Closure (~) l l'
      => Quotient.equalityClosure (\new Equivalence (Array (\Sigma R M)) (Closure (~)) {
        | ~-transitive => ctrans
        | ~-reflexive => cin (~-perm eperm-refl)
        | ~-symmetric => Closure.isSymmetric $ \lam p => later (~-sym p)
      }) cin $ path (\lam i => c i)

    \lemma unique-sum {M : \Set} {R : AddMonoid} (m : M) {l : Array (\Sigma R M)} (c : \Pi (j : Fin l.len) -> (l j). = m)
      : inMS l = inMS ((R.BigSum (map __. l), m) :: nil) \elim l
      | nil => inv $ monoidSet-ext $ ~-pequiv (~-zro idp)
      | s :: l => inv $ monoidSet-ext $ ~-pequiv (mkcon ~-+ {nil} m idp idp) *> Closure.toEquality inMS~ ~-pequiv (~_++-right {M} {R} {(s.,m) :: nil} $ toClosure $ inv $ unique-sum m $ \lam j => c $ suc j) *> pmap (\lam x => inMS~ ((s.,x) :: l)) (inv (c ))
  }

\open MonoidSet

\func msMonomial {M : \Set} {R : AddMonoid} (r : R) (m : M) : MonoidSet M R
  => inMS ((r,m) :: nil)

\lemma monoidSet-ext {M : \Set} {R : AddMonoid} {x y : Quotient {Array (\Sigma R M)} (~)} (p : x = y) : x = {MonoidSet M R} y
  => path (\lam i => p i)

\func monoidSet-coefs {M : \Set} {R : AbMonoid} (f : M -> Bool) (x : MonoidSet M R) : R \elim x
  | in~ l => R.BigSum $ map __. $ filter (\lam s => f s.) l
  | ~-equiv l l' r => monoidSet-coefs-coh r
  \where {
    \lemma monoidSet-coefs-coh {l l' : Array (\Sigma R M)} (e : l ~ l')
      : R.BigSum (map __. $ filter (\lam s => f s.) l) = R.BigSum (map __. $ filter (\lam s => f s.) l') \elim e
      | ~-perm e => R.BigSum_EPerm $ EPerm_map __. $ EPerm_filter (\lam s => f s.) e
      | ~-sym e => inv (monoidSet-coefs-coh e)
      | ~-zro {m} idp => cases (f m) \with {
        | false => idp
        | true => zro-left
      }
      | ~-+ m idp idp => cases (f m) \with {
        | false => idp
        | true => +-assoc
      }
  }

\instance MonoidAbMonoid (M : \Set) (R : AddMonoid) : AbMonoid (MonoidSet M R)
  | zro => in~ nil
  | + (x y : MonoidSet M R) : MonoidSet M R \with {
    | in~ l, in~ l' => in~ (l ++ l')
    | in~ l, ~-equiv l1 l2 r => monoidSet-ext $ ~-pequiv (~-perm eperm-++-comm) *> ~-pequiv (~_++-left r) *> ~-pequiv (~-perm eperm-++-comm)
    | ~-equiv l1 l2 r, in~ l' => monoidSet-ext $ ~-pequiv (~_++-left r)
  }
  | zro-left {x : MonoidSet M R} : in~ nil + x = x \elim x {
    | in~ l => idp
  }
  | +-assoc {x y z : MonoidSet M R} : (x + y) + z = x + (y + z) \elim x, y, z {
    | in~ l1, in~ l2, in~ l3 => monoidSet-ext $ pmap in~ ++-assoc
  }
  | +-comm {x y : MonoidSet M R} : x + y = y + x \elim x, y {
    | in~ l, in~ l' => monoidSet-ext $ ~-pequiv (~-perm eperm-++-comm)
  }
  \where \open MonoidSet

\instance MonoidAbGroup (M : \Set) (R : AddGroup) : AbGroup
  | AbMonoid => MonoidAbMonoid M R
  | negative (x : MonoidSet M R) : MonoidSet M R \with {
    | in~ l => in~ (map func l)
    | ~-equiv l l' r => monoidSet-ext $ Closure.toEquality inMS~ ~-pequiv (~_negative (cin r))
  }
  | negative-left {x : MonoidSet M R} : negative x + x =  \elim x {
    | in~ l => monoidSet-ext $ ~_negative-left l
  }
  \where {
    \open Transitive(Closure,cin,ctrans)

    \func func {M : \Set} {R : AddGroup} (s : \Sigma R M) => (R.negative s., s.)

    \func ~_negative {M : \Set} {R : AddGroup} {l l' : Array (\Sigma R M)} (p : Closure (~) l l')
      : Closure (~) (map func l) (map func l') \elim p
      | cin (~-perm e) => cin $ ~-perm (EPerm_map func e)
      | cin (~-sym p) => Closure.isSymmetric (\lam r => ~-sym r) $ ~_negative (cin p)
      | cin (~-zro {m} idp) => cin $ ~-zro $ pmap (\lam x => (x, m) :: map func l') R.negative_zro
      | cin (~-+ {l''} m idp idp) => ctrans (cin (~-+ m (pmap (\lam x => (x,m) :: map func l'') R.negative_+) idp)) $ cin $ ~-perm (eperm-swap idp idp idp)
      | ctrans r1 r2 => ctrans (~_negative r1) (~_negative r2)

    \func ~_negative-left {M : \Set} {R : AddGroup} (l : Array (\Sigma R M)) : inMS~ (map func l ++ l) = inMS~ nil \elim l
      | nil => idp
      | a :: l => ~-pequiv (~-perm $ EPerm_++-swap {_} {map func (a :: l)}) *> ~-pequiv (~-sym $ ~-+ a. (cong $ inv negative-right) idp) *> ~-pequiv (~-zro idp) *> ~_negative-left l
  }

\instance MonoidSemiring (M : AddMonoid) (R : Semiring) : Semiring
  | AbMonoid => MonoidAbMonoid M R
  | ide => in~ ((,) :: nil)
  | * (x y : MonoidSet M R) : MonoidSet M R \elim x, y {
    | in~ l, in~ l' => in~ (pairs func l l')
    | in~ l, ~-equiv l1 l2 r => monoidSet-ext $ Closure.toEquality inMS~ ~-pequiv (*-coh-right r)
    | ~-equiv l1 l2 r, in~ l => monoidSet-ext $ ~-pequiv (~-perm pairs-flip) *> Closure.toEquality inMS~ ~-pequiv (*-coh-right {AddMonoid.op M} {Semiring.op R} r) *> ~-pequiv (~-perm pairs-flip)
  }
  | ide-left {x} => \case \elim x \with {
    | in~ l => monoidSet-ext ide-left-aux
  }
  | ide-right {x} => \case \elim x \with {
    | in~ l => monoidSet-ext $ ~-pequiv (~-perm pairs-flip) *> ide-left-aux {AddMonoid.op M} {Semiring.op R}
  }
  | *-assoc {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ l1, in~ l2, in~ l3 => monoidSet-ext $ ~-pequiv $ ~-perm $ eperm-= $ pairs-assoc $ \lam {a} {b} {c} => ext (R.*-assoc, +-assoc)
  }
  | ldistr {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ l1, in~ l2, in~ l3 => monoidSet-ext $ ~-pequiv (~-perm pairs_++-right)
  }
  | rdistr {x} {y} {z} => \case \elim x, \elim y, \elim z \with {
    | in~ l1, in~ l2, in~ l3 => monoidSet-ext (pmap inMS~ pairs_++-left)
  }
  | zro_*-left {x} => \case \elim x \with {
    | in~ l => idp
  }
  | zro_*-right {x} => \case \elim x \with {
    | in~ l => monoidSet-ext (pmap inMS~ pairs_nil)
  }
  \where {
    \open pairs

    \func func {M : AddMonoid} {R : Semiring} (s t : \Sigma R M) => (s. R.* t., s. + t.)

    \lemma ide-left-aux {M : AddMonoid} {R : Semiring} {l : Array (\Sigma R M)} : inMS~ (map (func (,)) l ++ nil) = inMS~ l
      => ~-pequiv $ ~-perm $ eperm-= $ ++_nil *> arrayExt {_} {_} {map (func (,)) l} (\lam j => ext (R.ide-left, zro-left))

    \func *-coh-right {M : AddMonoid} {R : Semiring} {l l1 l2 : Array (\Sigma R M)} (r : l1 ~ l2) : Closure (~) (pairs func l l1) (pairs func l l2) \elim l
      | nil => cin (~-perm eperm-refl)
      | a :: l => ~_++ (cin $ ~_map (\new AddMonoidHom R R (a. R.*) zro_*-right ldistr) (a. +) r) (*-coh-right r)
  }

\instance MonoidRing (M : AddMonoid) (R : Ring) : Ring
  | Semiring => MonoidSemiring M R
  | AbGroup => MonoidAbGroup M R

\instance MonoidCSemiring (M : AbMonoid) (R : CSemiring) : CSemiring
  | Semiring => MonoidSemiring M R
  | *-comm {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => monoidSet-ext $ ~-pequiv (~-perm pairs.pairs-flip) *> cong (ext $ \lam t s => ext (*-comm, +-comm))
  }

\func monoidRingHom {M : AddMonoid} {R : Ring} : RingHom R (MonoidRing M R) \cowith
  | func a => inMS~ ((a,M.zro) :: nil)
  | func-+ => monoidSet-ext $ ~-pequiv $ mkcon ~-+ {nil} M.zro idp idp
  | func-ide => idp
  | func-* => rewriteI {} M.zro-left idp

\instance MonoidAlgebra (M : AbMonoid) (R : CRing) : CAlgebra { | R => R }
  => homAlgebra {R} {\new CRing { | Ring => MonoidRing M R | *-comm => *-comm }} monoidRingHom

\func monoidSet-map {M N : \Set} (f : M -> N) (g : AddMonoidHom) (x : MonoidSet M g.Dom) : MonoidSet N g.Cod \elim x
  | in~ l => inMS~ $ map (\lam s => (g s., f s.)) l
  | ~-equiv l l' r => monoidSet-ext $ ~-pequiv (~_map g f r)

\func monoidSet-hom {M N : \Set} (f : M -> N) (g : AddMonoidHom) : AddMonoidHom (MonoidAbMonoid M g.Dom) (MonoidAbMonoid N g.Cod) (monoidSet-map f g) \cowith
  | func-zro => idp
  | func-+ {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pmap inMS $ map_++ (\lam s => (g s., f s.))
  }

\func monoidSet-semiringHom (f : AddMonoidHom) (g : SemiringHom) : SemiringHom (MonoidSemiring f.Dom g.Dom) (MonoidSemiring f.Cod g.Cod) \cowith
  | AddMonoidHom => monoidSet-hom f g
  | func-ide => pmap2 (\lam x y => inMS ((x,y) :: nil)) g.func-ide f.func-zro
  | func-* {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pmap inMS $ pairs.pairs_map (\lam s => (g s., f s.)) $ \lam {a} {b} => ext (g.func-*, f.func-+)
  }

\func monoidSet-ringHom (f : AddMonoidHom) (g : RingHom) : RingHom (MonoidRing f.Dom g.Dom) (MonoidRing f.Cod g.Cod) \cowith
  | SemiringHom => monoidSet-semiringHom f g

\lemma msMonomial_+ {M : \Set} {R : AddMonoid} {a b : R} {m : M} : msMonomial (a + b) m = msMonomial a m + msMonomial b m
  => monoidSet-ext $ ~-pequiv $ mkcon ~-+ {nil} m idp idp

\lemma msMonomial_0 {M : \Set} {R : AddMonoid} {m : M} : msMonomial R.zro m = 
  => monoidSet-ext $ ~-pequiv $ MonoidSet.~-zro idp

\lemma msMonomial_* {M : AddMonoid} {R : Semiring} {a b : R} : msMonomial (a * b) M.zro = msMonomial a M.zro * msMonomial b M.zro
  => monoidSet-ext $ unfold MonoidSemiring.func $ rewrite zro-left idp

\lemma msMonomial-split {M : AddMonoid} {R : Semiring} {a : R} {m : M} : msMonomial a M.zro * msMonomial R.ide m = msMonomial a m
  => pmap2 (\lam x y => inMS ((x,y) :: nil)) ide-right zro-left

\lemma msMonomial_BigSum {M : \Set} {R : AddMonoid} {l : Array (\Sigma R M)} : AddMonoid.BigSum (map (\lam s => msMonomial s. s.) l) = inMS l \elim l
  | nil => idp
  | s :: l => pmap (_ +) msMonomial_BigSum

\lemma msMonomial_BigProd {M : AddMonoid} {R : Semiring} (l : Array (\Sigma R M))
  : Monoid.BigProd (map (\lam s => msMonomial s. s.) l) = msMonomial (Monoid.BigProd $ map __. l) (AddMonoid.BigSum $ map __. l) \elim l
  | nil => idp
  | s :: l => pmap (_ *) (msMonomial_BigProd l)

\lemma msMonomial_BigProd_ide {M : AddMonoid} {R : Semiring} {l : Array M}
  : Monoid.BigProd (map (\lam m => msMonomial R.ide m) l) = msMonomial R.ide (AddMonoid.BigSum l)
  => msMonomial_BigProd (map (\lam m => (R.ide,m)) l) *> pmap (msMonomial __ _) Monoid.BigProd_replicate1

\func evalMS {M : \Set} {R : Semiring} (x : MonoidSet M R) (f : M -> R) : R \elim x
  | in~ l => R.BigSum $ map (\lam s => s. * f s.) l
  | ~-equiv l l' r => evalMS-coh f r
  \where {
    \lemma evalMS-coh {M : \Set} {R : Semiring} (f : M -> R) {l l' : Array (\Sigma R M)} (r : l ~ l')
      : R.BigSum (map (\lam s => s. * f s.) l) = R.BigSum (map (\lam s => s. * f s.) l') \elim r
      | ~-perm e => R.BigSum_EPerm $ EPerm_map (\lam s => s. * f s.) e
      | ~-sym r => inv (evalMS-coh f r)
      | ~-zro idp => pmap (`+ _) zro_*-left *> zro-left
      | ~-+ m idp idp => pmap (`+ _) rdistr *> +-assoc
  }

\func evalMSMonoidHom {M : \Set} {R : Semiring} (f : M -> R) : AddMonoidHom (MonoidAbMonoid M R) R \cowith
  | func => evalMS __ f
  | func-zro => idp
  | func-+ {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pmap R.BigSum (map_++ (\lam s => s. * f s.)) *> R.BigSum_++
  }

\func evalMSSemiringHom {M : AddMonoid} {R : CSemiring} (f : MonoidHom M R) : SemiringHom (MonoidSemiring M R) R \cowith
  | AddMonoidHom => evalMSMonoidHom f
  | func-ide => simplify f.func-ide
  | func-* {x} {y} => \case \elim x, \elim y \with {
    | in~ l, in~ l' => pairs.pairs-distr (\lam s => s. * f s.) $ \lam {a} {b} => unfold MonoidSemiring.func (rewrite f.func-* equation)
  }

\func evalMSRingHom {M : AddMonoid} {R : CRing} (f : MonoidHom M R) : RingHom (MonoidRing M R) R \cowith
  | SemiringHom => evalMSSemiringHom f

\lemma evalMS_monomial {M : AddPointed} {R : Semiring} {f : PointedHom M R} {a : R} : evalMS (msMonomial a M.zro) f = a
  => zro-right *> pmap (a *) func-ide *> ide-right

\lemma evalMS_map {M N : AddMonoid} {R : CRing} {f : M -> N} {x : MonoidSet M R} {g : N -> R}
  : evalMS (monoidSet-map f (id R) x) g = evalMS x (\lam m => g (f m)) \elim x
  | in~ l => idp

\lemma evalMS_map2 {M : \Set} {R S : Semiring} {x : MonoidSet M R} {f : M -> R} (g : SemiringHom R S)
  : evalMS (monoidSet-map (\lam y => y) g x) (\lam m => g (f m)) = g (evalMS x f) \elim x
  | in~ l => inv $ g.func-BigSum *> pmap AddMonoid.BigSum (exts \lam j => g.func-*)

\func polyToMonoidSet {M : AddMonoid} {R : Semiring} (m : M) (p : Poly R) : MonoidSet M R \elim p
  | pzero => 
  | padd p a => polyToMonoidSet m p * msMonomial  m + msMonomial a zro
  | peq i => ~-pequiv {_} {_} {(R.zro,M.zro) :: nil} {nil} (MonoidSet.~-zro idp) i

\func polyToMonoidSetHom {M : AddMonoid} {R : Ring} (m : M) : AddMonoidHom (PolyRing R) (MonoidRing M R) \cowith
  | func => polyToMonoidSet m
  | func-zro => idp
  | func-+ {p q : Poly R} : polyToMonoidSet m (p + q) = polyToMonoidSet m p + polyToMonoidSet m q \elim p, q {
    | pzero, q => inv zro-left
    | p, pzero => pmap (polyToMonoidSet m) +-comm *> inv zro-right
    | padd p a, padd q b => rewrite (func-+,rdistr,msMonomial_+) $ +-assoc *> pmap (_ +) (later (inv +-assoc) *> pmap (`+ _) +-comm *> +-assoc) *> inv +-assoc
  }

\func polyToMonoidSetRingHom {M : AbMonoid} {R : CRing} (m : M) : RingHom (PolyRing R) (MonoidRing M R) \cowith
  | AddMonoidHom => polyToMonoidSetHom m
  | func-ide => idp
  | func-* {p q : Poly R} : polyToMonoidSet m (p * q) = polyToMonoidSet m p * polyToMonoidSet m q \elim p {
    | pzero => inv zro_*-left
    | padd p a => polyToMonoidSetHom.func-+ *> pmap2 (+) (pmap (_ +) msMonomial_0 *> zro-right *> pmap (`* _) func-* *> *-assoc *> pmap (_ *) *-comm *> inv *-assoc) func-*c *> inv rdistr
  }
  \where {
    \lemma func-*c {m : M} {a : R} {p : Poly R} : polyToMonoidSet m (a PolyRing.*c p) = msMonomial a zro * polyToMonoidSet m p \elim p
      | pzero => idp
      | padd p b => pmap (__ * _ + _) func-*c *> pmap2 (+) *-assoc simplify *> inv ldistr
  }

\lemma polyToMonoidSet-eval {R : CRing} {M : AddMonoid} {p : Poly R} {f : MonoidHom M R} {m : M} : evalMS (polyToMonoidSet m p) f = polyEval p (f m) \elim p
  | pzero => idp
  | padd p a => func-+ {evalMSRingHom f} *> pmap2 (+) (func-* *> pmap2 (*) polyToMonoidSet-eval simplify) (unfold $ rewrite f.func-ide simplify)

\lemma monoidRingHom-unique {M : AddMonoid} {R S : CRing} {f g : RingHom (MonoidRing M R) S} (p : \Pi (r : R) -> f (msMonomial r zro) = g (msMonomial r zro)) (q : \Pi (m : M) -> f (msMonomial  m) = g (msMonomial  m)) (x : MonoidSet M R) : f x = g x \elim x
  | in~ l => pmap f monoidSet-list *> f.func-BigSum *> pmap AddMonoid.BigSum (exts \lam j => simplify *> f.func-* *> pmap2 (*) (p (l j).) (q (l j).) *> inv g.func-* *> simplify) *> inv g.func-BigSum *> inv (pmap g monoidSet-list)
  \where {
    \lemma monoidSet-list {M : \Set} {R : AddMonoid} {l : Array (\Sigma R M)} : inMS l = AddMonoid.BigSum \lam j => msMonomial (l j). (l j). \elim l
      | nil => idp
      | a :: l => pmap (_ +) monoidSet-list
  }