comparison agda/deltaM/monad.agda @ 130:ac45d065cbf2

Prove all Monad-laws for Delta with Monad
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:46:20 +0900
parents d57c88171f38
children d205ff1e406f
comparison
equal deleted inserted replaced
129:d57c88171f38 130:ac45d065cbf2
25 deconstruct-id {n = O} (deltaM x) = refl 25 deconstruct-id {n = O} (deltaM x) = refl
26 deconstruct-id {n = S n} (deltaM x) = refl 26 deconstruct-id {n = S n} (deltaM x) = refl
27 27
28 headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} 28 headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
29 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 29 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
30 (f : A -> B) -> (x : (DeltaM M A (S n))) -> 30 (f : A -> B) -> (x : (DeltaM M A (S n))) ->
31 ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x 31 ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x
32 headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl 32 headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl
33 headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl 33 headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
34 34
35 tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} 35 tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat}
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) ->
152 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) 152 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
153 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) 153 (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
154 ≡⟨ refl ⟩ 154 ≡⟨ refl ⟩
155 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) 155 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
156 (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) 156 (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))
157 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de))) 157 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de)))
158 (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩ 158 (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩
159 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) 159 deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))
160 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d)))))) 160 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d))))))
161 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) 161 ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de))))
162 (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩ 162 (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩
252 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d 252 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
253 deltaM-left-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin 253 deltaM-left-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin
254 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 254 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
255 deltaM-mu (deltaM (mono (fmap F deltaM-eta x))) ≡⟨ refl ⟩ 255 deltaM-mu (deltaM (mono (fmap F deltaM-eta x))) ≡⟨ refl ⟩
256 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x))))))) ≡⟨ refl ⟩ 256 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x))))))) ≡⟨ refl ⟩
257 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x)))) 257 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x))))
258 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩ 258 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩
259 deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x))) 259 deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x)))
260 ≡⟨ refl ⟩ 260 ≡⟨ refl ⟩
261 deltaM (mono (mu M (fmap F (eta M) x))) 261 deltaM (mono (mu M (fmap F (eta M) x)))
262 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩ 262 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩
263 deltaM (mono x) 263 deltaM (mono x)
264 264
292 deltaM (delta x (unDeltaM {M = M} (deltaM d))) 292 deltaM (delta x (unDeltaM {M = M} (deltaM d)))
293 ≡⟨ refl ⟩ 293 ≡⟨ refl ⟩
294 deltaM (delta x d) 294 deltaM (delta x d)
295 295
296 296
297 -}
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)
303
304 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} 297 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
305 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 298 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
306 (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n)) (S n)) -> 299 (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n)) (S n)) ->
307 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) 300 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
308 deltaM-association-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin 301 deltaM-association-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin
337 deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) 330 deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x)))))))
338 ≡⟨ refl ⟩ 331 ≡⟨ refl ⟩
339 deltaM-mu (deltaM-mu (deltaM (mono x))) 332 deltaM-mu (deltaM-mu (deltaM (mono x)))
340 333
341 334
342 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = {!!} 335
343 {-
344 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin 336 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
345 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) 337 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))
346 ≡⟨ refl ⟩ 338 ≡⟨ refl ⟩
347 deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d))) 339 deltaM-mu (deltaM (delta (fmap F deltaM-mu x) (delta-fmap (fmap F deltaM-mu) d)))
348 ≡⟨ refl ⟩ 340 ≡⟨ refl ⟩
445 deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} (deltaM (delta x d))))) 437 deltaM-mu (deltaM (delta (mu M (fmap F headDeltaM (headDeltaM {M = M} (deltaM (delta x d)))))
446 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d)))))))) 438 (unDeltaM {A = DeltaM M A (S (S n))} {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
447 ≡⟨ refl ⟩ 439 ≡⟨ refl ⟩
448 deltaM-mu (deltaM-mu (deltaM (delta x d))) 440 deltaM-mu (deltaM-mu (deltaM (delta x d)))
449 441
450 -} 442
451 443
452 {- 444
453 445
454 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} 446 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
455 {M : Set l -> Set l} 447 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
456 (functorM : Functor M) 448 Monad {l} (\A -> DeltaM M A (S n)) (deltaM-is-functor {l} {n})
457 (M : Monad M functorM) -> 449 deltaM-is-monad {l} {A} {n} {T} {F} {M} =
458 Monad {l} (\A -> DeltaM M {functorM} {M} A (S n)) (deltaM-is-functor {l} {n})
459 deltaM-is-monad {l} {A} {n} {M} functorM M =
460 record { mu = deltaM-mu 450 record { mu = deltaM-mu
461 ; eta = deltaM-eta 451 ; eta = deltaM-eta
462 ; eta-is-nt = deltaM-eta-is-nt 452 ; eta-is-nt = deltaM-eta-is-nt
463 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x))) 453 ; mu-is-nt = (\f x -> (sym (deltaM-mu-is-nt f x)))
464 ; association-law = (deltaM-association-law M functorM M) 454 ; association-law = deltaM-association-law
465 ; left-unity-law = deltaM-left-unity-law 455 ; left-unity-law = deltaM-left-unity-law
466 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) 456 ; right-unity-law = (\x -> (sym (deltaM-right-unity-law x)))
467 } 457 }
468 458
469 459
470 460
471 -} 461