\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Data.Array
\import Data.Or
\import Function.Meta ($)
\import Logic
\import Meta
\import Paths
\import Paths.Meta
\import Set
\import Set.Category
\import Set.Fin

\class Group \extends CancelMonoid {
  | inverse : E -> E
  | inverse-left {x : E} : inverse x * x = ide
  | inverse-right {x : E} : x * inverse x = ide

  | cancel_*-left x {y} {z} p =>
      y                   ==< inv ide-left >==
      ide * y             ==< pmap (`* y) (inv inverse-left) >==
      (inverse x * x) * y ==< *-assoc >==
      inverse x * (x * y) ==< pmap (inverse x *) p >==
      inverse x * (x * z) ==< inv *-assoc >==
      (inverse x * x) * z ==< pmap (`* z) inverse-left >==
      ide * z             ==< ide-left >==
      z                   `qed
  | cancel_*-right z {x} {y} p =>
      x                   ==< inv ide-right >==
      x * ide             ==< pmap (x *) (inv inverse-right) >==
      x * (z * inverse z) ==< inv *-assoc >==
      (x * z) * inverse z ==< pmap (`* inverse z) p >==
      (y * z) * inverse z ==< *-assoc >==
      y * (z * inverse z) ==< pmap (y *) inverse-right >==
      y * ide             ==< ide-right >==
      y                   `qed

  \lemma inverse-isInv {x : E} : inverse (inverse x) = x =>
     AddGroup.negative-isInv {AddGroup.fromGroup \this}

  \lemma inverse_ide : inverse ide = ide
    => inv ide-right *> inverse-left

  \lemma inverse_* {x y : E}  : inverse (x * y) = inverse y * inverse x => cancel_*-left (x * y) (
    (x * y) / (x * y)         ==< inverse-right >==
    ide                       ==< inv inverse-right >==
    x / x                     ==< pmap (x *) (inv ide-left) >==
    x * (ide / x)             ==< pmap (x * (__ / x)) (inv inverse-right) >==
    x * ((y / y) / x)         ==< pmap (x *) *-assoc >==
    x * (y * (inverse y / x)) ==< inv *-assoc >==
    (x * y) * (inverse y / x) `qed)

  \lemma inverse_pow {x : E} {n : Nat} : inverse (pow x n) = pow (inverse x) n \elim n
    |  => inverse_ide
    | suc n => inverse_* *> pmap (_ *) inverse_pow *> pow-left

  \lemma makeInv (a : E) : Inv a (inverse a) \cowith
    | inv-left => inverse-left
    | inv-right => inverse-right

  \func op : Group \cowith
    | Monoid => Monoid.op
    | inverse => inverse
    | inverse-left => inverse-right
    | inverse-right => inverse-left

  \lemma check-for-inv {x y : E} (p : x * y = ide) : y = inverse x
    => simplify in pmap (inverse x *) p

  \lemma equality-check {g h : E} (p : inverse g * h = ide) : g = h
    => inv $ simplify in pmap (g *) p

  \lemma equality-corrolary (g h : E) (p : g = h) : inverse g * h = ide =>
    inverse g * h ==< pmap (inverse g *) (inv p) >==
    inverse g * g ==< inverse-left >==
    ide `qed
} \where {
  \open Monoid(Inv)

  \lemma inverse-equality {X : \Set} (G H : Group X) (z : G.ide = H.ide) (m : \Pi {x y : G} -> x G.* y = x H.* y) (e : G) : G.inverse e = H.inverse e
    => pmap (\lam (x : Inv) => x.inv) (Inv.levelProp {G}
        (\new Inv e (G.inverse e) G.inverse-left G.inverse-right)
        (\new Inv e (H.inverse e) (m *> H.inverse-left *> inv z) (m *> H.inverse-right *> inv z)))

  \func equals (G H : Group) (p : G = {Monoid} H) : G = H
    => exts Group {
         | Monoid => p
         | inverse => inverse-equality
       }
    \where {
      \lemma inverse-equality (e : G) : coe (p @ __) (inverse e) right = inverse (coe (p @ __) e right)
        => \let | h' {H' : Monoid} (q : G = {Monoid} H') => transport (\lam (H' : Monoid) => MonoidHom G H') q (MonoidCat.id G)
                | h => transport (MonoidHom G H __) (Jl (\lam (H' : Monoid) q => func {h' q} = (\lam x => coe (q @ __) x right)) idp p) (h' p)
                | e' => coe (p @ __) e right
           \in MonoidHom.presInvElem h
                (\new Inv e (inverse e) inverse-left inverse-right)
                (\new Inv e' (inverse e') inverse-left inverse-right)
    }
}

\func conjugate {E : Group} (g : E) (h : E) : E => g * h * inverse g

\func conjugate-via-id {E : Group} (g : E) : conjugate E.ide g = g =>
  conjugate E.ide g ==< idp >==
  E.ide * g * inverse E.ide ==< E.*-assoc >==
  E.ide * (g * inverse E.ide) ==< E.ide-left >==
  g * (inverse E.ide) ==< pmap (g * ) E.inverse_ide >==
  g * E.ide ==< E.ide-right >==
  g `qed

\func conjugate-id  {E : Group} (g : E) : conjugate g E.ide = E.ide =>
  conjugate g E.ide ==< idp >==
  g * E.ide * (inverse g) ==< pmap (\lam z => z * (inverse g)) E.ide-right >==
  g * (inverse g) ==< E.inverse-right >==
  E.ide `qed



\func \infixl  / {G : Group} (x y : G) => x * inverse y

\class AddGroup \extends AddMonoid {
  | negative : E -> E
  | negative-left {x : E} : negative x + x = zro
  | negative-right {x : E} : x + negative x = zro

  \lemma cancel-left (x : E) {y z : E} (p : x + y = x + z) : y = z =>
    Group.cancel_*-left {toGroup \this} x p

  \lemma cancel-right (z : E) {x y : E} (p : x + z = y + z) : x = y =>
    Group.cancel_*-right {toGroup \this} z p

  \lemma negative-isInv {x : E} : negative (negative x) = x =>
    cancel-left (negative x) (negative-right *> inv negative-left)

  \lemma negative_+ {x y : E} : negative (x + y) = negative y - x
    => Group.inverse_* {toGroup \this}

  \lemma negative_zro : negative zro = zro
    => inv zro-right *> negative-left

  \lemma minus_zro {x : E} : x - zro = x
    => pmap (x +) negative_zro *> zro-right

  \lemma fromZero {x y : E} (x-y=0 : x - y = zro) : x = y =>
    x                    ==< inv zro-right >==
    x + zro              ==< pmap (x +) (inv negative-left) >==
    x + (negative y + y) ==< inv +-assoc >==
    x - y + y            ==< pmap (`+ y) x-y=0 >==
    zro + y              ==< zro-left >==
    y                    `qed

  \lemma toZero {x y : E} (x=y : x = y) : x - y = zro => rewriteI x=y negative-right

  \lemma diff_+ {x y z : E} : (z - y) + (y - x) = z - x =>
    (z - y) + (y - x)          ==< +-assoc >==
    z + (negative y + (y - x)) ==< inv (pmap (z +) +-assoc) >==
    z + ((negative y + y) - x) ==< pmap (z + (__ - x)) negative-left >==
    z + (zro - x)              ==< pmap (z +) zro-left >==
    z - x                      `qed
} \where {
    \use \coerce fromGroup (G : Group) => \new AddGroup G.E G.ide (G.*) G.ide-left G.ide-right G.*-assoc G.inverse G.inverse-left G.inverse-right
    \use \coerce toGroup (G : AddGroup) => \new Group G.E G.zro (G.+) G.zro-left G.zro-right G.+-assoc G.negative G.negative-left G.negative-right

    \lemma negative-equality {X : \Set} (A B : AddGroup X) (z : A.zro = B.zro) (m : \Pi {x y : A} -> x A.+ y = x B.+ y) (e : A) : A.negative e = B.negative e
      => Group.inverse-equality A B z m e

  -- | An additive group with a tight apartness relation.
  \class With# \extends AddGroup, Set# {
    | \fix  #0 : E -> \Prop
    | #0-zro : Not (zro `#0)
    | #0-negative {x : E} : x `#0 -> negative x `#0
    | #0-+ {x y : E} : (x + y) `#0 -> x `#0 || y `#0
    | #0-tight {x : E} : Not (x `#0) -> x = zro

    | # x y => (x - y) `#0
    | #-irreflexive x-x#0 => #0-zro (transport #0 negative-right x-x#0)
    | #-symmetric x-y#0 => transport #0 (negative_+ *> pmap (`+ negative _) negative-isInv) (#0-negative x-y#0)
    | #-comparison x y z x-z#0 => #0-+ (transport #0 (inv diff_+) x-z#0)
    | tightness x-y/#0 => fromZero (#0-tight x-y/#0)

    \lemma apartNonZero {x : E} (x#0 : x `#0) : x /= zro
      => \lam x=0 => #0-zro (transport #0 x=0 x#0)

    \lemma #0-negative-inv {x : E} (p : negative x `#0) : x `#0
      => transport #0 negative-isInv (#0-negative p)

    \lemma #0-+-left {x y : E} (x#0 : #0 x) : #0 (x + y) || #0 y
      => ||.map (\lam r => r) #0-negative-inv $ #0-+ $ transportInv #0 (+-assoc *> pmap (x +) negative-right *> zro-right) x#0

    \lemma #0-+-right {x y : E} (y#0 : #0 y) : #0 (x + y) || #0 x
      => ||.rec' (\lam r => byRight (#0-negative-inv r)) byLeft $ #0-+ {_} {negative x} {x + y} $ transportInv #0 simplify y#0
  }

  -- | An additive group with decidable equality.
  \class Dec \extends With#, DecSet {
    | nonZeroApart {x : E} (x/=0 : x /= zro) : x `#0
    | #0-negative x#0 => nonZeroApart (\lam -x=0 => #0-zro (transport #0 (inv negative-isInv *> pmap negative -x=0 *> negative_zro) x#0))
    | #0-+ {x} {y} x+y#0 => \case decideEq y zro \with {
      | yes y=0 => byLeft (transport #0 (pmap (x +) y=0 *> zro-right) x+y#0)
      | no y/=0 => byRight (nonZeroApart y/=0)
    }
    | #0-tight {x} x/#0 => \case decideEq x zro \with {
      | yes x=0 => x=0
      | no x/=0 => absurd (x/#0 (nonZeroApart x/=0))
    }
    | nonEqualApart p => nonZeroApart (\lam x-y=0 => p (fromZero x-y=0))

    \default #0 x : \Prop => x /= zro
    \default #0-zro (zro/=0 : #0 zro) : Empty => zro/=0 idp
    \default nonZeroApart \as notEqualApartImpl {x} x#0 : #0 x => x#0

    \lemma decide#0 (a : E) : Or (a = ) (a With#.`#0) \level Or.levelProp (\lam p q => apartNonZero q p)
      => \case decideEq a  \with {
        | yes e => inl e
        | no q => inr (nonZeroApart q)
      }
  }
}

\func \infixl  - {G : AddGroup} (x y : G) => x + negative y

\class CGroup \extends Group, CancelCMonoid
  | inverse-right => *-comm *> inverse-left

\class AbGroup \extends AddGroup, AbMonoid {
  | negative-right => +-comm *> negative-left

  \lemma BigSum_negative {l : Array E} : negative (BigSum l) = BigSum (map negative l) \elim l
    | nil => negative_zro
    | a :: l => negative_+ *> +-comm *> pmap (_ +) BigSum_negative

  \lemma sum-cancel-left {x y z : E} : x + z - (x + y) = z - y
    => pmap (_ +) negative_+ *> pmap2 (+) +-comm +-comm *> +-assoc *> pmap (z +) (inv +-assoc *> pmap (`- y) negative-right *> zro-left)

  \lemma diff-cancel-left {x y z : E} : x - z - (x - y) = y - z
    => sum-cancel-left *> +-comm *> pmap (`- z) negative-isInv
} \where {
    \use \coerce fromCGroup (G : CGroup) => \new AbGroup G.E G.ide (G.*) G.ide-left G.ide-right G.*-assoc G.inverse G.inverse-left G.*-comm
    \use \coerce toCGroup (G : AbGroup) => \new CGroup G.E G.zro (G.+) G.zro-left G.zro-right G.+-assoc G.negative G.negative-left G.+-comm

    \func equals (A B : AbGroup) (p : A = {AddGroup} B) : A = B
      => path (\lam i => \new AbGroup {
        | AddGroup => p @ i
        | +-comm => prop-dpi (\Pi {x y : p @ __} -> x + y = y + x) A.+-comm B.+-comm @ i
      })
  }

\class FinGroup \extends Group, FinSet