Mercurial > hg > Members > atton > delta_monad

changeset 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
files agda/deltaM/monad.agda
diffstat 1 files changed, 41 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/agda/deltaM/monad.agda	Tue Feb 03 12:24:26 2015 +0900
+++ b/agda/deltaM/monad.agda	Tue Feb 03 12:42:28 2015 +0900
@@ -74,7 +74,7 @@
 
 
 
-
+{-
 -- main proofs
 
 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
@@ -186,7 +186,7 @@
   ≡⟨ refl ⟩
   deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d)))
   ∎
-{-
+
 
 
 
@@ -296,12 +296,50 @@
 
 -}
 
+postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
+                  {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
+                  (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
+                  deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
 
 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
                          {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
                          (d : DeltaM M (DeltaM M (DeltaM M A (S n)) (S n))  (S n)) ->
                          deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
-deltaM-association-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x)) = {!!}
+deltaM-association-law {l} {A}   {O} {T} {F} {M} (deltaM (mono x))    = begin
+  deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x)))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (fmap F deltaM-mu x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-mu x)))))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-mu x))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-mu headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ deltaM-mu) x)))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (((mu M) ∙ (fmap F headDeltaM)) ∙ headDeltaM) x)))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F headDeltaM ((mu M) ∙ (fmap F headDeltaM)) x) ⟩
+  deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) ∙ (fmap F headDeltaM)) x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M ((((fmap F (((mu M) ∙ (fmap F headDeltaM)))) (fmap F headDeltaM x))))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (fmap F headDeltaM) (mu M) (fmap F headDeltaM x)) ⟩
+  deltaM (mono (mu M (((fmap F (mu M)) ∙ (fmap F (fmap F headDeltaM))) (fmap F headDeltaM x))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (mu M) ((fmap F (fmap F headDeltaM) (fmap F headDeltaM x))))))
+  ≡⟨ cong (\de -> deltaM (mono de)) (association-law M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x))) ⟩
+  deltaM (mono (mu M (mu M (fmap F (fmap F headDeltaM) (fmap F headDeltaM x)))))
+  ≡⟨ cong (\de -> deltaM (mono (mu M de))) (mu-is-nt M headDeltaM (fmap F headDeltaM x)) ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (mu M (fmap F (headDeltaM {M = M}) x)))))
+  ≡⟨ refl ⟩
+  deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x)))))))
+  ≡⟨ refl ⟩
+  deltaM-mu (deltaM-mu (deltaM (mono x)))
+
+  ∎
+deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = {!!}
 {-
 deltaM-association-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
   deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d)))