Mercurial > hg > Members > atton > delta_monad

comparison agda/similar.agda @ 41:23474bf242c6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof monad-law-h-2, trying monad-law-h-3
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 19 Oct 2014 17:41:51 +0900
parents a7cd7740f33e
children 1df4f9d88025
comparison
equal deleted inserted replaced
40:a7cd7740f33e 41:23474bf242c6
32 32
33 -- Monad (Haskell) 33 -- Monad (Haskell)
34 return : {l : Level} {A : Set l} -> A -> Similar A 34 return : {l : Level} {A : Set l} -> A -> Similar A
35 return = eta 35 return = eta
36 36
37 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} -> 37
38 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
38 (x : Similar A) -> (f : A -> (Similar B)) -> (Similar B) 39 (x : Similar A) -> (f : A -> (Similar B)) -> (Similar B)
39 x >>= f = mu (fmap f x) 40 x >>= f = mu (fmap f x)
40 41
41 42
42 43
59 60
60 -- Monad-laws (Category) 61 -- Monad-laws (Category)
61 62
62 -- monad-law-1 : join . fmap join = join . join 63 -- monad-law-1 : join . fmap join = join . join
63 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s) 64 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
64 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _)) 65 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _))
65 ly (similar _ (similar _ _ _ _) lly (similar _ _ llly y))) = begin 66 ly (similar _ (similar _ _ _ _) lly (similar _ _ llly y))) = begin
66 similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y 67 similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y
67 ≡⟨ cong (\left-list -> similar left-list x (ly ++ (lly ++ llly)) y) (list-associative lx llx lllx) ⟩ 68 ≡⟨ cong (\left-list -> similar left-list x (ly ++ (lly ++ llly)) y) (list-associative lx llx lllx) ⟩
68 similar (lx ++ llx ++ lllx) x (ly ++ (lly ++ llly)) y 69 similar (lx ++ llx ++ lllx) x (ly ++ (lly ++ llly)) y
69 ≡⟨ cong (\right-list -> similar (lx ++ llx ++ lllx) x right-list y ) (list-associative ly lly llly) ⟩ 70 ≡⟨ cong (\right-list -> similar (lx ++ llx ++ lllx) x right-list y ) (list-associative ly lly llly) ⟩
98 99
99 100
100 -- Monad-laws (Haskell) 101 -- Monad-laws (Haskell)
101 -- monad-law-h-1 : return a >>= k = k a 102 -- monad-law-h-1 : return a >>= k = k a
102 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} -> 103 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} ->
103 (a : A) -> (k : A -> (Similar B)) -> 104 (a : A) -> (k : A -> (Similar B)) ->
104 (return a >>= k) ≡ (k a) 105 (return a >>= k) ≡ (k a)
105 monad-law-h-1 a k = begin 106 monad-law-h-1 a k = begin
106 return a >>= k 107 return a >>= k
107 ≡⟨ refl ⟩ 108 ≡⟨ refl ⟩
108 mu (fmap k (return a)) 109 mu (fmap k (return a))
117 ≡⟨ refl ⟩ 118 ≡⟨ refl ⟩
118 k a 119 k a
119 ∎ 120 ∎
120 121
121 -- monad-law-h-2 : m >>= return = m 122 -- monad-law-h-2 : m >>= return = m
122 -- monad-law-h-3 : m >>= (× -> k x >>= h) = (m >>= k) >>= h 123 monad-law-h-2 : {l : Level}{A : Set l} -> (m : Similar A) -> (m >>= return) ≡ m
124 monad-law-h-2 (similar lx x ly y) = monad-law-2-1 (similar lx x ly y)
125
126
127 -- monad-law-h-3 : m >>= (\x -> k x >>= h) = (m >>= k) >>= h
128 monad-law-h-3 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
129 (m : Similar A) -> (k : A -> (Similar B)) -> (h : B -> (Similar C)) ->
130 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h)
131 monad-law-h-3 (similar lx x ly y) k h = begin
132 ((similar lx x ly y) >>= (\x -> (k x) >>= h))
133 ≡⟨ refl ⟩
134 mu (fmap (\x -> k x >>= h) (similar lx x ly y))
135 ≡⟨ refl ⟩
136 (mu ∙ fmap (\x -> k x >>= h)) (similar lx x ly y)
137 ≡⟨ refl ⟩
138 (mu ∙ fmap (\x -> mu (fmap h (k x)))) (similar lx x ly y)
139 ≡⟨ refl ⟩
140 (mu ∙ fmap (mu ∙ (\x -> fmap h (k x)))) (similar lx x ly y)
141 ≡⟨ refl ⟩
142 (mu ∙ (fmap mu ∙ (fmap (\x -> fmap h (k x))))) (similar lx x ly y)
143 ≡⟨ refl ⟩
144 --(mu ∙ (mu ∙ (fmap (\x -> fmap h (k x))))) (similar lx x ly y)
145 {!!}
146 ≡⟨ {!!} ⟩
147 (mu ∙ fmap h) (mu (fmap k (similar lx x ly y)))
148 ≡⟨ refl ⟩
149 mu (fmap h (mu (fmap k (similar lx x ly y))))
150 ≡⟨ refl ⟩
151 (mu (fmap k (similar lx x ly y))) >>= h
152 ≡⟨ refl ⟩
153 ((similar lx x ly y) >>= k) >>= h
154 ∎