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)