Mercurial > hg > Members > atton > delta_monad

comparison agda/similar.agda @ 33:0bc402f970b3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof Monad-law 1
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 18 Oct 2014 14:04:33 +0900
parents 71906644d206
children b7c4e6276bcf
comparison
equal deleted inserted replaced
32:71906644d206 33:0bc402f970b3
23 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x 23 returnS x = similar [[ (show x) ]] x [[ (show x) ]] x
24 24
25 returnSS : {A : Set} -> A -> A -> Similar A 25 returnSS : {A : Set} -> A -> A -> Similar A
26 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y 26 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y
27 27
28
28 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu 29 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu
29
30
31 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s) 30 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
32 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _)) 31 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _))
33 ly (similar _ (similar _ _ _ _) lly (similar _ _ llly y))) = begin 32 ly (similar _ (similar _ _ _ _) lly (similar _ _ llly y))) = begin
34 similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y 33 similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y
35 ≡⟨ {!!} ⟩ 34 ≡⟨ cong (\left-list -> similar left-list x (ly ++ (lly ++ llly)) y) (list-associative lx llx lllx) ⟩
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 similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y 37 similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y
37 ∎ 38 ∎
38 39
39 {- 40 {-
40 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id 41 --monad-law-2 : mu ∙ fmap return ≡ mu ∙ return ≡id