git.iko.soy/Idris-dev
on master help sign in
Merge pull request #10 from dpmulligan/master
7cca84fEdwin Brady
lib/prelude/algebra.idr+56−6
compare with master
unifiedsplit
@@ -2,12 +2,16 @@ module prelude.algebra
2
2
3import builtins
3import builtins
4
4
5+-- XXX: change?
6+infixl 6 <->
7+infixl 6 <+>
8+infixl 6 <*>
9+
5%access public
10%access public
6
11
7−-- XXX: change?
12+--------------------------------------------------------------------------------
8−infix 6 <->
13+-- A modest class hierarchy
9−infix 6 <+>
14+--------------------------------------------------------------------------------
10−infix 6 <*>
11
15
12-- Sets equipped with a single binary operation that is associative. Must
16-- Sets equipped with a single binary operation that is associative. Must
13-- satisfy the following laws:
17-- satisfy the following laws:
@@ -16,6 +20,9 @@ infix 6 <*>
16class Semigroup a where
20class Semigroup a where
17 (<+>) : a -> a -> a
21 (<+>) : a -> a -> a
18
22
23+class Semigroup a => VerifiedSemigroup a where
24+ semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
25+
19-- Sets equipped with a single binary operation that is associative, along with
26-- Sets equipped with a single binary operation that is associative, along with
20-- a neutral element for that binary operation. Must satisfy the following
27-- a neutral element for that binary operation. Must satisfy the following
21-- laws:
28-- laws:
@@ -27,6 +34,10 @@ class Semigroup a where
27class Semigroup a => Monoid a where
34class Semigroup a => Monoid a where
28 neutral : a
35 neutral : a
29
36
37+class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
38+ monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
39+ monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
40+
30-- Sets equipped with a single binary operation that is associative, along with
41-- Sets equipped with a single binary operation that is associative, along with
31-- a neutral element for that binary operation and inverses for all elements.
42-- a neutral element for that binary operation and inverses for all elements.
32-- Must satisfy the following laws:
43-- Must satisfy the following laws:
@@ -41,6 +52,10 @@ class Semigroup a => Monoid a where
41class Monoid a => Group a where
52class Monoid a => Group a where
42 inverse : a -> a
53 inverse : a -> a
43
54
55+class (VerifiedMonoid a, Group a) => VerifiedGroup a where
56+ groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
57+ groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
58+
44(<->) : Group a => a -> a -> a
59(<->) : Group a => a -> a -> a
45(<->) left right = left <+> (inverse right)
60(<->) left right = left <+> (inverse right)
46
61
@@ -59,6 +74,9 @@ class Monoid a => Group a where
59-- forall a, inverse a <+> a == neutral
74-- forall a, inverse a <+> a == neutral
60class Group a => AbelianGroup a where { }
75class Group a => AbelianGroup a where { }
61
76
77+class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
78+ abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
79+
62-- Sets equipped with two binary operations, one associative and commutative
80-- Sets equipped with two binary operations, one associative and commutative
63-- supplied with a neutral element, and the other associative, with
81-- supplied with a neutral element, and the other associative, with
64-- distributivity laws relating the two operations. Must satisfy the following
82-- distributivity laws relating the two operations. Must satisfy the following
@@ -81,6 +99,11 @@ class Group a => AbelianGroup a where { }
81class AbelianGroup a => Ring a where
99class AbelianGroup a => Ring a where
82 (<*>) : a -> a -> a
100 (<*>) : a -> a -> a
83
101
102+class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
103+ ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
104+ ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
105+ ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
106+
84-- Sets equipped with two binary operations, one associative and commutative
107-- Sets equipped with two binary operations, one associative and commutative
85-- supplied with a neutral element, and the other associative supplied with a
108-- supplied with a neutral element, and the other associative supplied with a
86-- neutral element, with distributivity laws relating the two operations. Must
109-- neutral element, with distributivity laws relating the two operations. Must
@@ -106,6 +129,10 @@ class AbelianGroup a => Ring a where
106class Ring a => RingWithUnity a where
129class Ring a => RingWithUnity a where
107 unity : a
130 unity : a
108
131
132+class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
133+ ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
134+ ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
135+
109-- Sets equipped with a binary operation that is commutative, associative and
136-- Sets equipped with a binary operation that is commutative, associative and
110-- idempotent. Must satisfy the following laws:
137-- idempotent. Must satisfy the following laws:
111-- Associativity of join:
138-- Associativity of join:
@@ -118,6 +145,11 @@ class Ring a => RingWithUnity a where
118class JoinSemilattice a where
145class JoinSemilattice a where
119 join : a -> a -> a
146 join : a -> a -> a
120
147
148+class JoinSemilattice a => VerifiedJoinSemilattice a where
149+ joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
150+ joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
151+ joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
152+
121-- Sets equipped with a binary operation that is commutative, associative and
153-- Sets equipped with a binary operation that is commutative, associative and
122-- idempotent. Must satisfy the following laws:
154-- idempotent. Must satisfy the following laws:
123-- Associativity of meet:
155-- Associativity of meet:
@@ -130,6 +162,11 @@ class JoinSemilattice a where
130class MeetSemilattice a where
162class MeetSemilattice a where
131 meet : a -> a -> a
163 meet : a -> a -> a
132
164
165+class MeetSemilattice a => VerifiedMeetSemilattice a where
166+ meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
167+ meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
168+ meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
169+
133-- Sets equipped with a binary operation that is commutative, associative and
170-- Sets equipped with a binary operation that is commutative, associative and
134-- idempotent and supplied with a neutral element. Must satisfy the following
171-- idempotent and supplied with a neutral element. Must satisfy the following
135-- laws:
172-- laws:
@@ -139,13 +176,16 @@ class MeetSemilattice a where
139-- forall a b, join a b == join b a
176-- forall a b, join a b == join b a
140-- Idempotency of join:
177-- Idempotency of join:
141-- forall a, join a a == a
178-- forall a, join a a == a
142−-- Neutral for join:
179+-- Bottom:
143-- forall a, join a bottom == bottom
180-- forall a, join a bottom == bottom
144-- Join semilattices capture the notion of sets with a "least upper bound"
181-- Join semilattices capture the notion of sets with a "least upper bound"
145-- equipped with a "bottom" element.
182-- equipped with a "bottom" element.
146class JoinSemilattice a => BoundedJoinSemilattice a where
183class JoinSemilattice a => BoundedJoinSemilattice a where
147 bottom : a
184 bottom : a
148
185
186+class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
187+ boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
188+
149-- Sets equipped with a binary operation that is commutative, associative and
189-- Sets equipped with a binary operation that is commutative, associative and
150-- idempotent and supplied with a neutral element. Must satisfy the following
190-- idempotent and supplied with a neutral element. Must satisfy the following
151-- laws:
191-- laws:
@@ -155,13 +195,16 @@ class JoinSemilattice a => BoundedJoinSemilattice a where
155-- forall a b, meet a b == meet b a
195-- forall a b, meet a b == meet b a
156-- Idempotency of meet:
196-- Idempotency of meet:
157-- forall a, meet a a == a
197-- forall a, meet a a == a
158−-- Neutral for meet:
198+-- Top:
159-- forall a, meet a top == top
199-- forall a, meet a top == top
160-- Meet semilattices capture the notion of sets with a "greatest lower bound"
200-- Meet semilattices capture the notion of sets with a "greatest lower bound"
161-- equipped with a "top" element.
201-- equipped with a "top" element.
162class MeetSemilattice a => BoundedMeetSemilattice a where
202class MeetSemilattice a => BoundedMeetSemilattice a where
163 top : a
203 top : a
164
204
205+class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
206+ boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
207+
165-- Sets equipped with two binary operations that are both commutative,
208-- Sets equipped with two binary operations that are both commutative,
166-- associative and idempotent, along with absorbtion laws for relating the two
209-- associative and idempotent, along with absorbtion laws for relating the two
167-- binary operations. Must satisfy the following:
210-- binary operations. Must satisfy the following:
@@ -179,6 +222,10 @@ class MeetSemilattice a => BoundedMeetSemilattice a where
179-- forall a b, join a (meet a b) == a
222-- forall a b, join a (meet a b) == a
180class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
223class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
181
224
225+class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
226+ latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
227+ latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
228+
182-- Sets equipped with two binary operations that are both commutative,
229-- Sets equipped with two binary operations that are both commutative,
183-- associative and idempotent and supplied with neutral elements, along with
230-- associative and idempotent and supplied with neutral elements, along with
184-- absorbtion laws for relating the two binary operations. Must satisfy the
231-- absorbtion laws for relating the two binary operations. Must satisfy the
@@ -199,6 +246,9 @@ class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
199-- forall a, meet a top == top
246-- forall a, meet a top == top
200-- forall a, join a bottom == bottom
247-- forall a, join a bottom == bottom
201class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
248class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }
249+
250+class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
251+
202
252
203-- XXX todo:
253-- XXX todo:
204-- Fields and vector spaces.
254-- Fields and vector spaces.
lib/prelude/nat.idr+87−77
@@ -44,6 +44,51 @@ total power : Nat -> Nat -> Nat
44power base O = S O
44power base O = S O
45power base (S exp) = mult base $ power base exp
45power base (S exp) = mult base $ power base exp
46
46
47+--------------------------------------------------------------------------------
48+-- Comparisons
49+--------------------------------------------------------------------------------
50+
51+data LTE : Nat -> Nat -> Set where
52+ lteZero : LTE O right
53+ lteSucc : LTE left right -> LTE (S left) (S right)
54+
55+total GTE : Nat -> Nat -> Set
56+GTE left right = LTE right left
57+
58+total LT : Nat -> Nat -> Set
59+LT left right = LTE (S left) right
60+
61+total GT : Nat -> Nat -> Set
62+GT left right = LT right left
63+
64+total lte : Nat -> Nat -> Bool
65+lte O right = True
66+lte left O = False
67+lte (S left) (S right) = lte left right
68+
69+total gte : Nat -> Nat -> Bool
70+gte left right = lte right left
71+
72+total lt : Nat -> Nat -> Bool
73+lt left right = lte (S left) right
74+
75+total gt : Nat -> Nat -> Bool
76+gt left right = lt right left
77+
78+total minimum : Nat -> Nat -> Nat
79+minimum left right =
80+ if lte left right then
81+ left
82+ else
83+ right
84+
85+total maximum : Nat -> Nat -> Nat
86+maximum left right =
87+ if lte left right then
88+ right
89+ else
90+ left
91+
47--------------------------------------------------------------------------------
92--------------------------------------------------------------------------------
48-- Type class instances
93-- Type class instances
49--------------------------------------------------------------------------------
94--------------------------------------------------------------------------------
@@ -85,35 +130,48 @@ record Multiplicative : Set where
85record Additive : Set where
130record Additive : Set where
86 getAdditive : Nat -> Additive
131 getAdditive : Nat -> Additive
87
132
88−-- XXX: infix operators don't seem to be being exported correctly from
89−-- algebra.idr?
90−--instance Monoid Multiplicative where
133+instance Semigroup Multiplicative where
91−-- neutral = getMultiplicative $ S O
92−-- left <+> right = getMultiplicative $ left' * right'
134+ (<+>) left right = getMultiplicative $ left' * right'
93−-- where
135+ where
94−-- left' : Nat
136+ left' : Nat
95−-- left' =
137+ left' =
96−-- case left of
138+ case left of
97−-- getMultiplicative m => m
139+ getMultiplicative m => m
98−
140+
99−-- right' : Nat
141+ right' : Nat
100−-- right' =
142+ right' =
101−-- case right of
143+ case right of
102−-- getMultiplicative m => m
144+ getMultiplicative m => m
103−
145+
104−--instance Monoid Additive where
146+instance Semigroup Additive where
105−-- neutral = getAdditive $ O
106−-- left <+> right = getAdditive $ left' + right'
147+ left <+> right = getAdditive $ left' + right'
107−-- where
148+ where
108−-- left' : Nat
149+ left' : Nat
109−-- left' =
150+ left' =
110−-- case left of
151+ case left of
111−-- getAdditive m => m
152+ getAdditive m => m
112−
153+
113−-- right' : Nat
154+ right' : Nat
114−-- right' =
155+ right' =
115−-- case right of
156+ case right of
116−-- getAdditive m => m
157+ getAdditive m => m
158+
159+instance Monoid Multiplicative where
160+ neutral = getMultiplicative $ S O
161+
162+instance Monoid Additive where
163+ neutral = getAdditive O
164+
165+instance MeetSemilattice Nat where
166+ meet = minimum
167+
168+instance JoinSemilattice Nat where
169+ join = maximum
170+
171+instance Lattice Nat where { }
172+
173+instance BoundedJoinSemilattice Nat where
174+ bottom = O
117
175
118--------------------------------------------------------------------------------
176--------------------------------------------------------------------------------
119-- Auxilliary notions
177-- Auxilliary notions
@@ -136,51 +194,6 @@ fib (S (S n)) = fib (S n) + fib n
136-- GCD and LCM
194-- GCD and LCM
137--------------------------------------------------------------------------------
195--------------------------------------------------------------------------------
138
196
139−--------------------------------------------------------------------------------
140−-- Comparisons
141−--------------------------------------------------------------------------------
142−
143−data LTE : Nat -> Nat -> Set where
144− lteZero : LTE O right
145− lteSucc : LTE left right -> LTE (S left) (S right)
146−
147−total GTE : Nat -> Nat -> Set
148−GTE left right = LTE right left
149−
150−total LT : Nat -> Nat -> Set
151−LT left right = LTE (S left) right
152−
153−total GT : Nat -> Nat -> Set
154−GT left right = LT right left
155−
156−total lte : Nat -> Nat -> Bool
157−lte O right = True
158−lte left O = False
159−lte (S left) (S right) = lte left right
160−
161−total gte : Nat -> Nat -> Bool
162−gte left right = lte right left
163−
164−total lt : Nat -> Nat -> Bool
165−lt left right = lte (S left) right
166−
167−total gt : Nat -> Nat -> Bool
168−gt left right = lt right left
169−
170−total minimum : Nat -> Nat -> Nat
171−minimum left right =
172− if lte left right then
173− left
174− else
175− right
176−
177−total maximum : Nat -> Nat -> Nat
178−maximum left right =
179− if lte left right then
180− right
181− else
182− left
183−
184--------------------------------------------------------------------------------
197--------------------------------------------------------------------------------
185-- Division and modulus
198-- Division and modulus
186--------------------------------------------------------------------------------
199--------------------------------------------------------------------------------
@@ -712,9 +725,6 @@ plusZeroRightNeutralStepCase = proof {
712 trivial;
725 trivial;
713}
726}
714
727
715−
716−---------- Proofs ----------
717−
718maximumCommutativeStepCase = proof {
728maximumCommutativeStepCase = proof {
719 intros;
729 intros;
720 rewrite (boolElimSuccSucc (lte left right) right left);
730 rewrite (boolElimSuccSucc (lte left right) right left);