Mercurial > hg > Members > atton > delta_monad

comparison agda/delta/monad.agda @ 108:d47aea3f9246

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Delete comment outed temporary code
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 28 Jan 2015 22:26:01 +0900
parents caaf364f45ac
children e6bcc7467335
comparison
equal deleted inserted replaced
107:caaf364f45ac 108:d47aea3f9246
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10 open ≡-Reasoning 10 open ≡-Reasoning
11 11
12 module delta.monad where 12 module delta.monad where
13 13
14 tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat} 14 tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat}
15 (f : A -> B) -> (d : Delta A (S (S n))) -> 15 (f : A -> B) -> (d : Delta A (S (S n))) ->
16 (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d 16 (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d
17 tailDelta-is-nt f (delta x d) = refl 17 tailDelta-is-nt f (delta x d) = refl
18
18 19
19 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m : Nat) 20 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m : Nat)
20 (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) -> 21 (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) ->
21 delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d) 22 delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d)
22 tailDelta-to-tail-nt O O f (mono (delta x d)) = refl 23 tailDelta-to-tail-nt O O f (mono (delta x d)) = refl
28 delta (mono (f xx)) 29 delta (mono (f xx))
29 (delta-fmap (delta-fmap f) (delta-fmap tailDelta d)) 30 (delta-fmap (delta-fmap f) (delta-fmap tailDelta d))
30 ∎ 31 ∎
31 tailDelta-to-tail-nt (S n) (S m) f (delta (delta x (delta xx d)) ds) = begin 32 tailDelta-to-tail-nt (S n) (S m) f (delta (delta x (delta xx d)) ds) = begin
32 delta (delta (f xx) (delta-fmap f d)) 33 delta (delta (f xx) (delta-fmap f d))
33 (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds)) 34 (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds))
34 ≡⟨ cong (\de -> delta (delta (f xx) (delta-fmap f d)) de) (tailDelta-to-tail-nt n (S m) f ds) ⟩ 35 ≡⟨ cong (\de -> delta (delta (f xx) (delta-fmap f d)) de) (tailDelta-to-tail-nt n (S m) f ds) ⟩
35 delta (delta (f xx) (delta-fmap f d)) 36 delta (delta (f xx) (delta-fmap f d))
36 (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds)) 37 (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds))
37 ∎ 38 ∎
38
39 39
40 40
41 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat} 41 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
42 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x) 42 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
43 delta-eta-is-nt {n = O} f x = refl 43 delta-eta-is-nt {n = O} f x = refl
68 ≡ 68 ≡
69 (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta d))) 69 (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta d)))
70 delta-fmap-mu-to-tail O O (mono (delta d ds)) = refl 70 delta-fmap-mu-to-tail O O (mono (delta d ds)) = refl
71 delta-fmap-mu-to-tail O (S n) (mono (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds))) = refl 71 delta-fmap-mu-to-tail O (S n) (mono (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds))) = refl
72 delta-fmap-mu-to-tail (S n) O (delta (delta (delta x (mono xx)) (mono (delta dx (mono dxx)))) ds) = begin 72 delta-fmap-mu-to-tail (S n) O (delta (delta (delta x (mono xx)) (mono (delta dx (mono dxx)))) ds) = begin
73 delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds)) 73 delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds))
74 ≡⟨ cong (\de -> delta (mono dxx) de) (delta-fmap-mu-to-tail n O ds) ⟩ 74 ≡⟨ cong (\de -> delta (mono dxx) de) (delta-fmap-mu-to-tail n O ds) ⟩
75 delta (mono dxx) 75 delta (mono dxx)
76 (delta-fmap delta-mu 76 (delta-fmap delta-mu
77 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) 77 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))
78 ∎ 78 ∎
90 -- monad-law-1 : join . delta-fmap join = join . join 90 -- monad-law-1 : join . delta-fmap join = join . join
91 monad-law-1 : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) -> 91 monad-law-1 : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
92 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d) 92 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
93 monad-law-1 {n = O} (mono d) = refl 93 monad-law-1 {n = O} (mono d) = refl
94 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin 94 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin
95 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) 95 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
96 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩ 96 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩
97 delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) 97 delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
98 ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩ 98 ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
99 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))) 99 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
100 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩ 100 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩
101 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) 101 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds))))
102 ∎ 102 ∎
103
104
105 {-
106 begin
107 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ {!!} ⟩
108 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds))))
109 ∎
110 -}
111 {-
112 monad-law-1 {n = S O} (delta (delta (delta _ _) _) (mono (delta (delta _ (mono _)) (mono (delta _ (mono _)))))) = refl
113 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin
114 (delta-mu ∙ delta-fmap delta-mu) (delta (delta (delta x d) dd) ds) ≡⟨ refl ⟩
115 delta-mu (delta-fmap delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
116 delta-mu (delta (delta-mu (delta (delta x d) dd)) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
117 delta-mu (delta (delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta dd))) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
118 delta-mu (delta (delta x (delta-mu (delta-fmap tailDelta dd))) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
119 delta (headDelta (delta x (delta-mu (delta-fmap tailDelta dd)))) (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ refl ⟩
120 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
121 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (functor-law-2 tailDelta delta-mu ds)) ⟩
122 delta x (delta-mu (delta-fmap (tailDelta {n = n} ∙ delta-mu {n = (S n)}) ds))
123 -- ≡⟨ cong (\ff -> delta x (delta-mu (delta-fmap ff ds))) hoge ⟩
124 ≡⟨ {!!} ⟩
125 delta x (delta-mu (delta-fmap (((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) ∙ tailDelta) ds))
126 ≡⟨ cong (\de -> delta x (delta-mu de)) (functor-law-2 (delta-mu ∙ (delta-fmap tailDelta)) tailDelta ds ) ⟩
127 delta x (delta-mu (delta-fmap ((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) (delta-fmap tailDelta ds)))
128 ≡⟨ cong (\de -> delta x (delta-mu de)) (functor-law-2 delta-mu (delta-fmap tailDelta) (delta-fmap tailDelta ds)) ⟩
129 delta x (delta-mu (delta-fmap (delta-mu {n = n}) (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
130 ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
131 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
132 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds)) ⟩
133 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
134 delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
135 delta-mu (delta (delta x d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
136 delta-mu (delta (headDelta (delta (delta x d) dd)) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
137 delta-mu (delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
138 (delta-mu ∙ delta-mu) (delta (delta (delta x d) dd) ds)
139 ∎
140 -}
141 {-
142 begin
143 (delta-mu ∙ delta-fmap delta-mu) (delta d ds) ≡⟨ refl ⟩
144 delta-mu (delta-fmap delta-mu (delta d ds)) ≡⟨ refl ⟩
145 delta-mu (delta (delta-mu d) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
146 delta (headDelta (delta-mu d)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ {!!} ⟩
147 delta (headDelta (headDelta d)) (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
148 delta-mu (delta (headDelta d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
149 delta-mu (delta-mu (delta d ds)) ≡⟨ refl ⟩
150 (delta-mu ∙ delta-mu) (delta d ds)
151 ∎
152 -}
153
154
155 103
156 104
157 delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d 105 delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d
158 delta-right-unity-law (mono x) = refl 106 delta-right-unity-law (mono x) = refl
159 delta-right-unity-law (delta x d) = begin 107 delta-right-unity-law (delta x d) = begin