git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4733 from clayrat/bool-lattice

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

commitbc1c500c91e35f31926eb5d6383771a69b9669b5 authorNiklas Larsson <metaniklas@gmail.com> dateSun 7 Jul 2019, 23:28 (7 years ago) parentfd5dfd9977f1c0
3 files changed+104−2
compare with master
unifiedsplit
libs/contrib/Control/Algebra/Lattice.idr+16 libs/contrib/Data/Bool/Extra.idr+52−2 libs/contrib/Interfaces/Verified.idr+36
libs/contrib/Control/Algebra/Lattice.idr+16
@@ -25,6 +25,9 @@ implementation JoinSemilattice Nat where
2525implementation Ord a => JoinSemilattice (MaxiphobicHeap a) where
2626 join = merge
2727
28+JoinSemilattice Bool where
29+ join a b = a || b
30+
2831||| Sets equipped with a binary operation that is commutative, associative and
2932||| idempotent. Must satisfy the following laws:
3033|||
@@ -42,6 +45,9 @@ interface MeetSemilattice a where
4245implementation MeetSemilattice Nat where
4346 meet = minimum
4447
48+MeetSemilattice Bool where
49+ meet a b = a && b
50+
4551||| Sets equipped with a binary operation that is commutative, associative and
4652||| idempotent and supplied with a unitary element. Must satisfy the following
4753||| laws:
@@ -63,6 +69,9 @@ interface JoinSemilattice a => BoundedJoinSemilattice a where
6369implementation BoundedJoinSemilattice Nat where
6470 bottom = Z
6571
72+BoundedJoinSemilattice Bool where
73+ bottom = False
74+
6675||| Sets equipped with a binary operation that is commutative, associative and
6776||| idempotent and supplied with a unitary element. Must satisfy the following
6877||| laws:
@@ -81,6 +90,9 @@ implementation BoundedJoinSemilattice Nat where
8190interface MeetSemilattice a => BoundedMeetSemilattice a where
8291 top : a
8392
93+BoundedMeetSemilattice Bool where
94+ top = True
95+
8496||| Sets equipped with two binary operations that are both commutative,
8597||| associative and idempotent, along with absorbtion laws for relating the two
8698||| binary operations. Must satisfy the following:
@@ -101,6 +113,8 @@ interface (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
101113
102114implementation Lattice Nat where { }
103115
116+Lattice Bool where { }
117+
104118||| Sets equipped with two binary operations that are both commutative,
105119||| associative and idempotent and supplied with neutral elements, along with
106120||| absorbtion laws for relating the two binary operations. Must satisfy the
@@ -122,3 +136,5 @@ implementation Lattice Nat where { }
122136||| forall a, meet a top == top
123137||| forall a, join a bottom == bottom
124138interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
139+
140+BoundedLattice Bool where { }
libs/contrib/Data/Bool/Extra.idr+52−2
@@ -3,6 +3,12 @@ module Data.Bool.Extra
33%access public export
44%default total
55
6+notInvolutive : (x : Bool) -> not (not x) = x
7+notInvolutive True = Refl
8+notInvolutive False = Refl
9+
10+-- AND
11+
612andSameNeutral : (x : Bool) -> x && x = x
713andSameNeutral False = Refl
814andSameNeutral True = Refl
@@ -15,6 +21,20 @@ andTrueNeutral : (x : Bool) -> x && True = x
1521andTrueNeutral False = Refl
1622andTrueNeutral True = Refl
1723
24+andAssociative : (x, y, z : Bool) -> x && (y && z) = (x && y) && z
25+andAssociative True _ _ = Refl
26+andAssociative False _ _ = Refl
27+
28+andCommutative : (x, y : Bool) -> x && y = y && x
29+andCommutative x True = andTrueNeutral x
30+andCommutative x False = andFalseFalse x
31+
32+andNotFalse : (x : Bool) -> x && not x = False
33+andNotFalse False = Refl
34+andNotFalse True = Refl
35+
36+-- OR
37+
1838orSameNeutral : (x : Bool) -> x || x = x
1939orSameNeutral False = Refl
2040orSameNeutral True = Refl
@@ -27,6 +47,36 @@ orTrueTrue : (x : Bool) -> x || True = True
2747orTrueTrue False = Refl
2848orTrueTrue True = Refl
2949
30−orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x
50+orAssociative : (x, y, z : Bool) -> x || (y || z) = (x || y) || z
51+orAssociative True _ _ = Refl
52+orAssociative False _ _ = Refl
53+
54+orCommutative : (x, y : Bool) -> x || y = y || x
55+orCommutative x True = orTrueTrue x
56+orCommutative x False = orFalseNeutral x
57+
58+orNotTrue : (x : Bool) -> x || not x = True
59+orNotTrue False = Refl
60+orNotTrue True = Refl
61+
62+-- interaction & De Morgan's laws
63+
64+orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x
3165orSameAndRightNeutral False _ = Refl
32−orSameAndRightNeutral True _ = Refl
66+orSameAndRightNeutral True _ = Refl
67+
68+andDistribOrR : (x, y, z : Bool) -> x && (y || z) = (x && y) || (x && z)
69+andDistribOrR False _ _ = Refl
70+andDistribOrR True _ _ = Refl
71+
72+orDistribAndR : (x, y, z : Bool) -> x || (y && z) = (x || y) && (x || z)
73+orDistribAndR False _ _ = Refl
74+orDistribAndR True _ _ = Refl
75+
76+notAndIsOr : (x, y : Bool) -> not (x && y) = not x || not y
77+notAndIsOr False _ = Refl
78+notAndIsOr True _ = Refl
79+
80+notOrIsAnd : (x, y : Bool) -> not (x || y) = not x && not y
81+notOrIsAnd False _ = Refl
82+notOrIsAnd True _ = Refl
libs/contrib/Interfaces/Verified.idr+36
@@ -6,6 +6,7 @@ import Control.Algebra.NumericImplementations
66import Control.Algebra.VectorSpace
77import Data.Vect
88import Data.ZZ
9+import Data.Bool.Extra
910
1011%default total
1112%access public export
@@ -317,7 +318,42 @@ interface JoinSemilattice a => VerifiedJoinSemilattice a where
317318 joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
318319 joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
319320
321+VerifiedJoinSemilattice Nat where
322+ joinSemilatticeJoinIsAssociative = maximumAssociative
323+ joinSemilatticeJoinIsCommutative = maximumCommutative
324+ joinSemilatticeJoinIsIdempotent = maximumIdempotent
325+
326+VerifiedJoinSemilattice Bool where
327+ joinSemilatticeJoinIsAssociative = orAssociative
328+ joinSemilatticeJoinIsCommutative = orCommutative
329+ joinSemilatticeJoinIsIdempotent = orSameNeutral
330+
320331interface MeetSemilattice a => VerifiedMeetSemilattice a where
321332 meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
322333 meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
323334 meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
335+
336+VerifiedMeetSemilattice Nat where
337+ meetSemilatticeMeetIsAssociative = minimumAssociative
338+ meetSemilatticeMeetIsCommutative = minimumCommutative
339+ meetSemilatticeMeetIsIdempotent = minimumIdempotent
340+
341+VerifiedMeetSemilattice Bool where
342+ meetSemilatticeMeetIsAssociative = andAssociative
343+ meetSemilatticeMeetIsCommutative = andCommutative
344+ meetSemilatticeMeetIsIdempotent = andSameNeutral
345+
346+interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
347+ joinBottomIsIdentity : (x : a) -> join x Lattice.bottom = x
348+
349+VerifiedBoundedJoinSemilattice Nat where
350+ joinBottomIsIdentity = maximumZeroNLeft
351+
352+VerifiedBoundedJoinSemilattice Bool where
353+ joinBottomIsIdentity = orFalseNeutral
354+
355+interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
356+ meetTopIsIdentity : (x : a) -> meet x Lattice.top = x
357+
358+VerifiedBoundedMeetSemilattice Bool where
359+ meetTopIsIdentity = andTrueNeutral