Mercurial > hg > Members > atton > delta_monad
annotate agda/deltaM.agda @ 111:9fe3d0bd1149
Prove right-unity-law on DeltaM
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 29 Jan 2015 11:42:22 +0900 |
parents | 5bd5f4a7ce8d |
children | 0a3b6cb91a05 |
rev | line source |
---|---|
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
3 open import basic |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import delta |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import delta.functor |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import nat |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import laws |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 module deltaM where |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 -- DeltaM definitions |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 data DeltaM {l : Level} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 (M : {l' : Level} -> Set l' -> Set l') |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 {functorM : {l' : Level} -> Functor {l'} M} |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
101
diff
changeset
|
16 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} M functorM} |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 (A : Set l) |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
18 : (Nat -> Set l) where |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
19 deltaM : {n : Nat} -> Delta (M A) (S n) -> DeltaM M {functorM} {monadM} A (S n) |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 -- DeltaM utils |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
24 headDeltaM : {l : Level} {A : Set l} {n : Nat} |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 {M : {l' : Level} -> Set l' -> Set l'} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 {functorM : {l' : Level} -> Functor {l'} M} |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
101
diff
changeset
|
27 {monadM : {l' : Level} -> Monad {l'} M functorM} |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
28 -> DeltaM M {functorM} {monadM} A (S n) -> M A |
100
d8cd880f1d78
Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
29 headDeltaM (deltaM d) = headDelta d |
d8cd880f1d78
Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
30 |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
32 tailDeltaM : {l : Level} {A : Set l} {n : Nat} |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 {M : {l' : Level} -> Set l' -> Set l'} |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 {functorM : {l' : Level} -> Functor {l'} M} |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
101
diff
changeset
|
35 {monadM : {l' : Level} -> Monad {l'} M functorM} |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
36 -> DeltaM {l} M {functorM} {monadM} A (S (S n)) -> DeltaM M {functorM} {monadM} A (S n) |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
37 tailDeltaM {_} {n} (deltaM d) = deltaM (tailDelta d) |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
40 appendDeltaM : {l : Level} {A : Set l} {n m : Nat} |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
41 {M : {l' : Level} -> Set l' -> Set l'} |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
42 {functorM : {l' : Level} -> Functor {l'} M} |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
43 {monadM : {l' : Level} -> Monad {l'} M functorM} -> |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
44 DeltaM M {functorM} {monadM} A (S n) -> |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
45 DeltaM M {functorM} {monadM} A (S m) -> |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
46 DeltaM M {functorM} {monadM} A ((S n) + (S m)) |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
47 appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
48 |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
50 |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
51 |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
52 -- functor definitions |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
53 open Functor |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
54 deltaM-fmap : {l : Level} {A B : Set l} {n : Nat} |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
55 {M : {l' : Level} -> Set l' -> Set l'} |
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
56 {functorM : {l' : Level} -> Functor {l'} M} |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
101
diff
changeset
|
57 {monadM : {l' : Level} -> Monad {l'} M functorM} |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
58 -> (A -> B) -> DeltaM M {functorM} {monadM} A (S n) -> DeltaM M {functorM} {monadM} B (S n) |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
59 deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
60 |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
61 |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
62 |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
63 |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
64 -- monad definitions |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
65 open Monad |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
66 |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
67 deltaM-eta : {l : Level} {A : Set l} {n : Nat} |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
68 {M : {l' : Level} -> Set l' -> Set l'} |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
69 {functorM : {l' : Level} -> Functor {l'} M} |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
70 {monadM : {l' : Level} -> Monad {l'} M functorM} -> |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
71 A -> (DeltaM M {functorM} {monadM} A (S n)) |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
72 deltaM-eta {n = n} {monadM = mm} x = deltaM (delta-eta {n = n} (eta mm x)) |
100
d8cd880f1d78
Redefine some functions DeltaM in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
95
diff
changeset
|
73 |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
74 deltaM-mu : {l : Level} {A : Set l} {n : Nat} |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
75 {M : {l' : Level} -> Set l' -> Set l'} |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
76 {functorM : {l' : Level} -> Functor {l'} M} |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
77 {monadM : {l' : Level} -> Monad {l'} M functorM} -> |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
78 DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n) -> |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
79 DeltaM M {functorM} {monadM} A (S n) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
80 deltaM-mu {n = O} {functorM = fm} {monadM = mm} (deltaM (mono x)) = deltaM (mono (mu mm (fmap fm headDeltaM x))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
81 deltaM-mu {n = S n} {functorM = fm} {monadM = mm} (deltaM (delta x d)) = appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
82 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
109
diff
changeset
|
83 |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
84 |
109
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
85 deltaM-bind : {l : Level} {A B : Set l} |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
86 {n : Nat} |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
87 {M : {l' : Level} -> Set l' -> Set l'} |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
88 {functorM : {l' : Level} -> Functor {l'} M} |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
89 {monadM : {l' : Level} -> Monad {l'} M functorM} -> |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
90 (DeltaM M {functorM} {monadM} A (S n)) -> |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
91 (A -> DeltaM M {functorM} {monadM} B (S n)) |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
92 -> DeltaM M {functorM} {monadM} B (S n) |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
93 deltaM-bind {n = O} {monadM = mm} (deltaM (mono x)) f = deltaM (mono (bind mm x (headDeltaM ∙ f))) |
5bd5f4a7ce8d
Redefine DeltaM that length fixed
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
94 deltaM-bind {n = S n} {monadM = mm} (deltaM (delta x d)) f = appendDeltaM (deltaM (mono (bind mm x (headDeltaM ∙ f)))) |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
95 (deltaM-bind (deltaM d) (tailDeltaM ∙ f)) |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
96 |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
97 |