Mercurial > hg > Members > atton > delta_monad
changeset 115:e6bcc7467335
Temporary commit : Proving association-law ...
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 01 Feb 2015 17:06:55 +0900 |
| parents | 08403eb8db8b |
| children | f02c5ad4a327 |
| files | agda/delta/monad.agda agda/deltaM.agda agda/deltaM/monad.agda agda/laws.agda |
| diffstat | 4 files changed, 112 insertions(+), 78 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/delta/monad.agda Fri Jan 30 22:17:46 2015 +0900 +++ b/agda/delta/monad.agda Sun Feb 01 17:06:55 2015 +0900 @@ -147,6 +147,7 @@ return = delta-eta; bind = delta-bind; eta-is-nt = delta-eta-is-nt; + mu-is-nt = delta-mu-is-nt; association-law = monad-law-1; left-unity-law = delta-left-unity-law ; right-unity-law = \x -> (sym (delta-right-unity-law x)) }
--- a/agda/deltaM.agda Fri Jan 30 22:17:46 2015 +0900 +++ b/agda/deltaM.agda Sun Feb 01 17:06:55 2015 +0900 @@ -41,6 +41,10 @@ appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) +dmap : {l : Level} {A B : Set l} {n : Nat} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> + (M A -> B) -> DeltaM M {functorM} {monadM} A (S n) -> Delta B (S n) +dmap f (deltaM d) = delta-fmap f d -- functor definitions
--- a/agda/deltaM/monad.agda Fri Jan 30 22:17:46 2015 +0900 +++ b/agda/deltaM/monad.agda Sun Feb 01 17:06:55 2015 +0900 @@ -36,10 +36,11 @@ -- main proofs -deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} +postulate deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} (f : A -> B) -> (x : A) -> ((deltaM-eta {l} {B} {n} {M} {functorM} {monadM} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x) +{- deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin deltaM-eta {n = O} (f x) ≡⟨ refl ⟩ deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩ @@ -56,6 +57,7 @@ ≡⟨ refl ⟩ deltaM-fmap f (deltaM-eta {n = S n} x) ∎ +-} postulate deltaM-right-unity-law : {l : Level} {A : Set l} {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat} @@ -168,88 +170,114 @@ -} +fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} + {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} + (x : M (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n))) -> +-- (fmap fm headDeltaM (fmap fm deltaM-mu x)) ≡ (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))) +-- fmap fm (headDeltaM ∙ deltaM-mu) x ≡ fmap fm (fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) x + headDeltaM (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡ deltaM (mono (mu mm (fmap fm headDeltaM x))) +fmap-headDeltaM-with-deltaM-mu {l} {A} {O} {M} {fm} {mm} x = {!!} +fmap-headDeltaM-with-deltaM-mu {n = S n} x = {!!} + +deltaM-mono : {l : Level} {A : Set l} + {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} + (d : M A) -> DeltaM M {fm} {mm} A (S O) +deltaM-mono x = deltaM (mono x) + +fmap-headDeltaM-with-deltaM-mono : {l : Level} {A : Set l} + {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} + (x : M (M A)) -> + fmap fm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) ∙ deltaM-mono) x ≡ x +fmap-headDeltaM-with-deltaM-mono {fm = fm} x = preserve-id fm x + + + + +deltaM-association-law : {l : Level} {A : Set l} {n : Nat} + (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) + (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} 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} M fm mm (deltaM (mono x)) = begin + deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (\x -> (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩ + + deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (\x -> (deltaM-mono (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (deltaM-mono ∙ (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (((fmap fm (deltaM-mono)) ∙ (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mono (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))))) + ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (covariant fm deltaM-mu headDeltaM x )) ⟩ + + deltaM (mono (mu mm (fmap fm (headDeltaM ∙ deltaM-mono) ((fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) + ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-mono ((fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)) ⟩ + + deltaM (mono (mu mm (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))) ≡⟨ refl ⟩ + + + +{- + {!!} + + + + deltaM (mono (mu mm (fmap fm (headDeltaM) (fmap fm + (\x -> ((deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {O} {M} {fm} {mm} )(headDeltaM {l} {DeltaM M {fm} {mm} A (S O)} {O} {M} {fm} {mm} x))))))) x)))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (\x -> ((deltaM-mono (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩ + + deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (deltaM-mono ∙ (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (((fmap fm deltaM-mono) ∙ (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (((fmap fm deltaM-mono (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))))))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm (headDeltaM ∙ deltaM-mono) (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x)))) + ≡⟨ {!!} ⟩ +-- ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-eta (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x)) ⟩ +-} + deltaM (mono (mu mm (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm ((mu mm) ∙ (\x -> (fmap fm headDeltaM (headDeltaM x)))) x))) ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm ((mu mm) ∙ ((fmap fm headDeltaM) ∙ headDeltaM)) x))) + ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (covariant fm ((fmap fm headDeltaM) ∙ headDeltaM) (mu mm) x) ⟩ + deltaM (mono (mu mm (((fmap fm (mu mm)) ∙ (fmap fm ((fmap fm headDeltaM) ∙ headDeltaM))) x))) + ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm (mu mm) ((fmap fm ((fmap fm headDeltaM) ∙ headDeltaM) x))) )) + ≡⟨ cong (\de -> deltaM (mono (mu mm (fmap fm (mu mm) de)))) (covariant fm headDeltaM (fmap fm headDeltaM) x) ⟩ + deltaM (mono (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))) + ≡⟨ cong (\de -> deltaM (mono de)) (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩ + deltaM (mono (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))) + ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩ + deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩ + deltaM-mu (deltaM-mu (deltaM (mono x))) + ∎ +deltaM-association-law {n = S n} M fm mm (deltaM (delta x d)) = begin + deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩ + appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ {!!} ⟩ + + appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ≡⟨ {!!} ⟩ + deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩ + deltaM-mu (deltaM-mu (deltaM (delta x d))) + ∎ + + + deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} {M : Set l -> Set l} (functorM : Functor M) (monadM : Monad M functorM) -> Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n}) -deltaM-is-monad functorM monadM = record - { mu = deltaM-mu; - eta = deltaM-eta; - return = deltaM-eta; - bind = deltaM-bind; - association-law = {!!}; - left-unity-law = deltaM-left-unity-law; - right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; - eta-is-nt = deltaM-eta-is-nt - } - - - - +deltaM-is-monad {l} {A} {n} {M} functorM monadM = + record { mu = deltaM-mu; + eta = deltaM-eta; + return = deltaM-eta; + bind = deltaM-bind; + association-law = (deltaM-association-law M functorM monadM) ; + left-unity-law = deltaM-left-unity-law; + right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; + eta-is-nt = deltaM-eta-is-nt } -{- -deltaM-association-law : {l : Level} {A : Set l} - {M : {l' : Level} -> Set l' -> Set l'} - (functorM : {l' : Level} -> Functor {l'} M) - (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM) - -> (d : DeltaM M (DeltaM M (DeltaM M {functorM} {monadM} A))) - -> ((deltaM-mu ∙ (deltaM-fmap deltaM-mu)) d) ≡ ((deltaM-mu ∙ deltaM-mu) d) -deltaM-association-law functorM monadM (deltaM (mono x)) = begin - (deltaM-mu ∙ deltaM-fmap deltaM-mu) (deltaM (mono x)) ≡⟨ refl ⟩ - deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ - deltaM-mu (deltaM (delta-fmap (fmap functorM deltaM-mu) (mono x))) ≡⟨ {!!} ⟩ - deltaM-mu (deltaM (mono (bind monadM x headDeltaM))) ≡⟨ refl ⟩ - deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ - deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ - (deltaM-mu ∙ deltaM-mu) (deltaM (mono x)) ∎ -deltaM-association-law functorM monadM (deltaM (delta x d)) = {!!} --} - -{- - -nya : {l : Level} {A B C : Set l} -> - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M } - {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} - (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M {functorM} {monadM} B)) -> (g : B -> (DeltaM M C)) -> - (x : M A) -> - (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡ - (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g) -nya = {!!} - -deltaM-monad-law-h-3 : {l : Level} {A B C : Set l} -> - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M } - {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM} - (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M B)) -> (g : B -> (DeltaM M C)) -> - (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡ (deltaM-bind (deltaM-bind m f) g) -{- -deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin - (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩ - - (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩ - (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g) ≡⟨ refl ⟩ - (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩ - (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g) ∎ --} - -deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin - (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩ - (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩ --- (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡⟨ {!!} ⟩ - deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩ - deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩ - (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩ - (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g) - ∎ -deltaM-monad-law-h-3 (deltaM (delta x d)) f g = {!!} -{- - begin - (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡⟨ {!!} ⟩ - (deltaM-bind (deltaM-bind m f) g) - ∎ --} --}
--- a/agda/laws.agda Fri Jan 30 22:17:46 2015 +0900 +++ b/agda/laws.agda Sun Feb 01 17:06:55 2015 +0900 @@ -43,6 +43,7 @@ right-unity-law : {A : Set l} -> (x : M A) -> id x ≡ (mu ∙ eta) x field -- natural transformations eta-is-nt : {A B : Set l} -> (f : A -> B) -> (x : A) -> (eta ∙ f) x ≡ fmap functorM f (eta x) + mu-is-nt : {A B : Set l} -> (f : A -> B) -> (x : M (M A)) -> mu (fmap functorM (fmap functorM f) x) ≡ fmap functorM f (mu x) open Monad \ No newline at end of file