# HG changeset patch # User Yasutaka Higa # Date 1422622651 -32400 # Node ID 0a3b6cb91a05daf540913b0f3a87d14682b9dfc4 # Parent 9fe3d0bd1149bc245a93213152daf3c05d25af61 Prove left-unity-law for DeltaM diff -r 9fe3d0bd1149 -r 0a3b6cb91a05 agda/delta/functor.agda --- a/agda/delta/functor.agda Thu Jan 29 11:42:22 2015 +0900 +++ b/agda/delta/functor.agda Fri Jan 30 21:57:31 2015 +0900 @@ -1,5 +1,6 @@ open import Level open import Relation.Binary.PropositionalEquality +open ≡-Reasoning open import basic open import delta @@ -22,22 +23,21 @@ 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) +delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} + {f g : A -> B} -> (eq : (x : A) -> f x ≡ g x) (d : Delta A (S n)) -> + delta-fmap f d ≡ delta-fmap g d +delta-fmap-equiv {f = f} {g = g} eq (mono x) = begin + mono (f x) ≡⟨ cong (\he -> (mono he)) (eq x) ⟩ + mono (g x) ∎ +delta-fmap-equiv {f = f} {g = g} eq (delta x d) = begin + delta (f x) (delta-fmap f d) ≡⟨ cong (\hx -> (delta hx (delta-fmap f d))) (eq x) ⟩ + delta (g x) (delta-fmap f d) ≡⟨ cong (\fx -> (delta (g x) fx)) (delta-fmap-equiv {f = f} {g = g} eq d) ⟩ + delta (g x) (delta-fmap g d) ∎ + delta-is-functor : {l : Level} {n : Nat} -> Functor {l} (\A -> Delta A (S n)) delta-is-functor = record { fmap = delta-fmap ; preserve-id = functor-law-1; - covariant = \f g -> functor-law-2 g f} - - -open ≡-Reasoning -delta-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} - (f g : A -> B) (eq : f ≡ g) (d : Delta A (S n)) -> - delta-fmap f d ≡ delta-fmap g d -delta-fmap-equiv f g eq (mono x) = begin - mono (f x) ≡⟨ cong (\h -> (mono (h x))) eq ⟩ - mono (g x) ∎ -delta-fmap-equiv f g eq (delta x d) = begin - delta (f x) (delta-fmap f d) ≡⟨ cong (\h -> (delta (h x) (delta-fmap f d))) eq ⟩ - delta (g x) (delta-fmap f d) ≡⟨ cong (\fx -> (delta (g x) fx)) (delta-fmap-equiv f g eq d) ⟩ - delta (g x) (delta-fmap g d) ∎ + covariant = \f g -> functor-law-2 g f; + fmap-equiv = delta-fmap-equiv } diff -r 9fe3d0bd1149 -r 0a3b6cb91a05 agda/deltaM.agda --- a/agda/deltaM.agda Thu Jan 29 11:42:22 2015 +0900 +++ b/agda/deltaM.agda Fri Jan 30 21:57:31 2015 +0900 @@ -11,9 +11,9 @@ -- DeltaM definitions data DeltaM {l : Level} - (M : {l' : Level} -> Set l' -> Set l') - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} {A : Set l'} -> Monad {l'} M functorM} + (M : Set l -> Set l) + {functorM : Functor M} + {monadM : Monad M functorM} (A : Set l) : (Nat -> Set l) where deltaM : {n : Nat} -> Delta (M A) (S n) -> DeltaM M {functorM} {monadM} A (S n) @@ -22,28 +22,22 @@ -- DeltaM utils headDeltaM : {l : Level} {A : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> DeltaM M {functorM} {monadM} A (S n) -> M A headDeltaM (deltaM d) = headDelta d tailDeltaM : {l : Level} {A : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> DeltaM {l} M {functorM} {monadM} A (S (S n)) -> DeltaM M {functorM} {monadM} A (S n) tailDeltaM {_} {n} (deltaM d) = deltaM (tailDelta d) appendDeltaM : {l : Level} {A : Set l} {n m : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} -> + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> DeltaM M {functorM} {monadM} A (S n) -> DeltaM M {functorM} {monadM} A (S m) -> - DeltaM M {functorM} {monadM} A ((S n) + (S m)) + DeltaM M {functorM} {monadM} A ((S n) + (S m)) appendDeltaM (deltaM d) (deltaM dd) = deltaM (deltaAppend d dd) @@ -52,9 +46,7 @@ -- functor definitions open Functor deltaM-fmap : {l : Level} {A B : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> (A -> B) -> DeltaM M {functorM} {monadM} A (S n) -> DeltaM M {functorM} {monadM} B (S n) deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) @@ -65,16 +57,12 @@ open Monad deltaM-eta : {l : Level} {A : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} -> + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> A -> (DeltaM M {functorM} {monadM} A (S n)) deltaM-eta {n = n} {monadM = mm} x = deltaM (delta-eta {n = n} (eta mm x)) deltaM-mu : {l : Level} {A : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} -> + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} -> DeltaM M {functorM} {monadM} (DeltaM M {functorM} {monadM} A (S n)) (S n) -> DeltaM M {functorM} {monadM} A (S n) deltaM-mu {n = O} {functorM = fm} {monadM = mm} (deltaM (mono x)) = deltaM (mono (mu mm (fmap fm headDeltaM x))) @@ -84,9 +72,9 @@ deltaM-bind : {l : Level} {A B : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} -> + {M : Set l -> Set l} + {functorM : Functor M} + {monadM : Monad M functorM} -> (DeltaM M {functorM} {monadM} A (S n)) -> (A -> DeltaM M {functorM} {monadM} B (S n)) -> DeltaM M {functorM} {monadM} B (S n) diff -r 9fe3d0bd1149 -r 0a3b6cb91a05 agda/deltaM/functor.agda --- a/agda/deltaM/functor.agda Thu Jan 29 11:42:22 2015 +0900 +++ b/agda/deltaM/functor.agda Fri Jan 30 21:57:31 2015 +0900 @@ -14,9 +14,9 @@ deltaM-preserve-id : {l : Level} {A : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - (functorM : {l' : Level} -> Functor {l'} M) - {monadM : {l' : Level} -> Monad {l'} M functorM} + {M : Set l -> Set l} + (functorM : Functor M) + {monadM : Monad M functorM} -> (d : DeltaM M {functorM} {monadM} A (S n)) -> deltaM-fmap id d ≡ id d deltaM-preserve-id functorM (deltaM (mono x)) = begin deltaM-fmap id (deltaM (mono x)) ≡⟨ refl ⟩ @@ -44,9 +44,9 @@ deltaM-covariant : {l : Level} {A B C : Set l} {n : Nat} -> - {M : {l' : Level} -> Set l' -> Set l'} - (functorM : {l' : Level} -> Functor {l'} M) - {monadM : {l' : Level} -> Monad {l'} M functorM} + {M : Set l -> Set l} + (functorM : Functor M) + {monadM : Monad M functorM} (f : B -> C) -> (g : A -> B) -> (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-fmap (f ∙ g)) d ≡ ((deltaM-fmap f) ∙ (deltaM-fmap g)) d deltaM-covariant functorM f g (deltaM (mono x)) = begin @@ -79,12 +79,29 @@ (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) ∎ +postulate deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} + {M : Set l -> Set l} + {functorM : Functor M} + {monadM : Monad M functorM} + {f g : A -> B} + (eq : (x : A) -> f x ≡ g x) + (d : DeltaM M {functorM} {monadM} A (S n)) -> + deltaM-fmap f d ≡ deltaM-fmap g d +{- +deltaM-fmap-equiv {n = O} f g eq (deltaM (mono x)) = begin + {!!} ≡⟨ {!!} ⟩ + {!!} + ∎ +deltaM-fmap-equiv {n = S n} f g eq d = {!!} +-} deltaM-is-functor : {l : Level} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M } - {monadM : {l' : Level} -> Monad {l'} M functorM} + {M : Set l -> Set l} + {functorM : Functor M } + {monadM : Monad M functorM} -> Functor {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) deltaM-is-functor {_} {_} {_} {functorM} = record { fmap = deltaM-fmap ; preserve-id = deltaM-preserve-id functorM ; - covariant = (\f g -> deltaM-covariant functorM g f)} + covariant = (\f g -> deltaM-covariant functorM g f); + fmap-equiv = deltaM-fmap-equiv + } diff -r 9fe3d0bd1149 -r 0a3b6cb91a05 agda/deltaM/monad.agda --- a/agda/deltaM/monad.agda Thu Jan 29 11:42:22 2015 +0900 +++ b/agda/deltaM/monad.agda Fri Jan 30 21:57:31 2015 +0900 @@ -18,13 +18,10 @@ -deltaM-right-unity-law : {l : Level} {A : Set l} - {M : {l' : Level} -> Set l' -> Set l'} - {functorM : {l' : Level} -> Functor {l'} M} - {monadM : {l' : Level} -> Monad {l'} M functorM} - {n : Nat} - (d : DeltaM M {functorM} {monadM} A (S n)) -> - (deltaM-mu ∙ deltaM-eta) d ≡ id d +postulate deltaM-right-unity-law : {l : Level} {A : Set l} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat} + (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d +{- deltaM-right-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ deltaM-mu (deltaM (mono (eta mm (deltaM (mono x))))) ≡⟨ refl ⟩ @@ -39,7 +36,7 @@ ≡⟨ refl ⟩ deltaM-mu (deltaM (delta (eta mm (deltaM (delta x d))) (delta-eta (eta mm (deltaM (delta x d)))))) ≡⟨ refl ⟩ - appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (eta mm (deltaM (delta x d))))))) + appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (eta mm (deltaM (delta x d))))))) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) @@ -49,7 +46,7 @@ ≡⟨ refl ⟩ appendDeltaM (deltaM (mono (mu mm (eta mm x)))) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) - ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) + ≡⟨ cong (\de -> appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d)))))))) (sym (right-unity-law mm x)) ⟩ appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta mm (deltaM (delta x d))))))) ≡⟨ refl ⟩ @@ -67,41 +64,95 @@ ≡⟨ refl ⟩ deltaM (delta x d) ∎ +-} + + +fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} + (x : M A) -> (fmap functorM ((headDeltaM {l} {A} {n} {M} {functorM} {monadM}) ∙ deltaM-eta) x) ≡ fmap functorM (eta monadM) x +fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x = refl +fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x = refl + +fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} + (d : DeltaM M {functorM} {monadM} A (S n)) -> + deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d +fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl +fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl + -{- -deltaM-left-unity-law : {l : Level} {A : Set l} - {M : {l' : Level} -> Set l' -> Set l'} - (functorM : {l' : Level} -> Functor {l'} M) - (monadM : {l' : Level} -> Monad {l'} M functorM) - (d : DeltaM M {functorM} {monadM} A (S O)) -> +deltaM-left-unity-law : {l : Level} {A : Set l} + {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} + {n : Nat} + (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d -deltaM-left-unity-law functorM monadM (deltaM (mono x)) = begin - (deltaM-mu ∙ deltaM-fmap deltaM-eta) (deltaM (mono x)) ≡⟨ refl ⟩ - deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ - deltaM-mu (deltaM (mono (fmap functorM deltaM-eta x))) ≡⟨ refl ⟩ - deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩ - deltaM (mono (mu monadM (fmap functorM headDeltaM (fmap functorM deltaM-eta x)))) ≡⟨ {!!} ⟩ +deltaM-left-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin + deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) + ≡⟨ refl ⟩ + deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (mono x))) + ≡⟨ refl ⟩ + deltaM-mu (deltaM (mono (fmap fm deltaM-eta x))) + ≡⟨ refl ⟩ + deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {O} {M}) (fmap fm deltaM-eta x)))) + ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (covariant fm deltaM-eta headDeltaM x)) ⟩ + deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) ∙ deltaM-eta) x))) + ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x) ⟩ + deltaM (mono (mu mm (fmap fm (eta mm) x))) + ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law mm x) ⟩ + deltaM (mono x) + ∎ +deltaM-left-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin + deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d))) + ≡⟨ refl ⟩ + deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (delta x d))) + ≡⟨ refl ⟩ + deltaM-mu (deltaM (delta (fmap fm deltaM-eta x) (delta-fmap (fmap fm deltaM-eta) d))) + ≡⟨ refl ⟩ + appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {S n} {M} {fm} {mm}) (fmap fm deltaM-eta x))))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) + ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))) + (sym (covariant fm deltaM-eta headDeltaM x)) ⟩ + appendDeltaM (deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {S n} {M} {fm} {mm}) ∙ deltaM-eta) x)))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) + ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))) + (fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x) ⟩ + appendDeltaM (deltaM (mono (mu mm (fmap fm (eta mm) x)))) + (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) - id (deltaM (mono x)) - ∎ -deltaM-left-unity-law functorM monadM (deltaM (delta x ())) --} + ≡⟨ cong (\de -> (appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))))) + (left-unity-law mm x) ⟩ + appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))) + ≡⟨ refl ⟩ + appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap deltaM-eta (deltaM d)))) + ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (sym (covariant deltaM-is-functor deltaM-eta tailDeltaM (deltaM d))) ⟩ + appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ deltaM-eta) (deltaM d))) + ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (fmap-tailDeltaM-with-deltaM-eta (deltaM d)) ⟩ + appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d))) + ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-left-unity-law (deltaM d)) ⟩ + appendDeltaM (deltaM (mono x)) (deltaM d) + ≡⟨ refl ⟩ + deltaM (delta x d) + ∎ + + deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} - {M : {l' : Level} -> Set l' -> Set l'} - (functorM : {l' : Level} -> Functor {l'} M) - (monadM : {l' : Level}-> Monad {l'} M functorM) -> - Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) deltaM-is-functor + {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 = {!!}; + left-unity-law = deltaM-left-unity-law; right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; - eta-is-nt = {!!} + eta-is-nt = {!!} } diff -r 9fe3d0bd1149 -r 0a3b6cb91a05 agda/laws.agda --- a/agda/laws.agda Thu Jan 29 11:42:22 2015 +0900 +++ b/agda/laws.agda Fri Jan 30 21:57:31 2015 +0900 @@ -4,14 +4,15 @@ module laws where -record Functor {l : Level} (F : {l' : Level} -> Set l' -> Set l') : Set (suc l) where +record Functor {l : Level} (F : Set l -> Set l) : Set (suc l) where field fmap : {A B : Set l} -> (A -> B) -> (F A) -> (F B) field preserve-id : {A : Set l} (x : F A) → fmap id x ≡ id x covariant : {A B C : Set l} (f : A -> B) -> (g : B -> C) -> (x : F A) -> fmap (g ∙ f) x ≡ ((fmap g) ∙ (fmap f)) x - + field + fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (x : F A) -> fmap f x ≡ fmap g x open Functor record NaturalTransformation {l : Level} (F G : {l' : Level} -> Set l' -> Set l') @@ -29,8 +30,8 @@ -- simple Monad definition. without NaturalTransformation (mu, eta) and monad-law with f. -record Monad {l : Level} (M : {ll : Level} -> Set ll -> Set ll) - (functorM : Functor {l} M) +record Monad {l : Level} (M : Set l -> Set l) + (functorM : Functor M) : Set (suc l) where field -- category mu : {A : Set l} -> M (M A) -> M A