Mercurial > hg > Members > atton > delta_monad
changeset 126:5902b2a24abf
Prove mu-is-nt for DeltaM with fmap-equiv
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 03 Feb 2015 11:45:33 +0900 |
| parents | 6dcc68ef8f96 |
| children | d56596e4e784 |
| files | agda/delta/functor.agda agda/deltaM.agda agda/deltaM/functor.agda agda/deltaM/monad.agda agda/laws.agda |
| diffstat | 5 files changed, 140 insertions(+), 19 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/delta/functor.agda Mon Feb 02 14:09:30 2015 +0900 +++ b/agda/delta/functor.agda Tue Feb 03 11:45:33 2015 +0900 @@ -24,9 +24,24 @@ 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 {l} {A} {B} {O} {f} {g} eq (mono x) = begin + mono (f x) ≡⟨ cong mono (eq x) ⟩ + mono (g x) + ∎ +delta-fmap-equiv {l} {A} {B} {S n} {f} {g} eq (delta x d) = begin + delta (f x) (delta-fmap f d) ≡⟨ cong (\de -> delta de (delta-fmap f d)) (eq x) ⟩ + delta (g x) (delta-fmap f d) ≡⟨ cong (\de -> delta (g x) de) (delta-fmap-equiv 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 - } +delta-is-functor = record { fmap = delta-fmap + ;preserve-id = functor-law-1 + ; covariant = \f g -> functor-law-2 g f + ; fmap-equiv = delta-fmap-equiv + }
--- a/agda/deltaM.agda Mon Feb 02 14:09:30 2015 +0900 +++ b/agda/deltaM.agda Tue Feb 03 11:45:33 2015 +0900 @@ -57,7 +57,7 @@ deltaM-fmap : {l : Level} {A B : Set l} {n : Nat} {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> (A -> B) -> DeltaM M A (S n) -> DeltaM M B (S n) -deltaM-fmap {l} {A} {B} {n} {M} {functorM} f (deltaM d) = deltaM (fmap delta-is-functor (fmap functorM f) d) +deltaM-fmap {l} {A} {B} {n} {M} {functorM} f d = deltaM (fmap delta-is-functor (fmap functorM f) (unDeltaM d))
--- a/agda/deltaM/functor.agda Mon Feb 02 14:09:30 2015 +0900 +++ b/agda/deltaM/functor.agda Tue Feb 03 11:45:33 2015 +0900 @@ -75,6 +75,25 @@ (deltaM-fmap f ∙ deltaM-fmap g) (deltaM (delta x d)) ∎ +deltaM-fmap-equiv : {l : Level} {A B : Set l} {n : Nat} + {T : Set l -> Set l} {F : Functor T} {M : Monad T F} + {f g : A -> B} + (eq : (x : A) -> f x ≡ g x) -> (d : DeltaM M A (S n)) -> + deltaM-fmap f d ≡ deltaM-fmap g d +deltaM-fmap-equiv {l} {A} {B} {O} {T} {F} {M} {f} {g} eq (deltaM (mono x)) = begin + deltaM-fmap f (deltaM (mono x)) ≡⟨ refl ⟩ + deltaM (mono (fmap F f x)) ≡⟨ cong (\de -> deltaM (mono de)) (fmap-equiv F eq x) ⟩ + deltaM (mono (fmap F g x)) ≡⟨ refl ⟩ + deltaM-fmap g (deltaM (mono x)) + ∎ +deltaM-fmap-equiv {l} {A} {B} {S n} {T} {F} {M} {f} {g} eq (deltaM (delta x d)) = begin + deltaM-fmap f (deltaM (delta x d)) ≡⟨ refl ⟩ + deltaM (delta (fmap F f x) (delta-fmap (fmap F f) d)) ≡⟨ cong (\de -> deltaM (delta de (delta-fmap (fmap F f) d))) (fmap-equiv F eq x) ⟩ + deltaM (delta (fmap F g x) (delta-fmap (fmap F f) d)) ≡⟨ cong (\de -> deltaM (delta (fmap F g x) de)) (delta-fmap-equiv (fmap-equiv F eq) d) ⟩ + deltaM (delta (fmap F g x) (delta-fmap (fmap F g) d)) ≡⟨ refl ⟩ + deltaM-fmap g (deltaM (delta x d)) + ∎ + deltaM-is-functor : {l : Level} {n : Nat} @@ -83,6 +102,7 @@ deltaM-is-functor {F = F} = record { fmap = deltaM-fmap ; preserve-id = deltaM-preserve-id {F = F} ; covariant = (\f g -> deltaM-covariant {F = F} g f) + ; fmap-equiv = deltaM-fmap-equiv }
--- a/agda/deltaM/monad.agda Mon Feb 02 14:09:30 2015 +0900 +++ b/agda/deltaM/monad.agda Tue Feb 03 11:45:33 2015 +0900 @@ -25,6 +25,19 @@ deconstruct-id {n = O} (deltaM x) = refl deconstruct-id {n = S n} (deltaM x) = refl +headDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} + {T : Set l -> Set l} {F : Functor T} {M : Monad T F} + (f : A -> B) -> (x : (DeltaM M A (S n))) -> + ((fmap F f) ∙ headDeltaM) x ≡ (headDeltaM ∙ (deltaM-fmap f)) x +headDeltaM-with-f {n = O} f (deltaM (mono x)) = refl +headDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl + +tailDeltaM-with-f : {l : Level} {A B : Set l} {n : Nat} + {T : Set l -> Set l} {F : Functor T} {M : Monad T F} + (f : A -> B) -> (d : (DeltaM M A (S (S n)))) -> + (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d +tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl +tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} @@ -91,12 +104,26 @@ -postulate deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} +deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} {T : Set l -> Set l} {F : Functor T} {M : Monad T F} (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) -> deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d) +deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = {- deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = begin + deltaM-fmap f (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ + deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) ≡⟨ refl ⟩ + deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ refl ⟩ + deltaM (mono (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ {!!} ⟩ + deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) ≡⟨ refl ⟩ + deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩ + deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩ + deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x))) + ∎ +-} + + begin deltaM-fmap f (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x)))) @@ -104,26 +131,83 @@ deltaM (mono (fmap F f (mu M (fmap F headDeltaM x)))) ≡⟨ cong (\de -> deltaM (mono de)) (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩ deltaM (mono (mu M (fmap F (fmap F f) (fmap F headDeltaM x)))) - ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩ + ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F headDeltaM (fmap F f) x)) ⟩ deltaM (mono (mu M (fmap F ((fmap F f) ∙ headDeltaM) x))) - ≡⟨ {!!} ⟩ - deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))) - ≡⟨ {!!} ⟩ + ≡⟨ cong (\de -> deltaM (mono (mu M de))) (fmap-equiv F (headDeltaM-with-f f) x) ⟩ deltaM (mono (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x))) ≡⟨ cong (\de -> deltaM (mono (mu M de))) (covariant F (deltaM-fmap f) (headDeltaM) x) ⟩ - deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) + deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) ≡⟨ refl ⟩ - deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) - ≡⟨ refl ⟩ + deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) + ≡⟨ refl ⟩ deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩ deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x))) ∎ -deltaM-mu-is-nt {n = S n} f (deltaM (delta x d)) = {!!} --} +deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin + deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩ + deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d))))) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d)))))))) + ≡⟨ refl ⟩ + deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ refl ⟩ + deltaM (delta (fmap F f (mu M (fmap F (headDeltaM {M = M}) x))) + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta de + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) + (sym (mu-is-nt M f (fmap F headDeltaM x))) ⟩ + deltaM (delta (mu M (fmap F (fmap F f) (fmap F (headDeltaM {M = M}) x))) + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) + (sym (covariant F headDeltaM (fmap F f) x)) ⟩ + deltaM (delta (mu M (fmap F ((fmap F f) ∙ (headDeltaM {M = M})) x)) + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M de) (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))))) + (fmap-equiv F (headDeltaM-with-f f) x) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (delta-fmap (fmap F f) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ refl ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-fmap f (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM de))) + (deltaM-mu-is-nt {l} {A} {B} {n} {T} {F} {M} f (deltaM-fmap tailDeltaM (deltaM d))) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (deltaM-fmap {n = n} f) (deltaM-fmap {n = n} (tailDeltaM {n = n}) (deltaM d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) + (sym (deltaM-covariant (deltaM-fmap f) tailDeltaM (deltaM d))) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap {n = n} ((deltaM-fmap {n = n} f) ∙ (tailDeltaM {n = n})) (deltaM d))))) + + ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) + (sym (deltaM-fmap-equiv (tailDeltaM-with-f f) (deltaM d))) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM ∙ (deltaM-fmap f)) (deltaM d))))) + ≡⟨ cong (\de -> deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) (unDeltaM {M = M} (deltaM-mu de)))) + (deltaM-covariant tailDeltaM (deltaM-fmap f) (deltaM d)) ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-fmap (deltaM-fmap f) (deltaM d)))))) + ≡⟨ refl ⟩ + deltaM (delta (mu M (fmap F ((headDeltaM {M = M}) ∙ (deltaM-fmap f)) x)) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))) + ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d))))))) + (covariant F (deltaM-fmap f) headDeltaM x) ⟩ + deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x))) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F (deltaM-fmap f)) d)))))) + ≡⟨ refl ⟩ + deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))))) + (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d)))))))) + ≡⟨ refl ⟩ + deltaM-mu (deltaM (delta (fmap F (deltaM-fmap f) x) (delta-fmap (fmap F (deltaM-fmap f)) d))) + ≡⟨ refl ⟩ + deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (delta x d))) + ∎ + + +{- deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat} {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d @@ -154,10 +238,10 @@ ≡⟨ refl ⟩ deltaM (delta (mu M (eta M x)) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) - ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))) + ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d)))))))))) (sym (right-unity-law M x)) ⟩ deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-eta (eta M (deltaM (delta x d))))))))) - ≡⟨ refl ⟩ + ≡⟨ refl ⟩ deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM (delta-fmap (fmap F tailDeltaM) (delta-eta (eta M (deltaM (delta x d))))))))) ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM de))))) (sym (delta-eta-is-nt (fmap F tailDeltaM) (eta M (deltaM (delta x d))))) ⟩ @@ -177,7 +261,7 @@ -{- + postulate deltaM-left-unity-law : {l : Level} {A : Set l}
--- a/agda/laws.agda Mon Feb 02 14:09:30 2015 +0900 +++ b/agda/laws.agda Tue Feb 03 11:45:33 2015 +0900 @@ -7,10 +7,12 @@ 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 + field -- laws 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 -- proof assistant + fmap-equiv : {A B : Set l} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> (fx : F A) -> fmap f fx ≡ fmap g fx open Functor record NaturalTransformation {l : Level} (F G : Set l -> Set l)