git.iko.soy/Idris-dev
on master help sign in
Add implementation of `VerifiedSemigroup Nat`, and others along the same lines, all in contrib.
6490356Chris Gibbs
libs/contrib/Control/Algebra/NumericImplementations.idr+26−6
compare with master
unifiedsplit
@@ -9,6 +9,8 @@ import Data.ZZ
9
9
10%access public export
10%access public export
11
11
12+-- Integer
13+
12Semigroup Integer where
14Semigroup Integer where
13 (<+>) = (+)
15 (<+>) = (+)
14
16
@@ -18,7 +20,7 @@ Monoid Integer where
18Group Integer where
20Group Integer where
19 inverse = (* -1)
21 inverse = (* -1)
20
22
21−AbelianGroup Integer where
23+AbelianGroup Integer where
22
24
23Ring Integer where
25Ring Integer where
24 (<.>) = (*)
26 (<.>) = (*)
@@ -26,6 +28,7 @@ Ring Integer where
26RingWithUnity Integer where
28RingWithUnity Integer where
27 unity = 1
29 unity = 1
28
30
31+-- Int
29
32
30Semigroup Int where
33Semigroup Int where
31 (<+>) = (+)
34 (<+>) = (+)
@@ -44,6 +47,7 @@ Ring Int where
44RingWithUnity Int where
47RingWithUnity Int where
45 unity = 1
48 unity = 1
46
49
50+-- Double
47
51
48Semigroup Double where
52Semigroup Double where
49 (<+>) = (+)
53 (<+>) = (+)
@@ -65,30 +69,46 @@ RingWithUnity Double where
65Field Double where
69Field Double where
66 inverseM f _ = 1 / f
70 inverseM f _ = 1 / f
67
71
72+-- Nat
68
73
69−Semigroup Nat where
74+[PlusNatSemi] Semigroup Nat where
70 (<+>) = (+)
75 (<+>) = (+)
71
76
72−Monoid Nat where
77+[PlusNatMonoid] Monoid Nat using PlusNatSemi where
73 neutral = 0
78 neutral = 0
74
79
80+[MultNatSemi] Semigroup Nat where
81+ (<+>) = (*)
82+
83+[MultNatMonoid] Monoid Nat using MultNatSemi where
84+ neutral = 1
85+
86+-- ZZ
87+
75−Semigroup ZZ where
88+[PlusZZSemi] Semigroup ZZ where
76 (<+>) = (+)
89 (<+>) = (+)
77
90
78−Monoid ZZ where
91+[PlusZZMonoid] Monoid ZZ using PlusZZSemi where
79 neutral = 0
92 neutral = 0
80
93
81−Group ZZ where
94+Group ZZ using PlusZZMonoid where
82 inverse = (* -1)
95 inverse = (* -1)
83
96
84AbelianGroup ZZ where
97AbelianGroup ZZ where
85
98
99+[MultZZSemi] Semigroup ZZ where
100+ (<+>) = (*)
101+
102+[MultZZMonoid] Monoid ZZ using MultZZSemi where
103+ neutral = 1
104+
86Ring ZZ where
105Ring ZZ where
87 (<.>) = (*)
106 (<.>) = (*)
88
107
89RingWithUnity ZZ where
108RingWithUnity ZZ where
90 unity = 1
109 unity = 1
91
110
111+-- Complex
92
112
93Semigroup a => Semigroup (Complex a) where
113Semigroup a => Semigroup (Complex a) where
94 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
114 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
libs/contrib/Interfaces/Verified.idr+107−8
@@ -2,7 +2,9 @@ module Interfaces.Verified
2
2
3import Control.Algebra
3import Control.Algebra
4import Control.Algebra.Lattice
4import Control.Algebra.Lattice
5+import Control.Algebra.NumericImplementations
5import Control.Algebra.VectorSpace
6import Control.Algebra.VectorSpace
7+import Data.ZZ
6
8
7%access public export
9%access public export
8
10
@@ -19,6 +21,14 @@ interface Functor f => VerifiedFunctor (f : Type -> Type) where
19 (g1 : a -> b) -> (g2 : b -> c) ->
21 (g1 : a -> b) -> (g2 : b -> c) ->
20 map (g2 . g1) x = (map g2 . map g1) x
22 map (g2 . g1) x = (map g2 . map g1) x
21
23
24+-- TODO VerifiedFunctor instances for: List, Stream, Either e
25+
26+VerifiedFunctor Maybe where
27+ functorIdentity Nothing = Refl
28+ functorIdentity (Just x) = Refl
29+ functorComposition Nothing g1 g2 = Refl
30+ functorComposition (Just x) g1 g2 = Refl
31+
22interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
32interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
23 applicativeMap : (x : f a) -> (g : a -> b) ->
33 applicativeMap : (x : f a) -> (g : a -> b) ->
24 map g x = pure g <*> x
34 map g x = pure g <*> x
@@ -30,6 +40,25 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
40 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
31 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
41 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
32
42
43+VerifiedApplicative Maybe where
44+ applicativeMap Nothing g = Refl
45+ applicativeMap (Just x) g = Refl
46+ applicativeIdentity Nothing = Refl
47+ applicativeIdentity (Just x) = Refl
48+ applicativeComposition Nothing Nothing Nothing = Refl
49+ applicativeComposition Nothing Nothing (Just x) = Refl
50+ applicativeComposition Nothing (Just x) Nothing = Refl
51+ applicativeComposition Nothing (Just x) (Just y) = Refl
52+ applicativeComposition (Just x) Nothing Nothing = Refl
53+ applicativeComposition (Just x) Nothing (Just y) = Refl
54+ applicativeComposition (Just x) (Just y) Nothing = Refl
55+ applicativeComposition (Just x) (Just y) (Just z) = Refl
56+ applicativeHomomorphism x g = Refl
57+ applicativeInterchange x Nothing = Refl
58+ applicativeInterchange x (Just y) = Refl
59+
60+-- TODO VerifiedApplicative instances for: List, Stream, Either e
61+
33interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
62interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
34 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
63 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
35 mf <*> mx = mf >>= \f =>
64 mf <*> mx = mf >>= \f =>
@@ -40,6 +69,19 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
40 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
69 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
41 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
70 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
42
71
72+-- The believe_me is there because idris won't seem to unify (pure x = Just x) with Refl
73+VerifiedMonad Maybe where
74+ monadApplicative Nothing Nothing = Refl
75+ monadApplicative Nothing (Just x) = Refl
76+ monadApplicative (Just x) Nothing = Refl
77+ monadApplicative (Just x) (Just y) = Refl
78+ monadLeftIdentity x f = Refl
79+ monadRightIdentity Nothing = Refl
80+ monadRightIdentity (Just x) = (believe_me (Refl {A = Maybe a} {x = Just x}))
81+ monadAssociativity Nothing f g = Refl
82+ monadAssociativity (Just x) f g = Refl
83+
84+-- TODO VerifiedMonad instances for: List, Stream, Either e
43
85
44interface Semigroup a => VerifiedSemigroup a where
86interface Semigroup a => VerifiedSemigroup a where
45 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
87 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
@@ -47,42 +89,99 @@ interface Semigroup a => VerifiedSemigroup a where
47implementation VerifiedSemigroup (List a) where
89implementation VerifiedSemigroup (List a) where
48 semigroupOpIsAssociative = appendAssociative
90 semigroupOpIsAssociative = appendAssociative
49
91
50−--implementation VerifiedSemigroup Nat where
92+[PlusNatSemiV] VerifiedSemigroup Nat using PlusNatSemi where
51−-- semigroupOpIsAssociative = plusAssociative
93+ semigroupOpIsAssociative = plusAssociative
52
94
95+[MultNatSemiV] VerifiedSemigroup Nat using MultNatSemi where
96+ semigroupOpIsAssociative = multAssociative
97+
98+[PlusZZSemiV] VerifiedSemigroup ZZ using PlusZZSemi where
99+ semigroupOpIsAssociative = plusAssociativeZ
100+
101+[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
102+ semigroupOpIsAssociative = multAssociativeZ
103+
104+-- TODO Verified versions of...
105+-- (Semigroup m, Semigroup n) => Semigroup (m, n) where
106+-- (a, b) <+> (c, d) = (a <+> c, b <+> d)
107+--
108+-- Semigroup (Maybe a)
109+--
110+-- [collectJust] Semigroup a => Semigroup (Maybe a)
111+--
112+-- libs/base/Data/Morphisms.idr: implementation Monoid (Endomorphism a)
53
113
54interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
114interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
55 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
115 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
56 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
116 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
57
117
58−-- implementation VerifiedMonoid Nat where
118+[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
59−-- monoidNeutralIsNeutralL = plusZeroRightNeutral
119+ monoidNeutralIsNeutralL = plusZeroRightNeutral
60−-- monoidNeutralIsNeutralR = plusZeroLeftNeutral
120+ monoidNeutralIsNeutralR = plusZeroLeftNeutral
121+
122+[MultNatMonoidV] VerifiedMonoid Nat using MultNatSemiV, MultNatMonoid where
123+ monoidNeutralIsNeutralL = multOneRightNeutral
124+ monoidNeutralIsNeutralR = multOneLeftNeutral
125+
126+[PlusZZMonoidV] VerifiedMonoid ZZ using PlusZZSemiV, PlusZZMonoid where
127+ monoidNeutralIsNeutralL = plusZeroRightNeutralZ
128+ monoidNeutralIsNeutralR = plusZeroLeftNeutralZ
129+
130+[MultZZMonoidV] VerifiedMonoid ZZ using MultZZSemiV, MultZZMonoid where
131+ monoidNeutralIsNeutralL = multOneRightNeutralZ
132+ monoidNeutralIsNeutralR = multOneLeftNeutralZ
61
133
62implementation VerifiedMonoid (List a) where
134implementation VerifiedMonoid (List a) where
63 monoidNeutralIsNeutralL = appendNilRightNeutral
135 monoidNeutralIsNeutralL = appendNilRightNeutral
64 monoidNeutralIsNeutralR xs = Refl
136 monoidNeutralIsNeutralR xs = Refl
65
137
138+-- TODO Verified versions of...
139+-- (Monoid m, Monoid n) => Monoid (m, n) where
140+-- neutral = (neutral, neutral)
141+--
142+-- Monoid (Maybe a)
143+
66interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
144interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
67 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
145 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
68 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
146 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
69
147
148+VerifiedGroup ZZ using PlusZZMonoidV where
149+ groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
150+ rewrite multNegLeftZ 0 k in
151+ rewrite multOneLeftNeutralZ k in
152+ plusNegateInverseLZ k
153+ groupInverseIsInverseR k = rewrite sym $ multCommutativeZ (NegS 0) k in
154+ rewrite multNegLeftZ 0 k in
155+ rewrite multOneLeftNeutralZ k in
156+ plusNegateInverseRZ k
157+
70interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
158interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
71 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
159 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
72
160
161+VerifiedAbelianGroup ZZ where
162+ abelianGroupOpIsCommutative = plusCommutativeZ
163+
73interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
164interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
74 total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
165 total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
75 total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
166 total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
76 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
167 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
77
168
169+VerifiedRing ZZ where
170+ ringOpIsAssociative = multAssociativeZ
171+ ringOpIsDistributiveL = multDistributesOverPlusRightZ
172+ ringOpIsDistributiveR = multDistributesOverPlusLeftZ
173+
78interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
174interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
79 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
175 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
80 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
176 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
81
177
82−--interface (VerifiedRingWithUnity a, Field a) => VerifiedField a where
178+VerifiedRingWithUnity ZZ where
83−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity
179+ ringWithUnityIsUnityL = multOneRightNeutralZ
84−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity
180+ ringWithUnityIsUnityR = multOneLeftNeutralZ
85
181
182+--interface (VerifiedRingWithUnity a, Field a) => VerifiedField a where
183+-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = Algebra.neutral)) -> l <.> (inverseM l notId) = Algebra.unity
184+-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = Algebra.neutral)) -> (inverseM r notId) <.> r = Algebra.unity
86
185
87interface JoinSemilattice a => VerifiedJoinSemilattice a where
186interface JoinSemilattice a => VerifiedJoinSemilattice a where
88 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
187 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r