0 | module Algebra.Group
  1 |
  2 | import Data.List
  3 | import Data.List1
  4 | import Data.List1.Properties
  5 | import Data.Nat
  6 | import Syntax.PreorderReasoning
  7 |
  8 | %default total
  9 |
 10 | --------------------------------------------------------------------------------
 11 | --          "Operators"
 12 | --------------------------------------------------------------------------------
 13 |
 14 | export infixl 8 `p`,`sub`
 15 |
 16 | export infixl 9 `m`
 17 |
 18 | --------------------------------------------------------------------------------
 19 | --          Laws
 20 | --------------------------------------------------------------------------------
 21 |
 22 | ||| A unary operation on a type, for instance `negate`.
 23 | public export
 24 | 0 Op1 : Type -> Type
 25 | Op1 a = a -> a
 26 |
 27 | ||| A binary operation on a type, for instance `(+)`.
 28 | public export
 29 | 0 Op2 : Type -> Type
 30 | Op2 a = a -> a -> a
 31 |
 32 | ||| Proposition that the given binary operation is associative.
 33 | public export %tcinline
 34 | 0 Assoc : Op2 a -> Type
 35 | Assoc p = (u,v,w : a) -> u `p` (v `p` w) === (u `p` v) `p` w
 36 |
 37 | ||| Proposition that the given binary operation is associative.
 38 | public export %tcinline
 39 | 0 Associative : Op2 a -> Type
 40 | Associative p = {u,v,w : a} -> u `p` (v `p` w) === (u `p` v) `p` w
 41 |
 42 | ||| Proposition that the given binary operation is commutative.
 43 | public export
 44 | 0 Commutative : Op2 a -> Type
 45 | Commutative p = {u,v : a} -> u `p` v === v `p` u
 46 |
 47 | ||| Proposition that `z` is a left neutral element for the
 48 | ||| given binary operation.
 49 | public export
 50 | 0 LeftNeutral : (z : a) -> Op2 a -> Type
 51 | LeftNeutral z p = {u : a} -> z `p` u === u
 52 |
 53 | ||| Proposition that `z` is a right neutral element for the
 54 | ||| given binary operation.
 55 | public export
 56 | 0 RightNeutral : (z : a) -> Op2 a -> Type
 57 | RightNeutral z p = {u : a} -> u `p` z === u
 58 |
 59 | ||| Proposition that `i` is the left inverse of the given binary operation.
 60 | public export
 61 | 0 LeftInverse : (z : a) -> (i : Op1 a) -> Op2 a -> Type
 62 | LeftInverse z i p = {u : a} -> i u `p` u === z
 63 |
 64 | ||| Proposition that `i` is the right inverse of the given binary operation.
 65 | public export
 66 | 0 RightInverse : (z : a) -> (i : Op1 a) -> Op2 a -> Type
 67 | RightInverse z i p = {u : a} -> u `p` i u === z
 68 |
 69 | --------------------------------------------------------------------------------
 70 | --          Lemmata
 71 | --------------------------------------------------------------------------------
 72 |
 73 | ||| For a commutative operation, the left neutral element is also a
 74 | ||| right neutral element
 75 | export
 76 | rightNeutral : LeftNeutral z p -> Commutative p -> RightNeutral z p
 77 | rightNeutral ln com = Calc $
 78 |   |~ p u z
 79 |   ~~ p z u ... com
 80 |   ~~ u     ... ln
 81 |
 82 | ||| For a commutative operation, the right neutral element is also a
 83 | ||| left neutral element
 84 | export
 85 | leftNeutral : RightNeutral z p -> Commutative p -> LeftNeutral z p
 86 | leftNeutral rn com = Calc $
 87 |   |~ z `p` u
 88 |   ~~ u `p` z ... com
 89 |   ~~ u       ... rn
 90 |
 91 | ||| For a commutative operation, the left inverse is also a right inverse.
 92 | export
 93 | rightInverse : LeftInverse z i p -> Commutative p -> RightInverse z i p
 94 | rightInverse li com = Calc $
 95 |   |~ u `p` (i u)
 96 |   ~~ (i u) `p` u ... com
 97 |   ~~ z           ... li
 98 |
 99 | ||| For a commutative operation, the right inverse is also a left inverse.
100 | export
101 | leftInverse : RightInverse z i p -> Commutative p -> LeftInverse z i p
102 | leftInverse ri com = Calc $
103 |   |~ (i u) `p` u
104 |   ~~ u `p` (i u) ... com
105 |   ~~ z           ... ri
106 |
107 | --------------------------------------------------------------------------------
108 | --          Semigroup
109 | --------------------------------------------------------------------------------
110 |
111 | ||| A `Semigroup` is a set with a binary associative operation.
112 | public export
113 | record Semigroup (a : Type) (p : Op2 a) where
114 |   constructor MkSemigroup
115 |   associative : Associative p
116 |
117 | ||| Like a semigroup but the binary operation is also commutative.
118 | public export
119 | record CommutativeSemigroup (a : Type) (p : Op2 a) where
120 |   constructor MkCommutativeSemigroup
121 |   associative : Associative p
122 |   commutative : Commutative p
123 |
124 | namespace CommutativeSemigroup
125 |
126 |   ||| A commutative semigroup is also a semigroup.
127 |   export
128 |   (.sgrp) : CommutativeSemigroup a p -> Semigroup a p
129 |   c.sgrp = MkSemigroup c.associative
130 |
131 | --------------------------------------------------------------------------------
132 | --          Monoid
133 | --------------------------------------------------------------------------------
134 |
135 | ||| A `Monoid` is a set with a binary associative operation and a
136 | ||| neutral element `z` for that operation.
137 | public export
138 | record Monoid (a : Type) (z : a) (p : Op2 a) where
139 |   constructor MkMonoid
140 |   associative  : Associative p
141 |   rightNeutral : RightNeutral z p
142 |   leftNeutral  : LeftNeutral z p
143 |
144 | namespace Monoid
145 |
146 |   ||| A monoid is also a semigroup
147 |   export
148 |   (.sgrp) : Monoid a z p -> Semigroup a p
149 |   m.sgrp = MkSemigroup m.associative
150 |
151 | ||| Like `Monoid` but with a binary operation that is also commutative.
152 | public export
153 | record CommutativeMonoid (a : Type) (z : a) (p : Op2 a) where
154 |   constructor MkCommutativeMonoid
155 |   associative : Associative p
156 |   commutative : Commutative p
157 |   leftNeutral : LeftNeutral z p
158 |
159 | public export
160 | mkCommutativeMonoid :
161 |      {a : Type}
162 |   -> {z : a}
163 |   -> {p : Op2 a}
164 |   -> ((u,v,w : a) -> u `p` (v `p` w) === (u `p` v) `p` w)
165 |   -> ((u,v   : a) -> u `p` v === v `p` u)
166 |   -> ((u     : a) -> z `p` u === u)
167 |   -> CommutativeMonoid a z p
168 | mkCommutativeMonoid assoc comm ln =
169 |   MkCommutativeMonoid (assoc _ _ _) (comm _ _) (ln _)
170 |
171 | namespace CommutativeMonoid
172 |
173 |   ||| A commutative monoid is also a semigroup
174 |   export
175 |   (.sgrp) : CommutativeMonoid a z p -> Semigroup a p
176 |   m.sgrp = MkSemigroup m.associative
177 |
178 |   ||| A commutative monoid is also a semigroup
179 |   export
180 |   (.csgrp) : CommutativeMonoid a z p -> CommutativeSemigroup a p
181 |   m.csgrp = MkCommutativeSemigroup m.associative m.commutative
182 |
183 |   ||| For a commutative monoid, `z` is a right neutral element.
184 |   export
185 |   (.rightNeutral) : CommutativeMonoid a z p -> RightNeutral z p
186 |   m.rightNeutral = rightNeutral {p} m.leftNeutral m.commutative
187 |
188 |   ||| A commutative monoid is also a monoid
189 |   export
190 |   (.mon) : CommutativeMonoid a z p -> Monoid a z p
191 |   m.mon = MkMonoid m.associative m.rightNeutral m.leftNeutral
192 |
193 | --------------------------------------------------------------------------------
194 | --          Group
195 | --------------------------------------------------------------------------------
196 |
197 | ||| A `Group` is a monoid with an inverse operation.
198 | public export
199 | record Group (a : Type) (z : a) (i : Op1 a) (p : Op2 a) where
200 |   constructor MkGroup
201 |   associative  : Associative p
202 |   leftNeutral  : LeftNeutral z p
203 |   rightNeutral : RightNeutral z p
204 |   leftInverse  : LeftInverse z i p
205 |   rightInverse : RightInverse z i p
206 |
207 | ||| In a group, the binary operation is injective when applied
208 | ||| from the left.
209 | export
210 | 0 leftInjective :
211 |      Group a z i p
212 |   -> {u,v,w : a}
213 |   -> u `p` v === u `p` w
214 |   -> v === w
215 | leftInjective g prf = Calc $
216 |   |~ v
217 |   ~~ z `p` v           ..< g.leftNeutral
218 |   ~~ (i u `p` u) `p` v ..< cong (`p` v) g.leftInverse
219 |   ~~ i u `p` (u `p` v) ..< g.associative
220 |   ~~ i u `p` (u `p` w) ... cong (i u `p`) prf
221 |   ~~ (i u `p` u) `p` w ... g.associative
222 |   ~~ z `p` w           ... cong (`p` w) g.leftInverse
223 |   ~~ w                 ... g.leftNeutral
224 |
225 | ||| In a group, from `p v u === z` follows `u === i v`.
226 | export
227 | 0 solveInverseLeft :
228 |      Group a z i p
229 |   -> {u,v : a}
230 |   -> v `p` u === z
231 |   -> u === i v
232 | solveInverseLeft g prf = leftInjective g $ Calc $
233 |   |~ v `p` u
234 |   ~~ z         ... prf
235 |   ~~ v `p` i v ..< g.rightInverse
236 |
237 | ||| In a group, the inverse of a product is the product of inverses
238 | ||| (in reverse order).
239 | export
240 | 0 invertProduct :
241 |      Group a z i p
242 |   -> {u,v : a}
243 |   -> i (u `p` v) === i v `p` i u
244 | invertProduct g = sym $ solveInverseLeft g $ Calc $
245 |   |~ (u `p` v) `p` (i v `p` i u)
246 |   ~~ u `p` (v `p` (i v `p` i u)) ..< g.associative
247 |   ~~ u `p` ((v `p` i v) `p` i u) ... cong (u `p`) g.associative
248 |   ~~ u `p` (z `p` i u)           ... cong (\q => u `p` (q `p` i u)) g.rightInverse
249 |   ~~ u `p` i u                   ... cong (u `p`) g.leftNeutral
250 |   ~~ z                           ... g.rightInverse
251 |
252 | ||| In a group, the binary operation is injective when applied
253 | ||| from the right.
254 | export
255 | 0 rightInjective :
256 |      Group a z i p
257 |   -> {u,v,w : a}
258 |   -> v `p` u === w `p` u
259 |   -> v === w
260 | rightInjective g prf = Calc $
261 |   |~ v
262 |   ~~ v `p` z           ..< g.rightNeutral
263 |   ~~ v `p` (u `p` i u) ..< cong (p v) g.rightInverse
264 |   ~~ (v `p` u) `p` i u ... g.associative
265 |   ~~ (w `p` u) `p` i u ... cong (`p` i u) prf
266 |   ~~ w `p` (u `p` i u) ..< g.associative
267 |   ~~ w `p` z           ... cong (w `p`) g.rightInverse
268 |   ~~ w                 ... g.rightNeutral
269 |
270 | ||| In a group, from `p u v === z` follows `u === i v`.
271 | export
272 | 0 solveInverseRight :
273 |      Group a z i p
274 |   -> {u,v : a}
275 |   -> u `p` v === z
276 |   -> u === i v
277 | solveInverseRight g prf = rightInjective g $ Calc $
278 |   |~ u `p` v
279 |   ~~ z         ... prf
280 |   ~~ i v `p` v ..< g.leftInverse
281 |
282 | ||| In a group, the inverse of the neutral element is
283 | ||| the neutral element itself.
284 | export
285 | 0 inverseZero : Group a z i p -> i z === z
286 | inverseZero g = sym $ solveInverseRight g $ g.rightNeutral
287 |
288 | ||| In a group, inverting an value twice yields the original value.
289 | export
290 | 0 inverseInvolutory : Group a z i p -> {u : a} -> i (i u) === u
291 | inverseInvolutory g = sym $ solveInverseRight g g.rightInverse
292 |
293 | namespace Group
294 |
295 |   ||| A group is also a semigroup
296 |   export
297 |   (.sgrp) : Group a z i p -> Semigroup a p
298 |   g.sgrp = MkSemigroup g.associative
299 |
300 |   ||| A group is also a monoid
301 |   export
302 |   (.mon) : Group a z i p -> Monoid a z p
303 |   g.mon = MkMonoid g.associative g.rightNeutral g.leftNeutral
304 |
305 | ||| An abelian group is a group with a commutative binary operation.
306 | public export
307 | record AbelianGroup (a : Type) (z : a) (i : Op1 a) (p : Op2 a) where
308 |   constructor MkAbelianGroup
309 |   associative  : Associative p
310 |   commutative  : Commutative p
311 |   leftNeutral  : LeftNeutral z p
312 |   leftInverse  : LeftInverse z i p
313 |
314 | namespace AbelianGroup
315 |
316 |   ||| An abelian group is also a semigroup
317 |   export
318 |   (.sgrp) : AbelianGroup a z i p -> Semigroup a p
319 |   g.sgrp = MkSemigroup g.associative
320 |
321 |   ||| An abelian group is also a commutative monoid
322 |   export
323 |   (.cmon) : AbelianGroup a z i p -> CommutativeMonoid a z p
324 |   g.cmon = MkCommutativeMonoid g.associative g.commutative g.leftNeutral
325 |
326 |   ||| An abelian group is also a commutative semigroup
327 |   export
328 |   (.csgrp) : AbelianGroup a z i p -> CommutativeSemigroup a p
329 |   g.csgrp = g.cmon.csgrp
330 |
331 |   ||| For an abelian group, `z` is a right neutral element.
332 |   export
333 |   (.rightNeutral) : AbelianGroup a z i p -> RightNeutral z p
334 |   g.rightNeutral = g.cmon.rightNeutral
335 |
336 |   ||| For an abelian group, `i` is a right inverse.
337 |   export
338 |   (.rightInverse) : AbelianGroup a z i p -> RightInverse z i p
339 |   g.rightInverse = rightInverse {p} g.leftInverse g.commutative
340 |
341 |   ||| An abelian group is also a monoid
342 |   export
343 |   (.mon) : AbelianGroup a z i p -> Monoid a z p
344 |   g.mon = g.cmon.mon
345 |
346 |   ||| An abelian group is also a group
347 |   export
348 |   (.grp) : AbelianGroup a z i p -> Group a z i p
349 |   g.grp =
350 |     MkGroup
351 |       g.associative
352 |       g.leftNeutral
353 |       g.rightNeutral
354 |       g.leftInverse
355 |       g.rightInverse
356 |
357 | --------------------------------------------------------------------------------
358 | --          List1
359 | --------------------------------------------------------------------------------
360 |
361 | export
362 | 0 sgrp_list1 : Semigroup (List1 a) (++)
363 | sgrp_list1 = MkSemigroup (appendAssociative _ _ _)
364 |
365 | --------------------------------------------------------------------------------
366 | --          List
367 | --------------------------------------------------------------------------------
368 |
369 | export
370 | 0 mon_list : Monoid (List a) [] (++)
371 | mon_list = MkMonoid (appendAssociative _ _ _) (appendNilRightNeutral _) Refl
372 |
373 | --------------------------------------------------------------------------------
374 | --          Nat
375 | --------------------------------------------------------------------------------
376 |
377 | export
378 | 0 cmon_nat_plus : CommutativeMonoid Nat Z (+)
379 | cmon_nat_plus =
380 |   mkCommutativeMonoid plusAssociative plusCommutative plusZeroLeftNeutral
381 |
382 | export
383 | 0 cmon_nat_mult : CommutativeMonoid Nat 1 (*)
384 | cmon_nat_mult =
385 |   mkCommutativeMonoid multAssociative multCommutative multOneLeftNeutral
386 |
387 | --------------------------------------------------------------------------------
388 | --          Maybe
389 | --------------------------------------------------------------------------------
390 |
391 | namespace Maybe
392 |   export
393 |   0 appendAssoc : Associative ((<+>) {ty = Maybe a})
394 |   appendAssoc {u = Just vx} = Refl
395 |   appendAssoc {u = Nothing} = Refl
396 |
397 |   export
398 |   0 appendRightNeutral : RightNeutral Nothing ((<+>) {ty = Maybe a})
399 |   appendRightNeutral {u = Just _}  = Refl
400 |   appendRightNeutral {u = Nothing} = Refl
401 |
402 | ||| The default monoid for `Maybe` provided by the prelude:
403 | ||| Returns the first non-empty value (if any).
404 | export
405 | 0 mon_maybe : Monoid (Maybe a) Nothing (<+>)
406 | mon_maybe = MkMonoid appendAssoc appendRightNeutral Refl
407 |
408 | ||| Use a binary function to combine two `Maybe`s in case both
409 | ||| are `Just`s.
410 | |||
411 | ||| This is an associative function, if `p` is associative. It is
412 | ||| commutative if `p` is commutative.
413 | public export
414 | union : (p : a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
415 | union p Nothing  m        = m
416 | union p (Just u) Nothing  = Just u
417 | union p (Just u) (Just v) = Just $ p u v
418 |
419 | namespace Union
420 |   export
421 |   0 unionAssoc : Associative p -> Associative (union p)
422 |   unionAssoc {u=Nothing}                         s = Refl
423 |   unionAssoc {u=Just u}  {v=Nothing}             s = Refl
424 |   unionAssoc {u=Just u}  {v=Just v}  {w=Nothing} s = Refl
425 |   unionAssoc {u=Just u}  {v=Just v}  {w=Just w}  s = cong Just s
426 |
427 |   export
428 |   0 unionCommutative : Commutative p -> Commutative (union p)
429 |   unionCommutative {u=Nothing} {v=Nothing} _ = Refl
430 |   unionCommutative {u=Nothing} {v=Just v}  _ = Refl
431 |   unionCommutative {u=Just u}  {v=Nothing} _ = Refl
432 |   unionCommutative {u=Just u}  {v=Just v}  s = cong Just s
433 |
434 |   export
435 |   0 unionRightNeutral : RightNeutral Nothing (union p)
436 |   unionRightNeutral {u = Just _}  = Refl
437 |   unionRightNeutral {u = Nothing} = Refl
438 |
439 | export
440 | 0 mon_union : Associative p -> Monoid (Maybe a) Nothing (union p)
441 | mon_union ap = MkMonoid (unionAssoc ap) unionRightNeutral Refl
442 |
443 | export
444 | 0 cmon_union :
445 |      CommutativeSemigroup a p
446 |   -> CommutativeMonoid (Maybe a) Nothing (union p)
447 | cmon_union s =
448 |   MkCommutativeMonoid
449 |     (mon_union s.associative).associative
450 |     (unionCommutative s.commutative)
451 |     Refl
452 |
453 | --------------------------------------------------------------------------------
454 | --          Ordering
455 | --------------------------------------------------------------------------------
456 |
457 | namespace Ordering
458 |   export
459 |   0 appendAssoc : Associative ((<+>) {ty = Ordering})
460 |   appendAssoc {u = EQ} = Refl
461 |   appendAssoc {u = LT} = Refl
462 |   appendAssoc {u = GT} = Refl
463 |
464 |   export
465 |   0 appendRightNeutral : RightNeutral EQ ((<+>) {ty = Ordering})
466 |   appendRightNeutral {u = EQ} = Refl
467 |   appendRightNeutral {u = LT} = Refl
468 |   appendRightNeutral {u = GT} = Refl
469 |
470 | ||| The default monoid for `Ordering` provided by the prelude:
471 | ||| Returns the first non-`EQ` value (if any).
472 | export
473 | 0 mon_ordering : Monoid Ordering EQ (<+>)
474 | mon_ordering = MkMonoid appendAssoc appendRightNeutral Refl
475 |
476 | --------------------------------------------------------------------------------
477 | --          Unit
478 | --------------------------------------------------------------------------------
479 |
480 | namespace Unit
481 |   export
482 |   neg : () -> ()
483 |   neg _ = ()
484 |
485 |   export
486 |   0 appendLeftNeutral : LeftNeutral MkUnit ((<+>) {ty = Unit})
487 |   appendLeftNeutral {u = ()} = Refl
488 |
489 | ||| The default group for `Unit` provided by the prelude.
490 | export
491 | 0 agrp_unit : AbelianGroup Unit MkUnit Unit.neg (<+>)
492 | agrp_unit = MkAbelianGroup Refl Refl appendLeftNeutral Refl
493 |
494 | --------------------------------------------------------------------------------
495 | --          Primitives
496 | --------------------------------------------------------------------------------
497 |
498 | unsafeRefl : a === b
499 | unsafeRefl = believe_me (Refl {x = a})
500 |
501 | export
502 | 0 mon_string : Monoid String "" Prelude.String.(++)
503 | mon_string = MkMonoid unsafeRefl unsafeRefl unsafeRefl
504 |
505 | export
506 | 0 plus_bits8 : AbelianGroup Bits8 0 Prelude.negate Prelude.(+)
507 | plus_bits8 = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
508 |
509 | export
510 | 0 mult_bits8 : CommutativeMonoid Bits8 1 Prelude.(*)
511 | mult_bits8 = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
512 |
513 | export
514 | 0 plus_bits16 : AbelianGroup Bits16 0 Prelude.negate Prelude.(+)
515 | plus_bits16 = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
516 |
517 | export
518 | 0 mult_bits16 : CommutativeMonoid Bits16 1 Prelude.(*)
519 | mult_bits16 = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
520 |
521 | export
522 | 0 plus_bits32 : AbelianGroup Bits32 0 Prelude.negate Prelude.(+)
523 | plus_bits32 = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
524 |
525 | export
526 | 0 mult_bits32 : CommutativeMonoid Bits32 1 Prelude.(*)
527 | mult_bits32 = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
528 |
529 | export
530 | 0 plus_bits64 : AbelianGroup Bits64 0 Prelude.negate Prelude.(+)
531 | plus_bits64 = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
532 |
533 | export
534 | 0 mult_bits64 : CommutativeMonoid Bits64 1 Prelude.(*)
535 | mult_bits64 = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
536 |
537 | export
538 | 0 plus_int8 : AbelianGroup Int8 0 Prelude.negate Prelude.(+)
539 | plus_int8 = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
540 |
541 | export
542 | 0 mult_int8 : CommutativeMonoid Int8 1 Prelude.(*)
543 | mult_int8 = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
544 |
545 | export
546 | 0 plus_int16 : AbelianGroup Int16 0 Prelude.negate Prelude.(+)
547 | plus_int16 = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
548 |
549 | export
550 | 0 mult_int16 : CommutativeMonoid Int16 1 Prelude.(*)
551 | mult_int16 = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
552 |
553 | export
554 | 0 plus_int32 : AbelianGroup Int32 0 Prelude.negate Prelude.(+)
555 | plus_int32 = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
556 |
557 | export
558 | 0 mult_int32 : CommutativeMonoid Int32 1 Prelude.(*)
559 | mult_int32 = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
560 |
561 | export
562 | 0 plus_int64 : AbelianGroup Int64 0 Prelude.negate Prelude.(+)
563 | plus_int64 = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
564 |
565 | export
566 | 0 mult_int64 : CommutativeMonoid Int64 1 Prelude.(*)
567 | mult_int64 = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
568 |
569 | export
570 | 0 plus_integer : AbelianGroup Integer 0 Prelude.negate Prelude.(+)
571 | plus_integer = MkAbelianGroup unsafeRefl unsafeRefl unsafeRefl unsafeRefl
572 |
573 | export
574 | 0 mult_integer : CommutativeMonoid Integer 1 Prelude.(*)
575 | mult_integer = MkCommutativeMonoid unsafeRefl unsafeRefl unsafeRefl
576 |