git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3790 from atacratic/VerifiedImpls
391e012Ahmad Salim Al-Sibahi
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+81−37
@@ -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,12 @@ 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+VerifiedFunctor Maybe where
25+ functorIdentity Nothing = Refl
26+ functorIdentity (Just x) = Refl
27+ functorComposition Nothing g1 g2 = Refl
28+ functorComposition (Just x) g1 g2 = Refl
29+
22interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
30interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
23 applicativeMap : (x : f a) -> (g : a -> b) ->
31 applicativeMap : (x : f a) -> (g : a -> b) ->
24 map g x = pure g <*> x
32 map g x = pure g <*> x
@@ -30,6 +38,23 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
30 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
38 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
31 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
39 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
32
40
41+VerifiedApplicative Maybe where
42+ applicativeMap Nothing g = Refl
43+ applicativeMap (Just x) g = Refl
44+ applicativeIdentity Nothing = Refl
45+ applicativeIdentity (Just x) = Refl
46+ applicativeComposition Nothing Nothing Nothing = Refl
47+ applicativeComposition Nothing Nothing (Just x) = Refl
48+ applicativeComposition Nothing (Just x) Nothing = Refl
49+ applicativeComposition Nothing (Just x) (Just y) = Refl
50+ applicativeComposition (Just x) Nothing Nothing = Refl
51+ applicativeComposition (Just x) Nothing (Just y) = Refl
52+ applicativeComposition (Just x) (Just y) Nothing = Refl
53+ applicativeComposition (Just x) (Just y) (Just z) = Refl
54+ applicativeHomomorphism x g = Refl
55+ applicativeInterchange x Nothing = Refl
56+ applicativeInterchange x (Just y) = Refl
57+
33interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
58interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
34 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
59 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
35 mf <*> mx = mf >>= \f =>
60 mf <*> mx = mf >>= \f =>
@@ -40,6 +65,16 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
40 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
65 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
41 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
66 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
42
67
68+VerifiedMonad Maybe where
69+ monadApplicative Nothing Nothing = Refl
70+ monadApplicative Nothing (Just x) = Refl
71+ monadApplicative (Just x) Nothing = Refl
72+ monadApplicative (Just x) (Just y) = Refl
73+ monadLeftIdentity x f = Refl
74+ monadRightIdentity Nothing = Refl
75+ monadRightIdentity (Just x) = Refl
76+ monadAssociativity Nothing f g = Refl
77+ monadAssociativity (Just x) f g = Refl
43
78
44interface Semigroup a => VerifiedSemigroup a where
79interface Semigroup a => VerifiedSemigroup a where
45 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
80 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
@@ -47,17 +82,37 @@ interface Semigroup a => VerifiedSemigroup a where
47implementation VerifiedSemigroup (List a) where
82implementation VerifiedSemigroup (List a) where
48 semigroupOpIsAssociative = appendAssociative
83 semigroupOpIsAssociative = appendAssociative
49
84
50−--implementation VerifiedSemigroup Nat where
85+[PlusNatSemiV] VerifiedSemigroup Nat using PlusNatSemi where
51−-- semigroupOpIsAssociative = plusAssociative
86+ semigroupOpIsAssociative = plusAssociative
87+
88+[MultNatSemiV] VerifiedSemigroup Nat using MultNatSemi where
89+ semigroupOpIsAssociative = multAssociative
52
90
91+[PlusZZSemiV] VerifiedSemigroup ZZ using PlusZZSemi where
92+ semigroupOpIsAssociative = plusAssociativeZ
93+
94+[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
95+ semigroupOpIsAssociative = multAssociativeZ
53
96
54interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
97interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
55 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
98 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
56 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
99 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
57
100
58−-- implementation VerifiedMonoid Nat where
101+[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
59−-- monoidNeutralIsNeutralL = plusZeroRightNeutral
102+ monoidNeutralIsNeutralL = plusZeroRightNeutral
60−-- monoidNeutralIsNeutralR = plusZeroLeftNeutral
103+ monoidNeutralIsNeutralR = plusZeroLeftNeutral
104+
105+[MultNatMonoidV] VerifiedMonoid Nat using MultNatSemiV, MultNatMonoid where
106+ monoidNeutralIsNeutralL = multOneRightNeutral
107+ monoidNeutralIsNeutralR = multOneLeftNeutral
108+
109+[PlusZZMonoidV] VerifiedMonoid ZZ using PlusZZSemiV, PlusZZMonoid where
110+ monoidNeutralIsNeutralL = plusZeroRightNeutralZ
111+ monoidNeutralIsNeutralR = plusZeroLeftNeutralZ
112+
113+[MultZZMonoidV] VerifiedMonoid ZZ using MultZZSemiV, MultZZMonoid where
114+ monoidNeutralIsNeutralL = multOneRightNeutralZ
115+ monoidNeutralIsNeutralR = multOneLeftNeutralZ
61
116
62implementation VerifiedMonoid (List a) where
117implementation VerifiedMonoid (List a) where
63 monoidNeutralIsNeutralL = appendNilRightNeutral
118 monoidNeutralIsNeutralL = appendNilRightNeutral
@@ -67,22 +122,39 @@ interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
67 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
122 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
68 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
123 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
69
124
125+VerifiedGroup ZZ using PlusZZMonoidV where
126+ groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in
127+ rewrite multNegLeftZ 0 k in
128+ rewrite multOneLeftNeutralZ k in
129+ plusNegateInverseLZ k
130+ groupInverseIsInverseR k = rewrite sym $ multCommutativeZ (NegS 0) k in
131+ rewrite multNegLeftZ 0 k in
132+ rewrite multOneLeftNeutralZ k in
133+ plusNegateInverseRZ k
134+
70interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
135interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
71 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
136 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
72
137
138+VerifiedAbelianGroup ZZ where
139+ abelianGroupOpIsCommutative = plusCommutativeZ
140+
73interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
141interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
74 total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
142 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)
143 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)
144 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
77
145
146+VerifiedRing ZZ where
147+ ringOpIsAssociative = multAssociativeZ
148+ ringOpIsDistributiveL = multDistributesOverPlusRightZ
149+ ringOpIsDistributiveR = multDistributesOverPlusLeftZ
150+
78interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
151interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
79 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
152 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
80 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
153 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
81
154
82−--interface (VerifiedRingWithUnity a, Field a) => VerifiedField a where
155+VerifiedRingWithUnity ZZ where
83−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity
156+ ringWithUnityIsUnityL = multOneRightNeutralZ
84−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity
157+ ringWithUnityIsUnityR = multOneLeftNeutralZ
85−
86
158
87interface JoinSemilattice a => VerifiedJoinSemilattice a where
159interface JoinSemilattice a => VerifiedJoinSemilattice a where
88 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
160 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
@@ -93,31 +165,3 @@ interface MeetSemilattice a => VerifiedMeetSemilattice a where
93 total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
165 total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
94 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
166 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
95 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
167 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
96−
97−{- FIXME: Some maintenance required here.
98− Algebra.top and Algebra.bottom don't exist!
99−-}
100−{-
101−
102−interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
103− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e Algebra.bottom = e
104−
105−interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
106− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e Algebra.top = e
107−
108−interface (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
109− total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
110− total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
111−
112−interface (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
113−
114−
115−--interface (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
116−-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
117−-- total moduleScalarUnityIsUnity : (v : b) -> Algebra.unity {a} <#> v = v
118−-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
119−-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
120−
121−--interface (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
122−
123−-}