@@ -214,6 +214,24 @@ VerifiedMonad List where
214214 (foldrConcatEq' (g1 x) (foldr (\x1, meth => g1 x1 ++ meth) [] xs) g2)
215215 (cong $ monadAssociativity xs g1 g2)
216216
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
234+
217235interface Semigroup a => VerifiedSemigroup a where
218236 semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
219237