@@ -13,24 +13,26 @@ infixl 6 <*>
1313-- A modest class hierarchy
1414--------------------------------------------------------------------------------
1515
16−-- Sets equipped with a single binary operation that is associative. Must
17−-- satisfy the following laws:
18−-- Associativity of <+>:
19−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
16+||| Sets equipped with a single binary operation that is associative. Must
17+||| satisfy the following laws:
18+|||
19+||| + Associativity of `<+>`:
20+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
2021class Semigroup a where
2122 (<+>) : a -> a -> a
2223
2324class Semigroup a => VerifiedSemigroup a where
2425 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
2526
26−-- Sets equipped with a single binary operation that is associative, along with
27−-- a neutral element for that binary operation. Must satisfy the following
28−-- laws:
29−-- Associativity of <+>:
30−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
31−-- Neutral for <+>:
32−-- forall a, a <+> neutral == a
33−-- forall a, neutral <+> a == a
27+||| Sets equipped with a single binary operation that is associative, along with
28+||| a neutral element for that binary operation. Must satisfy the following
29+||| laws:
30+|||
31+||| + Associativity of `<+>`:
32+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
33+||| + Neutral for `<+>`:
34+||| forall a, a <+> neutral == a
35+||| forall a, neutral <+> a == a
3436class Semigroup a => Monoid a where
3537 neutral : a
3638
@@ -38,17 +40,17 @@ class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
3840 total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
3941 total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
4042
41−-- Sets equipped with a single binary operation that is associative, along with
42−-- a neutral element for that binary operation and inverses for all elements.
43−-- Must satisfy the following laws:
44−-- Associativity of <+>:
45−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
46−-- Neutral for <+>:
47−-- forall a, a <+> neutral == a
48−-- forall a, neutral <+> a == a
49−-- Inverse for <+>:
50−-- forall a, a <+> inverse a == neutral
51−-- forall a, inverse a <+> a == neutral
43+||| Sets equipped with a single binary operation that is associative, along with
44+||| a neutral element for that binary operation and inverses for all elements.
45+||| Must satisfy the following laws:
46+||| + Associativity of `<+>`:
47+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
48+||| + Neutral for `<+>`:
49+||| forall a, a <+> neutral == a
50+||| forall a, neutral <+> a == a
51+||| + Inverse for `<+>`:
52+||| forall a, a <+> inverse a == neutral
53+||| forall a, inverse a <+> a == neutral
5254class Monoid a => Group a where
5355 inverse : a -> a
5456
@@ -59,73 +61,76 @@ class (VerifiedMonoid a, Group a) => VerifiedGroup a where
5961(<->) : Group a => a -> a -> a
6062(<->) left right = left <+> (inverse right)
6163
62−-- Sets equipped with a single binary operation that is associative and
63−-- commutative, along with a neutral element for that binary operation and
64−-- inverses for all elements. Must satisfy the following laws:
65−-- Associativity of <+>:
66−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
67−-- Commutativity of <+>:
68−-- forall a b, a <+> b == b <+> a
69−-- Neutral for <+>:
70−-- forall a, a <+> neutral == a
71−-- forall a, neutral <+> a == a
72−-- Inverse for <+>:
73−-- forall a, a <+> inverse a == neutral
74−-- forall a, inverse a <+> a == neutral
64+||| Sets equipped with a single binary operation that is associative and
65+||| commutative, along with a neutral element for that binary operation and
66+||| inverses for all elements. Must satisfy the following laws:
67+|||
68+||| + Associativity of `<+>`:
69+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
70+||| + Commutativity of `<+>`:
71+||| forall a b, a <+> b == b <+> a
72+||| + Neutral for `<+>`:
73+||| forall a, a <+> neutral == a
74+||| forall a, neutral <+> a == a
75+||| + Inverse for `<+>`:
76+||| forall a, a <+> inverse a == neutral
77+||| forall a, inverse a <+> a == neutral
7578class Group a => AbelianGroup a where { }
7679
7780class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
7881 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
7982
80−-- Sets equipped with two binary operations, one associative and commutative
81−-- supplied with a neutral element, and the other associative, with
82−-- distributivity laws relating the two operations. Must satisfy the following
83−-- laws:
84−-- Associativity of <+>:
85−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
86−-- Commutativity of <+>:
87−-- forall a b, a <+> b == b <+> a
88−-- Neutral for <+>:
89−-- forall a, a <+> neutral == a
90−-- forall a, neutral <+> a == a
91−-- Inverse for <+>:
92−-- forall a, a <+> inverse a == neutral
93−-- forall a, inverse a <+> a == neutral
94−-- Associativity of <*>:
95−-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
96−-- Distributivity of <*> and <->:
97−-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
98−-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
83+||| Sets equipped with two binary operations, one associative and commutative
84+||| supplied with a neutral element, and the other associative, with
85+||| distributivity laws relating the two operations. Must satisfy the following
86+||| laws:
87+|||
88+||| + Associativity of `<+>`:
89+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
90+||| + Commutativity of `<+>`:
91+||| forall a b, a <+> b == b <+> a
92+||| + Neutral for `<+>`:
93+||| forall a, a <+> neutral == a
94+||| forall a, neutral <+> a == a
95+||| + Inverse for `<+>`:
96+||| forall a, a <+> inverse a == neutral
97+||| forall a, inverse a <+> a == neutral
98+||| + Associativity of `<*>`:
99+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
100+||| + Distributivity of `<*>` and `<->`:
101+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
102+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
99103class AbelianGroup a => Ring a where
100104 (<*>) : a -> a -> a
101105
102106class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
103107 total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
104108 total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
105− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
109+ total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (c <*> r)
106110
107−-- Sets equipped with two binary operations, one associative and commutative
108−-- supplied with a neutral element, and the other associative supplied with a
109−-- neutral element, with distributivity laws relating the two operations. Must
110−-- satisfy the following laws:
111−-- Associativity of <+>:
112−-- forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
113−-- Commutativity of <+>:
114−-- forall a b, a <+> b == b <+> a
115−-- Neutral for <+>:
116−-- forall a, a <+> neutral == a
117−-- forall a, neutral <+> a == a
118−-- Inverse for <+>:
119−-- forall a, a <+> inverse a == neutral
120−-- forall a, inverse a <+> a == neutral
121−-- Associativity of <*>:
122−-- forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
123−-- Neutral for <*>:
124−-- forall a, a <*> unity == a
125−-- forall a, unity <*> a == a
126−-- Distributivity of <*> and <->:
127−-- forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
128−-- forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
111+||| Sets equipped with two binary operations, one associative and commutative
112+||| supplied with a neutral element, and the other associative supplied with a
113+||| neutral element, with distributivity laws relating the two operations. Must
114+||| satisfy the following laws:
115+|||
116+||| + Associativity of `<+>`:
117+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
118+||| + Commutativity of `<+>`:
119+||| forall a b, a <+> b == b <+> a
120+||| + Neutral for `<+>`:
121+||| forall a, a <+> neutral == a
122+||| forall a, neutral <+> a == a
123+||| + Inverse for `<+>`:
124+||| forall a, a <+> inverse a == neutral
125+||| forall a, inverse a <+> a == neutral
126+||| + Associativity of `<*>a:
127+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
128+||| + Neutral for `<*>`:
129+||| forall a, a <*> unity == a
130+||| forall a, unity <*> a == a
131+||| + Distributivity of `<*>` and `<->`:
132+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
133+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
129134class Ring a => RingWithUnity a where
130135 unity : a
131136
@@ -133,15 +138,17 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
133138 total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
134139 total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
135140
136−-- Sets equipped with a binary operation that is commutative, associative and
137−-- idempotent. Must satisfy the following laws:
138−-- Associativity of join:
139−-- forall a b c, join a (join b c) == join (join a b) c
140−-- Commutativity of join:
141−-- forall a b, join a b == join b a
142−-- Idempotency of join:
143−-- forall a, join a a == a
144−-- Join semilattices capture the notion of sets with a "least upper bound".
141+||| Sets equipped with a binary operation that is commutative, associative and
142+||| idempotent. Must satisfy the following laws:
143+|||
144+||| + Associativity of join:
145+||| forall a b c, join a (join b c) == join (join a b) c
146+||| + Commutativity of join:
147+||| forall a b, join a b == join b a
148+||| + Idempotency of join:
149+||| forall a, join a a == a
150+|||
151+||| Join semilattices capture the notion of sets with a "least upper bound".
145152class JoinSemilattice a where
146153 join : a -> a -> a
147154
@@ -150,15 +157,17 @@ class JoinSemilattice a => VerifiedJoinSemilattice a where
150157 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
151158 total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
152159
153−-- Sets equipped with a binary operation that is commutative, associative and
154−-- idempotent. Must satisfy the following laws:
155−-- Associativity of meet:
156−-- forall a b c, meet a (meet b c) == meet (meet a b) c
157−-- Commutativity of meet:
158−-- forall a b, meet a b == meet b a
159−-- Idempotency of meet:
160−-- forall a, meet a a == a
161−-- Meet semilattices capture the notion of sets with a "greatest lower bound".
160+||| Sets equipped with a binary operation that is commutative, associative and
161+||| idempotent. Must satisfy the following laws:
162+|||
163+||| + Associativity of meet:
164+||| forall a b c, meet a (meet b c) == meet (meet a b) c
165+||| + Commutativity of meet:
166+||| forall a b, meet a b == meet b a
167+||| + Idempotency of meet:
168+||| forall a, meet a a == a
169+|||
170+||| Meet semilattices capture the notion of sets with a "greatest lower bound".
162171class MeetSemilattice a where
163172 meet : a -> a -> a
164173
@@ -167,84 +176,90 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where
167176 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
168177 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
169178
170−-- Sets equipped with a binary operation that is commutative, associative and
171−-- idempotent and supplied with a neutral element. Must satisfy the following
172−-- laws:
173−-- Associativity of join:
174−-- forall a b c, join a (join b c) == join (join a b) c
175−-- Commutativity of join:
176−-- forall a b, join a b == join b a
177−-- Idempotency of join:
178−-- forall a, join a a == a
179−-- Bottom:
180−-- forall a, join a bottom == bottom
181−-- Join semilattices capture the notion of sets with a "least upper bound"
182−-- equipped with a "bottom" element.
179+||| Sets equipped with a binary operation that is commutative, associative and
180+||| idempotent and supplied with a neutral element. Must satisfy the following
181+||| laws:
182+|||
183+||| + Associativity of join:
184+||| forall a b c, join a (join b c) == join (join a b) c
185+||| + Commutativity of join:
186+||| forall a b, join a b == join b a
187+||| + Idempotency of join:
188+||| forall a, join a a == a
189+||| + Bottom:
190+||| forall a, join a bottom == bottom
191+|||
192+||| Join semilattices capture the notion of sets with a "least upper bound"
193+||| equipped with a "bottom" element.
183194class JoinSemilattice a => BoundedJoinSemilattice a where
184195 bottom : a
185196
186197class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
187198 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
188199
189−-- Sets equipped with a binary operation that is commutative, associative and
190−-- idempotent and supplied with a neutral element. Must satisfy the following
191−-- laws:
192−-- Associativity of meet:
193−-- forall a b c, meet a (meet b c) == meet (meet a b) c
194−-- Commutativity of meet:
195−-- forall a b, meet a b == meet b a
196−-- Idempotency of meet:
197−-- forall a, meet a a == a
198−-- Top:
199−-- forall a, meet a top == top
200−-- Meet semilattices capture the notion of sets with a "greatest lower bound"
201−-- equipped with a "top" element.
200+||| Sets equipped with a binary operation that is commutative, associative and
201+||| idempotent and supplied with a neutral element. Must satisfy the following
202+||| laws:
203+|||
204+||| + Associativity of meet:
205+||| forall a b c, meet a (meet b c) == meet (meet a b) c
206+||| + Commutativity of meet:
207+||| forall a b, meet a b == meet b a
208+||| + Idempotency of meet:
209+||| forall a, meet a a == a
210+||| + Top:
211+||| forall a, meet a top == top
212+|||
213+||| Meet semilattices capture the notion of sets with a "greatest lower bound"
214+||| equipped with a "top" element.
202215class MeetSemilattice a => BoundedMeetSemilattice a where
203216 top : a
204217
205218class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
206219 total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
207220
208−-- Sets equipped with two binary operations that are both commutative,
209−-- associative and idempotent, along with absorbtion laws for relating the two
210−-- binary operations. Must satisfy the following:
211−-- Associativity of meet and join:
212−-- forall a b c, meet a (meet b c) == meet (meet a b) c
213−-- forall a b c, join a (join b c) == join (join a b) c
214−-- Commutativity of meet and join:
215−-- forall a b, meet a b == meet b a
216−-- forall a b, join a b == join b a
217−-- Idempotency of meet and join:
218−-- forall a, meet a a == a
219−-- forall a, join a a == a
220−-- Absorbtion laws for meet and join:
221−-- forall a b, meet a (join a b) == a
222−-- forall a b, join a (meet a b) == a
221+||| Sets equipped with two binary operations that are both commutative,
222+||| associative and idempotent, along with absorbtion laws for relating the two
223+||| binary operations. Must satisfy the following:
224+|||
225+||| + Associativity of meet and join:
226+||| forall a b c, meet a (meet b c) == meet (meet a b) c
227+||| forall a b c, join a (join b c) == join (join a b) c
228+||| + Commutativity of meet and join:
229+||| forall a b, meet a b == meet b a
230+||| forall a b, join a b == join b a
231+||| + Idempotency of meet and join:
232+||| forall a, meet a a == a
233+||| forall a, join a a == a
234+||| + Absorbtion laws for meet and join:
235+||| forall a b, meet a (join a b) == a
236+||| forall a b, join a (meet a b) == a
223237class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
224238
225239class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
226240 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
227241 total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
228242
229−-- Sets equipped with two binary operations that are both commutative,
230−-- associative and idempotent and supplied with neutral elements, along with
231−-- absorbtion laws for relating the two binary operations. Must satisfy the
232−-- following:
233−-- Associativity of meet and join:
234−-- forall a b c, meet a (meet b c) == meet (meet a b) c
235−-- forall a b c, join a (join b c) == join (join a b) c
236−-- Commutativity of meet and join:
237−-- forall a b, meet a b == meet b a
238−-- forall a b, join a b == join b a
239−-- Idempotency of meet and join:
240−-- forall a, meet a a == a
241−-- forall a, join a a == a
242−-- Absorbtion laws for meet and join:
243−-- forall a b, meet a (join a b) == a
244−-- forall a b, join a (meet a b) == a
245−-- Neutral for meet and join:
246−-- forall a, meet a top == top
247−-- forall a, join a bottom == bottom
243+||| Sets equipped with two binary operations that are both commutative,
244+||| associative and idempotent and supplied with neutral elements, along with
245+||| absorbtion laws for relating the two binary operations. Must satisfy the
246+||| following:
247+|||
248+||| + Associativity of meet and join:
249+||| forall a b c, meet a (meet b c) == meet (meet a b) c
250+||| forall a b c, join a (join b c) == join (join a b) c
251+||| + Commutativity of meet and join:
252+||| forall a b, meet a b == meet b a
253+||| forall a b, join a b == join b a
254+||| + Idempotency of meet and join:
255+||| forall a, meet a a == a
256+||| forall a, join a a == a
257+||| + Absorbtion laws for meet and join:
258+||| forall a b, meet a (join a b) == a
259+||| forall a b, join a (meet a b) == a
260+||| + Neutral for meet and join:
261+||| forall a, meet a top == top
262+||| forall a, join a bottom == bottom
248263class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
249264
250265class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }