Add occurs check for terms.

1 files changed, 74 insertions, 2 deletions

diff --git a/src/Data/Maybe/Properties.idr b/src/Data/Maybe/Properties.idr
index 495256e..99a3507 100644
--- a/src/Data/Maybe/Properties.idr
+++ b/src/Data/Maybe/Properties.idr
@@ -1,10 +1,82 @@
 module Data.Maybe.Properties
 
+import Control.Function
+import Data.Maybe
+
+public export
+data IsNothing : Maybe a -> Type where
+  ItIsNothing : IsNothing Nothing
+
+%inline
 export
 mapFusion : (s : Maybe a) -> (f . g) <$> s = f <$> [| g s |]
 mapFusion Nothing = Refl
 mapFusion (Just x) = Refl
 
+%inline
+export
+extractIsJust : {x : Maybe a} -> (0 _ : IsJust x) -> (y ** x = Just y)
+extractIsJust ItIsJust = (_ ** Refl)
+
+%inline
+export
+mapIsJust : (0 f : a -> b) -> IsJust x -> IsJust (map f x)
+mapIsJust f ItIsJust = ItIsJust
+
+%inline
+export
+mapJustInverse :
+  (0 f : a -> b) ->
+  (x : Maybe a) ->
+  (0 _ : map f x = Just y) ->
+  (z ** (x = Just z, y = f z))
+mapJustInverse f (Just x) prf = (x ** (Refl, sym $ injective prf))
+
+%inline
+export
+mapNothing : (0 f : a -> b) -> IsNothing x -> IsNothing (map f x)
+mapNothing f ItIsNothing = ItIsNothing
+
+%inline
+export
+mapNothingInverse :
+  (0 f : a -> b) ->
+  (x : Maybe a) ->
+  (0 _ : IsNothing (map f x)) ->
+  IsNothing x
+mapNothingInverse f Nothing prf = ItIsNothing
+
+%inline
+export
+appIsJust : IsJust f -> IsJust x -> IsJust (f <*> x)
+appIsJust ItIsJust ItIsJust = ItIsJust
+
+%inline
+export
+appJustInverse :
+  (f : Maybe (a -> b)) ->
+  (x : Maybe a) ->
+  (0 _ : f <*> x = Just y) ->
+  (f' ** x' ** (f = Just f', x = Just x', y = f' x'))
+appJustInverse (Just f) (Just x) prf = (f ** x ** (Refl, Refl, sym $ injective prf))
+
+%inline
+export
+appLeftNothingIsNothing : IsNothing f -> (0 x : Maybe a) -> IsNothing (f <*> x)
+appLeftNothingIsNothing ItIsNothing x = ItIsNothing
+
+%inline
+export
+appRightNothingIsNothing : (f : Maybe (a -> b)) -> IsNothing x -> IsNothing (f <*> x)
+appRightNothingIsNothing Nothing prf = ItIsNothing
+appRightNothingIsNothing (Just f) ItIsNothing = ItIsNothing
+
+%inline
 export
-appNothingRight : (0 f : a -> b) -> (y : Maybe a) -> Just f <*> y = Nothing -> y = Nothing
-appNothingRight f Nothing prf = Refl
+appNothingInverse :
+  (f : Maybe (a -> b)) ->
+  (x : Maybe a) ->
+  (0 _ : IsNothing (f <*> x)) ->
+  Either (IsNothing f) (IsNothing x)
+appNothingInverse Nothing x prf = Left ItIsNothing
+appNothingInverse (Just f) Nothing prf = Right ItIsNothing