\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.MonoidHom
\import Algebra.Pointed
\import Arith.Int()
\import Data.Array
\import Data.Fin
\import Data.Or
\import Equiv
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Set
\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

  \default inverse-left => make-inverse-left ide-right inverse inverse-right
  \default inverse-right => make-inverse-left {Semigroup.op} ide-left inverse inverse-left

  \default ide-left => make-ide-left ide-right inverse inverse-right inverse-left
  \default ide-right => make-ide-left {Semigroup.op} ide-left inverse inverse-left inverse-right

  | 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

  \func ipow (a : E) (x : Int) : E \elim x
    | pos n => pow a n
    | neg n => pow (inverse a) n

  \lemma ipow_+ {a : E} {x y : Int} : ipow a (x + y) = ipow a x * ipow a y \elim x, y
    | pos n, pos m => pow_+
    | pos n, neg m => ipow_-
    | neg n, pos m => ipow_- *> pow-comm2 (inverse-right *> inv inverse-left)
    | neg n, neg m => pow_+
    \where {
      \open Arith.Int.IntRing(+,+-comm)

      \lemma ipow_- {a : E} {n m : Nat} : ipow a (n Nat.- m) = pow a n * pow (inverse a) m \elim n, m
        | , m => inv ide-left
        | suc n,  => inv ide-right
        | suc n, suc m => equation.monoid {ipow_-, inv (pow-left {_} {inverse a}), inverse-right {_} {a}}
    }

  \lemma ipow_negaitve {a : E} {x : Int} : ipow a (negative x) = inverse (ipow a x) \elim x
    | pos n => inv inverse_pow
    | neg n => inv inverse-isInv *> pmap inverse inverse_pow
    \where \open Arith.Int.IntRing(negative)

  \lemma ipow_* {a : E} {x y : Int} : ipow a (x * y) = ipow (ipow a x) y \elim x, y
    | pos n, pos m => pow_*
    | pos n, neg m => pow_* *> pmap (pow __ m) (inv inverse_pow)
    | neg (suc n), pos m => pow_*
    | neg (suc n), neg m => pow_* *> pmap (pow __ m) (inv (inverse_pow {_} {_} {suc n} *> pmap (pow __ (suc n)) inverse-isInv))
    \where \open Arith.Int.IntRing(*)

  \lemma ipow_ide {x : Int} : ipow ide x = ide \elim x
    | pos n => pow_ide
    | neg n => pmap (pow __ n) inverse_ide *> pow_ide

  \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

  \protected \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 MonoidHom.id
                | h => transport (MonoidHom G H __) (Jl (\lam (H' : Monoid) q => (h' q).func = (\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)
    }

  \private \lemma make-inverse-left {M : Semigroup} {ide : M} (ide-right : \Pi {x : M} -> x * ide = x) (inverse : M -> M) (inverse-right : \Pi {x : M} -> x * inverse x = ide) {x : M} : inverse x * x = ide
    => \have | inverse-x-idempotent : (inverse x * x) * (inverse x * x) = inverse x * x =>
                (inverse x * x) * (inverse x * x) ==< *-assoc >==
                inverse x * (x * (inverse x * x)) ==< pmap (inverse x *) (inv *-assoc) >==
                inverse x * ((x * inverse x) * x) ==< cong inverse-right >==
                inverse x * (ide * x)             ==< inv *-assoc >==
                (inverse x * ide) * x             ==< cong ide-right >==
                inverse x * x                     `qed
             | idempotent-is-trivial {a : M} (a-idempotent : a * a = a) : a = ide =>
                a                   ==< inv ide-right >==
                a * ide             ==< cong (inv inverse-right) >==
                a * (a * inverse a) ==< inv *-assoc >==
                (a * a) * inverse a ==< cong a-idempotent >==
                a * inverse a       ==< inverse-right >==
                ide                 `qed
       \in idempotent-is-trivial inverse-x-idempotent

  \private \lemma make-ide-left {M : Semigroup} {ide : M} (ide-right : \Pi {x : M} -> * x ide = x) (inverse : M -> M)
    (inverse-right : \Pi {x : M} -> x * inverse x = ide) (inverse-left : \Pi {x : M} -> inverse x * x = ide) {x : M} : * ide x = x
    => ide * x              ==< pmap (`* x) (inv inverse-right) >==
       (x * inverse x) * x  ==< *-assoc >==
       x * (inverse x * x)  ==< cong inverse-left >==
       x * ide              ==< ide-right >==
       x                      `qed

  \func translate-is-Equiv {G : Group} (h : G) : QEquiv (h *) \cowith
    | ret => inverse h *
    | ret_f _ => rewrite (inv G.*-assoc, G.inverse-left, G.ide-left) idp
    | f_sec _ => rewrite (inv G.*-assoc, G.inverse-right, G.ide-left) idp

  \class Dec \extends Group, DecSet
}

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

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

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

\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_- {x y : E} : negative (x - y) = y - x
    => negative_+ *> pmap (`- x) negative-isInv

  \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 *n_negative {n : Nat} {a : E} : n *n negative a = negative (n *n a)
    => *n_pow *> inv \this.inverse_pow *> inv (pmap negative *n_pow)

  \func \infixl  *i (x : Int) (a : E) : E \elim x
    | pos n => n *n a
    | neg n => n *n negative a

  \protected \lemma *i_ipow {x : Int} {a : E} : x *i a = \this.ipow a x \elim x
    | pos n => *n_pow
    | neg n => *n_pow

  \lemma *i-assoc {x y : Int} {a : E} : (x * y) *i a = x *i (y *i a)
    => pmap (`*i _) *-comm *> *i_ipow *> \this.ipow_* *> inv (pmap (_ *i) *i_ipow *> *i_ipow)
    \where \open Arith.Int.IntRing(*,*-comm)

  \lemma *i-rdistr {x y : Int} {a : E} : (x Arith.Int.IntRing.+ y) *i a = x *i a + y *i a
    => *i_ipow *> \this.ipow_+ *> inv (pmap2 (+) *i_ipow *i_ipow)

  \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.+-assoc G.zro-left G.zro-right 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

    \lemma #0-BigSum {l : Array E} (p : BigSum l `#0) : ∃ (j : Fin l.len) (l j `#0) \elim l
      | nil => absurd (#0-zro p)
      | a :: l => \case #0-+ p \with {
        | byLeft a#0 => inP (, a#0)
        | byRight p' => \case #0-BigSum p' \with {
          | inP (j,lj#0) => inP (suc j, lj#0)
        }
      }

    \lemma #0-BigSum-conv {l : Array E} {i : Fin l.len} (p : l i `#0) : BigSum l `#0 || (\Sigma (j : Fin l.len) (j /= i) (l j `#0)) \elim l, i
      | a :: l,  => \case #0-+-left p \with {
        | byLeft r => byLeft r
        | byRight l#0 => \case #0-BigSum l#0 \with {
          | inP (j,lj#0) => byRight (suc j, \case __ \with {}, lj#0)
        }
      }
      | a :: l, suc i => \case #0-BigSum-conv p \with {
        | byLeft l#0 => \case #0-+-right {_} {a} l#0 \with {
          | byLeft r => byLeft r
          | byRight a#0 => byRight (, \case __ \with {}, a#0)
        }
        | byRight (j,j/=i,lj#0) => byRight (suc j, fsuc/= j/=i, lj#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

  \lemma ipow_*-comm {a b : E} {x : Int} : ipow (a * b) x = ipow a x * ipow b x \elim x
    | pos n => pow_*-comm
    | neg n => pmap (pow __ n) (inverse_* *> *-comm) *> pow_*-comm

  \lemma BigProd_inverse {l : Array E} : inverse (BigProd l) = BigProd (map inverse l)
    => AbGroup.BigSum_negative {AbGroup.fromCGroup \this}

  \lemma BigProd_ipow {k : Int} {l : Array E} : BigProd (\lam i => ipow (l i) k) = ipow (BigProd l) k \elim k
    | pos n => BigProd_pow
    | neg n => later (BigProd-ext {_} {l.len} \lam i => inv inverse_pow) *> inv BigProd_inverse *> pmap inverse BigProd_pow *> inverse_pow
}

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

  \lemma *n-ldistr_- {n : Nat} {a b : E} : n *n (a - b) = n *n a - n *n b
    => *n-ldistr *> pmap (_ +) *n_negative

  \lemma *i-ldistr {a b : E} {x : Int} : x *i (a + b) = x *i a + x *i b
    => *i_ipow *> \this.ipow_*-comm *> inv (pmap2 (+) *i_ipow *i_ipow)

  \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 sum-cancel-right {x y z : E} : z + x - (y + x) = z - y
    => rewrite (+-comm {_} {z}, +-comm {_} {y}) sum-cancel-left

  \lemma diff-cancel-left {x y z : E} : x - z - (x - y) = y - z
    => sum-cancel-left *> +-comm *> pmap (`- z) negative-isInv

  \lemma negative_+-comm {x y : E} : negative (x + y) = negative x - y
    => negative_+ *> +-comm

  \lemma diff_sum {x y z : E} : x - (y + z) = x - y - z
    => pmap (x +) negative_+-comm *> inv +-assoc

  \lemma diff_diff {x y z : E} : x - (y - z) = x - y + z
    => diff_sum *> pmap (x - y + __) 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.+-assoc G.zro-left G.zro-right 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, Group.Dec, FinSet