module Interfaces.Verified import Control.Algebra import Control.Algebra.Lattice import Control.Algebra.NumericImplementations import Control.Algebra.VectorSpace import Data.Vect import Data.ZZ %default total %access public export -- Due to these being basically unused and difficult to implement, -- they're in contrib for a bit. Once a design is found that lets them -- be implemented for a number of implementations, and we get those -- implementations, then some of them can move back to base (or even -- prelude, in the cases of Functor, Applicative, Monad, Semigroup, -- and Monoid). interface Functor f => VerifiedFunctor (f : Type -> Type) where functorIdentity : {a : Type} -> (g : a -> a) -> ((v : a) -> g v = v) -> (x : f a) -> map g x = x functorComposition : {a : Type} -> {b : Type} -> (x : f a) -> (g1 : a -> b) -> (g2 : b -> c) -> map (g2 . g1) x = (map g2 . map g1) x functorIdentity' : VerifiedFunctor f => (x : f a) -> map Basics.id x = x functorIdentity' {f} = functorIdentity {f} id (\x => Refl) VerifiedFunctor (Pair a) where functorIdentity g p (a,b) = rewrite p b in Refl functorComposition (a,b) g1 g2 = Refl VerifiedFunctor (Either a) where functorIdentity _ _ (Left _) = Refl functorIdentity _ p (Right x) = cong (p x) functorComposition (Left _) _ _ = Refl functorComposition (Right _) _ _ = Refl VerifiedFunctor Maybe where functorIdentity _ _ Nothing = Refl functorIdentity g p (Just x) = rewrite p x in Refl functorComposition Nothing g1 g2 = Refl functorComposition (Just x) g1 g2 = Refl VerifiedFunctor List where functorIdentity _ _ [] = Refl functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs) functorComposition [] _ _ = Refl functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl VerifiedFunctor (Vect n) where functorIdentity _ _ [] = Refl functorIdentity g p (x :: xs) = rewrite p x in cong (functorIdentity g p xs) functorComposition [] _ _ = Refl functorComposition (x :: xs) f g = rewrite functorComposition xs f g in Refl interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where applicativeMap : (x : f a) -> (g : a -> b) -> map g x = pure g <*> x applicativeIdentity : (x : f a) -> pure Basics.id <*> x = x applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) -> ((pure (.) <*> g2) <*> g1) <*> x = g2 <*> (g1 <*> x) applicativeHomomorphism : (x : a) -> (g : a -> b) -> (<*>) {f} (pure g) (pure x) = pure {f} (g x) applicativeInterchange : (x : a) -> (g : f (a -> b)) -> g <*> pure x = pure (\g' : (a -> b) => g' x) <*> g VerifiedApplicative (Either a) where applicativeMap (Left x) g = Refl applicativeMap (Right x) g = Refl applicativeIdentity (Left x) = Refl applicativeIdentity (Right x) = Refl applicativeComposition (Left x) (Left y) (Left z) = Refl applicativeComposition (Left x) (Left y) (Right z) = Refl applicativeComposition (Left x) (Right y) (Left z) = Refl applicativeComposition (Left x) (Right y) (Right z) = Refl applicativeComposition (Right x) (Left y) (Left z) = Refl applicativeComposition (Right x) (Left y) (Right z) = Refl applicativeComposition (Right x) (Right y) (Left z) = Refl applicativeComposition (Right x) (Right y) (Right z) = Refl applicativeHomomorphism x g = Refl applicativeInterchange x (Left y) = Refl applicativeInterchange x (Right y) = Refl private foldrConcatEq : (g1 : List (a -> b)) -> (g2 : List (a -> b)) -> (xs : List a) -> 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 foldrConcatEq [] _ _ = Refl foldrConcatEq (g1 :: gs1) gs2 xs = trans (cong $ foldrConcatEq gs1 gs2 xs) (appendAssociative (map g1 xs) (foldr (\f, meth => map f xs ++ meth) [] gs1) (foldr (\f, meth => map f xs ++ meth) [] gs2)) private foldrConcatEq' : (x1 : List a) -> (x2 : List a) -> (g : a -> List b) -> foldr (\x, meth => g x ++ meth) [] (x1 ++ x2) = foldr (\x, meth => g x ++ meth) [] x1 ++ foldr (\x, meth => g x ++ meth) [] x2 foldrConcatEq' [] _ _ = Refl foldrConcatEq' (x1 :: xs1) xs2 g = trans (cong {f=((++) $ g x1)} $ foldrConcatEq' xs1 xs2 g) (appendAssociative (g x1) (foldr (\x, meth => g x ++ meth) [] xs1) (foldr (\x, meth => g x ++ meth) [] xs2)) private foldrMapCombine : (xs : List a) -> (gs1 : List (a -> b)) -> (g2 : b -> c) -> map g2 (foldr (\g, meth => map g xs ++ meth) [] gs1) = foldr (\g, meth => map g xs ++ meth) [] (map ((.) g2) gs1) foldrMapCombine xs [] g2 = Refl foldrMapCombine xs (g1 :: gs1) g2 = trans (mapAppendDistributive g2 (map g1 xs) (foldr (\g, meth => map g xs ++ meth) [] gs1)) (appendCong2 (sym $ functorComposition xs g1 g2) (foldrMapCombine xs gs1 g2)) VerifiedApplicative List where applicativeMap [] f = Refl applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs applicativeComposition _ _ [] = Refl applicativeComposition xs gs1 (g2 :: gs2) = trans (trans (foldrConcatEq (map ((.) g2) gs1) (foldr (\g, meth => map g gs1 ++ meth) [] (map (.) gs2 ++ [])) xs) (cong $ applicativeComposition xs gs1 gs2)) (sym $ cong {f=(++ foldr (\g, meth => map g (foldr (\g', meth' => map g' xs ++ meth') [] gs1) ++ meth) [] gs2)} $ foldrMapCombine xs gs1 g2) applicativeHomomorphism x g = Refl applicativeInterchange x [] = Refl applicativeInterchange x (g :: gs) = cong $ applicativeInterchange x gs VerifiedApplicative (Vect n) where applicativeMap [] f = Refl applicativeMap (x :: xs) f = rewrite applicativeMap xs f in Refl applicativeIdentity xs = rewrite sym $ applicativeMap xs id in functorIdentity' xs applicativeComposition [] [] [] = Refl applicativeComposition (x :: xs) (f :: fs) (g :: gs) = rewrite applicativeComposition xs fs gs in Refl applicativeHomomorphism = prf where prf : with Vect ((x : a) -> (f : a -> b) -> zipWith Basics.apply (replicate m f) (replicate m x) = replicate m (f x)) prf {m = Z} x f = Refl prf {m = S k} x f = rewrite prf {m = k} x f in Refl applicativeInterchange = prf where prf : with Vect ((x : a) -> (f : Vect m (a -> b)) -> zipWith Basics.apply f (replicate m x) = zipWith Basics.apply (replicate m (\f' => f' x)) f) prf {m = Z} x [] = Refl prf {m = S k} x (f :: fs) = rewrite prf x fs in Refl VerifiedApplicative Maybe where applicativeMap Nothing g = Refl applicativeMap (Just x) g = Refl applicativeIdentity Nothing = Refl applicativeIdentity (Just x) = Refl applicativeComposition Nothing Nothing Nothing = Refl applicativeComposition Nothing Nothing (Just x) = Refl applicativeComposition Nothing (Just x) Nothing = Refl applicativeComposition Nothing (Just x) (Just y) = Refl applicativeComposition (Just x) Nothing Nothing = Refl applicativeComposition (Just x) Nothing (Just y) = Refl applicativeComposition (Just x) (Just y) Nothing = Refl applicativeComposition (Just x) (Just y) (Just z) = Refl applicativeHomomorphism x g = Refl applicativeInterchange x Nothing = Refl applicativeInterchange x (Just y) = Refl interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where monadApplicative : (mf : m (a -> b)) -> (mx : m a) -> mf <*> mx = mf >>= \f => mx >>= \x => pure (f x) monadLeftIdentity : (x : a) -> (f : a -> m b) -> pure x >>= f = f x monadRightIdentity : (mx : m a) -> mx >>= Applicative.pure = mx monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) -> (mx >>= f) >>= g = mx >>= (\x => f x >>= g) VerifiedMonad (Either a) where monadApplicative (Left x) (Left y) = Refl monadApplicative (Left x) (Right y) = Refl monadApplicative (Right x) (Left y) = Refl monadApplicative (Right x) (Right y) = Refl monadLeftIdentity x f = Refl monadRightIdentity (Left x) = Refl monadRightIdentity (Right x) = Refl monadAssociativity (Left x) f g = Refl monadAssociativity (Right x) f g = Refl VerifiedMonad Maybe where monadApplicative Nothing Nothing = Refl monadApplicative Nothing (Just x) = Refl monadApplicative (Just x) Nothing = Refl monadApplicative (Just x) (Just y) = Refl monadLeftIdentity x f = Refl monadRightIdentity Nothing = Refl monadRightIdentity (Just x) = Refl monadAssociativity Nothing f g = Refl monadAssociativity (Just x) f g = Refl VerifiedMonad List where monadApplicative [] _ = Refl monadApplicative (x :: xs) [] = Refl monadApplicative (g :: gs) xs = appendCong2 (mapFoldrEq g xs) (monadApplicative gs xs) where mapFoldrEq : (f : a -> b) -> (x : List a) -> map f x = foldr (\x1, meth => f x1 :: meth) [] x mapFoldrEq _ [] = Refl mapFoldrEq f (_ :: x) = cong $ mapFoldrEq f x monadLeftIdentity x f = appendNilRightNeutral (f x) monadRightIdentity [] = Refl monadRightIdentity (x :: xs) = cong $ monadRightIdentity xs monadAssociativity [] _ _ = Refl monadAssociativity (x :: xs) g1 g2 = trans (foldrConcatEq' (g1 x) (foldr (\x1, meth => g1 x1 ++ meth) [] xs) g2) (cong $ monadAssociativity xs g1 g2) interface (Alternative f, VerifiedApplicative f) => VerifiedAlternative (f : Type -> Type) where alternativeLeftIdentity : (x : f a) -> Applicative.empty <|> x = x alternativeRightIdentity : (x : f a) -> x <|> Applicative.empty = x alternativeAssociativity : (x : f a) -> (y : f a) -> (z : f a) -> x <|> (y <|> z) = (x <|> y) <|> z VerifiedAlternative Maybe where alternativeLeftIdentity _ = Refl alternativeRightIdentity Nothing = Refl alternativeRightIdentity (Just _) = Refl alternativeAssociativity Nothing _ _ = Refl alternativeAssociativity (Just _) _ _ = Refl VerifiedAlternative List where alternativeLeftIdentity _ = Refl alternativeRightIdentity = appendNilRightNeutral alternativeAssociativity = appendAssociative interface Semigroup a => VerifiedSemigroup a where semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r implementation VerifiedSemigroup (List a) where semigroupOpIsAssociative = appendAssociative [PlusNatSemiV] VerifiedSemigroup Nat using PlusNatSemi where semigroupOpIsAssociative = plusAssociative [MultNatSemiV] VerifiedSemigroup Nat using MultNatSemi where semigroupOpIsAssociative = multAssociative [PlusZZSemiV] VerifiedSemigroup ZZ using PlusZZSemi where semigroupOpIsAssociative = plusAssociativeZ [MultZZSemiV] VerifiedSemigroup ZZ using MultZZSemi where semigroupOpIsAssociative = multAssociativeZ interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r [PlusNatMonoidV] VerifiedMonoid Nat using PlusNatSemiV, PlusNatMonoid where monoidNeutralIsNeutralL = plusZeroRightNeutral monoidNeutralIsNeutralR = plusZeroLeftNeutral [MultNatMonoidV] VerifiedMonoid Nat using MultNatSemiV, MultNatMonoid where monoidNeutralIsNeutralL = multOneRightNeutral monoidNeutralIsNeutralR = multOneLeftNeutral [PlusZZMonoidV] VerifiedMonoid ZZ using PlusZZSemiV, PlusZZMonoid where monoidNeutralIsNeutralL = plusZeroRightNeutralZ monoidNeutralIsNeutralR = plusZeroLeftNeutralZ [MultZZMonoidV] VerifiedMonoid ZZ using MultZZSemiV, MultZZMonoid where monoidNeutralIsNeutralL = multOneRightNeutralZ monoidNeutralIsNeutralR = multOneLeftNeutralZ implementation VerifiedMonoid (List a) where monoidNeutralIsNeutralL = appendNilRightNeutral monoidNeutralIsNeutralR xs = Refl interface (VerifiedMonoid a, Group a) => VerifiedGroup a where groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral VerifiedGroup ZZ using PlusZZMonoidV where groupInverseIsInverseL k = rewrite sym $ multCommutativeZ (NegS 0) k in rewrite multNegLeftZ 0 k in rewrite multOneLeftNeutralZ k in plusNegateInverseLZ k groupInverseIsInverseR k = rewrite sym $ multCommutativeZ (NegS 0) k in rewrite multNegLeftZ 0 k in rewrite multOneLeftNeutralZ k in plusNegateInverseRZ k interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l VerifiedAbelianGroup ZZ where abelianGroupOpIsCommutative = plusCommutativeZ interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r) ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r) VerifiedRing ZZ where ringOpIsAssociative = multAssociativeZ ringOpIsDistributiveL = multDistributesOverPlusRightZ ringOpIsDistributiveR = multDistributesOverPlusLeftZ interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r VerifiedRingWithUnity ZZ where ringWithUnityIsUnityL = multOneRightNeutralZ ringWithUnityIsUnityR = multOneLeftNeutralZ interface JoinSemilattice a => VerifiedJoinSemilattice a where joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e interface MeetSemilattice a => VerifiedMeetSemilattice a where meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e