Mercurial > hg > Members > atton > delta_monad
annotate agda/deltaM/monad.agda @ 116:f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 01 Feb 2015 17:55:39 +0900 |
parents | e6bcc7467335 |
children | 6f86b55bf8b4 |
rev | line source |
---|---|
98
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Relation.Binary.PropositionalEquality |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open ≡-Reasoning |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import basic |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import delta |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import delta.functor |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
8 open import delta.monad |
98
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import deltaM |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import deltaM.functor |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
11 open import nat |
98
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 open import laws |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 module deltaM.monad where |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 open Functor |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 open NaturalTransformation |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 open Monad |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
b7f0879e854e
Trying Monad-laws for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
20 -- sub proofs |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
21 |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
22 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
23 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
24 (x : M A) -> (fmap functorM ((headDeltaM {l} {A} {n} {M} {functorM} {monadM}) ∙ deltaM-eta) x) ≡ fmap functorM (eta monadM) x |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
25 fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x = refl |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
26 fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x = refl |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
27 |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
28 |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
29 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
30 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
31 (d : DeltaM M {functorM} {monadM} A (S n)) -> |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
32 deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
33 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
34 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
35 |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
36 |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
37 -- main proofs |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
38 |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
39 postulate deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
40 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
41 (f : A -> B) -> (x : A) -> |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
42 ((deltaM-eta {l} {B} {n} {M} {functorM} {monadM} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x) |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
43 {- |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
44 deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
45 deltaM-eta {n = O} (f x) ≡⟨ refl ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
46 deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
47 deltaM (mono (fmap fm f (eta mm x))) ≡⟨ refl ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
48 deltaM-fmap f (deltaM-eta {n = O} x) ∎ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
49 deltaM-eta-is-nt {l} {A} {B} {S n} {M} {fm} {mm} f x = begin |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
50 deltaM-eta {n = S n} (f x) ≡⟨ refl ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
51 deltaM (delta-eta {n = S n} (eta mm (f x))) ≡⟨ refl ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
52 deltaM (delta (eta mm (f x)) (delta-eta (eta mm (f x)))) |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
53 ≡⟨ cong (\de -> deltaM (delta de (delta-eta de))) (eta-is-nt mm f x) ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
54 deltaM (delta (fmap fm f (eta mm x)) (delta-eta (fmap fm f (eta mm x)))) |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
55 ≡⟨ cong (\de -> deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
56 deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x)))) |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
57 ≡⟨ refl ⟩ |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
58 deltaM-fmap f (deltaM-eta {n = S n} x) |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
59 ∎ |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
60 -} |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
98
diff
changeset
|
61 |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
62 postulate deltaM-right-unity-law : {l : Level} {A : Set l} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
63 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
64 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
65 {- |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
66 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
67 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
68 deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
69 deltaM (mono (mu mm (fmap fm (headDeltaM {M = M})(eta mm (deltaM (mono x)))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
70 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (eta-is-nt mm headDeltaM (deltaM (mono x)) )) ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
71 deltaM (mono (mu mm (eta mm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) (deltaM (mono x)))))) ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
72 deltaM (mono (mu mm (eta mm x))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (right-unity-law mm x)) ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
73 deltaM (mono x) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
74 ∎ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
75 deltaM-right-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
76 deltaM-mu (deltaM-eta (deltaM (delta x d))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
77 ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
78 deltaM-mu (deltaM (delta (eta mm (deltaM (delta x d))) (delta-eta (eta mm (deltaM (delta x d)))))) |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
79 ≡⟨ refl ⟩ |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
80 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (eta mm (deltaM (delta x d))))))) |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
81 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
82 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
83 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
84 (sym (eta-is-nt mm headDeltaM (deltaM (delta x d)))) ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
85 appendDeltaM (deltaM (mono (mu mm (eta mm ((headDeltaM {monadM = mm}) (deltaM (delta x d))))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
86 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
87 ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
88 appendDeltaM (deltaM (mono (mu mm (eta mm x)))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
89 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
90 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
91 (sym (right-unity-law mm x)) ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
92 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) |
103
a271f3ff1922
Delte type dependencie in Monad record for escape implicit type conflict
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
102
diff
changeset
|
93 ≡⟨ refl ⟩ |
111
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
94 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-eta (eta mm (deltaM (delta x d))))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
95 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM de))) (sym (eta-is-nt delta-is-monad (fmap fm tailDeltaM) (eta mm (deltaM (delta x d))))) ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
96 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (fmap fm tailDeltaM (eta mm (deltaM (delta x d))))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
97 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta de)))) (sym (eta-is-nt mm tailDeltaM (deltaM (delta x d)))) ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
98 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (tailDeltaM (deltaM (delta x d))))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
99 ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
100 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM (delta-eta (eta mm (deltaM d))))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
101 ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
102 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-eta (deltaM d))) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
103 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-right-unity-law (deltaM d)) ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
104 appendDeltaM (deltaM (mono x)) (deltaM d) |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
105 ≡⟨ refl ⟩ |
9fe3d0bd1149
Prove right-unity-law on DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
104
diff
changeset
|
106 deltaM (delta x d) |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
98
diff
changeset
|
107 ∎ |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
108 -} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
109 |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
110 |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
111 |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
112 |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
113 |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
114 postulate deltaM-left-unity-law : {l : Level} {A : Set l} |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
115 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
116 {n : Nat} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
117 (d : 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
|
118 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
119 {- |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
120 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
121 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
122 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
123 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (mono x))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
124 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
125 deltaM-mu (deltaM (mono (fmap fm deltaM-eta x))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
126 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
127 deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {O} {M}) (fmap fm deltaM-eta x)))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
128 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (covariant fm deltaM-eta headDeltaM x)) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
129 deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) ∙ deltaM-eta) x))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
130 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
131 deltaM (mono (mu mm (fmap fm (eta mm) x))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
132 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law mm x) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
133 deltaM (mono x) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
134 ∎ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
135 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
136 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
137 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
138 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (delta x d))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
139 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
140 deltaM-mu (deltaM (delta (fmap fm deltaM-eta x) (delta-fmap (fmap fm deltaM-eta) d))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
141 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
142 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {S n} {M} {fm} {mm}) (fmap fm deltaM-eta x))))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
143 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
144 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
145 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
146 (sym (covariant fm deltaM-eta headDeltaM x)) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
147 appendDeltaM (deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {S n} {M} {fm} {mm}) ∙ deltaM-eta) x)))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
148 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
149 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
150 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
151 (fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
152 appendDeltaM (deltaM (mono (mu mm (fmap fm (eta mm) x)))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
153 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
154 |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
155 ≡⟨ cong (\de -> (appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
156 (left-unity-law mm x) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
157 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
158 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
159 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap deltaM-eta (deltaM d)))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
160 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (sym (covariant deltaM-is-functor deltaM-eta tailDeltaM (deltaM d))) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
161 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ deltaM-eta) (deltaM d))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
162 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (fmap-tailDeltaM-with-deltaM-eta (deltaM d)) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
163 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d))) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
164 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-left-unity-law (deltaM d)) ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
165 appendDeltaM (deltaM (mono x)) (deltaM d) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
166 ≡⟨ refl ⟩ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
167 deltaM (delta x d) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
168 ∎ |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
169 |
114
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
170 -} |
08403eb8db8b
Prove natural transformation for deltaM-eta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
112
diff
changeset
|
171 |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
172 |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
173 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
174 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
175 (x : M (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n))) -> |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
176 -- (fmap fm headDeltaM (fmap fm deltaM-mu x)) ≡ (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
177 -- fmap fm (headDeltaM ∙ deltaM-mu) x ≡ fmap fm (fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) x |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
178 headDeltaM (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡ deltaM (mono (mu mm (fmap fm headDeltaM x))) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
179 fmap-headDeltaM-with-deltaM-mu {l} {A} {O} {M} {fm} {mm} x = {!!} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
180 fmap-headDeltaM-with-deltaM-mu {n = S n} x = {!!} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
181 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
182 deltaM-mono : {l : Level} {A : Set l} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
183 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
184 (d : M A) -> DeltaM M {fm} {mm} A (S O) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
185 deltaM-mono x = deltaM (mono x) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
186 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
187 fmap-headDeltaM-with-deltaM-mono : {l : Level} {A : Set l} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
188 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
189 (x : M (M A)) -> |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
190 fmap fm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) ∙ deltaM-mono) x ≡ x |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
191 fmap-headDeltaM-with-deltaM-mono {fm = fm} x = preserve-id fm x |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
192 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
193 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
194 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
195 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
196 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
197 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
198 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n)) (S n)) -> |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
199 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
200 deltaM-association-law {l} {A} {O} M fm mm (deltaM (mono x)) = begin |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
201 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ |
116
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
202 deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
203 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (fmap fm deltaM-mu x))))))) ≡⟨ refl ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
204 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
205 deltaM (mono (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
206 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) x)))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
207 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
208 (sym (covariant fm (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) headDeltaM x)) ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
209 deltaM (mono (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
210 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
211 ≡⟨ refl ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
212 deltaM (mono (mu mm (fmap fm (\d -> (headDeltaM {A = A} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x))) |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
213 ≡⟨ refl ⟩ |
116
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
214 deltaM (mono (mu mm (fmap fm (\d -> (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))) x))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
215 ≡⟨ refl ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
216 deltaM (mono (mu mm (fmap fm ((mu mm) ∙ (((fmap fm headDeltaM)) ∙ ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
217 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (covariant fm ((fmap fm headDeltaM) ∙ (headDeltaM)) (mu mm) x )⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
218 deltaM (mono (mu mm (((fmap fm (mu mm)) ∙ (fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
219 ≡⟨ refl ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
220 deltaM (mono (mu mm (fmap fm (mu mm) ((fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x)))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
221 ≡⟨ cong (\de -> deltaM (mono (mu mm (fmap fm (mu mm) de)))) (covariant fm headDeltaM (fmap fm headDeltaM) x) ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
222 deltaM (mono (mu mm (fmap fm (mu mm) (((fmap fm (fmap fm headDeltaM)) ∙ (fmap fm (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x)))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
223 ≡⟨ refl ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
224 deltaM (mono (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))) |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
225 ≡⟨ cong (\de -> deltaM (mono de)) (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩ |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
226 deltaM (mono (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
227 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩ |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
228 deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))) ≡⟨ refl ⟩ |
116
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
229 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM x)))))))) ≡⟨ refl ⟩ |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
230 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩ |
116
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
231 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M (DeltaM M A (S O)) (S O)} {monadM = mm} (deltaM (mono x))))))) ≡⟨ refl ⟩ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
232 deltaM-mu (deltaM-mu (deltaM (mono x))) ∎ |
f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
115
diff
changeset
|
233 |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
234 deltaM-association-law {n = S n} M fm mm (deltaM (delta x d)) = begin |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
235 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩ |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
236 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩ |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
237 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩ |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
238 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
239 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ {!!} ⟩ |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
240 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
241 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))))) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
242 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ≡⟨ {!!} ⟩ |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
243 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
244 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩ |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
245 deltaM-mu (deltaM-mu (deltaM (delta x d))) |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
246 ∎ |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
247 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
248 |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
249 |
104
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
250 |
ebd0d6e2772c
Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
103
diff
changeset
|
251 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} |
112
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
252 {M : Set l -> Set l} |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
253 (functorM : Functor M) |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
254 (monadM : Monad M functorM) -> |
0a3b6cb91a05
Prove left-unity-law for DeltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
111
diff
changeset
|
255 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n}) |
115
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
256 deltaM-is-monad {l} {A} {n} {M} functorM monadM = |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
257 record { mu = deltaM-mu; |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
258 eta = deltaM-eta; |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
259 return = deltaM-eta; |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
260 bind = deltaM-bind; |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
261 association-law = (deltaM-association-law M functorM monadM) ; |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
262 left-unity-law = deltaM-left-unity-law; |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
263 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; |
e6bcc7467335
Temporary commit : Proving association-law ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
114
diff
changeset
|
264 eta-is-nt = deltaM-eta-is-nt } |
102
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
98
diff
changeset
|
265 |
9c62373bd474
Trying right-unity-law on DeltaM. but do not fit implicit type in eta...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
98
diff
changeset
|
266 |