Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 78:f02391a7402f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove monad-law-2, 3
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 01 Dec 2014 12:23:26 +0900
parents 4b16b485a4b2
children 7307e43a3c76
comparison
equal deleted inserted replaced
77:4b16b485a4b2 78:f02391a7402f
118 functor-law-2 f g (mono x) = refl 118 functor-law-2 f g (mono x) = refl
119 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d) 119 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
120 120
121 121
122 -- Monad-laws (Category) 122 -- Monad-laws (Category)
123 123 {-
124 124
125 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) -> 125 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) ->
126 n-tail n (bind ds (n-tail m)) ≡ bind (n-tail n ds) (n-tail (m + n)) 126 n-tail n (bind ds (n-tail m)) ≡ bind (n-tail n ds) (n-tail (m + n))
127 monad-law-1-5 O O ds = refl 127 monad-law-1-5 O O ds = refl
128 monad-law-1-5 O (S n) (mono ds) = begin 128 monad-law-1-5 O (S n) (mono ds) = begin
327 ≡⟨ refl ⟩ 327 ≡⟨ refl ⟩
328 (mu ∙ mu) (delta x d) 328 (mu ∙ mu) (delta x d)
329 ∎ 329 ∎
330 330
331 331
332 332 -}
333 {- 333
334 monad-law-2-1 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta A) -> (bind (fmap eta d) (n-tail n)) ≡ d
335 monad-law-2-1 O (mono x) = refl
336 monad-law-2-1 O (delta x d) = begin
337 bind (fmap eta (delta x d)) (n-tail O) ≡⟨ refl ⟩
338 bind (delta (eta x) (fmap eta d)) id ≡⟨ refl ⟩
339 delta (headDelta (eta x)) (bind (fmap eta d) tailDelta) ≡⟨ refl ⟩
340 delta x (bind (fmap eta d) tailDelta) ≡⟨ cong (\de -> delta x de) (monad-law-2-1 (S O) d) ⟩
341 delta x d ∎
342 monad-law-2-1 (S n) (mono x) = begin
343 bind (fmap eta (mono x)) (n-tail (S n)) ≡⟨ refl ⟩
344 bind (mono (mono x)) (n-tail (S n)) ≡⟨ refl ⟩
345 n-tail (S n) (mono x) ≡⟨ tail-delta-to-mono (S n) x ⟩
346 mono x ∎
347 monad-law-2-1 (S n) (delta x d) = begin
348 bind (fmap eta (delta x d)) (n-tail (S n)) ≡⟨ refl ⟩
349 bind (delta (eta x) (fmap eta d)) (n-tail (S n)) ≡⟨ refl ⟩
350 delta (headDelta ((n-tail (S n) (eta x)))) (bind (fmap eta d) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
351 delta (headDelta ((n-tail (S n) (eta x)))) (bind (fmap eta d) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta (de)) (bind (fmap eta d) (n-tail (S (S n))))) (tail-delta-to-mono (S n) x) ⟩
352 delta (headDelta (eta x)) (bind (fmap eta d) (n-tail (S (S n)))) ≡⟨ refl ⟩
353 delta x (bind (fmap eta d) (n-tail (S (S n)))) ≡⟨ cong (\d -> delta x d) (monad-law-2-1 (S (S n)) d) ⟩
354 delta x d
355 ∎
356
357
334 -- monad-law-2 : join . fmap return = join . return = id 358 -- monad-law-2 : join . fmap return = join . return = id
335 -- monad-law-2-1 join . fmap return = join . return 359 -- monad-law-2 join . fmap return = join . return
336 monad-law-2-1 : {l : Level} {A : Set l} -> (d : Delta A) -> 360 monad-law-2 : {l : Level} {A : Set l} -> (d : Delta A) ->
337 (mu ∙ fmap eta) d ≡ (mu ∙ eta) d 361 (mu ∙ fmap eta) d ≡ (mu ∙ eta) d
338 monad-law-2-1 (mono x) = refl 362 monad-law-2 (mono x) = refl
339 monad-law-2-1 (delta x d) = {!!} 363 monad-law-2 (delta x d) = begin
340 364 (mu ∙ fmap eta) (delta x d) ≡⟨ refl ⟩
341 365 mu (fmap eta (delta x d)) ≡⟨ refl ⟩
342 -- monad-law-2-2 : join . return = id 366 mu (delta (mono x) (fmap eta d)) ≡⟨ refl ⟩
343 monad-law-2-2 : {l : Level} {A : Set l } -> (d : Delta A) -> (mu ∙ eta) d ≡ id d 367 delta (headDelta (mono x)) (bind (fmap eta d) tailDelta) ≡⟨ refl ⟩
344 monad-law-2-2 d = refl 368 delta x (bind (fmap eta d) tailDelta) ≡⟨ cong (\d -> delta x d) (monad-law-2-1 (S O) d) ⟩
369 (delta x d) ≡⟨ refl ⟩
370 mu (mono (delta x d)) ≡⟨ refl ⟩
371 mu (eta (delta x d)) ≡⟨ refl ⟩
372 (mu ∙ eta) (delta x d)
373 ∎
374
375
376 -- monad-law-2' : join . return = id
377 monad-law-2' : {l : Level} {A : Set l} -> (d : Delta A) -> (mu ∙ eta) d ≡ id d
378 monad-law-2' d = refl
345 379
346 380
347 -- monad-law-3 : return . f = fmap f . return 381 -- monad-law-3 : return . f = fmap f . return
348 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x 382 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x
349 monad-law-3 f x = refl 383 monad-law-3 f x = refl
350 384
351 385 {-
352 -- monad-law-4 : join . fmap (fmap f) = fmap f . join 386 -- monad-law-4 : join . fmap (fmap f) = fmap f . join
353 monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (d : Delta (Delta A)) -> 387 monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (d : Delta (Delta A)) ->
354 (mu ∙ fmap (fmap f)) d ≡ (fmap f ∙ mu) d 388 (mu ∙ fmap (fmap f)) d ≡ (fmap f ∙ mu) d
355 monad-law-4 f d = {!!} 389 monad-law-4 f d = {!!}
356 390