# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1417095897 -32400
# Node ID 18a20a14c4b2a83583bfd899343ba01fb032caa9
# Parent  295e8ed39c0c2cfd9507dba3e983957cf10a67ff
Change prove method. use Int ...

diff -r 295e8ed39c0c -r 18a20a14c4b2 agda/delta.agda
--- a/agda/delta.agda	Thu Nov 27 19:12:44 2014 +0900
+++ b/agda/delta.agda	Thu Nov 27 22:44:57 2014 +0900
@@ -16,9 +16,9 @@
 deltaAppend (mono x) d     = delta x d
 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
 
-headDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
-headDelta (mono x)    = mono x
-headDelta (delta x _) = mono x
+headDelta : {l : Level} {A : Set l} -> Delta A -> A
+headDelta (mono x)    = x
+headDelta (delta x _) = x
 
 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
 tailDelta (mono x)     = mono x
@@ -38,12 +38,11 @@
 
 bind : {l ll : Level} {A : Set l} {B : Set ll} -> (Delta A) -> (A -> Delta B) -> Delta B
 bind (mono x)    f = f x
-bind (delta x d) f = deltaAppend (headDelta (f x)) (bind d (tailDelta ∙ f))
+bind (delta x d) f = delta (headDelta (f x)) (bind d (tailDelta ∙ f))
 
 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
 mu d = bind d id
 
-
 returnS : {l : Level} {A : Set l} -> A -> Delta A
 returnS x = mono x
 
@@ -58,39 +57,12 @@
 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
         (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
 (mono x) >>= f    = f x
-(delta x d) >>= f = deltaAppend (headDelta (f x)) (d >>= (tailDelta ∙ f))
+(delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f))
 
 
 
 -- proofs
 
--- sub proofs
-
-head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} ->
-                                  (f : A -> B) (d : Delta A) -> (headDelta (fmap f d)) ≡ fmap f (headDelta d)
-head-delta-natural-transformation f (mono x)    = refl
-head-delta-natural-transformation f (delta x d) = refl
-
-tail-delta-natural-transfomation  : {l ll : Level} {A : Set l} {B : Set ll} ->
-                                  (f : A -> B) (d : Delta A) -> (tailDelta (fmap f d)) ≡ fmap f (tailDelta d)
-tail-delta-natural-transfomation f (mono x) = refl
-tail-delta-natural-transfomation f (delta x d) = refl
-
-delta-append-natural-transfomation : {l ll : Level} {A : Set l} {B : Set ll} ->
-                                  (f : A -> B) (d : Delta A) (dd : Delta A) ->
-                                  deltaAppend (fmap f d) (fmap f dd) ≡ fmap f (deltaAppend d dd)
-delta-append-natural-transfomation f (mono x) dd    = refl
-delta-append-natural-transfomation f (delta x d) dd = begin
-  deltaAppend (fmap f (delta x d)) (fmap f dd)
-  ≡⟨ refl ⟩
-  deltaAppend (delta (f x) (fmap f d)) (fmap f dd)
-  ≡⟨ refl ⟩
-  delta (f x) (deltaAppend (fmap f d) (fmap f dd))
-  ≡⟨ cong (\d -> delta (f x) d) (delta-append-natural-transfomation f d dd) ⟩
-  delta (f x) (fmap f (deltaAppend d dd))
-  ≡⟨ refl ⟩
-  fmap f (deltaAppend (delta x d) dd)
-  ∎
 -- Functor-laws
 
 -- Functor-law-1 : T(id) = id'
@@ -105,27 +77,166 @@
 functor-law-2 f g (mono x)    = refl
 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
 
-{-
+
 -- Monad-laws (Category)
 
+
+data Int : Set where
+  one : Int
+  succ : Int -> Int
+
+n-times-tail-delta : {l : Level} {A : Set l} -> Int -> ((Delta A) -> (Delta A))
+n-times-tail-delta one = tailDelta
+n-times-tail-delta (succ n) = (n-times-tail-delta n) ∙  tailDelta
+
+tail-delta-to-mono : {l : Level} {A : Set l} -> (n : Int) -> (x : A) ->
+  (n-times-tail-delta n) (mono x) ≡ (mono x)
+tail-delta-to-mono one x = refl
+tail-delta-to-mono (succ n) x = begin
+  n-times-tail-delta (succ n) (mono x)
+  ≡⟨ refl ⟩
+  n-times-tail-delta n (mono x)
+  ≡⟨ tail-delta-to-mono n x ⟩
+  mono x
+  ∎
+
+monad-law-1-4 : {l : Level} {A : Set l} -> (n : Int) (d : Delta (Delta A)) -> 
+  (headDelta ((n-times-tail-delta n) (headDelta ((n-times-tail-delta n) d)))) ≡ 
+  (headDelta ((n-times-tail-delta n) (mu d)))
+monad-law-1-4 one (mono d)     = refl
+monad-law-1-4 one (delta d (mono ds)) = refl
+monad-law-1-4 one (delta d (delta ds ds₁)) = refl
+monad-law-1-4 (succ n) (mono d) = begin
+  headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta (succ n) (mono d))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (headDelta ((n-times-tail-delta n) (mono d))))
+  ≡⟨ cong (\d -> headDelta (n-times-tail-delta (succ n) (headDelta d))) (tail-delta-to-mono n d) ⟩
+  headDelta (n-times-tail-delta (succ n) (headDelta (mono d)))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) d)
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (mu (mono d)))
+  ∎
+monad-law-1-4 (succ n) (delta d (mono ds)) = begin
+  headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta (succ n) (delta d (mono ds)))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta n (mono ds))))
+  ≡⟨ cong (\d -> headDelta (n-times-tail-delta (succ n) (headDelta d))) (tail-delta-to-mono n ds) ⟩
+  headDelta (n-times-tail-delta (succ n) (headDelta (mono ds)))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) ds)
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta n (tailDelta ds))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta n ((bind (mono ds) tailDelta)))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (delta (headDelta d) (bind (mono ds) tailDelta)))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (mu (delta d (mono ds))))
+ ∎
+monad-law-1-4 (succ n) (delta d (delta dd ds)) = begin
+  headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta (succ n) (delta d (delta dd ds)))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta n (delta dd ds))))
+  ≡⟨ {!!} ⟩ -- ?  
+
+  headDelta (n-times-tail-delta n (delta (headDelta (tailDelta dd)) (bind ds (tailDelta ∙ tailDelta))))
+  ≡⟨ {!!} ⟩
+  headDelta (n-times-tail-delta n (delta (headDelta (tailDelta dd)) (bind ds (tailDelta ∙ tailDelta ))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta n (bind (delta dd ds) (tailDelta)))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (delta (headDelta d) (bind (delta dd ds) (tailDelta))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (mu (delta d (delta dd ds))))
+  ∎
+
+
+
+
+monad-law-1-3 : {l : Level} {A : Set l} -> (i : Int) -> (d : Delta (Delta (Delta A))) -> 
+  (bind (fmap mu d) (n-times-tail-delta i) ≡ (bind (bind d (n-times-tail-delta i)) (n-times-tail-delta i)))
+monad-law-1-3 one (mono (mono d)) = refl
+monad-law-1-3 one (mono (delta d d₁)) = refl
+monad-law-1-3 one (delta d ds) = begin
+  bind (fmap mu (delta d ds)) (n-times-tail-delta one) 
+  ≡⟨ refl ⟩
+  bind (delta (mu d) (fmap mu ds)) (n-times-tail-delta one) 
+  ≡⟨ refl ⟩
+  delta (headDelta ((n-times-tail-delta one) (mu d))) (bind (fmap mu ds) ((n-times-tail-delta one) ∙ tailDelta))
+  ≡⟨ refl ⟩
+  delta (headDelta ((n-times-tail-delta one) (mu d))) (bind (fmap mu ds) (n-times-tail-delta (succ one)))
+  ≡⟨ cong (\dx -> delta (headDelta ((n-times-tail-delta one) (mu d))) dx) (monad-law-1-3 (succ one) ds) ⟩
+  delta (headDelta ((n-times-tail-delta one) (mu d))) (bind (bind ds (n-times-tail-delta (succ one))) (n-times-tail-delta (succ one)))
+  ≡⟨ cong (\dx -> delta dx (bind (bind ds (n-times-tail-delta (succ one))) (n-times-tail-delta (succ one )))) (sym (monad-law-1-4 one d)) ⟩
+  delta (headDelta ((n-times-tail-delta one) (headDelta ((n-times-tail-delta one) d)))) (bind (bind ds (n-times-tail-delta (succ one))) (n-times-tail-delta (succ one)))
+  ≡⟨ refl ⟩
+  delta (headDelta ((n-times-tail-delta one) (headDelta ((n-times-tail-delta one) d)))) ((bind (bind ds (n-times-tail-delta (succ one)))) ((n-times-tail-delta one) ∙ tailDelta))
+  ≡⟨ refl ⟩
+  bind (delta (headDelta ((n-times-tail-delta one) d)) (bind ds (n-times-tail-delta (succ one)))) (n-times-tail-delta one)
+  ≡⟨ refl ⟩
+  bind (delta (headDelta ((n-times-tail-delta one) d)) (bind ds ((n-times-tail-delta one) ∙ tailDelta))) (n-times-tail-delta one)
+  ≡⟨ refl ⟩
+  bind (bind (delta d ds) (n-times-tail-delta one)) (n-times-tail-delta one)
+  ∎
+monad-law-1-3 (succ i) d = {!!}
+
+
+monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (mu d) ≡ (headDelta (headDelta d))
+monad-law-1-2 (mono _)    = refl
+monad-law-1-2 (delta _ _) = refl
+
 -- monad-law-1 : join . fmap join = join . join
 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
-monad-law-1 d = ?
+monad-law-1 (mono d) = refl
+monad-law-1 (delta x d) = begin
+  (mu ∙ fmap mu) (delta x d)
+  ≡⟨ refl ⟩
+  mu (fmap mu (delta x d))
+  ≡⟨ refl ⟩
+  mu (delta (mu x) (fmap mu d))
+  ≡⟨ refl ⟩
+  delta (headDelta (mu x)) (bind (fmap mu d) tailDelta)
+  ≡⟨ cong (\x -> delta x (bind (fmap mu d) tailDelta)) (monad-law-1-2 x) ⟩
+  delta (headDelta (headDelta x)) (bind (fmap mu d) tailDelta)
+  ≡⟨ cong (\d -> delta (headDelta (headDelta x)) d) (monad-law-1-3 one d) ⟩
+  delta (headDelta (headDelta x)) (bind (bind d tailDelta) tailDelta)
+  ≡⟨ refl ⟩
+  mu (delta (headDelta x) (bind d tailDelta))
+  ≡⟨ refl ⟩
+  mu (mu (delta x d))
+  ≡⟨ refl ⟩
+  (mu ∙ mu) (delta x d)
+  ∎
+
+
+
+{-
+-- monad-law-2 : join . fmap return = join . return = id
+-- monad-law-2-1 join . fmap return = join . return
+monad-law-2-1 : {l : Level} {A : Set l} -> (d : Delta A) ->
+  (mu ∙ fmap eta) d ≡ (mu ∙ eta) d
+monad-law-2-1 (mono x) = refl
+monad-law-2-1 (delta x d) = {!!}
 
 
 -- monad-law-2-2 :  join . return = id
-monad-law-2-2 : {l : Level} {A : Set l } -> (s : Delta A) -> (mu ∙ eta) s ≡ id s
-monad-law-2-2 (similar lx x ly y) = refl
+monad-law-2-2 : {l : Level} {A : Set l } -> (d : Delta A) -> (mu ∙ eta) d ≡ id d
+monad-law-2-2 d = refl
+
 
 -- monad-law-3 : return . f = fmap f . return
 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x
 monad-law-3 f x = refl
 
+
 -- monad-law-4 : join . fmap (fmap f) = fmap f . join
-monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (s : Delta (Delta A)) ->
-              (mu ∙ fmap (fmap f)) s ≡ (fmap f ∙ mu) s
-monad-law-4 f (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = refl
--}
+monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (d : Delta (Delta A)) ->
+              (mu ∙ fmap (fmap f)) d ≡ (fmap f ∙ mu) d
+monad-law-4 f d = {!!}
+
+
+
 
 -- Monad-laws (Haskell)
 -- monad-law-h-1 : return a >>= k  =  k a
@@ -147,18 +258,6 @@
                 (m : Delta A)  -> (k : A -> (Delta B)) -> (h : B -> (Delta C)) ->
                 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h)
 monad-law-h-3 (mono x) k h    = refl
-monad-law-h-3 (delta x (mono xx)) k h = begin
-  delta x (mono xx) >>= (\x → k x >>= h)
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta ((\x -> k x >>= h) x)) ((mono xx) >>= (tailDelta ∙ ((\x → k x >>= h))))
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta ((\x -> k x >>= h) x)) ((tailDelta ∙ (\x → k x >>= h)) xx)
-  ≡⟨ refl ⟩
-  deltaAppend (headDelta (k x >>= h)) (tailDelta (k xx >>= h))
-  ≡⟨ {!!} ⟩ -- ?
-  deltaAppend (headDelta (k x)) (tailDelta (k xx)) >>= h
-  ≡⟨ refl ⟩
-  (delta x (mono xx) >>= k) >>= h
-  ∎
-monad-law-h-3 (delta x (delta xx d)) k h = {!!}
+monad-law-h-3 (delta x d) k h = {!!}
 
+-}
\ No newline at end of file