Mercurial > hg > Members > atton > delta_monad
changeset 79:7307e43a3c76
Prove monad-law-4
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 01 Dec 2014 17:25:59 +0900 |
| parents | f02391a7402f |
| children | fc5cd8c50312 |
| files | agda/delta.agda |
| diffstat | 1 files changed, 86 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/delta.agda Mon Dec 01 12:23:26 2014 +0900 +++ b/agda/delta.agda Mon Dec 01 17:25:59 2014 +0900 @@ -22,8 +22,8 @@ headDelta (delta x _) = x tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A -tailDelta (mono x) = mono x -tailDelta (delta _ d) = d +tailDelta (mono x) = mono x +tailDelta (delta _ d) = d n-tail : {l : Level} {A : Set l} -> Nat -> ((Delta A) -> (Delta A)) n-tail O = id @@ -32,7 +32,7 @@ -- Functor fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B) -fmap f (mono x) = mono (f x) +fmap f (mono x) = mono (f x) fmap f (delta x d) = delta (f x) (fmap f d) @@ -71,7 +71,7 @@ -- sub-proofs n-tail-plus : {l : Level} {A : Set l} -> (n : Nat) -> ((n-tail {l} {A} n) ∙ tailDelta) ≡ n-tail (S n) -n-tail-plus O = refl +n-tail-plus O = refl n-tail-plus (S n) = begin n-tail (S n) ∙ tailDelta ≡⟨ refl ⟩ (tailDelta ∙ (n-tail n)) ∙ tailDelta ≡⟨ refl ⟩ @@ -96,7 +96,7 @@ tail-delta-to-mono : {l : Level} {A : Set l} -> (n : Nat) -> (x : A) -> (n-tail n) (mono x) ≡ (mono x) -tail-delta-to-mono O x = refl +tail-delta-to-mono O x = refl tail-delta-to-mono (S n) x = begin n-tail (S n) (mono x) ≡⟨ refl ⟩ tailDelta (n-tail n (mono x)) ≡⟨ refl ⟩ @@ -104,6 +104,32 @@ tailDelta (mono x) ≡⟨ refl ⟩ mono x ∎ +head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} + -> (f : A -> B) -> (d : Delta A) -> headDelta (fmap f d) ≡ f (headDelta d) +head-delta-natural-transformation f (mono x) = refl +head-delta-natural-transformation f (delta x d) = refl + +n-tail-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} + -> (n : Nat) -> (f : A -> B) -> (d : Delta A) -> n-tail n (fmap f d) ≡ fmap f (n-tail n d) +n-tail-natural-transformation O f d = refl +n-tail-natural-transformation (S n) f (mono x) = begin + n-tail (S n) (fmap f (mono x)) ≡⟨ refl ⟩ + n-tail (S n) (mono (f x)) ≡⟨ tail-delta-to-mono (S n) (f x) ⟩ + (mono (f x)) ≡⟨ refl ⟩ + fmap f (mono x) ≡⟨ cong (\d -> fmap f d) (sym (tail-delta-to-mono (S n) x)) ⟩ + fmap f (n-tail (S n) (mono x)) ∎ +n-tail-natural-transformation (S n) f (delta x d) = begin + n-tail (S n) (fmap f (delta x d)) ≡⟨ refl ⟩ + n-tail (S n) (delta (f x) (fmap f d)) ≡⟨ cong (\t -> t (delta (f x) (fmap f d))) (sym (n-tail-plus n)) ⟩ + ((n-tail n) ∙ tailDelta) (delta (f x) (fmap f d)) ≡⟨ refl ⟩ + n-tail n (fmap f d) ≡⟨ n-tail-natural-transformation n f d ⟩ + fmap f (n-tail n d) ≡⟨ refl ⟩ + fmap f (((n-tail n) ∙ tailDelta) (delta x d)) ≡⟨ cong (\t -> fmap f (t (delta x d))) (n-tail-plus n) ⟩ + fmap f (n-tail (S n) (delta x d)) ∎ + + + + -- Functor-laws -- Functor-law-1 : T(id) = id' @@ -382,15 +408,67 @@ 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-1 : {l ll : Level} {A : Set l} {B : Set ll} -> (n : Nat) -> (f : A -> B) -> (ds : Delta (Delta A)) -> + bind (fmap (fmap f) ds) (n-tail n) ≡ fmap f (bind ds (n-tail n)) +monad-law-4-1 O f (mono d) = refl +monad-law-4-1 O f (delta d ds) = begin + bind (fmap (fmap f) (delta d ds)) (n-tail O) ≡⟨ refl ⟩ + bind (delta (fmap f d) (fmap (fmap f) ds)) (n-tail O) ≡⟨ refl ⟩ + delta (headDelta (fmap f d)) (bind (fmap (fmap f) ds) tailDelta) ≡⟨ cong (\de -> delta de (bind (fmap (fmap f) ds) tailDelta)) (head-delta-natural-transformation f d) ⟩ + delta (f (headDelta d)) (bind (fmap (fmap f) ds) tailDelta) ≡⟨ cong (\de -> delta (f (headDelta d)) de) (monad-law-4-1 (S O) f ds) ⟩ + delta (f (headDelta d)) (fmap f (bind ds tailDelta)) ≡⟨ refl ⟩ + fmap f (delta (headDelta d) (bind ds tailDelta)) ≡⟨ refl ⟩ + fmap f (bind (delta d ds) (n-tail O)) ∎ +monad-law-4-1 (S n) f (mono d) = begin + bind (fmap (fmap f) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩ + bind (mono (fmap f d)) (n-tail (S n)) ≡⟨ refl ⟩ + n-tail (S n) (fmap f d) ≡⟨ n-tail-natural-transformation (S n) f d ⟩ + fmap f (n-tail (S n) d) ≡⟨ refl ⟩ + fmap f (bind (mono d) (n-tail (S n))) + ∎ +monad-law-4-1 (S n) f (delta d ds) = begin + bind (fmap (fmap f) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩ + delta (headDelta (n-tail (S n) (fmap f d))) (bind (fmap (fmap f) ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩ + delta (headDelta (n-tail (S n) (fmap f d))) (bind (fmap (fmap f) ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta de) (bind (fmap (fmap f) ds) (n-tail (S (S n))))) (n-tail-natural-transformation (S n) f d) ⟩ + delta (headDelta (fmap f ((n-tail (S n) d)))) (bind (fmap (fmap f) ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta de (bind (fmap (fmap f) ds) (n-tail (S (S n))))) (head-delta-natural-transformation f (n-tail (S n) d)) ⟩ + delta (f (headDelta (n-tail (S n) d))) (bind (fmap (fmap f) ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (f (headDelta (n-tail (S n) d))) de) (monad-law-4-1 (S (S n)) f ds) ⟩ + delta (f (headDelta (n-tail (S n) d))) (fmap f (bind ds (n-tail (S (S n))))) ≡⟨ refl ⟩ + fmap f (delta (headDelta (n-tail (S n) d)) (bind ds (n-tail (S (S n))))) ≡⟨ refl ⟩ + fmap f (delta (headDelta (n-tail (S n) d)) (bind ds (tailDelta ∙ (n-tail (S n))))) ≡⟨ refl ⟩ + fmap f (bind (delta d ds) (n-tail (S n))) ∎ + + -- 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) (d : Delta (Delta A)) -> (mu ∙ fmap (fmap f)) d ≡ (fmap f ∙ mu) d -monad-law-4 f d = {!!} +monad-law-4 f (mono d) = refl +monad-law-4 f (delta (mono x) ds) = begin + (mu ∙ fmap (fmap f)) (delta (mono x) ds) ≡⟨ refl ⟩ + mu ( fmap (fmap f) (delta (mono x) ds)) ≡⟨ refl ⟩ + mu (delta (mono (f x)) (fmap (fmap f) ds)) ≡⟨ refl ⟩ + delta (headDelta (mono (f x))) (bind (fmap (fmap f) ds) tailDelta) ≡⟨ refl ⟩ + delta (f x) (bind (fmap (fmap f) ds) tailDelta) ≡⟨ cong (\de -> delta (f x) de) (monad-law-4-1 (S O) f ds) ⟩ + delta (f x) (fmap f (bind ds tailDelta)) ≡⟨ refl ⟩ + fmap f (delta x (bind ds tailDelta)) ≡⟨ refl ⟩ + fmap f (delta (headDelta (mono x)) (bind ds tailDelta)) ≡⟨ refl ⟩ + fmap f (mu (delta (mono x) ds)) ≡⟨ refl ⟩ + (fmap f ∙ mu) (delta (mono x) ds) ∎ +monad-law-4 f (delta (delta x d) ds) = begin + (mu ∙ fmap (fmap f)) (delta (delta x d) ds) ≡⟨ refl ⟩ + mu (fmap (fmap f) (delta (delta x d) ds)) ≡⟨ refl ⟩ + mu (delta (delta (f x) (fmap f d)) (fmap (fmap f) ds)) ≡⟨ refl ⟩ + delta (headDelta (delta (f x) (fmap f d))) (bind (fmap (fmap f) ds) tailDelta) ≡⟨ refl ⟩ + delta (f x) (bind (fmap (fmap f) ds) tailDelta) ≡⟨ cong (\de -> delta (f x) de) (monad-law-4-1 (S O) f ds) ⟩ + delta (f x) (fmap f (bind ds tailDelta)) ≡⟨ refl ⟩ + fmap f (delta x (bind ds tailDelta)) ≡⟨ refl ⟩ + fmap f (delta (headDelta (delta x d)) (bind ds tailDelta)) ≡⟨ refl ⟩ + fmap f (mu (delta (delta x d) ds)) ≡⟨ refl ⟩ + (fmap f ∙ mu) (delta (delta x d) ds) ∎ - +{- -- Monad-laws (Haskell) -- monad-law-h-1 : return a >>= k = k a monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} ->