bc1c500 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4733 from clayrat/bool-lattice

bc1c500Niklas Larsson7 years ago

libs/contrib/Control/Algebra/Lattice.idr+16

compare with master

unifiedsplit

@@ -25,6 +25,9 @@ implementation JoinSemilattice Nat where

25implementation Ord a => JoinSemilattice (MaxiphobicHeap a) where

26 join = merge

28+JoinSemilattice Bool where

29+ join a b = a || b

30+

28||| Sets equipped with a binary operation that is commutative, associative and

31||| Sets equipped with a binary operation that is commutative, associative and

29||| idempotent. Must satisfy the following laws:

32||| idempotent. Must satisfy the following laws:

30|||

33|||

@@ -42,6 +45,9 @@ interface MeetSemilattice a where

42implementation MeetSemilattice Nat where

45implementation MeetSemilattice Nat where

43 meet = minimum

46 meet = minimum

48+MeetSemilattice Bool where

49+ meet a b = a && b

50+

45||| Sets equipped with a binary operation that is commutative, associative and

51||| Sets equipped with a binary operation that is commutative, associative and

46||| idempotent and supplied with a unitary element. Must satisfy the following

52||| idempotent and supplied with a unitary element. Must satisfy the following

47||| laws:

53||| laws:

@@ -63,6 +69,9 @@ interface JoinSemilattice a => BoundedJoinSemilattice a where

63implementation BoundedJoinSemilattice Nat where

69implementation BoundedJoinSemilattice Nat where

64 bottom = Z

70 bottom = Z

72+BoundedJoinSemilattice Bool where

73+ bottom = False

74+

66||| Sets equipped with a binary operation that is commutative, associative and

75||| Sets equipped with a binary operation that is commutative, associative and

67||| idempotent and supplied with a unitary element. Must satisfy the following

76||| idempotent and supplied with a unitary element. Must satisfy the following

68||| laws:

77||| laws:

@@ -81,6 +90,9 @@ implementation BoundedJoinSemilattice Nat where

81interface MeetSemilattice a => BoundedMeetSemilattice a where

90interface MeetSemilattice a => BoundedMeetSemilattice a where

82 top : a

91 top : a

93+BoundedMeetSemilattice Bool where

94+ top = True

95+

84||| Sets equipped with two binary operations that are both commutative,

96||| Sets equipped with two binary operations that are both commutative,

85||| associative and idempotent, along with absorbtion laws for relating the two

97||| associative and idempotent, along with absorbtion laws for relating the two

86||| binary operations. Must satisfy the following:

98||| binary operations. Must satisfy the following:

@@ -101,6 +113,8 @@ interface (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }

101

113

102implementation Lattice Nat where { }

114implementation Lattice Nat where { }

103

115

116+Lattice Bool where { }

117+

104||| Sets equipped with two binary operations that are both commutative,

118||| Sets equipped with two binary operations that are both commutative,

105||| associative and idempotent and supplied with neutral elements, along with

119||| associative and idempotent and supplied with neutral elements, along with

106||| absorbtion laws for relating the two binary operations. Must satisfy the

120||| absorbtion laws for relating the two binary operations. Must satisfy the

@@ -122,3 +136,5 @@ implementation Lattice Nat where { }

122||| forall a, meet a top == top

136||| forall a, meet a top == top

123||| forall a, join a bottom == bottom

137||| forall a, join a bottom == bottom

124interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }

138interface (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

3%access public export

4%default total

6+notInvolutive : (x : Bool) -> not (not x) = x

7+notInvolutive True = Refl

8+notInvolutive False = Refl

10+-- AND

11+

6andSameNeutral : (x : Bool) -> x && x = x

12andSameNeutral : (x : Bool) -> x && x = x

7andSameNeutral False = Refl

13andSameNeutral False = Refl

8andSameNeutral True = Refl

14andSameNeutral True = Refl

@@ -15,6 +21,20 @@ andTrueNeutral : (x : Bool) -> x && True = x

15andTrueNeutral False = Refl

21andTrueNeutral False = Refl

16andTrueNeutral True = Refl

22andTrueNeutral True = Refl

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+

18orSameNeutral : (x : Bool) -> x || x = x

38orSameNeutral : (x : Bool) -> x || x = x

19orSameNeutral False = Refl

39orSameNeutral False = Refl

20orSameNeutral True = Refl

40orSameNeutral True = Refl

@@ -27,6 +47,36 @@ orTrueTrue : (x : Bool) -> x || True = True

27orTrueTrue False = Refl

47orTrueTrue False = Refl

28orTrueTrue True = Refl

48orTrueTrue True = Refl

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+

30−orSameAndRightNeutral : (x, right : Bool) -> x || (x && right) = x

64+orSameAndRightNeutral : (x, y : Bool) -> x || (x && y) = x

31orSameAndRightNeutral False _ = Refl

65orSameAndRightNeutral 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

6import Control.Algebra.VectorSpace

7import Data.Vect

8import Data.ZZ

9+import Data.Bool.Extra

10%default total

11%default total

11%access public export

12%access public export

@@ -317,7 +318,42 @@ interface JoinSemilattice a => VerifiedJoinSemilattice a where

317 joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

318 joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

318 joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

319 joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

319

320

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+

320interface MeetSemilattice a => VerifiedMeetSemilattice a where

331interface MeetSemilattice a => VerifiedMeetSemilattice a where

321 meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r

332 meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r

322 meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

333 meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

323 meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

334 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