git.iko.soy/Idris-dev
on master help sign in
Add implementation of `VerifiedSemigroup Nat`, and others along the same lines, all in contrib.

New interfaces and implementations in contrib, building up the coverage of `Verified` implementations which provide proof terms to witness that the base instance obeys the appropriate laws. Includes a back-compatibility breakage - demotion of the instance of `Semigroup Nat` into a named instance. Example: `VerifiedSemigroup Nat` contains a witness for associativity of the operation defined in `Semigroup Nat`. - New implementations of algebraic interfaces for numeric types, for example SemiGroup for multiplication on Nat (as well as addition). ZZ now has the whole numeric tower covered up to `RingWithUnity` - ditto Nat where appropriate. - All these instances now have `Verified` counterparts as well (libs/contrib/Interfaces/Verified.idr), for example the instance `[PlusNatSemiV] VerifiedSemigroup Nat` extends `[PlusNatSemi] Semigroup Nat` with a member that is a proof term `semigroupOpIsAssociative`. - Some non-numeric `Verified` interfaces and instances are added too - for example `VerifiedFunctor Maybe`. There are TODO placeholders for extending coverage further (`VerifiedFunctor List` for example). - Back-compatibility break in contrib: in libs/contrib/Control/Algebra/NumericImplementations.idr, the `Semigroup Nat` instance is demoted into a named instance called `PlusNatSemi`. This puts it on a par with the new `MultNatSemi`. Similarly `Monoid Nat`, `SemiGroup ZZ` and `Monoid ZZ`.

commit64903567c314842407bb06ddb58d2ede55e02049 authorChris Gibbs <atacratic@users.noreply.github.com> dateSun 30 Apr 2017, 01:40 (9 years ago) parente371823
2 files changed+133−14
compare with master
unifiedsplit
libs/contrib/Control/Algebra/NumericImplementations.idr+26−6 libs/contrib/Interfaces/Verified.idr+107−8
libs/contrib/Control/Algebra/NumericImplementations.idr+26−6
@@ -9,6 +9,8 @@ import Data.ZZ
99
1010%access public export
1111
12+-- Integer
13+
1214Semigroup Integer where
1315 (<+>) = (+)
1416
@@ -18,7 +20,7 @@ Monoid Integer where
1820Group Integer where
1921 inverse = (* -1)
2022
21−AbelianGroup Integer where
23+AbelianGroup Integer where
2224
2325Ring Integer where
2426 (<.>) = (*)
@@ -26,6 +28,7 @@ Ring Integer where
2628RingWithUnity Integer where
2729 unity = 1
2830
31+-- Int
2932
3033Semigroup Int where
3134 (<+>) = (+)
@@ -44,6 +47,7 @@ Ring Int where
4447RingWithUnity Int where
4548 unity = 1
4649
50+-- Double
4751
4852Semigroup Double where
4953 (<+>) = (+)
@@ -65,30 +69,46 @@ RingWithUnity Double where
6569Field Double where
6670 inverseM f _ = 1 / f
6771
72+-- Nat
6873
69−Semigroup Nat where
74+[PlusNatSemi] Semigroup Nat where
7075 (<+>) = (+)
7176
72−Monoid Nat where
77+[PlusNatMonoid] Monoid Nat using PlusNatSemi where
7378 neutral = 0
7479
75−Semigroup ZZ where
80+[MultNatSemi] Semigroup Nat where
81+ (<+>) = (*)
82+
83+[MultNatMonoid] Monoid Nat using MultNatSemi where
84+ neutral = 1
85+
86+-- ZZ
87+
88+[PlusZZSemi] Semigroup ZZ where
7689 (<+>) = (+)
7790
78−Monoid ZZ where
91+[PlusZZMonoid] Monoid ZZ using PlusZZSemi where
7992 neutral = 0
8093
81−Group ZZ where
94+Group ZZ using PlusZZMonoid where
8295 inverse = (* -1)
8396
8497AbelianGroup ZZ where
8598
99+[MultZZSemi] Semigroup ZZ where
100+ (<+>) = (*)
101+
102+[MultZZMonoid] Monoid ZZ using MultZZSemi where
103+ neutral = 1
104+
86105Ring ZZ where
87106 (<.>) = (*)
88107
89108RingWithUnity ZZ where
90109 unity = 1
91110
111+-- Complex
92112
93113Semigroup a => Semigroup (Complex a) where
94114 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)
libs/contrib/Interfaces/Verified.idr+107−8
@@ -2,7 +2,9 @@ module Interfaces.Verified
22
33import Control.Algebra
44import Control.Algebra.Lattice
5+import Control.Algebra.NumericImplementations
56import Control.Algebra.VectorSpace
7+import Data.ZZ
68
79%access public export
810
@@ -19,6 +21,14 @@ interface Functor f => VerifiedFunctor (f : Type -> Type) where
1921 (g1 : a -> b) -> (g2 : b -> c) ->
2022 map (g2 . g1) x = (map g2 . map g1) x
2123
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+
2232interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
2333 applicativeMap : (x : f a) -> (g : a -> b) ->
2434 map g x = pure g <*> x
@@ -30,6 +40,25 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
3040 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
3141 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
3242
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+
3362interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
3463 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
3564 mf <*> mx = mf >>= \f =>
@@ -40,6 +69,19 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
4069 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
4170 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
4271
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
4385
4486interface Semigroup a => VerifiedSemigroup a where
4587 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
@@ -47,42 +89,99 @@ interface Semigroup a => VerifiedSemigroup a where
4789implementation VerifiedSemigroup (List a) where
4890 semigroupOpIsAssociative = appendAssociative
4991
50−--implementation VerifiedSemigroup Nat where
51−-- semigroupOpIsAssociative = plusAssociative
92+[PlusNatSemiV] VerifiedSemigroup Nat using PlusNatSemi where
93+ semigroupOpIsAssociative = plusAssociative
5294
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)
53113
54114interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
55115 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
56116 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
57117
58−-- implementation VerifiedMonoid Nat where
59−-- monoidNeutralIsNeutralL = plusZeroRightNeutral
60−-- monoidNeutralIsNeutralR = plusZeroLeftNeutral
118+[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
119+ monoidNeutralIsNeutralL = plusZeroRightNeutral
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
61133
62134implementation VerifiedMonoid (List a) where
63135 monoidNeutralIsNeutralL = appendNilRightNeutral
64136 monoidNeutralIsNeutralR xs = Refl
65137
138+-- TODO Verified versions of...
139+-- (Monoid m, Monoid n) => Monoid (m, n) where
140+-- neutral = (neutral, neutral)
141+--
142+-- Monoid (Maybe a)
143+
66144interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
67145 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
68146 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
69147
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+
70158interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
71159 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
72160
161+VerifiedAbelianGroup ZZ where
162+ abelianGroupOpIsCommutative = plusCommutativeZ
163+
73164interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
74165 total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
75166 total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
76167 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
77168
169+VerifiedRing ZZ where
170+ ringOpIsAssociative = multAssociativeZ
171+ ringOpIsDistributiveL = multDistributesOverPlusRightZ
172+ ringOpIsDistributiveR = multDistributesOverPlusLeftZ
173+
78174interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
79175 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
80176 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
81177
82−--interface (VerifiedRingWithUnity a, Field a) => VerifiedField a where
83−-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity
84−-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity
178+VerifiedRingWithUnity ZZ where
179+ ringWithUnityIsUnityL = multOneRightNeutralZ
180+ ringWithUnityIsUnityR = multOneLeftNeutralZ
85181
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
86185
87186interface JoinSemilattice a => VerifiedJoinSemilattice a where
88187 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r