From d7ca30b710fc5321186ecaa31beeb3bcadfdbe79 Mon Sep 17 00:00:00 2001
From: Nick Drozd <nicholasdrozd@gmail.com>
Date: Wed, 10 Jun 2020 18:36:34 -0500
Subject: [PATCH 1/2] Add Algebra interfaces and laws

---
 libs/contrib/Control/Algebra.idr      | 154 ++++++++++++
 libs/contrib/Control/Algebra/Laws.idr | 331 ++++++++++++++++++++++++++
 libs/contrib/contrib.ipkg             |   3 +
 3 files changed, 488 insertions(+)
 create mode 100644 libs/contrib/Control/Algebra.idr
 create mode 100644 libs/contrib/Control/Algebra/Laws.idr

diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr
new file mode 100644
index 00000000000..f8d877ffa54
--- /dev/null
+++ b/libs/contrib/Control/Algebra.idr
@@ -0,0 +1,154 @@
+module Control.Algebra
+
+infixl 6 <->
+infixl 7 <.>
+
+public export
+interface Semigroup ty => SemigroupV ty where
+  semigroupOpIsAssociative : (l, c, r : ty) ->
+    l <+> (c <+> r) = (l <+> c) <+> r
+
+public export
+interface (Monoid ty, SemigroupV ty) => MonoidV ty where
+  monoidNeutralIsNeutralL : (l : ty) -> l <+> neutral {ty} = l
+  monoidNeutralIsNeutralR : (r : ty) -> neutral {ty} <+> r = r
+
+||| Sets equipped with a single binary operation that is associative,
+||| along with a neutral element for that binary operation and
+||| inverses for all elements. Satisfies the following laws:
+|||
+||| + Associativity of `<+>`:
+|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+||| + Neutral for `<+>`:
+|||     forall a,     a <+> neutral   == a
+|||     forall a,     neutral <+> a   == a
+||| + Inverse for `<+>`:
+|||     forall a,     a <+> inverse a == neutral
+|||     forall a,     inverse a <+> a == neutral
+public export
+interface MonoidV ty => Group ty where
+  inverse : ty -> ty
+
+  groupInverseIsInverseR : (r : ty) -> inverse r <+> r = neutral {ty}
+
+(<->) : Group ty => ty -> ty -> ty
+(<->) left right = left <+> (inverse right)
+
+||| Sets equipped with a single binary operation that is associative
+||| and commutative, along with a neutral element for that binary
+||| operation and inverses for all elements. Satisfies the following
+||| laws:
+|||
+||| + Associativity of `<+>`:
+|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+||| + Commutativity of `<+>`:
+|||     forall a b,   a <+> b         == b <+> a
+||| + Neutral for `<+>`:
+|||     forall a,     a <+> neutral   == a
+|||     forall a,     neutral <+> a   == a
+||| + Inverse for `<+>`:
+|||     forall a,     a <+> inverse a == neutral
+|||     forall a,     inverse a <+> a == neutral
+public export
+interface Group ty => AbelianGroup ty where
+  groupOpIsCommutative : (l, r : ty) -> l <+> r = r <+> l
+
+||| A homomorphism is a mapping that preserves group structure.
+public export
+interface (Group a, Group b) => GroupHomomorphism a b where
+  to : a -> b
+
+  toGroup : (x, y : a) ->
+    to (x <+> y) = (to x) <+> (to y)
+
+||| Sets equipped with two binary operations, one associative and
+||| commutative supplied with a neutral element, and the other
+||| associative, with distributivity laws relating the two operations.
+||| Satisfies the following laws:
+|||
+||| + Associativity of `<+>`:
+|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+||| + Commutativity of `<+>`:
+|||     forall a b,   a <+> b         == b <+> a
+||| + Neutral for `<+>`:
+|||     forall a,     a <+> neutral   == a
+|||     forall a,     neutral <+> a   == a
+||| + Inverse for `<+>`:
+|||     forall a,     a <+> inverse a == neutral
+|||     forall a,     inverse a <+> a == neutral
+||| + Associativity of `<.>`:
+|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+||| + Distributivity of `<.>` and `<+>`:
+|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
+|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
+public export
+interface Group ty => Ring ty where
+  (<.>) : ty -> ty -> ty
+
+  ringOpIsAssociative   : (l, c, r : ty) ->
+    l <.> (c <.> r) = (l <.> c) <.> r
+  ringOpIsDistributiveL : (l, c, r : ty) ->
+    l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
+  ringOpIsDistributiveR : (l, c, r : ty) ->
+    (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
+
+||| Sets equipped with two binary operations, one associative and
+||| commutative supplied with a neutral element, and the other
+||| associative supplied with a neutral element, with distributivity
+||| laws relating the two operations. Satisfies the following laws:
+|||
+||| +  Associativity of `<+>`:
+|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+||| + Commutativity of `<+>`:
+|||     forall a b,   a <+> b         == b <+> a
+||| + Neutral for `<+>`:
+|||     forall a,     a <+> neutral   == a
+|||     forall a,     neutral <+> a   == a
+||| + Inverse for `<+>`:
+|||     forall a,     a <+> inverse a == neutral
+|||     forall a,     inverse a <+> a == neutral
+||| + Associativity of `<.>`:
+|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+||| + Neutral for `<.>`:
+|||     forall a,     a <.> unity     == a
+|||     forall a,     unity <.> a     == a
+||| + Distributivity of `<.>` and `<+>`:
+|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
+|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
+public export
+interface Ring ty => RingWithUnity ty where
+  unity : ty
+
+  unityIsRingIdL : (l : ty) -> l <.> unity = l
+  unityIsRingIdR : (r : ty) -> unity <.> r = r
+
+||| Sets equipped with two binary operations – both associative,
+||| commutative and possessing a neutral element – and distributivity
+||| laws relating the two operations. All elements except the additive
+||| identity should have a multiplicative inverse. Should (but may
+||| not) satisfy the following laws:
+|||
+||| + Associativity of `<+>`:
+|||     forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
+||| + Commutativity of `<+>`:
+|||     forall a b,   a <+> b         == b <+> a
+||| + Neutral for `<+>`:
+|||     forall a,     a <+> neutral   == a
+|||     forall a,     neutral <+> a   == a
+||| + Inverse for `<+>`:
+|||     forall a,     a <+> inverse a == neutral
+|||     forall a,     inverse a <+> a == neutral
+||| + Associativity of `<.>`:
+|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+||| + Unity for `<.>`:
+|||     forall a,     a <.> unity     == a
+|||     forall a,     unity <.> a     == a
+||| + InverseM of `<.>`, except for neutral
+|||     forall a /= neutral,  a <.> inverseM a == unity
+|||     forall a /= neutral,  inverseM a <.> a == unity
+||| + Distributivity of `<.>` and `<+>`:
+|||     forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
+|||     forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
+public export
+interface RingWithUnity ty => Field ty where
+  inverseM : (x : ty) -> Not (x = neutral {ty}) -> ty
diff --git a/libs/contrib/Control/Algebra/Laws.idr b/libs/contrib/Control/Algebra/Laws.idr
new file mode 100644
index 00000000000..d08f2822a68
--- /dev/null
+++ b/libs/contrib/Control/Algebra/Laws.idr
@@ -0,0 +1,331 @@
+module Control.Algebra.Laws
+
+import Prelude
+import Control.Algebra
+
+%default total
+
+-- Monoids
+
+||| Inverses are unique.
+public export
+uniqueInverse : MonoidV ty => (x, y, z : ty) ->
+  y <+> x = neutral {ty} -> x <+> z = neutral {ty} -> y = z
+uniqueInverse x y z p q =
+  rewrite sym $ monoidNeutralIsNeutralL y in
+    rewrite sym q in
+      rewrite semigroupOpIsAssociative y x z in
+  rewrite p in
+    rewrite monoidNeutralIsNeutralR z in
+      Refl
+
+-- Groups
+
+||| Only identity is self-squaring.
+public export
+selfSquareId : Group ty => (x : ty) ->
+  x <+> x = x -> x = neutral {ty}
+selfSquareId x p =
+  rewrite sym $ monoidNeutralIsNeutralR x in
+    rewrite sym $ groupInverseIsInverseR x in
+  rewrite sym $ semigroupOpIsAssociative (inverse x) x x in
+    rewrite p in
+      Refl
+
+||| Inverse elements commute.
+public export
+inverseCommute : Group ty => (x, y : ty) ->
+  y <+> x = neutral {ty} -> x <+> y = neutral {ty}
+inverseCommute x y p = selfSquareId (x <+> y) prop where
+  prop : (x <+> y) <+> (x <+> y) = x <+> y
+  prop =
+    rewrite sym $ semigroupOpIsAssociative x y (x <+> y) in
+      rewrite semigroupOpIsAssociative y x y in
+    rewrite p in
+      rewrite monoidNeutralIsNeutralR y in
+        Refl
+
+||| Every element has a right inverse.
+public export
+groupInverseIsInverseL : Group ty => (x : ty) ->
+  x <+> inverse x = neutral {ty}
+groupInverseIsInverseL x =
+  inverseCommute x (inverse x) (groupInverseIsInverseR x)
+
+||| -(-x) = x
+public export
+inverseSquaredIsIdentity : Group ty => (x : ty) ->
+  inverse (inverse x) = x
+-- inverseSquaredIsIdentity x =
+--   let x' = inverse x in
+--     uniqueInverse
+--       x'
+--       (inverse x')
+--       x
+--       (groupInverseIsInverseR x')
+--       (groupInverseIsInverseR x)
+
+||| If every square in a group is identity, the group is commutative.
+public export
+squareIdCommutative : Group ty => (x, y : ty) ->
+  ((a : ty) -> a <+> a = neutral {ty}) ->
+  x <+> y = y <+> x
+-- squareIdCommutative x y p =
+--   let
+--     xy = x <+> y
+--     yx = y <+> x
+--       in
+--   uniqueInverse xy xy yx (p xy) prop where
+--     prop : (x <+> y) <+> (y <+> x) = neutral {ty}
+--     prop =
+--       rewrite sym $ semigroupOpIsAssociative x y (y <+> x) in
+--         rewrite semigroupOpIsAssociative y y x in
+--       rewrite p y in
+--         rewrite monoidNeutralIsNeutralR x in
+--           p x
+
+||| -0 = 0
+public export
+inverseNeutralIsNeutral : Group ty =>
+  inverse (neutral {ty}) = neutral {ty}
+-- inverseNeutralIsNeutral {ty} =
+--   let e = neutral {ty} in
+--     rewrite sym $ cong inverse (groupInverseIsInverseL e) in
+--       rewrite monoidNeutralIsNeutralR $ inverse e in
+--         inverseSquaredIsIdentity e
+
+||| -(x + y) = -y + -x
+public export
+inverseOfSum : Group ty => (l, r : ty) ->
+  inverse (l <+> r) = inverse r <+> inverse l
+-- inverseOfSum {ty} l r =
+--   let
+--     e = neutral {ty}
+--     il = inverse l
+--     ir = inverse r
+--     lr = l <+> r
+--     ilr = inverse lr
+--     iril = ir <+> il
+--     ile = il <+> e
+--       in
+--   -- expand
+--   rewrite sym $ monoidNeutralIsNeutralR ilr in
+--     rewrite sym $ groupInverseIsInverseR r in
+--       rewrite sym $ monoidNeutralIsNeutralL ir in
+--         rewrite sym $ groupInverseIsInverseR l in
+--   -- shuffle
+--   rewrite semigroupOpIsAssociative ir il l in
+--     rewrite sym $ semigroupOpIsAssociative iril l r in
+--       rewrite sym $ semigroupOpIsAssociative iril lr ilr in
+--   -- contract
+--   rewrite sym $ monoidNeutralIsNeutralL il in
+--     rewrite groupInverseIsInverseL lr in
+--       rewrite sym $ semigroupOpIsAssociative (ir <+> ile) l ile in
+--         rewrite semigroupOpIsAssociative l il e in
+--           rewrite groupInverseIsInverseL l in
+--             rewrite monoidNeutralIsNeutralL e in
+--               Refl
+
+||| y = z if x + y = x + z
+public export
+cancelLeft : Group ty => (x, y, z : ty) ->
+  x <+> y = x <+> z -> y = z
+cancelLeft x y z p =
+  rewrite sym $ monoidNeutralIsNeutralR y in
+    rewrite sym $ groupInverseIsInverseR x in
+      rewrite sym $ semigroupOpIsAssociative (inverse x) x y in
+        rewrite p in
+      rewrite semigroupOpIsAssociative (inverse x) x z in
+    rewrite groupInverseIsInverseR x in
+  monoidNeutralIsNeutralR z
+
+||| y = z if y + x = z + x.
+public export
+cancelRight : Group ty => (x, y, z : ty) ->
+  y <+> x = z <+> x -> y = z
+cancelRight x y z p =
+  rewrite sym $ monoidNeutralIsNeutralL y in
+    rewrite sym $ groupInverseIsInverseL x in
+      rewrite semigroupOpIsAssociative y x (inverse x) in
+        rewrite p in
+      rewrite sym $ semigroupOpIsAssociative z x (inverse x) in
+    rewrite groupInverseIsInverseL x in
+  monoidNeutralIsNeutralL z
+
+||| ab = 0 -> a = b^-1
+public export
+neutralProductInverseR : Group ty => (a, b : ty) ->
+  a <+> b = neutral {ty} -> a = inverse b
+neutralProductInverseR a b prf =
+  cancelRight  b a (inverse b) $
+    trans prf $ sym $ groupInverseIsInverseR b
+
+||| ab = 0 -> a^-1 = b
+public export
+neutralProductInverseL : Group ty => (a, b : ty) ->
+  a <+> b = neutral {ty} -> inverse a = b
+neutralProductInverseL a b prf =
+  cancelLeft a (inverse a) b $
+    trans (groupInverseIsInverseL a) $ sym prf
+
+||| For any a and b, ax = b and ya = b have solutions.
+public export
+latinSquareProperty : Group ty => (a, b : ty) ->
+  ((x : ty ** a <+> x = b),
+    (y : ty ** y <+> a = b))
+-- latinSquareProperty a b =
+--   let a' = inverse a in
+--     (((a' <+> b) **
+--       rewrite semigroupOpIsAssociative a a' b in
+--         rewrite groupInverseIsInverseL a in
+--           monoidNeutralIsNeutralR b),
+--     (b <+> a' **
+--       rewrite sym $ semigroupOpIsAssociative b a' a in
+--         rewrite groupInverseIsInverseR a in
+--           monoidNeutralIsNeutralL b))
+
+||| For any a, b, x, the solution to ax = b is unique.
+public export
+uniqueSolutionR : Group ty => (a, b, x, y : ty) ->
+  a <+> x = b -> a <+> y = b -> x = y
+uniqueSolutionR a b x y p q = cancelLeft a x y $ trans p (sym q)
+
+||| For any a, b, y, the solution to ya = b is unique.
+public export
+uniqueSolutionL : Group t => (a, b, x, y : t) ->
+  x <+> a = b -> y <+> a = b -> x = y
+uniqueSolutionL a b x y p q = cancelRight a x y $ trans p (sym q)
+
+||| -(x + y) = -x + -y
+public export
+inverseDistributesOverGroupOp : AbelianGroup ty => (l, r : ty) ->
+  inverse (l <+> r) = inverse l <+> inverse r
+inverseDistributesOverGroupOp l r =
+  rewrite groupOpIsCommutative (inverse l) (inverse r) in
+    inverseOfSum l r
+
+||| Homomorphism preserves neutral.
+public export
+homoNeutral : GroupHomomorphism a b =>
+  to (neutral {ty=a}) = neutral {ty=b}
+homoNeutral =
+  selfSquareId (to neutral) $
+    trans (sym $ toGroup neutral neutral) $
+      cong to $ monoidNeutralIsNeutralL neutral
+
+||| Homomorphism preserves inverses.
+public export
+homoInverse : GroupHomomorphism a b => (x : a) ->
+  the b (to $ inverse x) = the b (inverse $ to x)
+homoInverse x =
+  cancelRight (to x) (to $ inverse x) (inverse $ to x) $
+    trans (sym $ toGroup (inverse x) x) $
+      trans (cong to $ groupInverseIsInverseR x) $
+        trans homoNeutral $
+          sym $ groupInverseIsInverseR (to x)
+
+-- Rings
+
+||| 0x = x
+public export
+multNeutralAbsorbingL : Ring ty => (r : ty) ->
+  neutral {ty} <.> r = neutral {ty}
+-- multNeutralAbsorbingL {ty} r =
+--   let
+--     e = neutral {ty}
+--     ir = inverse r
+--     exr = e <.> r
+--     iexr = inverse exr
+--       in
+--   rewrite sym $ monoidNeutralIsNeutralR exr in
+--     rewrite sym $ groupInverseIsInverseR exr in
+--   rewrite sym $ semigroupOpIsAssociative iexr exr ((iexr <+> exr) <.> r) in
+--     rewrite groupInverseIsInverseR exr in
+--   rewrite sym $ ringOpIsDistributiveR e e r in
+--     rewrite monoidNeutralIsNeutralR e in
+--   groupInverseIsInverseR exr
+
+||| x0 = 0
+public export
+multNeutralAbsorbingR : Ring ty => (l : ty) ->
+  l <.> neutral {ty} = neutral {ty}
+-- multNeutralAbsorbingR {ty} l =
+--   let
+--     e = neutral {ty}
+--     il = inverse l
+--     lxe = l <.> e
+--     ilxe = inverse lxe
+--       in
+--   rewrite sym $ monoidNeutralIsNeutralL lxe in
+--     rewrite sym $ groupInverseIsInverseL lxe in
+--   rewrite semigroupOpIsAssociative (l <.> (lxe <+> ilxe)) lxe ilxe in
+--     rewrite groupInverseIsInverseL lxe in
+--   rewrite sym $ ringOpIsDistributiveL l e e in
+--     rewrite monoidNeutralIsNeutralL e in
+--   groupInverseIsInverseL lxe
+
+||| (-x)y = -(xy)
+public export
+multInverseInversesL : Ring ty => (l, r : ty) ->
+  inverse l <.> r = inverse (l <.> r)
+-- multInverseInversesL l r =
+--   let
+--     il = inverse l
+--     lxr = l <.> r
+--     ilxr = il <.> r
+--     i_lxr = inverse lxr
+--       in
+--   rewrite sym $ monoidNeutralIsNeutralR ilxr in
+--     rewrite sym $ groupInverseIsInverseR lxr in
+--       rewrite sym $ semigroupOpIsAssociative i_lxr lxr ilxr in
+--   rewrite sym $ ringOpIsDistributiveR l il r in
+--     rewrite groupInverseIsInverseL l in
+--   rewrite multNeutralAbsorbingL r in
+--     monoidNeutralIsNeutralL i_lxr
+
+||| x(-y) = -(xy)
+public export
+multInverseInversesR : Ring ty => (l, r : ty) ->
+  l <.> inverse r = inverse (l <.> r)
+-- multInverseInversesR l r =
+--   let
+--     ir = inverse r
+--     lxr = l <.> r
+--     lxir = l <.> ir
+--     ilxr = inverse lxr
+--       in
+--   rewrite sym $ monoidNeutralIsNeutralL lxir in
+--     rewrite sym $ groupInverseIsInverseL lxr in
+--       rewrite semigroupOpIsAssociative lxir lxr ilxr in
+--   rewrite sym $ ringOpIsDistributiveL l ir r in
+--     rewrite groupInverseIsInverseR r in
+--   rewrite multNeutralAbsorbingR l in
+--     monoidNeutralIsNeutralR ilxr
+
+||| (-x)(-y) = xy
+public export
+multNegativeByNegativeIsPositive : Ring ty => (l, r : ty) ->
+  inverse l <.> inverse r = l <.> r
+multNegativeByNegativeIsPositive l r =
+    rewrite multInverseInversesR (inverse l) r in
+    rewrite sym $ multInverseInversesL (inverse l) r in
+    rewrite inverseSquaredIsIdentity l in
+    Refl
+
+||| (-1)x = -x
+public export
+inverseOfUnityR : RingWithUnity ty => (x : ty) ->
+  inverse (unity {ty}) <.> x = inverse x
+inverseOfUnityR x =
+  rewrite multInverseInversesL unity x in
+    rewrite unityIsRingIdR x in
+      Refl
+
+||| x(-1) = -x
+public export
+inverseOfUnityL : RingWithUnity ty => (x : ty) ->
+  x <.> inverse (unity {ty}) = inverse x
+inverseOfUnityL x =
+  rewrite multInverseInversesR x unity in
+    rewrite unityIsRingIdL x in
+      Refl
diff --git a/libs/contrib/contrib.ipkg b/libs/contrib/contrib.ipkg
index a351ffa4b6f..812ee2c63fb 100644
--- a/libs/contrib/contrib.ipkg
+++ b/libs/contrib/contrib.ipkg
@@ -2,6 +2,9 @@ package contrib
 
 modules = Control.Delayed,
 
+          Control.Algebra,
+          Control.Algebra.Laws,
+
           Data.Linear.Array,
 
           Data.List.TailRec,

From 028a1cb9608196b44e866d436db83f5c41989a86 Mon Sep 17 00:00:00 2001
From: Nick Drozd <nicholasdrozd@gmail.com>
Date: Wed, 17 Jun 2020 20:01:01 -0500
Subject: [PATCH 2/2] Cut some let bindings

---
 libs/contrib/Control/Algebra/Laws.idr | 204 +++++++++++---------------
 1 file changed, 82 insertions(+), 122 deletions(-)

diff --git a/libs/contrib/Control/Algebra/Laws.idr b/libs/contrib/Control/Algebra/Laws.idr
index d08f2822a68..2c82b96153a 100644
--- a/libs/contrib/Control/Algebra/Laws.idr
+++ b/libs/contrib/Control/Algebra/Laws.idr
@@ -56,74 +56,59 @@ groupInverseIsInverseL x =
 public export
 inverseSquaredIsIdentity : Group ty => (x : ty) ->
   inverse (inverse x) = x
--- inverseSquaredIsIdentity x =
---   let x' = inverse x in
---     uniqueInverse
---       x'
---       (inverse x')
---       x
---       (groupInverseIsInverseR x')
---       (groupInverseIsInverseR x)
+inverseSquaredIsIdentity {ty} x =
+  uniqueInverse
+    (inverse x)
+    (inverse $ inverse x)
+    x
+    (groupInverseIsInverseR $ inverse x)
+    (groupInverseIsInverseR x)
 
 ||| If every square in a group is identity, the group is commutative.
 public export
 squareIdCommutative : Group ty => (x, y : ty) ->
   ((a : ty) -> a <+> a = neutral {ty}) ->
   x <+> y = y <+> x
--- squareIdCommutative x y p =
---   let
---     xy = x <+> y
---     yx = y <+> x
---       in
---   uniqueInverse xy xy yx (p xy) prop where
---     prop : (x <+> y) <+> (y <+> x) = neutral {ty}
---     prop =
---       rewrite sym $ semigroupOpIsAssociative x y (y <+> x) in
---         rewrite semigroupOpIsAssociative y y x in
---       rewrite p y in
---         rewrite monoidNeutralIsNeutralR x in
---           p x
+squareIdCommutative x y p =
+  uniqueInverse (x <+> y) (x <+> y) (y <+> x) (p (x <+> y)) prop where
+    prop : (x <+> y) <+> (y <+> x) = neutral {ty}
+    prop =
+      rewrite sym $ semigroupOpIsAssociative x y (y <+> x) in
+        rewrite semigroupOpIsAssociative y y x in
+      rewrite p y in
+        rewrite monoidNeutralIsNeutralR x in
+          p x
 
 ||| -0 = 0
 public export
 inverseNeutralIsNeutral : Group ty =>
   inverse (neutral {ty}) = neutral {ty}
--- inverseNeutralIsNeutral {ty} =
---   let e = neutral {ty} in
---     rewrite sym $ cong inverse (groupInverseIsInverseL e) in
---       rewrite monoidNeutralIsNeutralR $ inverse e in
---         inverseSquaredIsIdentity e
+inverseNeutralIsNeutral {ty} =
+  rewrite sym $ cong inverse (groupInverseIsInverseL (neutral {ty})) in
+    rewrite monoidNeutralIsNeutralR $ inverse (neutral {ty}) in
+      inverseSquaredIsIdentity (neutral {ty})
 
-||| -(x + y) = -y + -x
-public export
-inverseOfSum : Group ty => (l, r : ty) ->
-  inverse (l <+> r) = inverse r <+> inverse l
+-- ||| -(x + y) = -y + -x
+-- public export
+-- inverseOfSum : Group ty => (l, r : ty) ->
+--   inverse (l <+> r) = inverse r <+> inverse l
 -- inverseOfSum {ty} l r =
---   let
---     e = neutral {ty}
---     il = inverse l
---     ir = inverse r
---     lr = l <+> r
---     ilr = inverse lr
---     iril = ir <+> il
---     ile = il <+> e
---       in
 --   -- expand
---   rewrite sym $ monoidNeutralIsNeutralR ilr in
+--   rewrite sym $ monoidNeutralIsNeutralR $ inverse $ l <+> r in
 --     rewrite sym $ groupInverseIsInverseR r in
---       rewrite sym $ monoidNeutralIsNeutralL ir in
+--       rewrite sym $ monoidNeutralIsNeutralL $ inverse r in
 --         rewrite sym $ groupInverseIsInverseR l in
 --   -- shuffle
---   rewrite semigroupOpIsAssociative ir il l in
---     rewrite sym $ semigroupOpIsAssociative iril l r in
---       rewrite sym $ semigroupOpIsAssociative iril lr ilr in
+--   rewrite semigroupOpIsAssociative (inverse r) (inverse l) l in
+--     rewrite sym $ semigroupOpIsAssociative (inverse r <+> inverse l) l r in
+--       rewrite sym $ semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse $ l <+> r) in
 --   -- contract
---   rewrite sym $ monoidNeutralIsNeutralL il in
---     rewrite groupInverseIsInverseL lr in
---       rewrite sym $ semigroupOpIsAssociative (ir <+> ile) l ile in
---         rewrite semigroupOpIsAssociative l il e in
+--   rewrite sym $ monoidNeutralIsNeutralL $ inverse l in
+--     rewrite groupInverseIsInverseL $ l <+> r in
+--       rewrite sym $ semigroupOpIsAssociative (inverse r <+> (inverse l <+> neutral)) l (inverse l <+> neutral) in
+--         rewrite semigroupOpIsAssociative l (inverse l) neutral in
 --           rewrite groupInverseIsInverseL l in
---             rewrite monoidNeutralIsNeutralL e in
+--             rewrite monoidNeutralIsNeutralL $ the ty neutral in
 --               Refl
 
 ||| y = z if x + y = x + z
@@ -173,16 +158,15 @@ public export
 latinSquareProperty : Group ty => (a, b : ty) ->
   ((x : ty ** a <+> x = b),
     (y : ty ** y <+> a = b))
--- latinSquareProperty a b =
---   let a' = inverse a in
---     (((a' <+> b) **
---       rewrite semigroupOpIsAssociative a a' b in
---         rewrite groupInverseIsInverseL a in
---           monoidNeutralIsNeutralR b),
---     (b <+> a' **
---       rewrite sym $ semigroupOpIsAssociative b a' a in
---         rewrite groupInverseIsInverseR a in
---           monoidNeutralIsNeutralL b))
+latinSquareProperty a b =
+  ((((inverse a) <+> b) **
+    rewrite semigroupOpIsAssociative a (inverse a) b in
+      rewrite groupInverseIsInverseL a in
+        monoidNeutralIsNeutralR b),
+  (b <+> (inverse a) **
+    rewrite sym $ semigroupOpIsAssociative b (inverse a) a in
+      rewrite groupInverseIsInverseR a in
+        monoidNeutralIsNeutralL b))
 
 ||| For any a, b, x, the solution to ax = b is unique.
 public export
@@ -196,13 +180,13 @@ uniqueSolutionL : Group t => (a, b, x, y : t) ->
   x <+> a = b -> y <+> a = b -> x = y
 uniqueSolutionL a b x y p q = cancelRight a x y $ trans p (sym q)
 
-||| -(x + y) = -x + -y
-public export
-inverseDistributesOverGroupOp : AbelianGroup ty => (l, r : ty) ->
-  inverse (l <+> r) = inverse l <+> inverse r
-inverseDistributesOverGroupOp l r =
-  rewrite groupOpIsCommutative (inverse l) (inverse r) in
-    inverseOfSum l r
+-- ||| -(x + y) = -x + -y
+-- public export
+-- inverseDistributesOverGroupOp : AbelianGroup ty => (l, r : ty) ->
+--   inverse (l <+> r) = inverse l <+> inverse r
+-- inverseDistributesOverGroupOp l r =
+--   rewrite groupOpIsCommutative (inverse l) (inverse r) in
+--     inverseOfSum l r
 
 ||| Homomorphism preserves neutral.
 public export
@@ -230,77 +214,53 @@ homoInverse x =
 public export
 multNeutralAbsorbingL : Ring ty => (r : ty) ->
   neutral {ty} <.> r = neutral {ty}
--- multNeutralAbsorbingL {ty} r =
---   let
---     e = neutral {ty}
---     ir = inverse r
---     exr = e <.> r
---     iexr = inverse exr
---       in
---   rewrite sym $ monoidNeutralIsNeutralR exr in
---     rewrite sym $ groupInverseIsInverseR exr in
---   rewrite sym $ semigroupOpIsAssociative iexr exr ((iexr <+> exr) <.> r) in
---     rewrite groupInverseIsInverseR exr in
---   rewrite sym $ ringOpIsDistributiveR e e r in
---     rewrite monoidNeutralIsNeutralR e in
---   groupInverseIsInverseR exr
+multNeutralAbsorbingL {ty} r =
+  rewrite sym $ monoidNeutralIsNeutralR $ neutral <.> r in
+    rewrite sym $ groupInverseIsInverseR $ neutral <.> r in
+  rewrite sym $ semigroupOpIsAssociative (inverse $ neutral <.> r) (neutral <.> r) (((inverse $ neutral <.> r) <+> (neutral <.> r)) <.> r) in
+    rewrite groupInverseIsInverseR $ neutral <.> r in
+  rewrite sym $ ringOpIsDistributiveR neutral neutral r in
+    rewrite monoidNeutralIsNeutralR $ the ty neutral in
+  groupInverseIsInverseR $ neutral <.> r
 
 ||| x0 = 0
 public export
 multNeutralAbsorbingR : Ring ty => (l : ty) ->
   l <.> neutral {ty} = neutral {ty}
--- multNeutralAbsorbingR {ty} l =
---   let
---     e = neutral {ty}
---     il = inverse l
---     lxe = l <.> e
---     ilxe = inverse lxe
---       in
---   rewrite sym $ monoidNeutralIsNeutralL lxe in
---     rewrite sym $ groupInverseIsInverseL lxe in
---   rewrite semigroupOpIsAssociative (l <.> (lxe <+> ilxe)) lxe ilxe in
---     rewrite groupInverseIsInverseL lxe in
---   rewrite sym $ ringOpIsDistributiveL l e e in
---     rewrite monoidNeutralIsNeutralL e in
---   groupInverseIsInverseL lxe
+multNeutralAbsorbingR {ty} l =
+  rewrite sym $ monoidNeutralIsNeutralL $ l <.> neutral in
+    rewrite sym $ groupInverseIsInverseL $ l <.> neutral in
+  rewrite semigroupOpIsAssociative (l <.> ((l <.> neutral) <+> (inverse $ l <.> neutral))) (l <.> neutral) (inverse $ l <.> neutral) in
+    rewrite groupInverseIsInverseL $ l <.> neutral in
+  rewrite sym $ ringOpIsDistributiveL l neutral neutral in
+    rewrite monoidNeutralIsNeutralL $ the ty neutral in
+  groupInverseIsInverseL $ l <.> neutral
 
 ||| (-x)y = -(xy)
 public export
 multInverseInversesL : Ring ty => (l, r : ty) ->
   inverse l <.> r = inverse (l <.> r)
--- multInverseInversesL l r =
---   let
---     il = inverse l
---     lxr = l <.> r
---     ilxr = il <.> r
---     i_lxr = inverse lxr
---       in
---   rewrite sym $ monoidNeutralIsNeutralR ilxr in
---     rewrite sym $ groupInverseIsInverseR lxr in
---       rewrite sym $ semigroupOpIsAssociative i_lxr lxr ilxr in
---   rewrite sym $ ringOpIsDistributiveR l il r in
---     rewrite groupInverseIsInverseL l in
---   rewrite multNeutralAbsorbingL r in
---     monoidNeutralIsNeutralL i_lxr
+multInverseInversesL l r =
+  rewrite sym $ monoidNeutralIsNeutralR $ inverse l <.> r in
+    rewrite sym $ groupInverseIsInverseR $ l <.> r in
+      rewrite sym $ semigroupOpIsAssociative (inverse $ l <.> r) (l <.> r) (inverse l <.> r) in
+  rewrite sym $ ringOpIsDistributiveR l (inverse l) r in
+    rewrite groupInverseIsInverseL l in
+  rewrite multNeutralAbsorbingL r in
+    monoidNeutralIsNeutralL $ inverse $ l <.> r
 
 ||| x(-y) = -(xy)
 public export
 multInverseInversesR : Ring ty => (l, r : ty) ->
   l <.> inverse r = inverse (l <.> r)
--- multInverseInversesR l r =
---   let
---     ir = inverse r
---     lxr = l <.> r
---     lxir = l <.> ir
---     ilxr = inverse lxr
---       in
---   rewrite sym $ monoidNeutralIsNeutralL lxir in
---     rewrite sym $ groupInverseIsInverseL lxr in
---       rewrite semigroupOpIsAssociative lxir lxr ilxr in
---   rewrite sym $ ringOpIsDistributiveL l ir r in
---     rewrite groupInverseIsInverseR r in
---   rewrite multNeutralAbsorbingR l in
---     monoidNeutralIsNeutralR ilxr
+multInverseInversesR l r =
+  rewrite sym $ monoidNeutralIsNeutralL $ l <.> (inverse r) in
+    rewrite sym $ groupInverseIsInverseL (l <.> r) in
+      rewrite semigroupOpIsAssociative (l <.> (inverse r)) (l <.> r) (inverse $ l <.> r) in
+  rewrite sym $ ringOpIsDistributiveL l (inverse r) r in
+    rewrite groupInverseIsInverseR r in
+  rewrite multNeutralAbsorbingR l in
+    monoidNeutralIsNeutralR $ inverse $ l <.> r
 
 ||| (-x)(-y) = xy
 public export