\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Pointed
\import Algebra.Pointed.Sub
\import Algebra.Ring.Localization()
\import Arith.Nat
\import Data.Array
\import Function.Iterate
\import Logic
\import Logic.Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set

\class SubSemigroup \extends SubSet {
  \override S : Semigroup
  | contains_* {x y : S} : contains x -> contains y -> contains (x * y)

  \func ISemigroup : Semigroup \cowith
    | BaseSet => ISet
    | * x y => (x. * y., contains_* x. y.)
    | *-assoc => ext *-assoc
} \where {
  \func cStruct {A : CSemigroup} (S : SubSemigroup A) : CSemigroup \cowith
    | Semigroup => S.ISemigroup
    | *-comm => ext *-comm
}

\class SubMonoid \extends SubPointed, SubSemigroup {
  \override S : Monoid

  \func IMonoid : Monoid \cowith
    | Pointed => IPointed
    | Semigroup => ISemigroup
    | ide-left => ext ide-left
    | ide-right => ext ide-right

  \lemma contains_pow {x : S} (s : contains x) {n : Nat} : contains (Monoid.pow x n) \elim n
    |  => contains_ide
    | suc n => contains_* (contains_pow s) s

  \lemma sub-pow {x : IMonoid} {n : Nat} : (IMonoid.pow x n). = Monoid.pow x. n \elim n
    |  => idp
    | suc n => pmap (`* x.) sub-pow

  \func embedMonoid : MonoidHom IMonoid S \cowith
    | func => __.
    | func-ide => idp
    | func-* => idp
} \where {
  \func cStruct {A : CMonoid} (S : SubMonoid A) : CMonoid \cowith
    | Monoid => S.IMonoid
    | CSemigroup => SubSemigroup.cStruct S

  \func max {A : Monoid} : SubMonoid \cowith
    | SubPointed => SubPointed.max {A}
    | contains_* _ _ => ()

  \func closure {M : Monoid} (S : SubSet M) : SubMonoid M \cowith
    | contains x => ∃ (n : Nat) (iterr apl n S x)
    | contains_ide => inP (, byRight (byLeft idp))
    | contains_* {x} {y} (inP (n,xr)) (inP (m,yr)) => inP (suc (n ∨ m), byRight (byRight (x, y, apl-inc join-left x xr, apl-inc join-right y yr, idp)))
    \where {
      \open Algebra.Ring.Localization

      \lemma ext {M : Monoid} (S : SubSet M) : S <= closure S
        => \lam x x<-S => inP (, x<-S)

      \lemma univ (S' : SubMonoid M) (p : S <= S') (x : M) (q : closure S x) : S' x \elim q
        | inP (, x<-S) => p x x<-S
        | inP (suc n, byLeft x<-C) => univ S' p x (inP (n, x<-C))
        | inP (suc n, byRight (byLeft x=1)) => transport S' (inv x=1) S'.contains_ide
        | inP (suc n, byRight (byRight (y, z, y<-C, z<-C, x=y*z))) => transport S' (inv x=y*z) (S'.contains_* (univ S' p y (inP (n, y<-C))) (univ S' p z (inP (n, z<-C))))

      \func apl {M : Monoid} (S : SubSet M) : SubSet M \cowith
        | contains x => S x || (x = ) || (\Sigma (y z : M) (S y) (S z) (x = y * z))

      \lemma apl-inc {n m : Nat} (q : n <= m) (x : M) (p : iterr apl n S x) : iterr apl m S x
        => rewriteI (<=_exists q) (alt n (m -' n) x p)
        \where
          \lemma alt (n m : Nat) (x : M) (p : iterr apl n S x) : iterr apl (n + m) S x \elim m
            |  => p
            | suc m => byLeft (alt n m x p)
    }

  \func powers {M : Monoid} (a : M) : SubMonoid M \cowith
    | contains x => ∃ (n : Nat) (M.pow a n = x)
    | contains_ide => inP (, idp)
    | contains_* (inP (n,a^n=x)) (inP (m,a^m=y)) => inP (n Nat.+ m, M.pow_+ *> pmap2 (*) a^n=x a^m=y)
}

\class DecSubMonoid \extends SubMonoid, DecSubPointed {
  \override S : Monoid
}

\class SubAddMonoid \extends SubAddPointed {
  \override S : AddMonoid
  | contains_+ {x y : S} : contains x -> contains y -> contains (x + y)

  \func IAddMonoid : AddMonoid \cowith
    | AddPointed => IAddPointed
    | + x y => (x. + y., contains_+ x. y.)
    | zro-left => ext zro-left
    | zro-right => ext zro-right
    | +-assoc => ext +-assoc

  \lemma sub-BigSum {l : Array IAddMonoid} : (IAddMonoid.BigSum l). = AddMonoid.BigSum (map __. l) \elim l
    | nil => idp
    | a :: l => pmap (a. +) sub-BigSum
} \where {
  \func abStruct {A : AbMonoid} (S : SubAddMonoid A) : AbMonoid \cowith
    | AddMonoid => S.IAddMonoid
    | +-comm => ext +-comm

  \func max {A : AddMonoid} : SubAddMonoid \cowith
    | SubAddPointed => SubAddPointed.max {A}
    | contains_+ _ _ => ()
}