Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 64:15eec529dfc4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying prove monad-law-1 ...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 26 Nov 2014 16:17:53 +0900
parents 474ed34e4f02
children 6d0193011f89
comparison
equal deleted inserted replaced
63:474ed34e4f02 64:15eec529dfc4
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)) -> 140 monad-law-1-5 : {l : Level} {A : Set l} -> (ds : Delta (Delta A)) ->
141 tailDelta (bind ds (tailDelta ∙ id)) ≡ bind (tailDelta ds) (tailDelta ∙ tailDelta) 141 (tailDelta ∙ tailDelta) (bind ds tailDelta)
142 monad-law-1-4 (mono ds) = refl 142 ≡
143 monad-law-1-4 (delta (mono x) ds₁) = refl 143 bind ((tailDelta ∙ tailDelta) ds) ((tailDelta ∙ tailDelta) ∙ tailDelta)
144 monad-law-1-4 (delta (delta x (mono x₁)) ds₁) = refl 144 monad-law-1-5 (mono ds) = refl
145 monad-law-1-4 (delta (delta x (delta x₁ ds)) ds₁) = refl 145 monad-law-1-5 (delta (mono x) ds) = {!!}
146 monad-law-1-5 (delta (delta x d) ds) = {!!}
147
148 monad-law-1-4 : {l : Level} {A : Set l} -> (x : A) -> (ds : Delta (Delta (Delta A))) ->
149 delta x (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
150 ≡
151 bind (delta (mono x) (bind ds ((tailDelta ∙ tailDelta ) ∙ tailDelta))) (tailDelta ∙ tailDelta)
152 monad-law-1-4 x (mono (mono ds)) = refl
153 monad-law-1-4 x (mono (delta (mono xx) ds)) = begin
154 delta x (bind (fmap mu (mono (delta (mono xx) ds))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
155 ≡⟨ refl ⟩
156 delta x (bind (mono (mu (delta (mono xx) ds))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
157 ≡⟨ refl ⟩
158 delta x (bind (mono (bind (delta (mono xx) ds) id)) (tailDelta ∙ (tailDelta ∙ tailDelta)))
159 ≡⟨ refl ⟩
160 delta x (bind (mono (deltaAppend (headDelta (mono xx)) (bind ds tailDelta))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
161 ≡⟨ refl ⟩
162 delta x (bind (mono (deltaAppend (mono xx) (bind ds tailDelta))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
163 ≡⟨ refl ⟩
164 delta x (bind (mono (delta xx (bind ds tailDelta))) (tailDelta ∙ (tailDelta ∙ tailDelta)))
165 ≡⟨ refl ⟩
166 delta x ((tailDelta ∙ (tailDelta ∙ tailDelta)) (delta xx (bind ds tailDelta)))
167 ≡⟨ refl ⟩
168 delta x ((tailDelta ∙ tailDelta) (bind ds tailDelta))
169 ≡⟨ cong (\d -> delta x d) (monad-law-1-5 ds) ⟩
170 delta x (bind ((tailDelta ∙ tailDelta) ds) ((tailDelta ∙ tailDelta) ∙ tailDelta))
171 ≡⟨ refl ⟩
172 deltaAppend (mono x) (bind ((tailDelta ∙ tailDelta) ds) ((tailDelta ∙ tailDelta) ∙ tailDelta))
173 ≡⟨ refl ⟩
174 deltaAppend (headDelta ((tailDelta ∙ tailDelta) (mono x))) (bind ((tailDelta ∙ tailDelta) ds) ((tailDelta ∙ tailDelta) ∙ tailDelta))
175 ≡⟨ refl ⟩
176 bind (delta (mono x) ((tailDelta ∙ tailDelta) ds)) (tailDelta ∙ tailDelta)
177 ≡⟨ refl ⟩
178 bind (delta (mono x) (bind (mono (delta (mono xx) ds)) ((tailDelta ∙ tailDelta) ∙ tailDelta))) (tailDelta ∙ tailDelta)
179 ∎
180 monad-law-1-4 x (mono (delta (delta x₁ ds) ds₁)) = {!!}
181 monad-law-1-4 x (delta ds ds₁) = {!!}
146 182
147 monad-law-1-3 : {l : Level} {A : Set l} -> (ds : Delta (Delta A)) -> 183 monad-law-1-3 : {l : Level} {A : Set l} -> (ds : Delta (Delta A)) ->
148 tailDelta (bind ds tailDelta) ≡ bind (tailDelta ds) (tailDelta ∙ tailDelta) 184 tailDelta (bind ds tailDelta) ≡ bind (tailDelta ds) (tailDelta ∙ tailDelta)
149 monad-law-1-3 (mono ds) = refl 185 monad-law-1-3 (mono ds) = refl
150 monad-law-1-3 (delta (mono x) ds) = refl 186 monad-law-1-3 (delta (mono x) ds) = refl
151 monad-law-1-3 (delta (delta x (mono x₁)) ds) = refl 187 monad-law-1-3 (delta (delta x (mono x₁)) ds) = refl
152 monad-law-1-3 (delta (delta x (delta x₁ d)) ds) = refl 188 monad-law-1-3 (delta (delta x (delta x₁ d)) ds) = refl
153 189
154 monad-law-1-sub-sub : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> 190 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) 191 bind (fmap mu d) (tailDelta ∙ tailDelta) ≡ bind (bind d (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
156 monad-law-1-sub-sub (mono (mono d)) = refl 192 monad-law-1-sub-sub (mono (mono d)) = refl
157 monad-law-1-sub-sub (mono (delta (mono x) ds)) = begin 193 monad-law-1-sub-sub (mono (delta (mono x) ds)) = begin
158 bind (fmap mu (mono (delta (mono x) ds))) (tailDelta ∙ tailDelta) 194 bind (fmap mu (mono (delta (mono x) ds))) (tailDelta ∙ tailDelta)
159 ≡⟨ refl ⟩ 195 ≡⟨ refl ⟩
160 bind (mono (mu (delta (mono x) ds))) (tailDelta ∙ tailDelta) 196 bind (mono (mu (delta (mono x) ds))) (tailDelta ∙ tailDelta)
161 ≡⟨ refl ⟩ 197 ≡⟨ refl ⟩
168 bind (mono (delta x (bind ds tailDelta))) (tailDelta ∙ tailDelta) 204 bind (mono (delta x (bind ds tailDelta))) (tailDelta ∙ tailDelta)
169 ≡⟨ refl ⟩ 205 ≡⟨ refl ⟩
170 (tailDelta ∙ tailDelta) (delta x (bind ds tailDelta)) 206 (tailDelta ∙ tailDelta) (delta x (bind ds tailDelta))
171 ≡⟨ refl ⟩ 207 ≡⟨ refl ⟩
172 tailDelta (bind ds tailDelta) 208 tailDelta (bind ds tailDelta)
173 ≡⟨ monad-law-1-3 ds ⟩ -- ? 209 ≡⟨ monad-law-1-3 ds ⟩
174 bind (tailDelta ds) (tailDelta ∙ tailDelta) 210 bind (tailDelta ds) (tailDelta ∙ tailDelta)
175 ≡⟨ refl ⟩ 211 ≡⟨ refl ⟩
176 bind ((tailDelta ∙ tailDelta) (delta (mono x) ds)) (tailDelta ∙ tailDelta) 212 bind ((tailDelta ∙ tailDelta) (delta (mono x) ds)) (tailDelta ∙ tailDelta)
177 ≡⟨ refl ⟩ 213 ≡⟨ refl ⟩
178 bind (bind (mono (delta (mono x) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta) 214 bind (bind (mono (delta (mono x) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
195 (tailDelta ∙ tailDelta) (deltaAppend (mono x) (bind ds (tailDelta ∙ id))) 231 (tailDelta ∙ tailDelta) (deltaAppend (mono x) (bind ds (tailDelta ∙ id)))
196 ≡⟨ refl ⟩ 232 ≡⟨ refl ⟩
197 (tailDelta ∙ tailDelta) (delta x (bind ds (tailDelta ∙ id))) 233 (tailDelta ∙ tailDelta) (delta x (bind ds (tailDelta ∙ id)))
198 ≡⟨ refl ⟩ 234 ≡⟨ refl ⟩
199 tailDelta (bind ds (tailDelta ∙ id)) 235 tailDelta (bind ds (tailDelta ∙ id))
200 ≡⟨ monad-law-1-4 ds ⟩ 236 ≡⟨ monad-law-1-3 ds ⟩
201 bind (tailDelta ds) (tailDelta ∙ tailDelta) 237 bind (tailDelta ds) (tailDelta ∙ tailDelta)
202 ≡⟨ refl ⟩ 238 ≡⟨ refl ⟩
203 bind ((tailDelta ∙ tailDelta) (delta (delta x (mono x₁)) ds)) (tailDelta ∙ tailDelta) 239 bind ((tailDelta ∙ tailDelta) (delta (delta x (mono x₁)) ds)) (tailDelta ∙ tailDelta)
204 ≡⟨ refl ⟩ 240 ≡⟨ refl ⟩
205 bind (bind (mono (delta (delta x (mono x₁)) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta) 241 bind (bind (mono (delta (delta x (mono x₁)) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
208 bind (fmap mu (mono (delta (delta x (delta xx d)) ds))) (tailDelta ∙ tailDelta) 244 bind (fmap mu (mono (delta (delta x (delta xx d)) ds))) (tailDelta ∙ tailDelta)
209 ≡⟨ refl ⟩ 245 ≡⟨ refl ⟩
210 bind (mono (mu (delta (delta x (delta xx d)) ds))) (tailDelta ∙ tailDelta) 246 bind (mono (mu (delta (delta x (delta xx d)) ds))) (tailDelta ∙ tailDelta)
211 ≡⟨ refl ⟩ 247 ≡⟨ refl ⟩
212 (tailDelta ∙ tailDelta) (mu (delta (delta x (delta xx d)) ds)) 248 (tailDelta ∙ tailDelta) (mu (delta (delta x (delta xx d)) ds))
213 ≡⟨ {!!} ⟩ -- ? 249 ≡⟨ refl ⟩
250 (tailDelta ∙ tailDelta) (bind (delta (delta x (delta xx d)) ds) id)
251 ≡⟨ refl ⟩
252 (tailDelta ∙ tailDelta) (deltaAppend (headDelta (delta x (delta xx d))) (bind ds tailDelta))
253 ≡⟨ refl ⟩
254 (tailDelta ∙ tailDelta) (deltaAppend (mono x) (bind ds tailDelta))
255 ≡⟨ refl ⟩
256 (tailDelta ∙ tailDelta) (delta x (bind ds tailDelta))
257 ≡⟨ refl ⟩
258 tailDelta (bind ds tailDelta)
259 ≡⟨ monad-law-1-3 ds ⟩
260 bind (tailDelta ds) (tailDelta ∙ tailDelta)
261 ≡⟨ refl ⟩
262 bind ((tailDelta ∙ tailDelta) (delta (delta x (delta xx d)) ds)) (tailDelta ∙ tailDelta)
263 ≡⟨ refl ⟩
214 bind (bind (mono (delta (delta x (delta xx d)) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta) 264 bind (bind (mono (delta (delta x (delta xx d)) ds)) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
215 ∎ 265 ∎
216 monad-law-1-sub-sub (delta d ds) = {!!} 266 monad-law-1-sub-sub (delta (mono (mono x)) ds) = begin
217 267 bind (fmap mu (delta (mono (mono x)) ds)) (tailDelta ∙ tailDelta)
218 268 ≡⟨ refl ⟩
219 monad-law-1-sub : {l : Level } {A : Set l} -> (x : Delta (Delta A)) -> (d : Delta (Delta (Delta A))) -> 269 bind (delta (mu (mono (mono x))) (fmap mu ds)) (tailDelta ∙ tailDelta)
270 ≡⟨ refl ⟩
271 bind (delta (mono x) (fmap mu ds)) (tailDelta ∙ tailDelta)
272 ≡⟨ refl ⟩
273 deltaAppend (headDelta ((tailDelta ∙ tailDelta) (mono x))) (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
274 ≡⟨ refl ⟩
275 deltaAppend ((tailDelta ∙ tailDelta) (mono x)) (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
276 ≡⟨ refl ⟩
277 deltaAppend (mono x) (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
278 ≡⟨ refl ⟩
279 delta x (bind (fmap mu ds) (tailDelta ∙ (tailDelta ∙ tailDelta)))
280 ≡⟨ monad-law-1-4 x ds ⟩ -- ?
281 bind (delta (mono x) (bind ds ((tailDelta ∙ tailDelta ) ∙ tailDelta))) (tailDelta ∙ tailDelta)
282 ≡⟨ refl ⟩
283 bind (delta (tailDelta (mono x)) (bind ds (tailDelta ∙ (tailDelta ∙ tailDelta)))) (tailDelta ∙ tailDelta)
284 ≡⟨ refl ⟩
285 bind (deltaAppend (mono (mono x)) (bind ds (tailDelta ∙ (tailDelta ∙ tailDelta)))) (tailDelta ∙ tailDelta)
286 ≡⟨ refl ⟩
287 bind (deltaAppend (headDelta ((tailDelta ∙ tailDelta) (mono (mono x)))) (bind ds (tailDelta ∙ (tailDelta ∙ tailDelta)))) (tailDelta ∙ tailDelta)
288 ≡⟨ refl ⟩
289 bind (bind (delta (mono (mono x)) ds) (tailDelta ∙ tailDelta)) (tailDelta ∙ tailDelta)
290 ∎
291 monad-law-1-sub-sub (delta (mono (delta x d)) ds) = {!!}
292 monad-law-1-sub-sub (delta (delta d d₁) ds) = {!!}
293
294
295 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)) 296 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 297 monad-law-1-sub (mono (mono _)) (mono (mono _)) = refl
222 monad-law-1-sub (mono (mono _)) (mono (delta (mono _) _)) = refl 298 monad-law-1-sub (mono (mono _)) (mono (delta (mono _) _)) = refl
223 monad-law-1-sub (mono (mono _)) (mono (delta (delta _ _) _)) = refl 299 monad-law-1-sub (mono (mono _)) (mono (delta (delta _ _) _)) = refl
224 monad-law-1-sub (mono (mono x)) (delta (mono (mono xx)) d) = begin 300 monad-law-1-sub (mono (mono x)) (delta (mono (mono xx)) d) = begin