@@ -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,12 @@ 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+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+
2230interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
2331 applicativeMap : (x : f a) -> (g : a -> b) ->
2432 map g x = pure g <*> x
@@ -30,6 +38,23 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
3038 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
3139 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
3240
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+
3358interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
3459 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
3560 mf <*> mx = mf >>= \f =>
@@ -40,6 +65,16 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
4065 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
4166 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
4267
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
4378
4479interface Semigroup a => VerifiedSemigroup a where
4580 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
@@ -47,17 +82,37 @@ interface Semigroup a => VerifiedSemigroup a where
4782implementation VerifiedSemigroup (List a) where
4883 semigroupOpIsAssociative = appendAssociative
4984
50−--implementation VerifiedSemigroup Nat where
51−-- semigroupOpIsAssociative = plusAssociative
85+[PlusNatSemiV] VerifiedSemigroup Nat using PlusNatSemi where
86+ semigroupOpIsAssociative = plusAssociative
87+
88+[MultNatSemiV] VerifiedSemigroup Nat using MultNatSemi where
89+ semigroupOpIsAssociative = multAssociative
5290
91+[PlusZZSemiV] VerifiedSemigroup ZZ using PlusZZSemi where
92+ semigroupOpIsAssociative = plusAssociativeZ
93+
94+[MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where
95+ semigroupOpIsAssociative = multAssociativeZ
5396
5497interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
5598 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l
5699 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r
57100
58−-- implementation VerifiedMonoid Nat where
59−-- monoidNeutralIsNeutralL = plusZeroRightNeutral
60−-- monoidNeutralIsNeutralR = plusZeroLeftNeutral
101+[PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where
102+ monoidNeutralIsNeutralL = plusZeroRightNeutral
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
61116
62117implementation VerifiedMonoid (List a) where
63118 monoidNeutralIsNeutralL = appendNilRightNeutral
@@ -67,22 +122,39 @@ interface (VerifiedMonoid a, Group a) => VerifiedGroup a where
67122 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral
68123 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral
69124
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+
70135interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
71136 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
72137
138+VerifiedAbelianGroup ZZ where
139+ abelianGroupOpIsCommutative = plusCommutativeZ
140+
73141interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
74142 total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r
75143 total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)
76144 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)
77145
146+VerifiedRing ZZ where
147+ ringOpIsAssociative = multAssociativeZ
148+ ringOpIsDistributiveL = multDistributesOverPlusRightZ
149+ ringOpIsDistributiveR = multDistributesOverPlusLeftZ
150+
78151interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
79152 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l
80153 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r
81154
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
85−
155+VerifiedRingWithUnity ZZ where
156+ ringWithUnityIsUnityL = multOneRightNeutralZ
157+ ringWithUnityIsUnityR = multOneLeftNeutralZ
86158
87159interface JoinSemilattice a => VerifiedJoinSemilattice a where
88160 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
93165 total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
94166 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
95167 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−-}