Skip to content

Commit 7a378ab

Browse files
nickdrozdnickdrozd
committed
Add Algebra interfaces
1 parent 4aa1c1f commit 7a378ab

File tree

2 files changed

+166
-0
lines changed

2 files changed

+166
-0
lines changed

‎libs/contrib/Control/Algebra.idr‎

Lines changed: 165 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
1+
module Control.Algebra
2+
3+
infixl 6 <->
4+
infixl 7 <.>
5+
6+
||| Sets equipped with a single binary operation that is associative,
7+
||| along with a neutral element for that binary operation and
8+
||| inverses for all elements. Should (but may not) satisfy the
9+
||| following laws:
10+
|||
11+
||| + Associativity of `<+>`:
12+
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
13+
||| + Neutral for `<+>`:
14+
||| forall a, a <+> neutral == a
15+
||| forall a, neutral <+> a == a
16+
||| + Inverse for `<+>`:
17+
||| forall a, a <+> inverse a == neutral
18+
||| forall a, inverse a <+> a == neutral
19+
public export
20+
interface Monoid ty => Group ty where
21+
inverse : ty -> ty
22+
23+
(<->) : Group ty => ty -> ty -> ty
24+
(<->) left right = left <+> (inverse right)
25+
26+
||| Sets equipped with two binary operations, one associative and
27+
||| commutative supplied with a neutral element, and the other
28+
||| associative, with distributivity laws relating the two operations.
29+
||| Should (but may not) satisfy the following laws:
30+
|||
31+
||| + Associativity of `<+>`:
32+
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
33+
||| + Commutativity of `<+>`:
34+
||| forall a b, a <+> b == b <+> a
35+
||| + Neutral for `<+>`:
36+
||| forall a, a <+> neutral == a
37+
||| forall a, neutral <+> a == a
38+
||| + Inverse for `<+>`:
39+
||| forall a, a <+> inverse a == neutral
40+
||| forall a, inverse a <+> a == neutral
41+
||| + Associativity of `<.>`:
42+
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
43+
||| + Distributivity of `<.>` and `<+>`:
44+
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
45+
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
46+
public export
47+
interface Group ty => Ring ty where
48+
(<.>) : ty -> ty -> ty
49+
50+
||| Sets equipped with two binary operations, one associative and
51+
||| commutative supplied with a neutral element, and the other
52+
||| associative supplied with a neutral element, with distributivity
53+
||| laws relating the two operations. Should (but may not) satisfy the
54+
||| following laws:
55+
|||
56+
||| + Associativity of `<+>`:
57+
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
58+
||| + Commutativity of `<+>`:
59+
||| forall a b, a <+> b == b <+> a
60+
||| + Neutral for `<+>`:
61+
||| forall a, a <+> neutral == a
62+
||| forall a, neutral <+> a == a
63+
||| + Inverse for `<+>`:
64+
||| forall a, a <+> inverse a == neutral
65+
||| forall a, inverse a <+> a == neutral
66+
||| + Associativity of `<.>`:
67+
||| forall a b c, a <.> (b <.> c) == (a <.> b) <.> c
68+
||| + Neutral for `<.>`:
69+
||| forall a, a <.> unity == a
70+
||| forall a, unity <.> a == a
71+
||| + Distributivity of `<.>` and `<+>`:
72+
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
73+
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
74+
public export
75+
interface Ring ty => RingWithUnity ty where
76+
unity : ty
77+
78+
||| Sets equipped with two binary operations – both associative,
79+
||| commutative and possessing a neutral element – and distributivity
80+
||| laws relating the two operations. All elements except the additive
81+
||| identity should have a multiplicative inverse. Should (but may
82+
||| not) satisfy the following laws:
83+
|||
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+
||| + Unity for `<.>`:
97+
||| forall a, a <.> unity == a
98+
||| forall a, unity <.> a == a
99+
||| + InverseM of `<.>`, except for neutral
100+
||| forall a /= neutral, a <.> inverseM a == unity
101+
||| forall a /= neutral, inverseM a <.> a == unity
102+
||| + Distributivity of `<.>` and `<+>`:
103+
||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
104+
||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
105+
public export
106+
interface RingWithUnity ty => Field ty where
107+
inverseM : (x : ty) -> Not (x = neutral {ty}) -> ty
108+
109+
-- "Verified" Interfaces -----------------
110+
111+
public export
112+
interface Semigroup ty => VSemigroup ty where
113+
semigroupOpIsAssociative : (l, c, r : ty) ->
114+
l <+> (c <+> r) = (l <+> c) <+> r
115+
116+
public export
117+
interface (Monoid ty, VSemigroup ty) => VMonoid ty where
118+
monoidNeutralIsNeutralL : (l : ty) -> l <+> neutral {ty} = l
119+
monoidNeutralIsNeutralR : (r : ty) -> neutral {ty} <+> r = r
120+
121+
public export
122+
interface (VMonoid ty, Group ty) => VGroup ty where
123+
groupInverseIsInverseR : (r : ty) -> inverse r <+> r = neutral {ty}
124+
125+
||| Sets equipped with a single binary operation that is associative
126+
||| and commutative, along with a neutral element for that binary
127+
||| operation and inverses for all elements. Satisfies the following
128+
||| laws:
129+
|||
130+
||| + Associativity of `<+>`:
131+
||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
132+
||| + Commutativity of `<+>`:
133+
||| forall a b, a <+> b == b <+> a
134+
||| + Neutral for `<+>`:
135+
||| forall a, a <+> neutral == a
136+
||| forall a, neutral <+> a == a
137+
||| + Inverse for `<+>`:
138+
||| forall a, a <+> inverse a == neutral
139+
||| forall a, inverse a <+> a == neutral
140+
public export
141+
interface VGroup ty => AbelianGroup ty where
142+
groupOpIsCommutative : (l, r : ty) -> l <+> r = r <+> l
143+
144+
public export
145+
interface (AbelianGroup ty, Ring ty) => VRing ty where
146+
ringOpIsAssociative : (l, c, r : ty) ->
147+
l <.> (c <.> r) = (l <.> c) <.> r
148+
ringOpIsDistributiveL : (l, c, r : ty) ->
149+
l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
150+
ringOpIsDistributiveR : (l, c, r : ty) ->
151+
(l <+> c) <.> r = (l <.> r) <+> (c <.> r)
152+
153+
public export
154+
interface (VRing ty, RingWithUnity ty) => VRingWithUnity ty where
155+
unityIsRingIdL : (l : ty) -> l <.> unity {ty} = l
156+
unityIsRingIdR : (r : ty) -> unity {ty} <.> r = r
157+
158+
----------------------------------------
159+
160+
||| A homomorphism is a mapping that preserves group structure.
161+
public export
162+
interface (VGroup a, VGroup b) => GroupHomomorphism a b where
163+
to : a -> b
164+
toGroup : (x, y : a) ->
165+
to (x <+> y) = (to x) <+> (to y)

‎libs/contrib/contrib.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
package contrib
22

33
modules = Control.Delayed,
4+
Control.Algebra,
45

56
Data.List.TailRec,
67
Data.List.Equalities,

0 commit comments

Comments
 (0)