Add some "verified" implementations

libs/contrib/Control/Algebra.idr

@@ -22,22 +22,6 @@ interface Monoid a => Group a where
 (<->) : Group a => a -> a -> a
 (<->) 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. Must 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
-interface Group a => AbelianGroup a where { }
-
 ||| 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.  Must satisfy the following
@@ -58,7 +42,7 @@ interface Group a => AbelianGroup a where { }
 ||| + 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)
-interface AbelianGroup a => Ring a where
+interface Group a => Ring a where
   (<.>) : a -> a -> a
 
 ||| Sets equipped with two binary operations, one associative and commutative
@@ -145,3 +129,41 @@ 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
+
+||| 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. Must 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
+interface VerifiedGroup a => AbelianGroup a where
+  abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
+
+interface (AbelianGroup 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

@@ -0,0 +1,68 @@
+module Control.Algebra.ComplexImplementations
+
+import Data.Complex
+import Control.Algebra
+import Control.Algebra.Laws
+import Control.Algebra.VectorSpace
+
+%access public export
+%default total
+
+Semigroup a => Semigroup (Complex a) where
+  (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
+
+Monoid a => Monoid (Complex a) where
+  neutral = (neutral :+ neutral)
+
+Group a => Group (Complex a) where
+  inverse (r :+ i) = (inverse r :+ inverse i)
+
+Ring a => Ring (Complex a) where
+  (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
+
+RingWithUnity a => RingWithUnity (Complex a) where
+  unity = (unity :+ neutral)
+
+RingWithUnity a => Module a (Complex a) where
+  (<#>) x = map (x <.>)
+
+RingWithUnity a => InnerProductSpace a (Complex a) where
+  (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z
+
+----------------------------------------
+
+VerifiedSemigroup a => VerifiedSemigroup (Complex a) where
+  semigroupOpIsAssociative (a :+ x) (b :+ y) (c :+ z) =
+    rewrite semigroupOpIsAssociative a b c in
+      rewrite semigroupOpIsAssociative x y z in
+        Refl
+
+VerifiedMonoid t => VerifiedMonoid (Complex t) where
+  monoidNeutralIsNeutralL (a :+ x) =
+    rewrite monoidNeutralIsNeutralL a in
+      rewrite monoidNeutralIsNeutralL x in
+        Refl
+
+  monoidNeutralIsNeutralR (a :+ x) =
+    rewrite monoidNeutralIsNeutralR a in
+      rewrite monoidNeutralIsNeutralR x in
+        Refl
+
+VerifiedGroup t => VerifiedGroup (Complex t) where
+  groupInverseIsInverseR (r :+ i) =
+    rewrite groupInverseIsInverseR r in
+      rewrite groupInverseIsInverseR i in
+        Refl
+
+AbelianGroup t => AbelianGroup (Complex t) where
+  abelianGroupOpIsCommutative (a :+ i) (b :+ j) =
+    rewrite abelianGroupOpIsCommutative a b in
+      rewrite abelianGroupOpIsCommutative i j in
+        Refl
+
+-- An interface resolution bug seems to make this impossible to prove.
+
+-- https://github.com/idris-lang/Idris-dev/issues/4853
+-- https://github.com/idris-lang/Idris2/issues/72
+
+-- VerifiedRing t => VerifiedRing (Complex t) where

libs/contrib/Control/Algebra/CyclicGroup.idr

@@ -0,0 +1,63 @@
+import Control.Algebra
+
+import Data.ZZ
+
+%access public export
+%default total
+
+----------------------------------------
+
+-- The Verified constraints here are required
+-- to work around an interface resolution bug.
+
+-- https://github.com/idris-lang/Idris-dev/issues/4853
+-- https://github.com/idris-lang/Idris2/issues/72
+
+mtimes' : VerifiedMonoid a => (n : Nat) -> a -> a
+mtimes' Z x = neutral
+mtimes' (S k) x = x <+> mtimes' k x
+
+gtimes : VerifiedGroup a => (n : ZZ) -> a -> a
+gtimes (Pos k) x = mtimes' k x
+gtimes (NegS k) x = mtimes' (S k) (inverse x)
+
+----------------------------------------
+
+mtimesTimes : VerifiedMonoid a => (x : a) -> (n, m : Nat) ->
+  mtimes' (n + m) x = mtimes' n x <+> mtimes' m x
+mtimesTimes x Z m = sym $ monoidNeutralIsNeutralR $ mtimes' m x
+mtimesTimes x (S k) m =
+  rewrite mtimesTimes x k m in
+    semigroupOpIsAssociative x (mtimes' k x) (mtimes' m x)
+
+-- TODO: prove this. It's definitely true in spirit, and I'm pretty
+-- sure the implementation of gtimes is correct, but working with ZZ
+-- is not easy.
+postulate
+gtimesTimes : VerifiedGroup a => (x : a) -> (n, m : ZZ) ->
+  gtimes (n + m) x = gtimes n x <+> gtimes m x
+
+gtimesCommutes : VerifiedGroup a => (x : a) -> (n, m : ZZ) ->
+  gtimes n x <+> gtimes m x = gtimes m x <+> gtimes n x
+gtimesCommutes x n m =
+  rewrite sym $ gtimesTimes x n m in
+    rewrite plusCommutativeZ n m in
+      gtimesTimes x m n
+
+||| A cyclic group is a group in which every element can be gotten by
+||| repeatedly adding or subtracting a particular element known as the
+||| generator.
+interface VerifiedGroup a => CyclicGroup a where
+  generator : (g : a ** (x : a) -> (n : ZZ ** x = gtimes n g))
+
+||| Every cyclic group is commutative.
+CyclicGroup a => AbelianGroup a where
+  abelianGroupOpIsCommutative {a} l r =
+    let
+      (g ** gen) = generator {a=a}
+      (n ** gl) = gen l
+      (m ** gr) = gen r
+        in
+    rewrite gl in
+      rewrite gr in
+        gtimesCommutes g n m

libs/contrib/Control/Algebra/GroupHomomorphism.idr

@@ -0,0 +1,30 @@
+import Prelude.Algebra as A
+import Control.Algebra
+import Control.Algebra.Laws
+
+%access public export
+
+||| A homomorphism is a mapping that preserves group structure.
+interface (VerifiedGroup a, VerifiedGroup b) => GroupHomomorphism a b where
+  to : a -> b
+  toGroup : (x, y : a) ->
+    to (x <+> y) = (to x) <+> (to y)
+
+||| Homomorphism preserves neutral.
+homoNeutral : GroupHomomorphism a b =>
+  to (the a A.neutral) = the b A.neutral
+homoNeutral {a} =
+  let ae = the a A.neutral in
+    selfSquareId (to ae) $
+      trans (sym $ toGroup ae ae) $
+        cong {f = to} $ monoidNeutralIsNeutralL ae
+
+||| Homomorphism preserves inverses.
+homoInverse : GroupHomomorphism a b => (x : a) ->
+  the b (to $ inverse x) = the b (inverse $ to x)
+homoInverse {a} {b} x =
+  cancelRight (to x) (to $ inverse x) (inverse $ to x) $
+    trans (sym $ toGroup (inverse x) x) $
+      trans (cong {f = to} $ groupInverseIsInverseR x) $
+        trans (homoNeutral {a=a} {b=b}) $
+          sym $ groupInverseIsInverseR (to x)

libs/contrib/Control/Algebra/Laws.idr

@@ -2,9 +2,9 @@ module Control.Algebra.Laws
 
 import Prelude.Algebra as A
 import Control.Algebra as Alg
-import Interfaces.Verified
 
-%access export
+%access public export
+%default total
 
 -- Monoids
 
@@ -143,6 +143,20 @@ cancelRight x y z p =
     rewrite groupInverseIsInverseL x in
   monoidNeutralIsNeutralL z
 
+||| ab = 0 -> a = b^-1
+neutralProductInverseR : VerifiedGroup ty => (a, b : ty) ->
+  a <+> b = A.neutral -> a = inverse b
+neutralProductInverseR a b prf =
+  cancelRight  b a (inverse b) $
+    trans prf $ sym $ groupInverseIsInverseR b
+
+||| ab = 0 -> a^-1 = b
+neutralProductInverseL : VerifiedGroup ty => (a, b : ty) ->
+  a <+> b = A.neutral -> 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.
 latinSquareProperty : VerifiedGroup t => (a, b : t) ->
   ((x : t ** a <+> x = b),
@@ -169,7 +183,7 @@ uniqueSolutionL : VerifiedGroup t => (a, b, x, y : t) ->
 uniqueSolutionL a b x y p q = cancelRight a x y $ trans p (sym q)
 
 ||| -(x + y) = -x + -y in any verified abelian group.
-inverseDistributesOverGroupOp : VerifiedAbelianGroup t => (l, r : t) ->
+inverseDistributesOverGroupOp : AbelianGroup t => (l, r : t) ->
   inverse (l <+> r) = inverse l <+> inverse r
 inverseDistributesOverGroupOp l r =
   rewrite abelianGroupOpIsCommutative (inverse l) (inverse r) in

libs/contrib/Control/Algebra/NumericImplementations.idr

@@ -3,8 +3,6 @@
 module Control.Algebra.NumericImplementations
 
 import Control.Algebra
-import Control.Algebra.VectorSpace
-import Data.Complex
 import Data.ZZ
 
 %access public export
@@ -20,8 +18,6 @@ Monoid Integer where
 Group Integer where
   inverse = (* -1)
 
-AbelianGroup Integer where
-
 Ring Integer where
   (<.>) = (*)
 
@@ -39,8 +35,6 @@ Monoid Int where
 Group Int where
   inverse = (* -1)
 
-AbelianGroup Int where
-
 Ring Int where
   (<.>) = (*)
 
@@ -58,8 +52,6 @@ Monoid Double where
 Group Double where
   inverse = (* -1)
 
-AbelianGroup Double where
-
 Ring Double where
   (<.>) = (*)
 
@@ -94,8 +86,6 @@ Field Double where
 Group ZZ using PlusZZMonoid where
   inverse = (* -1)
 
-AbelianGroup ZZ where
-
 [MultZZSemi] Semigroup ZZ where
   (<+>) = (*)
 
@@ -107,28 +97,3 @@ Ring ZZ where
 
 RingWithUnity ZZ where
   unity = 1
-
--- Complex
-
-Semigroup a => Semigroup (Complex a) where
-  (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
-
-Monoid a => Monoid (Complex a) where
-  neutral = (neutral :+ neutral)
-
-Group a => Group (Complex a) where
-  inverse (r :+ i) = (inverse r :+ inverse i)
-
-Ring a => AbelianGroup (Complex a) where {}
-
-Ring a => Ring (Complex a) where
-  (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)
-
-RingWithUnity a => RingWithUnity (Complex a) where
-  unity = (unity :+ neutral)
-
-RingWithUnity a => Module a (Complex a) where
-  (<#>) x = map (x <.>)
-
-RingWithUnity a => InnerProductSpace a (Complex a) where
-  (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z

libs/contrib/Control/Algebra/VectorSpace.idr

@@ -20,7 +20,7 @@ infixr 2 <||>
 ||| + Distributivity of `<#>` and `<+>`:
 |||     forall a v w,  a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
 |||     forall a b v,  (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
-interface (RingWithUnity a, AbelianGroup b) => Module a b where
+interface RingWithUnity a => Module a b where
   (<#>) : a -> b -> b
 
 ||| A vector space is a module over a ring that is also a field