Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 129:d57c88171f38

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove assciation-law for DeltaM on (S O)
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:42:28 +0900
parents d9a30f696933
children ac45d065cbf2
comparison
equal deleted inserted replaced
128:d9a30f696933 129:d57c88171f38
72 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl 72 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl
73 73
74 74
75 75
76 76
77 77 {-
78 -- main proofs 78 -- main proofs
79 79
80 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} 80 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
81 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 81 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
82 (f : A -> B) -> (x : A) -> 82 (f : A -> B) -> (x : A) ->
184 ≡⟨ refl ⟩ 184 ≡⟨ refl ⟩
185 deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))) 185 deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))
186 ≡⟨ refl ⟩ 186 ≡⟨ refl ⟩
187 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d))) 187 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d)))
188 ∎ 188 ∎
189 {- 189
190 190
191 191
192 192
193 193
194 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat} 194 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
294 deltaM (delta x d) 294 deltaM (delta x d)
295 ∎ 295 ∎
296 296
297 -} 297 -}
298 298
299 postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
300 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
301 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
302 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
299 303
300 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} 304 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
301 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 305 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
302 (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n)) (S n)) -> 306 (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n)) (S n)) ->
303 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) 307 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
304 deltaM-association-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = {!!} 308 deltaM-association-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin
309 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x)))
310 ≡⟨ refl ⟩
311 deltaM-mu (deltaM (mono (fmap F deltaM-mu x)))
312 ≡⟨ refl ⟩
313 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-mu x)))))))
314 ≡⟨ refl ⟩
315 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-mu x))))
316 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-mu headDeltaM x)) ⟩
317 deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ deltaM-mu) x)))
318 ≡⟨ refl ⟩
319 deltaM (mono (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)))
320 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩
321 deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) ∙ (fmap F headDeltaM)) x))))
322 ≡⟨ refl ⟩
323 deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) (fmap F headDeltaM x))))))
324 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (fmap F headDeltaM) (mu M) (fmap F headDeltaM x)) ⟩
325 deltaM (mono (mu M (((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x))))
326 ≡⟨ refl ⟩
327 deltaM (mono (mu M (fmap F (mu M) ((fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))))
328 ≡⟨ cong (\de -> deltaM (mono de)) (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩
329 deltaM (mono (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x)))))
330 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩
331 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (mu M (fmap F (headDeltaM {M = M}) x)))))
332 ≡⟨ refl ⟩
333 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))))))
334 ≡⟨ refl ⟩
335 deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))
336 ≡⟨ refl ⟩
337 deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x)))))))
338 ≡⟨ refl ⟩
339 deltaM-mu (deltaM-mu (deltaM (mono x)))
340
341 ∎
342 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = {!!}
305 {- 343 {-
306 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin 344 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
307 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) 345 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
308 ≡⟨ refl ⟩ 346 ≡⟨ refl ⟩
309 deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))) 347 deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d)))