Mercurial > hg > Members > atton > delta_monad

comparison agda/similar.agda @ 34:b7c4e6276bcf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof Monad-law-2-1
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 18 Oct 2014 14:13:00 +0900
parents 0bc402f970b3
children c5cdbedc68ad
comparison
equal deleted inserted replaced
33:0bc402f970b3 34:b7c4e6276bcf
14 fmap f (similar xs x ys y) = similar xs (f x) ys (f y) 14 fmap f (similar xs x ys y) = similar xs (f x) ys (f y)
15 15
16 mu : {l : Level} {A : Set l} -> Similar (Similar A) -> Similar A 16 mu : {l : Level} {A : Set l} -> Similar (Similar A) -> Similar A
17 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y 17 mu (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = similar (lx ++ llx) x (ly ++ lly) y
18 18
19 return : {A : Set} -> A -> Similar A 19 return : {l : Level} {A : Set l} -> A -> Similar A
20 return x = similar [] x [] x 20 return x = similar [] x [] x
21 21
22 returnS : {A : Set} -> A -> Similar A 22 returnS : {A : Set} -> A -> Similar A
23 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x 23 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x
24 24
35 similar (lx ++ llx ++ lllx) x (ly ++ (lly ++ llly)) y 35 similar (lx ++ llx ++ lllx) x (ly ++ (lly ++ llly)) y
36 ≡⟨ cong (\right-list -> similar (lx ++ llx ++ lllx) x right-list y ) (list-associative ly lly llly) ⟩ 36 ≡⟨ cong (\right-list -> similar (lx ++ llx ++ lllx) x right-list y ) (list-associative ly lly llly) ⟩
37 similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y 37 similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y
38 ∎ 38 ∎
39 39
40
41 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡ id
42 monad-law-2-1 : {l : Level} {A : Set l} -> (s : Similar A) ->
43 (mu ∙ fmap return) s ≡ (mu ∙ return) s
44 monad-law-2-1 (similar lx x ly y) = begin
45 similar (lx ++ []) x (ly ++ []) y
46 ≡⟨ cong (\left-list -> similar left-list x (ly ++ []) y) (empty-append lx)⟩
47 similar lx x (ly ++ []) y
48 ≡⟨ cong (\right-list -> similar lx x right-list y) (empty-append ly) ⟩
49 similar lx x ly y
50 ∎
51
40 {- 52 {-
41 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id
42 monad-law-2-1 : mu ∙ fmap return ≡ mu ∙ return
43 monad-law-2-1 = {!!}
44
45 monad-law-2-2 : mu ∙ return ≡ id 53 monad-law-2-2 : mu ∙ return ≡ id
46 monad-law-2-2 = {!!} 54 monad-law-2-2 = {!!}
47 55
48 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return 56 monad-law-3 : ∀{f} -> return ∙ f ≡ fmap f ∙ return
49 monad-law-3 = {!!} 57 monad-law-3 = {!!}