Make algebra interfaces verified by default (#4739)

libs/base/Control/Isomorphism.idr

@@ -38,12 +38,31 @@ Category Iso where
   id = isoRefl
   (.) = flip isoTrans
 
+-- TODO : Prove these postulates! ------
+
+postulate private
+iso_semigroupOpIsAssociative : (l, c, r : Iso a a) ->
+  isoTrans l (isoTrans c r) = isoTrans (isoTrans l c) r
+
+postulate private
+iso_monoidNeutralIsNeutralL : (l : Iso a a) -> isoTrans l isoRefl = l
+
+postulate private
+iso_monoidNeutralIsNeutralR : (r : Iso a a) -> isoTrans isoRefl r = r
+
+----------------------------------------
+
 Semigroup (Iso a a) where
   (<+>) = isoTrans
 
+  semigroupOpIsAssociative = iso_semigroupOpIsAssociative
+
 Monoid (Iso a a) where
   neutral = isoRefl
 
+  monoidNeutralIsNeutralL = iso_monoidNeutralIsNeutralL
+  monoidNeutralIsNeutralR = iso_monoidNeutralIsNeutralR
+
 ||| Isomorphism is symmetric
 isoSym : Iso a b -> Iso b a
 isoSym (MkIso to from toFrom fromTo) = MkIso from to fromTo toFrom

libs/base/Control/Monad/Identity.idr

@@ -33,5 +33,13 @@ Enum a => Enum (Identity a) where
 (Semigroup a) => Semigroup (Identity a) where
   (<+>) x y = Id (runIdentity x <+> runIdentity y)
 
+  semigroupOpIsAssociative (Id l) (Id c) (Id r) =
+    rewrite semigroupOpIsAssociative l c r in Refl
+
 (Monoid a) => Monoid (Identity a) where
-  neutral = Id (neutral)
+  neutral = Id (neutral)
+
+  monoidNeutralIsNeutralL (Id l) =
+    rewrite monoidNeutralIsNeutralL l in Refl
+  monoidNeutralIsNeutralR (Id r) =
+    rewrite monoidNeutralIsNeutralR r in Refl

libs/base/Data/Morphisms.idr

@@ -28,18 +28,60 @@ Applicative (Morphism r) where
 Monad (Morphism r) where
   (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r
 
+-- Postulates --------------------------
+
+-- These are required for implementing verified interfaces.
+-- TODO : Prove them.
+
+postulate private
+morphism_assoc : Semigroup a => (f, g, h : r -> a) ->
+  Mor (\r => f r <+> (g r <+> h r)) = Mor (\r => f r <+> g r <+> h r)
+
+postulate private
+morphism_neutl : Monoid a => (f : r -> a) ->
+  Mor (\r => f r <+> Prelude.Algebra.neutral) = Mor f
+
+postulate private
+morphism_neutr : Monoid a => (f : r -> a) ->
+  Mor (\r => Prelude.Algebra.neutral <+> f r) = Mor f
+
+postulate private
+kleisli_assoc : (Semigroup a, Applicative f) => (i, j, k : s -> f a) ->
+   Kleisli (\r => pure (<+>) <*> i r <*> (pure (<+>) <*> j r <*> k r)) =
+     Kleisli (\r => pure (<+>) <*> (pure (<+>) <*> i r <*> j r) <*> k r)
+
+postulate private
+kleisli_neutl : (Monoid a, Applicative f) => (g : r -> f a) ->
+  Kleisli (\x => pure (<+>) <*> g x <*> pure Prelude.Algebra.neutral) = Kleisli g
+
+postulate private
+kleisli_neutr : (Monoid a, Applicative f) => (g : r -> f a) ->
+  Kleisli (\x => pure (<+>) <*> pure Prelude.Algebra.neutral <*> g x) = Kleisli g
+
+----------------------------------------
+
 Semigroup a => Semigroup (Morphism r a) where
   f <+> g = [| f <+> g |]
 
+  semigroupOpIsAssociative (Mor f) (Mor g) (Mor h) = morphism_assoc f g h
+
 Monoid a => Monoid (Morphism r a) where
   neutral = [| neutral |]
 
+  monoidNeutralIsNeutralL (Mor f) = morphism_neutl f
+  monoidNeutralIsNeutralR (Mor f) = morphism_neutr f
+
 Semigroup (Endomorphism a) where
   (Endo f) <+> (Endo g) = Endo $ g . f
 
+  semigroupOpIsAssociative (Endo _) (Endo _) (Endo _) = Refl
+
 Monoid (Endomorphism a) where
   neutral = Endo id
 
+  monoidNeutralIsNeutralL (Endo _) = Refl
+  monoidNeutralIsNeutralR (Endo _) = Refl
+
 Functor f => Functor (Kleislimorphism f a) where
   map f (Kleisli g) = Kleisli (map f . g)
 
@@ -51,12 +93,17 @@ Monad f => Monad (Kleislimorphism f a) where
   (Kleisli f) >>= g = Kleisli $ \r => applyKleisli (g !(f r)) r
 
 -- Applicative is a bit too strong, but there is no suitable superclass
-(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a) where
+(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f s a) where
   f <+> g = [| f <+> g |]
 
+  semigroupOpIsAssociative (Kleisli i) (Kleisli j) (Kleisli k) = kleisli_assoc i j k
+
 (Monoid a, Applicative f) => Monoid (Kleislimorphism f r a) where
   neutral = [| neutral |]
 
+  monoidNeutralIsNeutralL (Kleisli g) = kleisli_neutl g
+  monoidNeutralIsNeutralR (Kleisli g) = kleisli_neutr g
+
 Cast (Endomorphism a) (Morphism a a) where
   cast (Endo f) = Mor f
 

libs/contrib/Control/Algebra.idr

@@ -19,6 +19,8 @@ infixl 7 <.>
 interface Monoid a => Group a where
   inverse : a -> a
 
+  groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
+
 (<->) : Group a => a -> a -> a
 (<->) left right = left <+> (inverse right)
 
@@ -36,7 +38,8 @@ interface Monoid a => Group a where
 ||| + Inverse for `<+>`:
 |||     forall a,     a <+> inverse a == neutral
 |||     forall a,     inverse a <+> a == neutral
-interface Group a => AbelianGroup a where { }
+interface Group a => AbelianGroup a where
+  abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
 
 ||| Sets equipped with two binary operations, one associative and commutative
 ||| supplied with a neutral element, and the other associative, with
@@ -61,6 +64,10 @@ interface Group a => AbelianGroup a where { }
 interface AbelianGroup a => Ring a where
   (<.>) : a -> a -> a
 
+  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)
+
 ||| 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.  Must
@@ -87,6 +94,34 @@ interface AbelianGroup a => Ring a where
 interface Ring a => RingWithUnity a where
   unity : a
 
+  ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
+  ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
+
+||| Sets equipped with two binary operations, one associative and
+||| commutative supplied with a neutral element, and the other
+||| associative and commutative, with distributivity laws relating the
+||| two operations. 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
+||| + Associativity of `<.>`:
+|||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+||| + Commutativity of `<.>`:
+|||     forall a b,   a <.> b         == b <.> 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)
+interface Ring a => CommutativeRing a where
+  ringOpIsCommutative : (x, y : a) -> x <.> y = y <.> x
+
 ||| 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 must have a
@@ -104,6 +139,8 @@ interface Ring a => RingWithUnity a where
 |||     forall a,     inverse a <+> a == neutral
 ||| + Associativity of `<.>`:
 |||     forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
+||| + Commutativity of `<.>`:
+|||     forall a b,   a <.> b         == b <.> a
 ||| + Unity for `<.>`:
 |||     forall a,     a <.> unity     == a
 |||     forall a,     unity <.> a     == a
@@ -113,9 +150,12 @@ interface Ring a => RingWithUnity 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 RingWithUnity a => Field a where
+interface (RingWithUnity a, CommutativeRing a) => Field a where
   inverseM : (x : a) -> Not (x = Algebra.neutral) -> a
 
+  fieldInverseIsInverseR : (r : a) -> (p : Not (r = Algebra.neutral)) ->
+    inverseM r p <.> r = Algebra.unity
+
 sum' : (Foldable t, Monoid a) => t a -> a
 sum' = concat
 

libs/contrib/Control/Algebra/Lattice.idr

@@ -1,7 +1,7 @@
 module Control.Algebra.Lattice
 
 import Control.Algebra
-import Data.Heap
+import Data.Bool.Extra
 
 %access public export
 
@@ -19,14 +19,9 @@ import Data.Heap
 interface JoinSemilattice a where
   join : a -> a -> a
 
-implementation JoinSemilattice Nat where
-  join = maximum
-
-implementation Ord a => JoinSemilattice (MaxiphobicHeap a) where
-  join = merge
-
-JoinSemilattice Bool where
-  join a b = a || b
+  joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
+  joinSemilatticeJoinIsCommutative : (l, r : a)    -> join l r = join r l
+  joinSemilatticeJoinIsIdempotent  : (e : a)       -> join e e = e
 
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent.  Must satisfy the following laws:
@@ -42,11 +37,9 @@ JoinSemilattice Bool where
 interface MeetSemilattice a where
   meet : a -> a -> a
 
-implementation MeetSemilattice Nat where
-  meet = minimum
-
-MeetSemilattice Bool where
-  meet a b = a && b
+  meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
+  meetSemilatticeMeetIsCommutative : (l, r : a)    -> meet l r = meet r l
+  meetSemilatticeMeetIsIdempotent  : (e : a)       -> meet e e = e
 
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent and supplied with a unitary element.  Must satisfy the following
@@ -66,11 +59,7 @@ MeetSemilattice Bool where
 interface JoinSemilattice a => BoundedJoinSemilattice a where
   bottom  : a
 
-implementation BoundedJoinSemilattice Nat where
-  bottom = Z
-
-BoundedJoinSemilattice Bool where
-  bottom = False
+  joinBottomIsIdentity : (x : a) -> join x Lattice.bottom = x
 
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent and supplied with a unitary element.  Must satisfy the following
@@ -90,8 +79,7 @@ BoundedJoinSemilattice Bool where
 interface MeetSemilattice a => BoundedMeetSemilattice a where
   top : a
 
-BoundedMeetSemilattice Bool where
-  top = True
+  meetTopIsIdentity : (x : a) -> meet x Lattice.top = x
 
 ||| Sets equipped with two binary operations that are both commutative,
 ||| associative and idempotent, along with absorbtion laws for relating the two
@@ -111,10 +99,6 @@ BoundedMeetSemilattice Bool where
 |||     forall a b,   join a (meet a b) == a
 interface (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
 
-implementation Lattice Nat where { }
-
-Lattice Bool where { }
-
 ||| Sets equipped with two binary operations that are both commutative,
 ||| associative and idempotent and supplied with neutral elements, along with
 ||| absorbtion laws for relating the two binary operations.  Must satisfy the
@@ -137,4 +121,50 @@ Lattice Bool where { }
 |||     forall a,     join a bottom     == bottom
 interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
 
+-- Implementations ---------------------
+
+-- Nat
+
+JoinSemilattice Nat where
+  join = maximum
+  joinSemilatticeJoinIsAssociative = maximumAssociative
+  joinSemilatticeJoinIsCommutative = maximumCommutative
+  joinSemilatticeJoinIsIdempotent  = maximumIdempotent
+
+MeetSemilattice Nat where
+  meet = minimum
+  meetSemilatticeMeetIsAssociative = minimumAssociative
+  meetSemilatticeMeetIsCommutative = minimumCommutative
+  meetSemilatticeMeetIsIdempotent  = minimumIdempotent
+
+BoundedJoinSemilattice Nat where
+  bottom = Z
+  joinBottomIsIdentity = maximumZeroNLeft
+
+Lattice Nat where { }
+
+-- Bool
+
+JoinSemilattice Bool where
+  join a b = a || b
+  joinSemilatticeJoinIsAssociative = orAssociative
+  joinSemilatticeJoinIsCommutative = orCommutative
+  joinSemilatticeJoinIsIdempotent = orSameNeutral
+
+MeetSemilattice Bool where
+  meet a b = a && b
+  meetSemilatticeMeetIsAssociative = andAssociative
+  meetSemilatticeMeetIsCommutative = andCommutative
+  meetSemilatticeMeetIsIdempotent = andSameNeutral
+
+BoundedJoinSemilattice Bool where
+  bottom = False
+  joinBottomIsIdentity = orFalseNeutral
+
+BoundedMeetSemilattice Bool where
+  top = True
+  meetTopIsIdentity = andTrueNeutral
+
 BoundedLattice Bool where { }
+
+Lattice Bool where { }