changeset 33:0bc402f970b3

Proof Monad-law 1
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sat, 18 Oct 2014 14:04:33 +0900
parents 71906644d206
children b7c4e6276bcf
files agda/similar.agda
diffstat 1 files changed, 4 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/agda/similar.agda	Sat Oct 18 13:52:18 2014 +0900
+++ b/agda/similar.agda	Sat Oct 18 14:04:33 2014 +0900
@@ -25,14 +25,15 @@
 returnSS : {A : Set} -> A -> A -> Similar A
 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y
 
+
 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu
-
-
 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _)) 
                      ly (similar   _ (similar _ _ _ _)  lly (similar _ _  llly y))) = begin
     similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y
-  ≡⟨ {!!} ⟩
+  ≡⟨ cong (\left-list -> similar left-list x (ly ++ (lly ++ llly)) y) (list-associative lx llx lllx) ⟩
+    similar (lx ++ llx ++ lllx) x (ly ++ (lly ++ llly)) y
+  ≡⟨ cong (\right-list -> similar (lx ++ llx ++ lllx) x right-list y ) (list-associative ly lly llly) ⟩
     similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y