Add some algebra implementations

libs/base/Data/Bool/Xor.idr

@@ -42,14 +42,14 @@ notXorCancel False b = rewrite xorFalseNeutral b in
                        notInvolutive b
 
 export
-xorAssociative : (a, b, c : Bool) -> xor (xor a b) c = xor a (xor b c)
+xorAssociative : (a, b, c : Bool) -> xor a (xor b c) = xor (xor a b) c
 xorAssociative False b c =
   rewrite xorFalseNeutral b in
-  sym $ xorFalseNeutral (xor b c)
+  xorFalseNeutral $ xor b c
 xorAssociative True  b c =
   rewrite xorTrueNot b in
   rewrite xorTrueNot (xor b c) in
-  sym $ notXor b c
+  notXor b c
 
 export
 xorCommutative : (a, b : Bool) -> xor a b = xor b a

libs/base/Data/Nat.idr

@@ -583,3 +583,13 @@ export
 sucMinR : (l : Nat) -> minimum l (S l) = l
 sucMinR Z = Refl
 sucMinR (S l) = cong S $ sucMinR l
+
+-- Algebra -----------------------------
+
+public export
+Semigroup Nat where
+  (<+>) = plus
+
+public export
+Monoid Nat where
+  neutral = Z

libs/contrib/Control/Algebra/Implementations.idr

@@ -0,0 +1,21 @@
+module Control.Algebra.Implementations
+
+import Control.Algebra
+
+-- This file is for algebra implementations with nowhere else to go.
+
+%default total
+
+-- Functions ---------------------------
+
+Semigroup (ty -> ty) where
+  (<+>) = (.)
+
+SemigroupV (ty -> ty) where
+  semigroupOpIsAssociative _ _ _ = Refl
+
+Monoid (ty -> ty) where
+  neutral = id
+
+MonoidV (ty -> ty) where
+  monoidNeutralIsNeutralR _ = Refl

libs/contrib/Control/Algebra/Laws.idr

@@ -1,6 +1,5 @@
 module Control.Algebra.Laws
 
-import Prelude
 import Control.Algebra
 
 %default total

libs/contrib/Control/Monad/Algebra.idr

@@ -0,0 +1,18 @@
+module Control.Monad.Algebra
+
+import Control.Algebra
+import Control.Monad.Identity
+
+%default total
+
+public export
+SemigroupV ty => SemigroupV (Identity ty) where
+  semigroupOpIsAssociative (Id l) (Id c) (Id r) =
+    rewrite semigroupOpIsAssociative l c r in Refl
+
+public export
+MonoidV ty => MonoidV (Identity ty) where
+  monoidNeutralIsNeutralL (Id l) =
+    rewrite monoidNeutralIsNeutralL l in Refl
+  monoidNeutralIsNeutralR (Id r) =
+    rewrite monoidNeutralIsNeutralR r in Refl

libs/contrib/Data/Bool/Algebra.idr

@@ -0,0 +1,74 @@
+module Data.Bool.Algebra
+
+import Control.Algebra
+import Data.Bool.Xor
+
+%default total
+
+-- && is Bool -> Lazy Bool -> Bool,
+-- but Bool -> Bool -> Bool is required
+and : Bool -> Bool -> Bool
+and True True = True
+and _ _ = False
+
+Semigroup Bool where
+  (<+>) = xor
+
+SemigroupV Bool where
+  semigroupOpIsAssociative = xorAssociative
+
+Monoid Bool where
+  neutral = False
+
+MonoidV Bool where
+  monoidNeutralIsNeutralL True = Refl
+  monoidNeutralIsNeutralL False = Refl
+
+Group Bool where
+  -- Each Bool is its own additive inverse.
+  inverse = id
+
+  groupInverseIsInverseR True = Refl
+  groupInverseIsInverseR False = Refl
+
+AbelianGroup Bool where
+  groupOpIsCommutative = xorCommutative
+
+Ring Bool where
+  (<.>) = and
+
+  ringOpIsAssociative True True True = Refl
+  ringOpIsAssociative True True False = Refl
+  ringOpIsAssociative True False True = Refl
+  ringOpIsAssociative True False False = Refl
+  ringOpIsAssociative False True True = Refl
+  ringOpIsAssociative False False True = Refl
+  ringOpIsAssociative False True False = Refl
+  ringOpIsAssociative False False False = Refl
+
+  ringOpIsDistributiveL True True True = Refl
+  ringOpIsDistributiveL True True False = Refl
+  ringOpIsDistributiveL True False True = Refl
+  ringOpIsDistributiveL True False False = Refl
+  ringOpIsDistributiveL False True True = Refl
+  ringOpIsDistributiveL False False True = Refl
+  ringOpIsDistributiveL False True False = Refl
+  ringOpIsDistributiveL False False False = Refl
+
+  ringOpIsDistributiveR True True True = Refl
+  ringOpIsDistributiveR True True False = Refl
+  ringOpIsDistributiveR True False True = Refl
+  ringOpIsDistributiveR True False False = Refl
+  ringOpIsDistributiveR False True True = Refl
+  ringOpIsDistributiveR False False True = Refl
+  ringOpIsDistributiveR False True False = Refl
+  ringOpIsDistributiveR False False False = Refl
+
+RingWithUnity Bool where
+  unity = True
+
+  unityIsRingIdL True = Refl
+  unityIsRingIdL False = Refl
+
+  unityIsRingIdR True = Refl
+  unityIsRingIdR False = Refl

libs/contrib/Data/List/Algebra.idr

@@ -0,0 +1,15 @@
+module Data.List.Algebra
+
+import Control.Algebra
+import Data.List
+
+%default total
+
+public export
+SemigroupV (List ty) where
+  semigroupOpIsAssociative = appendAssociative
+
+public export
+MonoidV (List ty) where
+  monoidNeutralIsNeutralL = appendNilRightNeutral
+  monoidNeutralIsNeutralR _ = Refl

libs/contrib/Data/Morphisms/Algebra.idr

@@ -0,0 +1,15 @@
+module Data.Morphisms.Algebra
+
+import Control.Algebra
+import Data.Morphisms
+
+%default total
+
+public export
+SemigroupV (Endomorphism ty) where
+  semigroupOpIsAssociative (Endo _) (Endo _) (Endo _) = Refl
+
+public export
+MonoidV (Endomorphism ty) where
+  monoidNeutralIsNeutralL (Endo _) = Refl
+  monoidNeutralIsNeutralR (Endo _) = Refl

libs/contrib/Data/Nat/Algebra.idr

@@ -0,0 +1,15 @@
+module Data.Nat.Algebra
+
+import Control.Algebra
+import Data.Nat
+
+%default total
+
+public export
+SemigroupV Nat where
+  semigroupOpIsAssociative = plusAssociative
+
+public export
+MonoidV Nat where
+  monoidNeutralIsNeutralL = plusZeroRightNeutral
+  monoidNeutralIsNeutralR = plusZeroLeftNeutral

libs/contrib/contrib.ipkg

@@ -5,13 +5,18 @@ modules = Control.ANSI,
           Control.ANSI.CSI,
           Control.Delayed,
           Control.Linear.LIO,
+          Control.Monad.Algebra,
           Control.Monad.Syntax,
 
           Control.Algebra,
           Control.Algebra.Laws,
+          Control.Algebra.Implementations,
+
+          Data.Bool.Algebra,
 
           Data.Linear.Array,
 
+          Data.List.Algebra,
           Data.List.TailRec,
           Data.List.Equalities,
           Data.List.Reverse,
@@ -22,6 +27,9 @@ modules = Control.ANSI,
 
           Data.Logic.Propositional,
 
+          Data.Morphisms.Algebra,
+
+          Data.Nat.Algebra,
           Data.Nat.Ack,
           Data.Nat.Equational,
           Data.Nat.Fact,