Move verified algebra interfaces to Control.Algebra

I was running into some weird import issues, and this seems to solve
them. Interfaces.Verified as a module probably ought to be abolished,
as it really isn't very useful as a grouping.

Author: nickdrozd

libs/contrib/Control/Algebra.idr

@@ -145,3 +145,27 @@ mtimes (S k) x = stimes (S k) x
 --   Structures where "abs" make sense.
 --   Euclidean domains, etc.
 --   Where to put fromInteger and fromRational?
+
+-- "Verified" Interfaces -----------------
+
+interface Semigroup a => VerifiedSemigroup a where
+  semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
+
+interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
+  monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
+  monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
+
+interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
+  groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
+
+interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
+  abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
+
+interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
+  ringOpIsAssociative   : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
+  ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
+  ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
+
+interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
+  ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
+  ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r

libs/contrib/Control/Algebra/ComplexImplementations.idr

@@ -1,6 +1,5 @@
 module Control.Algebra.ComplexImplementations
 
-import Interfaces.Verified
 import Data.Complex
 import Control.Algebra
 import Control.Algebra.Laws

libs/contrib/Control/Algebra/Laws.idr

@@ -2,7 +2,6 @@ module Control.Algebra.Laws
 
 import Prelude.Algebra as A
 import Control.Algebra as Alg
-import Interfaces.Verified
 
 %access public export
 %default total

libs/contrib/Control/Algebra/VerifiedImplementations.idr

@@ -1,6 +1,5 @@
 module Control.VerifiedInterfaces
 
-import Interfaces.Verified
 import Control.Algebra
 import Control.Algebra.Lattice
 import Control.Algebra.NumericImplementations

libs/contrib/Control/Isomorphism/Vect.idr

@@ -2,7 +2,6 @@ module Control.Isomorphism.Vect
 
 import Control.Isomorphism
 import Data.Vect
-import Interfaces.Verified
 
 %default total
 %access public export

libs/contrib/Data/Bool/Algebra.idr

@@ -1,7 +1,6 @@
 module Data.Bool.Algebra
 
 import Control.Algebra
-import Interfaces.Verified
 
 %access public export
 %default total

libs/contrib/Data/BoundedList.idr

@@ -2,7 +2,7 @@ module Data.BoundedList
 
 import Data.Fin
 import Data.Vect
-import Interfaces.Verified
+import Control.Algebra
 
 %access public export
 %default total

libs/contrib/Data/Matrix/Algebraic.idr

@@ -3,10 +3,10 @@
 ||| and `Control.Algebra.VectorSpace`.
 module Data.Matrix.Algebraic
 
+import public Data.Vect
 import public Control.Algebra
 import public Control.Algebra.VectorSpace
 import public Control.Algebra.NumericImplementations
-import public Interfaces.Verified
 
 import public Data.Matrix
 
@@ -44,13 +44,6 @@ implementation Ring a => Ring (Vect n a) where
 implementation RingWithUnity a => RingWithUnity (Vect n a) where
   unity {n} = replicate n unity
 
-implementation RingWithUnity a => Module a (Vect n a) where
-  (<#>) r = map (r <.>)
-
-implementation RingWithUnity a => Module a (Vect n (Vect l a)) where
-  (<#>) r = map (r <#>)
--- should be Module a b => Module a (Vect n b), but results in 'overlapping implementation'
-
 -----------------------------------------------------------------------
 --                        (Ring) Vector functions
 -----------------------------------------------------------------------
@@ -212,3 +205,14 @@ VerifiedRingWithUnity a => VerifiedRingWithUnity (Vect n a) where
     rewrite ringWithUnityIsUnityL x in
       rewrite ringWithUnityIsUnityL xs in
         Refl
+
+-- Vector spaces -----------------------
+
+-- These need to come after the "verified" implementations because ???
+
+implementation RingWithUnity a => Module a (Vect n a) where
+  (<#>) r = map (r <.>)
+
+implementation RingWithUnity a => Module a (Vect n (Vect l a)) where
+  (<#>) r = map (r <#>)
+-- should be Module a b => Module a (Vect n b), but results in 'overlapping implementation'

libs/contrib/Data/Monoid.idr

@@ -2,7 +2,7 @@
 ||| https://hackage.haskell.org/package/base-4.9.0.0/docs/src/Data.Monoid.html
 module Data.Monoid
 
-import Interfaces.Verified
+import Control.Algebra
 
 %access public export
 %default total

libs/contrib/Data/Sign.idr

@@ -2,7 +2,6 @@ module Data.Sign
 
 import Prelude.Algebra
 import Control.Algebra
-import Interfaces.Verified
 
 %access public export