\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 | 0 => 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 7 / {G : Group} (x y : G) => x * inverse y

| 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 8 #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 = 0) (a With#.#0) \level Or.levelProp (\lam p q => apartNonZero q p)
=> \case decideEq a 0 \with {
| yes e => inl e
| no q => inr (nonZeroApart q)
}
}
}

\func \infixl 6 - {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