Merge pull request #4733 from clayrat/bool-lattice

expand Bool laws, add (verified) lattice instances for Bool & Nat

libs/contrib/Control/Algebra/Lattice.idr

@@ -25,6 +25,9 @@ implementation JoinSemilattice Nat where
 implementation Ord a => JoinSemilattice (MaxiphobicHeap a) where
   join = merge
 
+JoinSemilattice Bool where
+  join a b = a || b
+
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent.  Must satisfy the following laws:
 |||
@@ -42,6 +45,9 @@ interface MeetSemilattice a where
 implementation MeetSemilattice Nat where
   meet = minimum
 
+MeetSemilattice Bool where
+  meet a b = a && b
+
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent and supplied with a unitary element.  Must satisfy the following
 ||| laws:
@@ -63,6 +69,9 @@ interface JoinSemilattice a => BoundedJoinSemilattice a where
 implementation BoundedJoinSemilattice Nat where
   bottom = Z
 
+BoundedJoinSemilattice Bool where
+  bottom = False
+
 ||| Sets equipped with a binary operation that is commutative, associative and
 ||| idempotent and supplied with a unitary element.  Must satisfy the following
 ||| laws:
@@ -81,6 +90,9 @@ implementation BoundedJoinSemilattice Nat where
 interface MeetSemilattice a => BoundedMeetSemilattice a where
   top : a
 
+BoundedMeetSemilattice Bool where
+  top = True
+
 ||| Sets equipped with two binary operations that are both commutative,
 ||| associative and idempotent, along with absorbtion laws for relating the two
 ||| binary operations.  Must satisfy the following:
@@ -101,6 +113,8 @@ 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
@@ -122,3 +136,5 @@ implementation Lattice Nat where { }
 |||     forall a,     meet a top        == top
 |||     forall a,     join a bottom     == bottom
 interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
+
+BoundedLattice Bool where { }

libs/contrib/Data/Bool/Extra.idr

@@ -3,6 +3,12 @@ module Data.Bool.Extra
 %access public export
 %default total
 
+notInvolutive : (x : Bool) -> not (not x) = x
+notInvolutive True  = Refl
+notInvolutive False = Refl
+
+-- AND
+
 andSameNeutral : (x : Bool) -> x && x = x
 andSameNeutral False = Refl
 andSameNeutral True = Refl
@@ -15,6 +21,20 @@ andTrueNeutral : (x : Bool) -> x && True = x
 andTrueNeutral False = Refl
 andTrueNeutral True = Refl
 
+andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z
+andAssociative True  _ _ = Refl
+andAssociative False _ _ = Refl
+
+andCommutative : (x, y : Bool) -> x && y = y && x
+andCommutative x True  = andTrueNeutral x
+andCommutative x False = andFalseFalse x
+
+andNotFalse : (x : Bool) -> x && not x = False
+andNotFalse False = Refl
+andNotFalse True = Refl
+
+-- OR
+
 orSameNeutral : (x : Bool) -> x || x = x
 orSameNeutral False = Refl
 orSameNeutral True = Refl
@@ -27,6 +47,36 @@ orTrueTrue : (x : Bool) -> x || True = True
 orTrueTrue False = Refl
 orTrueTrue True = Refl
 
-orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x
+orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z
+orAssociative True  _ _ = Refl
+orAssociative False _ _ = Refl
+
+orCommutative : (x, y : Bool) -> x || y = y || x
+orCommutative x True  = orTrueTrue x
+orCommutative x False = orFalseNeutral x
+
+orNotTrue : (x : Bool) -> x || not x = True
+orNotTrue False = Refl
+orNotTrue True = Refl
+
+-- interaction & De Morgan's laws
+
+orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x
 orSameAndRightNeutral False _ = Refl
-orSameAndRightNeutral True _ = Refl
+orSameAndRightNeutral True  _ = Refl
+
+andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)
+andDistribOrR False _ _ = Refl
+andDistribOrR True  _ _ = Refl
+
+orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)
+orDistribAndR False _ _ = Refl
+orDistribAndR True  _ _ = Refl
+
+notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y
+notAndIsOr False _ = Refl
+notAndIsOr True  _ = Refl
+
+notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
+notOrIsAnd False _ = Refl
+notOrIsAnd True  _ = Refl

libs/contrib/Interfaces/Verified.idr

@@ -6,6 +6,7 @@ import Control.Algebra.NumericImplementations
 import Control.Algebra.VectorSpace
 import Data.Vect
 import Data.ZZ
+import Data.Bool.Extra
 
 %default total
 %access public export
@@ -317,7 +318,42 @@ interface JoinSemilattice a => VerifiedJoinSemilattice a where
   joinSemilatticeJoinIsCommutative : (l, r : a)    -> join l r = join r l
   joinSemilatticeJoinIsIdempotent  : (e : a)       -> join e e = e
 
+VerifiedJoinSemilattice Nat where
+  joinSemilatticeJoinIsAssociative = maximumAssociative
+  joinSemilatticeJoinIsCommutative = maximumCommutative
+  joinSemilatticeJoinIsIdempotent  = maximumIdempotent
+
+VerifiedJoinSemilattice Bool where
+  joinSemilatticeJoinIsAssociative = orAssociative
+  joinSemilatticeJoinIsCommutative = orCommutative
+  joinSemilatticeJoinIsIdempotent = orSameNeutral
+
 interface MeetSemilattice a => VerifiedMeetSemilattice a where
   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
+
+VerifiedMeetSemilattice Nat where
+  meetSemilatticeMeetIsAssociative = minimumAssociative
+  meetSemilatticeMeetIsCommutative = minimumCommutative
+  meetSemilatticeMeetIsIdempotent  = minimumIdempotent
+
+VerifiedMeetSemilattice Bool where
+  meetSemilatticeMeetIsAssociative = andAssociative
+  meetSemilatticeMeetIsCommutative = andCommutative
+  meetSemilatticeMeetIsIdempotent = andSameNeutral
+
+interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
+  joinBottomIsIdentity : (x : a) -> join x Lattice.bottom = x
+
+VerifiedBoundedJoinSemilattice Nat where
+  joinBottomIsIdentity = maximumZeroNLeft
+
+VerifiedBoundedJoinSemilattice Bool where
+  joinBottomIsIdentity = orFalseNeutral
+  
+interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
+  meetTopIsIdentity : (x : a) -> meet x Lattice.top = x
+
+VerifiedBoundedMeetSemilattice Bool where
+  meetTopIsIdentity = andTrueNeutral