Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 63:474ed34e4f02

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proving monad-law-1 ...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 25 Nov 2014 17:33:06 +0900
parents 0f308ddd6136
children 15eec529dfc4
comparison
equal deleted inserted replaced
62:0f308ddd6136 63:474ed34e4f02
89 ≡⟨ cong (\d -> delta (f x) d) (delta-append-natural-transfomation f d dd) ⟩ 89 ≡⟨ cong (\d -> delta (f x) d) (delta-append-natural-transfomation f d dd) ⟩
90 delta (f x) (fmap f (deltaAppend d dd)) 90 delta (f x) (fmap f (deltaAppend d dd))
91 ≡⟨ refl ⟩ 91 ≡⟨ refl ⟩
92 fmap f (deltaAppend (delta x d) dd) 92 fmap f (deltaAppend (delta x d) dd)
93 ∎ 93 ∎
94 94 {-
95 95
96 mu-head-delta : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> mu (headDelta d) ≡ headDelta (mu d) 96 mu-head-delta : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> mu (headDelta d) ≡ headDelta (mu d)
97 mu-head-delta (mono (mono x)) = refl 97 mu-head-delta (mono (mono x)) = refl
98 mu-head-delta (mono (delta x (mono xx))) = begin 98 mu-head-delta (mono (delta x (mono xx))) = begin
99 mu (headDelta (mono (delta x (mono xx)))) 99 mu (headDelta (mono (delta x (mono xx))))
118 ≡⟨ refl ⟩ 118 ≡⟨ refl ⟩
119 headDelta (mu (mono (delta x (mono xx)))) 119 headDelta (mu (mono (delta x (mono xx))))
120 ∎ 120 ∎
121 mu-head-delta (mono (delta x (delta x₁ d))) = {!!} 121 mu-head-delta (mono (delta x (delta x₁ d))) = {!!}
122 mu-head-delta (delta d dd) = {!!} 122 mu-head-delta (delta d dd) = {!!}
123 123 -}
124 -- Functor-laws 124 -- Functor-laws
125 125
126 -- Functor-law-1 : T(id) = id' 126 -- Functor-law-1 : T(id) = id'
127 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d 127 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d
128 functor-law-1 (mono x) = refl 128 functor-law-1 (mono x) = refl
134 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d 134 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d
135 functor-law-2 f g (mono x) = refl 135 functor-law-2 f g (mono x) = refl
136 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d) 136 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
137 137
138 -- Monad-laws (Category) 138 -- Monad-laws (Category)
139 {- 139
140 monad-law-1-4 : {l : Level} {A : Set l} -> (ds : Delta (Delta A)) ->
141 tailDelta (bind ds (tailDelta ∙ id)) ≡ bind (tailDelta ds) (tailDelta ∙ tailDelta)
142 monad-law-1-4 (mono ds) = refl
143 monad-law-1-4 (delta (mono x) ds₁) = refl
144 monad-law-1-4 (delta (delta x (mono x₁)) ds₁) = refl
145 monad-law-1-4 (delta (delta x (delta x₁ ds)) ds₁) = refl
146
147 monad-law-1-3 : {l : Level} {A : Set l} -> (ds : Delta (Delta A)) ->
148 tailDelta (bind ds tailDelta) ≡ bind (tailDelta ds) (tailDelta ∙ tailDelta)
149 monad-law-1-3 (mono ds) = refl
150 monad-law-1-3 (delta (mono x) ds) = refl
151 monad-law-1-3 (delta (delta x (mono x₁)) ds) = refl
152 monad-law-1-3 (delta (delta x (delta x₁ d)) ds) = refl
153
154 monad-law-1-sub-sub : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) ->
155 bind (fmap mu d) (tailDelta ∙ tailDelta) ≡ bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
156 monad-law-1-sub-sub (mono (mono d)) = refl
157 monad-law-1-sub-sub (mono (delta (mono x) ds)) = begin
158 bind (fmap mu (mono (delta (mono x) ds))) (tailDelta ∙ tailDelta)
159 ≡⟨ refl ⟩
160 bind (mono (mu (delta (mono x) ds))) (tailDelta ∙ tailDelta)
161 ≡⟨ refl ⟩
162 bind (mono (bind (delta (mono x) ds) id)) (tailDelta ∙ tailDelta)
163 ≡⟨ refl ⟩
164 bind (mono (deltaAppend (headDelta (mono x)) (bind ds tailDelta))) (tailDelta ∙ tailDelta)
165 ≡⟨ refl ⟩
166 bind (mono (deltaAppend (mono x) (bind ds tailDelta))) (tailDelta ∙ tailDelta)
167 ≡⟨ refl ⟩
168 bind (mono (delta x (bind ds tailDelta))) (tailDelta ∙ tailDelta)
169 ≡⟨ refl ⟩
170 (tailDelta ∙ tailDelta) (delta x (bind ds tailDelta))
171 ≡⟨ refl ⟩
172 tailDelta (bind ds tailDelta)
173 ≡⟨ monad-law-1-3 ds ⟩ -- ?
174 bind (tailDelta ds) (tailDelta ∙ tailDelta)
175 ≡⟨ refl ⟩
176 bind ((tailDelta ∙ tailDelta) (delta (mono x) ds)) (tailDelta ∙ tailDelta)
177 ≡⟨ refl ⟩
178 bind (bind (mono (delta (mono x) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
179 ≡⟨ refl ⟩
180 bind (bind (headDelta (tailDelta (mono (delta (mono x) ds)))) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
181 ≡⟨ refl ⟩
182 bind (bind (mono (delta (mono x) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
183 ∎
184 monad-law-1-sub-sub (mono (delta (delta x (mono x₁)) ds)) = begin
185 bind (fmap mu (mono (delta (delta x (mono x₁)) ds))) (tailDelta ∙ tailDelta)
186 ≡⟨ refl ⟩
187 bind (mono (mu (delta (delta x (mono x₁)) ds))) (tailDelta ∙ tailDelta)
188 ≡⟨ refl ⟩
189 (tailDelta ∙ tailDelta) (mu (delta (delta x (mono x₁)) ds))
190 ≡⟨ refl ⟩
191 (tailDelta ∙ tailDelta) (bind (delta (delta x (mono x₁)) ds) id)
192 ≡⟨ refl ⟩
193 (tailDelta ∙ tailDelta) (deltaAppend (headDelta (delta x (mono x₁))) (bind ds (tailDelta ∙ id)))
194 ≡⟨ refl ⟩
195 (tailDelta ∙ tailDelta) (deltaAppend (mono x) (bind ds (tailDelta ∙ id)))
196 ≡⟨ refl ⟩
197 (tailDelta ∙ tailDelta) (delta x (bind ds (tailDelta ∙ id)))
198 ≡⟨ refl ⟩
199 tailDelta (bind ds (tailDelta ∙ id))
200 ≡⟨ monad-law-1-4 ds ⟩
201 bind (tailDelta ds) (tailDelta ∙ tailDelta)
202 ≡⟨ refl ⟩
203 bind ((tailDelta ∙ tailDelta) (delta (delta x (mono x₁)) ds)) (tailDelta ∙ tailDelta)
204 ≡⟨ refl ⟩
205 bind (bind (mono (delta (delta x (mono x₁)) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
206 ∎
207 monad-law-1-sub-sub (mono (delta (delta x (delta xx d)) ds)) = begin
208 bind (fmap mu (mono (delta (delta x (delta xx d)) ds))) (tailDelta ∙ tailDelta)
209 ≡⟨ refl ⟩
210 bind (mono (mu (delta (delta x (delta xx d)) ds))) (tailDelta ∙ tailDelta)
211 ≡⟨ refl ⟩
212 (tailDelta ∙ tailDelta) (mu (delta (delta x (delta xx d)) ds))
213 ≡⟨ {!!} ⟩ -- ?
214 bind (bind (mono (delta (delta x (delta xx d)) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
215 ∎
216 monad-law-1-sub-sub (delta d ds) = {!!}
217
218
219 monad-law-1-sub : {l : Level } {A : Set l} -> (x : Delta (Delta A)) -> (d : Delta (Delta (Delta A))) ->
220 deltaAppend (headDelta (mu x)) (bind (fmap mu d) tailDelta) ≡ mu (deltaAppend (headDelta x) (bind d tailDelta))
221 monad-law-1-sub (mono (mono _)) (mono (mono _)) = refl
222 monad-law-1-sub (mono (mono _)) (mono (delta (mono _) _)) = refl
223 monad-law-1-sub (mono (mono _)) (mono (delta (delta _ _) _)) = refl
224 monad-law-1-sub (mono (mono x)) (delta (mono (mono xx)) d) = begin
225 deltaAppend (headDelta (mu (mono (mono x)))) (bind (fmap mu (delta (mono (mono xx)) d)) tailDelta)
226 ≡⟨ refl ⟩
227 deltaAppend (headDelta (mu (mono (mono x)))) (bind (delta (mu (mono (mono xx))) (fmap mu d)) tailDelta)
228 ≡⟨ refl ⟩
229 deltaAppend (headDelta (bind (mono (mono x)) id)) (bind (delta (mu (mono (mono xx))) (fmap mu d)) tailDelta)
230 ≡⟨ refl ⟩
231 deltaAppend (headDelta (mono x)) (bind (delta (mu (mono (mono xx))) (fmap mu d)) tailDelta)
232 ≡⟨ refl ⟩
233 deltaAppend (headDelta (mono x)) (bind (delta (mono xx) (fmap mu d)) tailDelta)
234 ≡⟨ refl ⟩
235 deltaAppend (mono x) (bind (delta (mono xx) (fmap mu d)) tailDelta)
236 ≡⟨ refl ⟩
237 deltaAppend (mono x) (bind (delta (mono xx) (fmap mu d)) tailDelta)
238 ≡⟨ refl ⟩
239 deltaAppend (mono x) (deltaAppend (tailDelta (mono xx)) (bind (fmap mu d) (tailDelta ∙ tailDelta)))
240 ≡⟨ refl ⟩
241 deltaAppend (mono x) (deltaAppend (mono xx) (bind (fmap mu d) (tailDelta ∙ tailDelta)))
242 ≡⟨ refl ⟩
243 deltaAppend (mono x) (deltaAppend (mu (mono (mono xx))) (bind (fmap mu d) (tailDelta ∙ tailDelta)))
244 ≡⟨ refl ⟩
245 deltaAppend (mono x) (deltaAppend (mono xx) (bind (fmap mu d) (tailDelta ∙ tailDelta)))
246 ≡⟨ refl ⟩
247 delta x (deltaAppend (mono xx) (bind (fmap mu d) (tailDelta ∙ tailDelta)))
248 ≡⟨ refl ⟩
249 delta x (delta xx (bind (fmap mu d) (tailDelta ∙ tailDelta)))
250 ≡⟨ cong (\d -> (delta x (delta xx d))) (monad-law-1-sub-sub d) ⟩ -- ???
251 delta x (delta xx (bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)))
252 ≡⟨ refl ⟩
253 delta x ((deltaAppend (mono xx) (bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta))))
254 ≡⟨ refl ⟩
255 delta x ((deltaAppend (tailDelta (mono xx)) (bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta))))
256 ≡⟨ refl ⟩
257 delta x (bind (delta (mono xx) (bind d (tailDelta ∙ tailDelta))) tailDelta)
258 ≡⟨ refl ⟩
259 delta x (bind (deltaAppend (mono (mono xx)) (bind d (tailDelta ∙ tailDelta))) tailDelta)
260 ≡⟨ refl ⟩
261 delta x (bind (deltaAppend (headDelta (tailDelta (mono (mono xx)))) (bind d (tailDelta ∙ tailDelta))) tailDelta)
262 ≡⟨ refl ⟩
263 delta x (bind (bind (delta (mono (mono xx)) d) tailDelta) tailDelta)
264 ≡⟨ refl ⟩
265 deltaAppend (mono x) (bind (bind (delta (mono (mono xx)) d) tailDelta) tailDelta)
266 ≡⟨ refl ⟩
267 bind (delta (mono x) (bind (delta (mono (mono xx)) d) tailDelta)) id
268 ≡⟨ refl ⟩
269 mu (delta (mono x) (bind (delta (mono (mono xx)) d) tailDelta))
270 ≡⟨ refl ⟩
271 mu (deltaAppend (mono (mono x)) (bind (delta (mono (mono xx)) d) tailDelta))
272 ≡⟨ refl ⟩
273 mu (deltaAppend (headDelta (mono (mono x))) (bind (delta (mono (mono xx)) d) tailDelta))
274 ∎
275 monad-law-1-sub (mono (mono x)) (delta (mono (delta x₁ d)) d₁) = {!!}
276 monad-law-1-sub (mono (mono x)) (delta (delta d d₁) d₂) = {!!}
277 monad-law-1-sub (mono (delta x x₁)) d = {!!}
278 monad-law-1-sub (delta x x₁) d = {!!}
279
140 -- monad-law-1 : join . fmap join = join . join 280 -- monad-law-1 : join . fmap join = join . join
141 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d) 281 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
142 monad-law-1 (mono d) = refl 282 monad-law-1 (mono d) = refl
283 monad-law-1 (delta x d) = begin
284 (mu ∙ (fmap mu)) (delta x d)
285 ≡⟨ refl ⟩
286 mu (fmap mu (delta x d))
287 ≡⟨ refl ⟩
288 mu (delta (mu x) (fmap mu d))
289 ≡⟨ refl ⟩
290 bind (delta (mu x) (fmap mu d)) id
291 ≡⟨ refl ⟩
292 deltaAppend (headDelta (mu x)) (bind (fmap mu d) tailDelta)
293 ≡⟨ monad-law-1-sub x d ⟩
294 mu (deltaAppend (headDelta x) (bind d tailDelta))
295 ≡⟨ refl ⟩
296 mu (bind (delta x d) id)
297 ≡⟨ refl ⟩
298 mu (mu (delta x d))
299 ≡⟨ refl ⟩
300 (mu ∙ mu) (delta x d)
301 ∎
302
303 -- split d
304 {-
143 monad-law-1 (delta x (mono d)) = begin 305 monad-law-1 (delta x (mono d)) = begin
306
144 (mu ∙ fmap mu) (delta x (mono d)) 307 (mu ∙ fmap mu) (delta x (mono d))
145 ≡⟨ refl ⟩ 308 ≡⟨ refl ⟩
146 mu (fmap mu (delta x (mono d))) 309 mu (fmap mu (delta x (mono d)))
147 ≡⟨ refl ⟩ 310 ≡⟨ refl ⟩
148 mu (delta (mu x) (mono (mu d))) 311 mu (delta (mu x) (mono (mu d)))
150 bind (delta (mu x) (mono (mu d))) id 313 bind (delta (mu x) (mono (mu d))) id
151 ≡⟨ refl ⟩ 314 ≡⟨ refl ⟩
152 deltaAppend (headDelta (mu x)) (bind (mono (mu d)) tailDelta) 315 deltaAppend (headDelta (mu x)) (bind (mono (mu d)) tailDelta)
153 ≡⟨ refl ⟩ 316 ≡⟨ refl ⟩
154 deltaAppend (headDelta (mu x)) (tailDelta (mu d)) 317 deltaAppend (headDelta (mu x)) (tailDelta (mu d))
155 ≡⟨ cong (\de -> deltaAppend de (tailDelta (mu d))) (head-delta-natural-transformation {!!} {!!}) ⟩
156 deltaAppend (mu (headDelta x)) (tailDelta (mu d))
157 ≡⟨ {!!} ⟩ 318 ≡⟨ {!!} ⟩
319 mu (deltaAppend (headDelta x) (tailDelta d))
320 ≡⟨ refl ⟩
321 mu (deltaAppend (headDelta x) (tailDelta (id d)))
322 ≡⟨ refl ⟩
323 mu (deltaAppend (headDelta x) ((tailDelta ∙ id) d))
324 ≡⟨ refl ⟩
325 mu (deltaAppend (headDelta x) (bind (mono d) (tailDelta ∙ id)))
326 ≡⟨ refl ⟩
327 mu (bind (delta x (mono d)) id)
328 ≡⟨ refl ⟩
329 mu (mu (delta x (mono d)))
330 ≡⟨ refl ⟩
158 (mu ∙ mu) (delta x (mono d)) 331 (mu ∙ mu) (delta x (mono d))
159 ∎ 332 ∎
160 monad-law-1 (delta x (delta d d₁)) = {!!} 333 monad-law-1 (delta x (delta d ds)) = begin
334 (mu ∙ fmap mu) (delta x (delta d ds))
335 ≡⟨ refl ⟩
336 mu (fmap mu (delta x (delta d ds)))
337 ≡⟨ refl ⟩
338 mu (delta (mu x) (delta (mu d) (fmap mu ds)))
339 ≡⟨ refl ⟩
340 bind (delta (mu x) (delta (mu d) (fmap mu ds))) id
341 ≡⟨ refl ⟩
342 deltaAppend (headDelta (mu x)) (bind (delta (mu d) (fmap mu ds)) tailDelta)
343 ≡⟨ refl ⟩
344 deltaAppend (headDelta (mu x)) (deltaAppend (headDelta (tailDelta (mu d))) (bind (fmap mu ds) (tailDelta ∙ tailDelta)))
345
346 ≡⟨ {!!} ⟩
347 (mu ∙ mu) (delta x (delta d ds))
348 ∎
161 -} 349 -}
162 350
163 351
164 {- 352 {-
165 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d) 353 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
204 mu (mu (delta x (mono d))) 392 mu (mu (delta x (mono d)))
205 ≡⟨ refl ⟩ 393 ≡⟨ refl ⟩
206 (mu ∙ mu) (delta x (mono d)) 394 (mu ∙ mu) (delta x (mono d))
207 ∎ 395 ∎
208 monad-law-1 (delta x (delta xx d)) = {!!} 396 monad-law-1 (delta x (delta xx d)) = {!!}
209 {- 397
210 monad-law-1 (delta x d) = begin 398 monad-law-1 (delta x d) = begin
211 (mu ∙ fmap mu) (delta x d) 399 (mu ∙ fmap mu) (delta x d)
212 ≡⟨ refl ⟩ 400 ≡⟨ refl ⟩
213 mu ((fmap mu) (delta x d)) 401 mu ((fmap mu) (delta x d))
214 ≡⟨ refl ⟩ 402 ≡⟨ refl ⟩
220 ≡⟨ refl ⟩ 408 ≡⟨ refl ⟩
221 deltaAppend (headDelta (mu x)) (bind (fmap mu d) (tailDelta ∙ id)) 409 deltaAppend (headDelta (mu x)) (bind (fmap mu d) (tailDelta ∙ id))
222 ≡⟨ {!!} ⟩ 410 ≡⟨ {!!} ⟩
223 (mu ∙ mu) (delta x d) 411 (mu ∙ mu) (delta x d)
224 ∎ 412 ∎
225 -} 413
226 -} 414
227 415
228 {- 416
229 -- monad-law-2-2 : join . return = id 417 -- monad-law-2-2 : join . return = id
230 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Delta A) -> (mu ∙ eta) s ≡ id s 418 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Delta A) -> (mu ∙ eta) s ≡ id s
231 monad-law-2-2 (similar lx x ly y) = refl 419 monad-law-2-2 (similar lx x ly y) = refl
232 420
233 -- monad-law-3 : return . f = fmap f . return 421 -- monad-law-3 : return . f = fmap f . return