blob: 99a3507ccc49ea53a687492a7b3b47f26d2c720f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
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
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
|
