Make algebra interfaces verified by default (#4739)

Previously there were interfaces for Semigroup, Monoid, etc, that were
just syntactic in nature, requiring only that operations like <+> or
elements like neutral exist. There was a corresponding set of
"verified" interfaces requiring that the expected laws actually hold.
Thus Semigroup required that the <+> operation exist, while
VerifiedSemigroup required that that operation actually be
associative.

Such an arrangement is annoying for two reasons.

First, extra paperwork. If I want to show that something really is a
semigroup, I have to write two implementation blocks, the "plain"
version and the "verified" version. On the other side, if I want to
add a new interface, then in order to keep with the existing style I
need to write both a "plain" version and a "verified" version. In some
cases, like AbelianGroup, the "plain" interface is empty, since it
doesn't add any new syntactic elements.

Second, proof. Suppose a type has been declared to be a Semigroup, but
VerifiedSemigroup hasn't been implemented for it. What can be assumed
about that type? Is its <+> operation associative or not? If it isn't,
why call it a semigroup? If it is, why not prove it? And if it can't
be proved, how do we know that it's true? The big selling point of
Idris is its expressive type system and strong compile-time
guarantees, so let's take advantage of that and verify by default.

Fixing the interfaces is easy -- just move the "verified" requirements
into the "plain" interface, and that's it.

In some cases there were implementations of the "verified" interfaces,
and those could also easily be copied over. More challenging are the
cases for which there were no verified implementations. There are
three ways of dealing with them:

  (1) Come up with the required proofs. This was done, for example,
      with `Semigroup a => Semigroup (Vect n a)` etc in
      contrib/Data/Matrix/Algebraic.idr, and also with easy ones like
      Maybe and Endomorphism.

  (2) Replace the interface with an "unverified" version, thereby
      highlighting the fact that the expected properties have not been
      proven. This was done with a few complicated data structures in
      contrib, like MaxiphobicHeap and SortedBag, as well as with
      primitive numeric types like Integer.

  (3) Assert without proof that the laws hold using believe_me and
      really_believe_me. This was done for cases in prelude and base
      for which proofs are impossible (eg String) or not obvious (eg
      Morphism and Kleislimorphism). Needless to say, these proofs
      should be implemented where possible. If these assertions are
      disliked, I would be happy to convert them to "unverified".

Note that this change only applies to those interfaces that belong to
"abstract algebra": semigroups, monoids, groups, and so on. There is a
whole other set of "plain"/"verified" interfaces dealing with
structures from "category theory". Those should also undergo this
unification, but I don't know how to do it just yet.

Author: nickdrozd

libs/base/Control/Isomorphism.idr

@@ -41,9 +41,17 @@ Category Iso where
 Semigroup (Iso a a) where
   (<+>) = isoTrans
 
+  semigroupOpIsAssociative (MkIso ato afrom atoFrom afromTo)
+                           (MkIso bto bfrom btoFrom bfromTo)
+                           (MkIso cto cfrom ctoFrom cfromTo) =
+    believe_me Iso
+
 Monoid (Iso a a) where
   neutral = isoRefl
 
+  monoidNeutralIsNeutralL (MkIso to from toFrom fromTo) = believe_me Iso
+  monoidNeutralIsNeutralR (MkIso to from toFrom fromTo) = believe_me Iso
+
 ||| 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

@@ -31,15 +31,28 @@ Monad (Morphism r) where
 Semigroup a => Semigroup (Morphism r a) where
   f <+> g = [| f <+> g |]
 
+  semigroupOpIsAssociative (Mor f) (Mor g) (Mor h) =
+    cong {f = Mor} $ believe_me Morphism
+
 Monoid a => Monoid (Morphism r a) where
   neutral = [| neutral |]
 
+  monoidNeutralIsNeutralL {r} {a} (Mor f) =
+    cong {f = Mor} $ believe_me Morphism
+  monoidNeutralIsNeutralR (Mor f) =
+    cong {f = Mor} $ believe_me Morphism
+
 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 +64,20 @@ 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) =
+    cong {f = Kleisli} $ believe_me Kleislimorphism
+
 (Monoid a, Applicative f) => Monoid (Kleislimorphism f r a) where
   neutral = [| neutral |]
 
+  monoidNeutralIsNeutralL (Kleisli g) =
+    cong {f = Kleisli} $ believe_me Kleislimorphism
+  monoidNeutralIsNeutralR (Kleisli g) =
+    cong {f = Kleisli} $ believe_me Kleislimorphism
+
 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
 
@@ -145,3 +185,33 @@ mtimes (S k) x = stimes (S k) x
 --   Structures where "abs" make sense.
 --   Euclidean domains, etc.
 --   Where to put fromInteger and fromRational?
+
+-- Unverified implementations ----------
+
+infixl 7 <?+>
+infixl 8 <?.>
+
+interface UnverifiedSemigroup a where
+  (<?+>) : a -> a -> a
+
+interface UnverifiedSemigroup a => UnverifiedMonoid a where
+  neut : a
+
+interface UnverifiedMonoid a => UnverifiedGroup a where
+  inv : a -> a
+
+interface UnverifiedGroup a => UnverifiedAbelianGroup a where { }
+
+interface UnverifiedAbelianGroup a => UnverifiedRing a where
+  (<?.>) : a -> a -> a
+
+interface UnverifiedRing a => UnverifiedRingWithUnity a where
+  un : a
+
+interface UnverifiedRingWithUnity a => UnverifiedField a where
+  inverse_M : (x : a) -> Not (x = Algebra.neut) -> a
+
+-- Lattices
+
+interface UnverifiedJoinSemilattice a where
+  join : a -> a -> a

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
@@ -109,11 +97,7 @@ BoundedMeetSemilattice Bool where
 ||| + Absorbtion laws for meet and join:
 |||     forall a b,   meet a (join a b) == a
 |||     forall a b,   join a (meet a b) == a
-interface (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
-
-implementation Lattice Nat where { }
-
-Lattice Bool where { }
+interface (JoinSemilattice a, MeetSemilattice a) => UnverifiedLattice a where { }
 
 ||| Sets equipped with two binary operations that are both commutative,
 ||| associative and idempotent and supplied with neutral elements, along with
@@ -135,6 +119,52 @@ Lattice Bool where { }
 ||| + Neutral for meet and join:
 |||     forall a,     meet a top        == top
 |||     forall a,     join a bottom     == bottom
-interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
+interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => UnverifiedBoundedLattice 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
+
+UnverifiedLattice 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
+
+UnverifiedBoundedLattice Bool where { }
 
-BoundedLattice Bool where { }
+UnverifiedLattice Bool where { }