@@ -30,12 +30,24 @@ VerifiedFunctor (Pair a) where
3030 functorIdentity g p (a,b) = rewrite p b in Refl
3131 functorComposition (a,b) g1 g2 = Refl
3232
33+VerifiedFunctor (Either a) where
34+ functorIdentity _ _ (Left _) = Refl
35+ functorIdentity _ p (Right x) = cong (p x)
36+ functorComposition (Left _) _ _ = Refl
37+ functorComposition (Right _) _ _ = Refl
38+
3339VerifiedFunctor Maybe where
3440 functorIdentity _ _ Nothing = Refl
3541 functorIdentity g p (Just x) = rewrite p x in Refl
3642 functorComposition Nothing g1 g2 = Refl
3743 functorComposition (Just x) g1 g2 = Refl
3844
45+VerifiedFunctor List where
46+ functorIdentity _ _ [] = Refl
47+ functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
48+ functorComposition [] _ _ = Refl
49+ functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl
50+
3951VerifiedFunctor (Vect n) where
4052 functorIdentity _ _ [] = Refl
4153 functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
@@ -53,6 +65,75 @@ interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type ->
5365 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
5466 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
5567
68+VerifiedApplicative (Either a) where
69+ applicativeMap (Left x) g = Refl
70+ applicativeMap (Right x) g = Refl
71+ applicativeIdentity (Left x) = Refl
72+ applicativeIdentity (Right x) = Refl
73+ applicativeComposition (Left x) (Left y) (Left z) = Refl
74+ applicativeComposition (Left x) (Left y) (Right z) = Refl
75+ applicativeComposition (Left x) (Right y) (Left z) = Refl
76+ applicativeComposition (Left x) (Right y) (Right z) = Refl
77+ applicativeComposition (Right x) (Left y) (Left z) = Refl
78+ applicativeComposition (Right x) (Left y) (Right z) = Refl
79+ applicativeComposition (Right x) (Right y) (Left z) = Refl
80+ applicativeComposition (Right x) (Right y) (Right z) = Refl
81+ applicativeHomomorphism x g = Refl
82+ applicativeInterchange x (Left y) = Refl
83+ applicativeInterchange x (Right y) = Refl
84+
85+private
86+foldrConcatEq : (g1 : List (a -> b)) -> (g2 : List (a -> b)) ->
87+ (xs : List a) ->
88+ foldr (\f, meth => map f xs ++ meth) [] (g1 ++ g2) = foldr (\f, meth => map f xs ++ meth) [] g1 ++ foldr (\f, meth => map f xs ++ meth) [] g2
89+foldrConcatEq [] _ _ = Refl
90+foldrConcatEq (g1 :: gs1) gs2 xs =
91+ trans
92+ (cong $ foldrConcatEq gs1 gs2 xs)
93+ (appendAssociative
94+ (map g1 xs)
95+ (foldr (\f, meth => map f xs ++ meth) [] gs1)
96+ (foldr (\f, meth => map f xs ++ meth) [] gs2))
97+
98+private
99+foldrConcatEq' : (x1 : List a) -> (x2 : List a) ->
100+ (g : a -> List b) ->
101+ foldr (\x, meth => g x ++ meth) [] (x1 ++ x2) = foldr (\x, meth => g x ++ meth) [] x1 ++ foldr (\x, meth => g x ++ meth) [] x2
102+foldrConcatEq' [] _ _ = Refl
103+foldrConcatEq' (x1 :: xs1) xs2 g =
104+ trans
105+ (cong {f=((++) $ g x1)} $ foldrConcatEq' xs1 xs2 g)
106+ (appendAssociative
107+ (g x1)
108+ (foldr (\x, meth => g x ++ meth) [] xs1)
109+ (foldr (\x, meth => g x ++ meth) [] xs2))
110+
111+private
112+foldrMapCombine : (xs : List a) -> (gs1 : List (a -> b)) -> (g2 : b -> c) ->
113+ map g2 (foldr (\g, meth => map g xs ++ meth) [] gs1) =
114+ foldr (\g, meth => map g xs ++ meth) [] (map ((.) g2) gs1)
115+foldrMapCombine xs [] g2 = Refl
116+foldrMapCombine xs (g1 :: gs1) g2 =
117+ trans
118+ (mapAppendDistributive g2 (map g1 xs) (foldr (\g, meth => map g xs ++ meth) [] gs1))
119+ (appendCong2 (sym $ functorComposition xs g1 g2) (foldrMapCombine xs gs1 g2))
120+
121+VerifiedApplicative List where
122+ applicativeMap [] f = Refl
123+ applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
124+ applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs
125+ applicativeComposition _ _ [] = Refl
126+ applicativeComposition xs gs1 (g2 :: gs2) = trans
127+ (trans
128+ (foldrConcatEq (map ((.) g2) gs1) (foldr (\g, meth => map g gs1 ++ meth) [] (map (.) gs2 ++ [])) xs)
129+ (cong $ applicativeComposition xs gs1 gs2))
130+ (sym $
131+ cong {f=(++ foldr (\g, meth => map g (foldr (\g', meth' => map g' xs ++ meth') [] gs1) ++ meth) [] gs2)} $
132+ foldrMapCombine xs gs1 g2)
133+ applicativeHomomorphism x g = Refl
134+ applicativeInterchange x [] = Refl
135+ applicativeInterchange x (g :: gs) = cong $ applicativeInterchange x gs
136+
56137VerifiedApplicative (Vect n) where
57138 applicativeMap [] f = Refl
58139 applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
@@ -95,16 +176,43 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
95176 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
96177 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
97178
179+VerifiedMonad (Either a) where
180+ monadApplicative (Left x) (Left y) = Refl
181+ monadApplicative (Left x) (Right y) = Refl
182+ monadApplicative (Right x) (Left y) = Refl
183+ monadApplicative (Right x) (Right y) = Refl
184+ monadLeftIdentity x f = Refl
185+ monadRightIdentity (Left x) = Refl
186+ monadRightIdentity (Right x) = Refl
187+ monadAssociativity (Left x) f g = Refl
188+ monadAssociativity (Right x) f g = Refl
189+
98190VerifiedMonad Maybe where
99− monadApplicative Nothing Nothing = Refl
100− monadApplicative Nothing (Just x) = Refl
101− monadApplicative (Just x) Nothing = Refl
102− monadApplicative (Just x) (Just y) = Refl
103− monadLeftIdentity x f = Refl
104− monadRightIdentity Nothing = Refl
105− monadRightIdentity (Just x) = Refl
106− monadAssociativity Nothing f g = Refl
107− monadAssociativity (Just x) f g = Refl
191+ monadApplicative Nothing Nothing = Refl
192+ monadApplicative Nothing (Just x) = Refl
193+ monadApplicative (Just x) Nothing = Refl
194+ monadApplicative (Just x) (Just y) = Refl
195+ monadLeftIdentity x f = Refl
196+ monadRightIdentity Nothing = Refl
197+ monadRightIdentity (Just x) = Refl
198+ monadAssociativity Nothing f g = Refl
199+ monadAssociativity (Just x) f g = Refl
200+
201+VerifiedMonad List where
202+ monadApplicative [] _ = Refl
203+ monadApplicative (x :: xs) [] = Refl
204+ monadApplicative (g :: gs) xs = appendCong2 (mapFoldrEq g xs) (monadApplicative gs xs) where
205+ mapFoldrEq : (f : a -> b) -> (x : List a) -> map f x = foldr (\x1, meth => f x1 :: meth) [] x
206+ mapFoldrEq _ [] = Refl
207+ mapFoldrEq f (_ :: x) = cong $ mapFoldrEq f x
208+ monadLeftIdentity x f = appendNilRightNeutral (f x)
209+ monadRightIdentity [] = Refl
210+ monadRightIdentity (x :: xs) = cong $ monadRightIdentity xs
211+ monadAssociativity [] _ _ = Refl
212+ monadAssociativity (x :: xs) g1 g2 =
213+ trans
214+ (foldrConcatEq' (g1 x) (foldr (\x1, meth => g1 x1 ++ meth) [] xs) g2)
215+ (cong $ monadAssociativity xs g1 g2)
108216
109217interface Semigroup a => VerifiedSemigroup a where
110218 semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r