Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 127:d56596e4e784

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove left-unity-law for DeltaM
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 Feb 2015 12:13:40 +0900
parents 5902b2a24abf
children d9a30f696933
comparison
equal deleted inserted replaced
126:5902b2a24abf 127:d56596e4e784
37 (f : A -> B) -> (d : (DeltaM M A (S (S n)))) -> 37 (f : A -> B) -> (d : (DeltaM M A (S (S n)))) ->
38 (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d 38 (tailDeltaM ∙ (deltaM-fmap f)) d ≡ ((deltaM-fmap f) ∙ tailDeltaM) d
39 tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl 39 tailDeltaM-with-f {n = O} f (deltaM (delta x d)) = refl
40 tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl 40 tailDeltaM-with-f {n = S n} f (deltaM (delta x d)) = refl
41 41
42 42 headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
43 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} 43 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
44 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 44 (x : DeltaM M A (S n)) ->
45 (x : T A) -> (fmap F ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x) ≡ fmap F (eta M) x 45 ((headDeltaM {n = n} {M = M}) ∙ deltaM-eta) x ≡ eta M x
46 fmap-headDeltaM-with-deltaM-eta {n = O} x = refl 46 headDeltaM-with-deltaM-eta {n = O} (deltaM (mono x)) = refl
47 fmap-headDeltaM-with-deltaM-eta {n = S n} x = refl 47 headDeltaM-with-deltaM-eta {n = S n} (deltaM (delta x d)) = refl
48
49 48
50 49
51 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} 50 fmap-tailDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
52 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 51 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
53 (d : DeltaM M A (S n)) -> 52 (d : DeltaM M A (S n)) ->
72 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl 71 fmap-tailDeltaM-with-deltaM-mu {n = O} (deltaM (mono x)) = refl
73 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl 72 fmap-tailDeltaM-with-deltaM-mu {n = S n} (deltaM d) = refl
74 73
75 74
76 75
77 76 {-
78 77
79 -- main proofs 78 -- main proofs
80 79
81 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} 80 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
82 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 81 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
106 105
107 deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} 106 deltaM-mu-is-nt : {l : Level} {A B : Set l} {n : Nat}
108 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} 107 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
109 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) -> 108 (f : A -> B) -> (d : DeltaM M (DeltaM M A (S n)) (S n)) ->
110 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d) 109 deltaM-fmap f (deltaM-mu d) ≡ deltaM-mu (deltaM-fmap (deltaM-fmap f) d)
111 deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = 110 deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = begin
112 {-
113 deltaM-mu-is-nt {l} {A} {B} {O} {T} {F} {M} f (deltaM (mono x)) = begin
114 deltaM-fmap f (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
115 deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono x))))))) ≡⟨ refl ⟩
116 deltaM-fmap f (deltaM (mono (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ refl ⟩
117 deltaM (mono (fmap F f (mu M (fmap F (headDeltaM {M = M}) x)))) ≡⟨ {!!} ⟩
118 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F (deltaM-fmap f) x)))) ≡⟨ refl ⟩
119 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F (deltaM-fmap f) x))))))) ≡⟨ refl ⟩
120 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩
121 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) ≡⟨ refl ⟩
122 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
123 ∎
124 -}
125
126 begin
127 deltaM-fmap f (deltaM-mu (deltaM (mono x))) 111 deltaM-fmap f (deltaM-mu (deltaM (mono x)))
128 ≡⟨ refl ⟩ 112 ≡⟨ refl ⟩
129 deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x)))) 113 deltaM-fmap f (deltaM (mono (mu M (fmap F headDeltaM x))))
130 ≡⟨ refl ⟩ 114 ≡⟨ refl ⟩
131 deltaM (mono (fmap F f (mu M (fmap F headDeltaM x)))) 115 deltaM (mono (fmap F f (mu M (fmap F headDeltaM x))))
142 ≡⟨ refl ⟩ 126 ≡⟨ refl ⟩
143 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x))) 127 deltaM-mu (deltaM (mono (fmap F (deltaM-fmap f) x)))
144 ≡⟨ refl ⟩ 128 ≡⟨ refl ⟩
145 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x))) 129 deltaM-mu (deltaM-fmap (deltaM-fmap f) (deltaM (mono x)))
146 ∎ 130 ∎
147
148 deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin 131 deltaM-mu-is-nt {l} {A} {B} {S n} {T} {F} {M} f (deltaM (delta x d)) = begin
149 deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩ 132 deltaM-fmap f (deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
150 deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d))))) 133 deltaM-fmap f (deltaM (delta (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (delta x d)))))
151 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d)))))))) 134 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta x d))))))))
152 ≡⟨ refl ⟩ 135 ≡⟨ refl ⟩
205 ∎ 188 ∎
206 189
207 190
208 191
209 192
210 {- 193
211 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat} 194 deltaM-right-unity-law : {l : Level} {A : Set l} {n : Nat}
212 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} -> 195 {T : Set l -> Set l} {F : Functor T} {M : Monad T F} ->
213 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d 196 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
214 deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin 197 deltaM-right-unity-law {l} {A} {O} {M} {fm} {mm} (deltaM (mono x)) = begin
215 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩ 198 deltaM-mu (deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
258 ≡⟨ refl ⟩ 241 ≡⟨ refl ⟩
259 deltaM (delta x d) 242 deltaM (delta x d)
260 ∎ 243 ∎
261 244
262 245
263 246 -}
264 247
265 248
266 249
267 postulate deltaM-left-unity-law : {l : Level} {A : Set l} 250 deltaM-left-unity-law : {l : Level} {A : Set l} {n : Nat}
268 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 251 {T : Set l -> Set l} {F : Functor T} {M : Monad T F}
269 {n : Nat} 252 (d : DeltaM M A (S n)) -> (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d
270 (d : DeltaM M {functorM} {monadM} A (S n)) -> 253 deltaM-left-unity-law {l} {A} {O} {T} {F} {M} (deltaM (mono x)) = begin
271 (deltaM-mu ∙ (deltaM-fmap deltaM-eta)) d ≡ id d 254 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x))) ≡⟨ refl ⟩
255 deltaM-mu (deltaM (mono (fmap F deltaM-eta x))) ≡⟨ refl ⟩
256 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (headDeltaM {M = M} (deltaM (mono (fmap F deltaM-eta x))))))) ≡⟨ refl ⟩
257 deltaM (mono (mu M (fmap F (headDeltaM {M = M}) (fmap F deltaM-eta x))))
258 ≡⟨ cong (\de -> deltaM (mono (mu M de))) (sym (covariant F deltaM-eta headDeltaM x)) ⟩
259 deltaM (mono (mu M (fmap F ((headDeltaM {n = O} {M = M}) ∙ deltaM-eta) x)))
260 ≡⟨ refl ⟩
261 deltaM (mono (mu M (fmap F (eta M) x)))
262 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law M x) ⟩
263 deltaM (mono x)
264 ∎
265 deltaM-left-unity-law {l} {A} {S n} {T} {F} {M} (deltaM (delta x d)) = begin
266 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d)))
267 ≡⟨ refl ⟩
268 deltaM-mu (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d)))
269 ≡⟨ refl ⟩
270 deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (headDeltaM {n = S n} {M = M} (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))))))
271 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM (deltaM (delta (fmap F deltaM-eta x) (delta-fmap (fmap F deltaM-eta) d))))))))
272 ≡⟨ refl ⟩
273 deltaM (delta (mu M (fmap F (headDeltaM {n = S n} {M = M}) (fmap F deltaM-eta x)))
274 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
275 ≡⟨ cong (\de -> deltaM (delta (mu M de) (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))))
276 (sym (covariant F deltaM-eta headDeltaM x)) ⟩
277 deltaM (delta (mu M (fmap F ((headDeltaM {n = S n} {M = M}) ∙ deltaM-eta) x))
278 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
279 ≡⟨ refl ⟩
280 deltaM (delta (mu M (fmap F (eta M) x))
281 (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
282 ≡⟨ cong (\de -> deltaM (delta de (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d)))))))
283 (left-unity-law M x) ⟩
284 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap F deltaM-eta) d))))))
285 ≡⟨ refl ⟩
286 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap (deltaM-eta {n = S n})(deltaM d))))))
287 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} (deltaM-mu de)))) (sym (deltaM-covariant tailDeltaM deltaM-eta (deltaM d))) ⟩
288 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ (deltaM-eta {n = S n})) (deltaM d)))))
289 ≡⟨ refl ⟩
290 deltaM (delta x (unDeltaM {M = M} (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d)))))
291 ≡⟨ cong (\de -> deltaM (delta x (unDeltaM {M = M} de))) (deltaM-left-unity-law (deltaM d)) ⟩
292 deltaM (delta x (unDeltaM {M = M} (deltaM d)))
293 ≡⟨ refl ⟩
294 deltaM (delta x d)
295 ∎
296
297
272 {- 298 {-
273 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {O} (deltaM (mono x)) = begin 299
274 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (mono x)))
275 ≡⟨ refl ⟩
276 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (mono x)))
277 ≡⟨ refl ⟩
278 deltaM-mu (deltaM (mono (fmap fm deltaM-eta x)))
279 ≡⟨ refl ⟩
280 deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {O} {M}) (fmap fm deltaM-eta x))))
281 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (covariant fm deltaM-eta headDeltaM x)) ⟩
282 deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) ∙ deltaM-eta) x)))
283 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x) ⟩
284 deltaM (mono (mu mm (fmap fm (eta mm) x)))
285 ≡⟨ cong (\de -> deltaM (mono de)) (left-unity-law mm x) ⟩
286 deltaM (mono x)
287 ∎
288 deltaM-left-unity-law {l} {A} {M} {fm} {mm} {S n} (deltaM (delta x d)) = begin
289 deltaM-mu (deltaM-fmap deltaM-eta (deltaM (delta x d)))
290 ≡⟨ refl ⟩
291 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-eta) (delta x d)))
292 ≡⟨ refl ⟩
293 deltaM-mu (deltaM (delta (fmap fm deltaM-eta x) (delta-fmap (fmap fm deltaM-eta) d)))
294 ≡⟨ refl ⟩
295 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {S n} {M} {fm} {mm}) (fmap fm deltaM-eta x)))))
296 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))
297 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de)))
298 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))))
299 (sym (covariant fm deltaM-eta headDeltaM x)) ⟩
300 appendDeltaM (deltaM (mono (mu mm (fmap fm ((headDeltaM {l} {A} {S n} {M} {fm} {mm}) ∙ deltaM-eta) x))))
301 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))
302 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm de)))
303 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d)))))
304 (fmap-headDeltaM-with-deltaM-eta {l} {A} {S n} {M} {fm} {mm} x) ⟩
305 appendDeltaM (deltaM (mono (mu mm (fmap fm (eta mm) x))))
306 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))
307
308 ≡⟨ cong (\de -> (appendDeltaM (deltaM (mono de)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))))
309 (left-unity-law mm x) ⟩
310 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-eta) d))))
311 ≡⟨ refl ⟩
312 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap (tailDeltaM {n = n})(deltaM-fmap deltaM-eta (deltaM d))))
313 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (sym (covariant deltaM-is-functor deltaM-eta tailDeltaM (deltaM d))) ⟩
314 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap ((tailDeltaM {n = n}) ∙ deltaM-eta) (deltaM d)))
315 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) (deltaM-mu de)) (fmap-tailDeltaM-with-deltaM-eta (deltaM d)) ⟩
316 appendDeltaM (deltaM (mono x)) (deltaM-mu (deltaM-fmap deltaM-eta (deltaM d)))
317 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono x)) de) (deltaM-left-unity-law (deltaM d)) ⟩
318 appendDeltaM (deltaM (mono x)) (deltaM d)
319 ≡⟨ refl ⟩
320 deltaM (delta x d)
321 ∎
322
323 -}
324 postulate nya : {l : Level} {A : Set l} 300 postulate nya : {l : Level} {A : Set l}
325 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) 301 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm)
326 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S O)) (S O)) (S O)) -> 302 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S O)) (S O)) (S O)) ->
327 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) 303 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
328 304