git.iko.soy/Idris-dev
on master help sign in
Merge pull request #4565 from stop-cran/master
bae730aNiklas Larsson
libs/contrib/Interfaces/Verified.idr+135−9
compare with master
unifiedsplit
@@ -30,12 +30,24 @@ VerifiedFunctor (Pair a) where
30 functorIdentity g p (a,b) = rewrite p b in Refl
30 functorIdentity g p (a,b) = rewrite p b in Refl
31 functorComposition (a,b) g1 g2 = Refl
31 functorComposition (a,b) g1 g2 = Refl
32
32
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+
33VerifiedFunctor Maybe where
39VerifiedFunctor Maybe where
34 functorIdentity _ _ Nothing = Refl
40 functorIdentity _ _ Nothing = Refl
35 functorIdentity g p (Just x) = rewrite p x in Refl
41 functorIdentity g p (Just x) = rewrite p x in Refl
36 functorComposition Nothing g1 g2 = Refl
42 functorComposition Nothing g1 g2 = Refl
37 functorComposition (Just x) g1 g2 = Refl
43 functorComposition (Just x) g1 g2 = Refl
38
44
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+
39VerifiedFunctor (Vect n) where
51VerifiedFunctor (Vect n) where
40 functorIdentity _ _ [] = Refl
52 functorIdentity _ _ [] = Refl
41 functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs)
53 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 ->
53 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
65 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
54 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
66 g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g
55
67
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+
56VerifiedApplicative (Vect n) where
137VerifiedApplicative (Vect n) where
57 applicativeMap [] f = Refl
138 applicativeMap [] f = Refl
58 applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
139 applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl
@@ -95,16 +176,61 @@ interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) w
95 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
176 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
96 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
177 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
97
178
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+
98VerifiedMonad Maybe where
190VerifiedMonad Maybe where
99− monadApplicative Nothing Nothing = Refl
191+ monadApplicative Nothing Nothing = Refl
100− monadApplicative Nothing (Just x) = Refl
192+ monadApplicative Nothing (Just x) = Refl
101− monadApplicative (Just x) Nothing = Refl
193+ monadApplicative (Just x) Nothing = Refl
102− monadApplicative (Just x) (Just y) = Refl
194+ monadApplicative (Just x) (Just y) = Refl
103− monadLeftIdentity x f = Refl
195+ monadLeftIdentity x f = Refl
104− monadRightIdentity Nothing = Refl
196+ monadRightIdentity Nothing = Refl
105− monadRightIdentity (Just x) = Refl
197+ monadRightIdentity (Just x) = Refl
106− monadAssociativity Nothing f g = Refl
198+ monadAssociativity Nothing f g = Refl
107− monadAssociativity (Just x) 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)
216+
217+interface (Alternative f, VerifiedApplicative f) => VerifiedAlternative (f : Type -> Type) where
218+ alternativeLeftIdentity : (x : f a) -> Applicative.empty <|> x = x
219+ alternativeRightIdentity : (x : f a) -> x <|> Applicative.empty = x
220+ alternativeAssociativity : (x : f a) -> (y : f a) -> (z : f a) ->
221+ x <|> (y <|> z) = (x <|> y) <|> z
222+
223+VerifiedAlternative Maybe where
224+ alternativeLeftIdentity _ = Refl
225+ alternativeRightIdentity Nothing = Refl
226+ alternativeRightIdentity (Just _) = Refl
227+ alternativeAssociativity Nothing _ _ = Refl
228+ alternativeAssociativity (Just _) _ _ = Refl
229+
230+VerifiedAlternative List where
231+ alternativeLeftIdentity _ = Refl
232+ alternativeRightIdentity = appendNilRightNeutral
233+ alternativeAssociativity = appendAssociative
108
234
109interface Semigroup a => VerifiedSemigroup a where
235interface Semigroup a => VerifiedSemigroup a where
110 semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
236 semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
libs/prelude/Prelude/List.idr+25−1
@@ -862,9 +862,33 @@ catMaybes (x::xs) =
862--------------------------------------------------------------------------------
862--------------------------------------------------------------------------------
863
863
864||| (::) is injective
864||| (::) is injective
865+consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
865−consInjective : (x :: xs) = (y :: ys) -> (x = y, xs = ys)
866+ (x :: xs) = (y :: ys) -> (x = y, xs = ys)
866consInjective Refl = (Refl, Refl)
867consInjective Refl = (Refl, Refl)
867
868
869+||| Two lists are equal, if their heads are equal and their tails are equal.
870+consCong2 : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
871+ x = y -> xs = ys -> x :: xs = y :: ys
872+consCong2 Refl Refl = Refl
873+
874+||| Appending pairwise equal lists gives equal lists
875+appendCong2 : {x1 : List a} -> {x2 : List a} ->
876+ {y1 : List b} -> {y2 : List b} ->
877+ x1 = y1 -> x2 = y2 -> x1 ++ x2 = y1 ++ y2
878+appendCong2 {x1=[]} {y1=(_ :: _)} Refl _ impossible
879+appendCong2 {x1=(_ :: _)} {y1=[]} Refl _ impossible
880+appendCong2 {x1=[]} {y1=[]} _ eq2 = eq2
881+appendCong2 {x1=(_ :: _)} {y1=(_ :: _)} eq1 eq2 =
882+ consCong2
883+ (fst $ consInjective eq1)
884+ (appendCong2 (snd $ consInjective eq1) eq2)
885+
886+||| List.map is distributive over appending.
887+mapAppendDistributive : (f : a -> b) -> (x : List a) -> (y : List a) ->
888+ map f (x ++ y) = map f x ++ map f y
889+mapAppendDistributive _ [] _ = Refl
890+mapAppendDistributive f (_ :: xs) y = cong $ mapAppendDistributive f xs y
891+
868||| The empty list is a right identity for append.
892||| The empty list is a right identity for append.
869appendNilRightNeutral : (l : List a) ->
893appendNilRightNeutral : (l : List a) ->
870 l ++ [] = l
894 l ++ [] = l