@@ -22,8 +22,6 @@ infixl 5 <#>
2222class Semigroup a where
2323 (<+>) : a -> a -> a
2424
25−class Semigroup a => VerifiedSemigroup a where
26− total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
2725
2826||| Sets equipped with a single binary operation that is associative, along with
2927||| a neutral element for that binary operation. Must satisfy the following
@@ -37,295 +35,3 @@ class Semigroup a => VerifiedSemigroup a where
3735class Semigroup a => Monoid a where
3836 neutral : a
3937
40−class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
41− total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
42− total monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
43−
44−||| Sets equipped with a single binary operation that is associative, along with
45−||| a neutral element for that binary operation and inverses for all elements.
46−||| Must satisfy the following laws:
47−||| + Associativity of `<+>`:
48−||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
49−||| + Neutral for `<+>`:
50−||| forall a, a <+> neutral == a
51−||| forall a, neutral <+> a == a
52−||| + Inverse for `<+>`:
53−||| forall a, a <+> inverse a == neutral
54−||| forall a, inverse a <+> a == neutral
55−class Monoid a => Group a where
56− inverse : a -> a
57−
58−class (VerifiedMonoid a, Group a) => VerifiedGroup a where
59− total groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
60− total groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
61−
62−(<->) : Group a => a -> a -> a
63−(<->) left right = left <+> (inverse right)
64−
65−||| Sets equipped with a single binary operation that is associative and
66−||| commutative, along with a neutral element for that binary operation and
67−||| inverses for all elements. Must satisfy the following laws:
68−|||
69−||| + Associativity of `<+>`:
70−||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
71−||| + Commutativity of `<+>`:
72−||| forall a b, a <+> b == b <+> a
73−||| + Neutral for `<+>`:
74−||| forall a, a <+> neutral == a
75−||| forall a, neutral <+> a == a
76−||| + Inverse for `<+>`:
77−||| forall a, a <+> inverse a == neutral
78−||| forall a, inverse a <+> a == neutral
79−class Group a => AbelianGroup a where { }
80−
81−class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
82− total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
83−
84−||| Sets equipped with two binary operations, one associative and commutative
85−||| supplied with a neutral element, and the other associative, with
86−||| distributivity laws relating the two operations. Must satisfy the following
87−||| laws:
88−|||
89−||| + Associativity of `<+>`:
90−||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
91−||| + Commutativity of `<+>`:
92−||| forall a b, a <+> b == b <+> a
93−||| + Neutral for `<+>`:
94−||| forall a, a <+> neutral == a
95−||| forall a, neutral <+> a == a
96−||| + Inverse for `<+>`:
97−||| forall a, a <+> inverse a == neutral
98−||| forall a, inverse a <+> a == neutral
99−||| + Associativity of `<.>`:
100−||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
101−||| + Distributivity of `<.>` and `<->`:
102−||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
103−||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
104−class AbelianGroup a => Ring a where
105− (<.>) : a -> a -> a
106−
107−class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
108− total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
109− total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
110− total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
111−
112−||| Sets equipped with two binary operations, one associative and commutative
113−||| supplied with a neutral element, and the other associative supplied with a
114−||| neutral element, with distributivity laws relating the two operations. Must
115−||| satisfy the following laws:
116−|||
117−||| + Associativity of `<+>`:
118−||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
119−||| + Commutativity of `<+>`:
120−||| forall a b, a <+> b == b <+> a
121−||| + Neutral for `<+>`:
122−||| forall a, a <+> neutral == a
123−||| forall a, neutral <+> a == a
124−||| + Inverse for `<+>`:
125−||| forall a, a <+> inverse a == neutral
126−||| forall a, inverse a <+> a == neutral
127−||| + Associativity of `<.>`:
128−||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
129−||| + Neutral for `<.>`:
130−||| forall a, a <.> unity == a
131−||| forall a, unity <.> a == a
132−||| + Distributivity of `<.>` and `<->`:
133−||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
134−||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
135−class Ring a => RingWithUnity a where
136− unity : a
137−
138−class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
139− total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
140− total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
141−
142−||| Sets equipped with a binary operation that is commutative, associative and
143−||| idempotent. Must satisfy the following laws:
144−|||
145−||| + Associativity of join:
146−||| forall a b c, join a (join b c) == join (join a b) c
147−||| + Commutativity of join:
148−||| forall a b, join a b == join b a
149−||| + Idempotency of join:
150−||| forall a, join a a == a
151−|||
152−||| Join semilattices capture the notion of sets with a "least upper bound".
153−class JoinSemilattice a where
154− join : a -> a -> a
155−
156−class JoinSemilattice a => VerifiedJoinSemilattice a where
157− total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
158− total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
159− total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
160−
161−||| Sets equipped with a binary operation that is commutative, associative and
162−||| idempotent. Must satisfy the following laws:
163−|||
164−||| + Associativity of meet:
165−||| forall a b c, meet a (meet b c) == meet (meet a b) c
166−||| + Commutativity of meet:
167−||| forall a b, meet a b == meet b a
168−||| + Idempotency of meet:
169−||| forall a, meet a a == a
170−|||
171−||| Meet semilattices capture the notion of sets with a "greatest lower bound".
172−class MeetSemilattice a where
173− meet : a -> a -> a
174−
175−class MeetSemilattice a => VerifiedMeetSemilattice a where
176− total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
177− total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
178− total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
179−
180−||| Sets equipped with a binary operation that is commutative, associative and
181−||| idempotent and supplied with a unitary element. Must satisfy the following
182−||| laws:
183−|||
184−||| + Associativity of join:
185−||| forall a b c, join a (join b c) == join (join a b) c
186−||| + Commutativity of join:
187−||| forall a b, join a b == join b a
188−||| + Idempotency of join:
189−||| forall a, join a a == a
190−||| + Bottom (Unitary Element):
191−||| forall a, join a bottom == a
192−|||
193−||| Join semilattices capture the notion of sets with a "least upper bound"
194−||| equipped with a "bottom" element.
195−class JoinSemilattice a => BoundedJoinSemilattice a where
196− bottom : a
197−
198−class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
199− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e
200−
201−||| Sets equipped with a binary operation that is commutative, associative and
202−||| idempotent and supplied with a unitary element. Must satisfy the following
203−||| laws:
204−|||
205−||| + Associativity of meet:
206−||| forall a b c, meet a (meet b c) == meet (meet a b) c
207−||| + Commutativity of meet:
208−||| forall a b, meet a b == meet b a
209−||| + Idempotency of meet:
210−||| forall a, meet a a == a
211−||| + Top (Unitary Element):
212−||| forall a, meet a top == a
213−|||
214−||| Meet semilattices capture the notion of sets with a "greatest lower bound"
215−||| equipped with a "top" element.
216−class MeetSemilattice a => BoundedMeetSemilattice a where
217− top : a
218−
219−class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
220− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = e
221−
222−||| Sets equipped with two binary operations that are both commutative,
223−||| associative and idempotent, along with absorbtion laws for relating the two
224−||| binary operations. Must satisfy the following:
225−|||
226−||| + Associativity of meet and join:
227−||| forall a b c, meet a (meet b c) == meet (meet a b) c
228−||| forall a b c, join a (join b c) == join (join a b) c
229−||| + Commutativity of meet and join:
230−||| forall a b, meet a b == meet b a
231−||| forall a b, join a b == join b a
232−||| + Idempotency of meet and join:
233−||| forall a, meet a a == a
234−||| forall a, join a a == a
235−||| + Absorbtion laws for meet and join:
236−||| forall a b, meet a (join a b) == a
237−||| forall a b, join a (meet a b) == a
238−class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
239−
240−class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
241− total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
242− total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
243−
244−||| Sets equipped with two binary operations that are both commutative,
245−||| associative and idempotent and supplied with neutral elements, along with
246−||| absorbtion laws for relating the two binary operations. Must satisfy the
247−||| following:
248−|||
249−||| + Associativity of meet and join:
250−||| forall a b c, meet a (meet b c) == meet (meet a b) c
251−||| forall a b c, join a (join b c) == join (join a b) c
252−||| + Commutativity of meet and join:
253−||| forall a b, meet a b == meet b a
254−||| forall a b, join a b == join b a
255−||| + Idempotency of meet and join:
256−||| forall a, meet a a == a
257−||| forall a, join a a == a
258−||| + Absorbtion laws for meet and join:
259−||| forall a b, meet a (join a b) == a
260−||| forall a b, join a (meet a b) == a
261−||| + Neutral for meet and join:
262−||| forall a, meet a top == top
263−||| forall a, join a bottom == bottom
264−class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
265−
266−class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
267−
268−-- Fields.
269−||| Sets equipped with two binary operations, both associative and commutative
270−||| supplied with a neutral element, with
271−||| distributivity laws relating the two operations. Must satisfy the following
272−||| laws:
273−|||
274−||| + Associativity of `<+>`:
275−||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
276−||| + Commutativity of `<+>`:
277−||| forall a b, a <+> b == b <+> a
278−||| + Neutral for `<+>`:
279−||| forall a, a <+> neutral == a
280−||| forall a, neutral <+> a == a
281−||| + Inverse for `<+>`:
282−||| forall a, a <+> inverse a == neutral
283−||| forall a, inverse a <+> a == neutral
284−||| + Associativity of `<.>`:
285−||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
286−||| + Unity for `<.>`:
287−||| forall a, a <.> unity == a
288−||| forall a, unity <.> a == a
289−||| + InverseM of `<.>`:
290−||| forall a, a <.> inverseM a == unity
291−||| forall a, inverseM a <.> a == unity
292−||| + Distributivity of `<.>` and `<->`:
293−||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
294−||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
295−class RingWithUnity a => Field a where
296− inverseM : a -> a
297−
298−class (VerifiedRing a, Field a) => VerifiedField a where
299− total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity
300− total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity
301−
302−||| A module over a ring is an additive abelian group of 'vectors' endowed with a
303−||| scale operation multiplying vectors by ring elements, and distributivity laws
304−||| relating the scale operation to both ring addition and module addition.
305−||| Must satisfy the following laws:
306−|||
307−||| + Compatibility of scalar multiplication with ring multiplication:
308−||| forall a b v, a <#> (b <#> v) = (a <.> b) <#> v
309−||| + Ring unity is the identity element of scalar multiplication:
310−||| forall v, unity <#> v = v
311−||| + Distributivity of `<#>` and `<+>`:
312−||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)
313−||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)
314−class (RingWithUnity a, AbelianGroup b) => Module a b where
315− (<#>) : a -> b -> b
316−
317−class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
318− total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
319− total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v
320− total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
321− total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
322−
323−||| A vector space is a module over a ring that is also a field
324−class (Field a, Module a b) => VectorSpace a b where {}
325−
326−class (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
327−
328−-- XXX todo:
329−-- Structures where "abs" make sense.
330−-- Euclidean domains, etc.
331−-- Where to put fromInteger and fromRational?