Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 117:6f86b55bf8b4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Temporary commit : Proving association-law ....
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Mon, 02 Feb 2015 09:57:37 +0900
parents f02c5ad4a327
children 53cb21845dea
comparison
equal deleted inserted replaced
116:f02c5ad4a327 117:6f86b55bf8b4
15 open Functor 15 open Functor
16 open NaturalTransformation 16 open NaturalTransformation
17 open Monad 17 open Monad
18 18
19 19
20 -- proof utils
21 deconstruct : {l : Level} {A : Set l} {n : Nat}
22 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
23 (d : DeltaM M {fm} {mm} A (S n)) -> Delta (M A) (S n)
24 deconstruct (deltaM d) = d
25
26
27
20 -- sub proofs 28 -- sub proofs
29
30 deconstruct-id : {l : Level} {A : Set l} {n : Nat}
31 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
32 (d : DeltaM M {fm} {mm} A (S n)) -> deltaM (deconstruct d) ≡ d
33 deconstruct-id {n = O} (deltaM x) = refl
34 deconstruct-id {n = S n} (deltaM x) = refl
35
36
37 headDeltaM-with-appendDeltaM : {l : Level} {A : Set l} {n m : Nat}
38 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
39 (d : DeltaM M {fm} {mm} A (S n)) -> (ds : DeltaM M {fm} {mm} A (S m)) ->
40 headDeltaM (appendDeltaM d ds) ≡ headDeltaM d
41 headDeltaM-with-appendDeltaM {l} {A} {n = O} {O} (deltaM (mono _)) (deltaM _) = refl
42 headDeltaM-with-appendDeltaM {l} {A} {n = O} {S m} (deltaM (mono _)) (deltaM _) = refl
43 headDeltaM-with-appendDeltaM {l} {A} {n = S n} {O} (deltaM (delta _ _)) (deltaM _) = refl
44 headDeltaM-with-appendDeltaM {l} {A} {n = S n} {S m} (deltaM (delta _ _)) (deltaM _) = refl
21 45
22 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat} 46 fmap-headDeltaM-with-deltaM-eta : {l : Level} {A : Set l} {n : Nat}
23 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 47 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
24 (x : M A) -> (fmap functorM ((headDeltaM {l} {A} {n} {M} {functorM} {monadM}) ∙ deltaM-eta) x) ≡ fmap functorM (eta monadM) x 48 (x : M A) -> (fmap functorM ((headDeltaM {l} {A} {n} {M} {functorM} {monadM}) ∙ deltaM-eta) x) ≡ fmap functorM (eta monadM) x
25 fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x = refl 49 fmap-headDeltaM-with-deltaM-eta {l} {A} {O} {M} {fm} {mm} x = refl
30 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 54 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
31 (d : DeltaM M {functorM} {monadM} A (S n)) -> 55 (d : DeltaM M {functorM} {monadM} A (S n)) ->
32 deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d 56 deltaM-fmap ((tailDeltaM {n = n} {monadM = monadM} ) ∙ deltaM-eta) d ≡ deltaM-fmap (deltaM-eta) d
33 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl 57 fmap-tailDeltaM-with-deltaM-eta {n = O} d = refl
34 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl 58 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
59
60
61 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
62 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
63 (x : M (DeltaM M {fm} {mm} (DeltaM M A (S n)) (S n))) ->
64 fmap fm (headDeltaM ∙ deltaM-mu) x ≡ fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x
65 fmap-headDeltaM-with-deltaM-mu {l} {A} {O} {M} {fm} {mm} x = refl
66 fmap-headDeltaM-with-deltaM-mu {l} {A} {S n} {M} {fm} {mm} x = begin
67 fmap fm (headDeltaM ∙ deltaM-mu) x ≡⟨ refl ⟩
68 fmap fm (headDeltaM ∙ (\d -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))))
69 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))))) x ≡⟨ refl ⟩
70 fmap fm (\d -> headDeltaM (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))))
71 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))))) x
72 ≡⟨ refl ⟩
73 fmap fm (\d -> headDeltaM (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))))
74 (deltaM (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM d))))))) x
75 ≡⟨ {!!} ⟩
76 fmap fm (\d -> headDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM d)))))) x ≡⟨ refl ⟩
77 fmap fm (\d -> (mu mm (fmap fm headDeltaM (headDeltaM d)))) x ≡⟨ {!!} ⟩
78 fmap fm (((mu mm) ∙ (fmap fm headDeltaM)) ∙ headDeltaM) x
79 ∎
80
35 81
36 82
37 -- main proofs 83 -- main proofs
38 84
39 postulate deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} 85 postulate deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
166 ≡⟨ refl ⟩ 212 ≡⟨ refl ⟩
167 deltaM (delta x d) 213 deltaM (delta x d)
168 ∎ 214 ∎
169 215
170 -} 216 -}
171 217 postulate nya : {l : Level} {A : Set l}
172 218 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm)
173 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat} 219 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S O)) (S O)) (S O)) ->
174 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm} 220 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
175 (x : M (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n))) -> 221
176 -- (fmap fm headDeltaM (fmap fm deltaM-mu x)) ≡ (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))) 222
177 -- fmap fm (headDeltaM ∙ deltaM-mu) x ≡ fmap fm (fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) x 223
178 headDeltaM (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡ deltaM (mono (mu mm (fmap fm headDeltaM x))) 224
179 fmap-headDeltaM-with-deltaM-mu {l} {A} {O} {M} {fm} {mm} x = {!!} 225
180 fmap-headDeltaM-with-deltaM-mu {n = S n} x = {!!}
181
182 deltaM-mono : {l : Level} {A : Set l}
183 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
184 (d : M A) -> DeltaM M {fm} {mm} A (S O)
185 deltaM-mono x = deltaM (mono x)
186
187 fmap-headDeltaM-with-deltaM-mono : {l : Level} {A : Set l}
188 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
189 (x : M (M A)) ->
190 fmap fm ((headDeltaM {l} {A} {O} {M} {fm} {mm}) ∙ deltaM-mono) x ≡ x
191 fmap-headDeltaM-with-deltaM-mono {fm = fm} x = preserve-id fm x
192
193
194 226
195 227
196 deltaM-association-law : {l : Level} {A : Set l} {n : Nat} 228 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
197 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) 229 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm)
198 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n)) (S n)) -> 230 (d : DeltaM M {fm} {mm} (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n)) (S n)) ->
199 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d) 231 deltaM-mu (deltaM-fmap deltaM-mu d) ≡ deltaM-mu (deltaM-mu d)
200 deltaM-association-law {l} {A} {O} M fm mm (deltaM (mono x)) = begin 232 deltaM-association-law {l} {A} {O} M fm mm (deltaM (mono x)) = nya {l} {A} M fm mm (deltaM (mono x))
233 {-
234 begin
201 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ 235 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
202 deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩ 236 deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩
203 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (fmap fm deltaM-mu x))))))) ≡⟨ refl ⟩ 237 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (fmap fm deltaM-mu x))))))) ≡⟨ refl ⟩
204 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩ 238 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩
205 deltaM (mono (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm 239 deltaM (mono (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm
228 deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))) ≡⟨ refl ⟩ 262 deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))) ≡⟨ refl ⟩
229 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM x)))))))) ≡⟨ refl ⟩ 263 deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M A (S O)} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM x)))))))) ≡⟨ refl ⟩
230 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩ 264 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩
231 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M (DeltaM M A (S O)) (S O)} {monadM = mm} (deltaM (mono x))))))) ≡⟨ refl ⟩ 265 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM {A = DeltaM M (DeltaM M A (S O)) (S O)} {monadM = mm} (deltaM (mono x))))))) ≡⟨ refl ⟩
232 deltaM-mu (deltaM-mu (deltaM (mono x))) ∎ 266 deltaM-mu (deltaM-mu (deltaM (mono x))) ∎
233 267 -}
234 deltaM-association-law {n = S n} M fm mm (deltaM (delta x d)) = begin 268 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = {!!}
269 {-
270 deltaM-association-law {l} {A} {S n} M fm mm (deltaM (delta x d)) = begin
235 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩ 271 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
236 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩ 272 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩
237 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩ 273 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩
238 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) 274 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
239 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ {!!} ⟩ 275 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ refl ⟩
240 276 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
277 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))
278 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) de)
279 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d)))))) ⟩
280
281 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
282 (deltaM (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
283 ≡⟨ refl ⟩
284 deltaM (deltaAppend (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))
285 (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
286 ≡⟨ refl ⟩
287 deltaM (delta (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))
288 (deconstruct {A = A} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) (delta-fmap (fmap fm deltaM-mu) d))))))
289 ≡⟨ {!!} ⟩
241 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))))) 290 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
242 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ≡⟨ {!!} ⟩ 291 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))
292 ≡⟨ cong (\de -> appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
293 (deltaM-mu (deltaM-fmap tailDeltaM de)))
294 (sym (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))) ⟩
295 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
296 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))))))
297
298 ≡⟨ refl ⟩
299 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
300 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ( (deltaM (delta (mu mm (fmap fm headDeltaM x))
301 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))
302 ≡⟨ refl ⟩
303 appendDeltaM (deltaM (mono (mu mm (fmap fm (headDeltaM {monadM = mm}) (headDeltaM {monadM = mm} ((deltaM (delta (mu mm (fmap fm headDeltaM x))
304 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))))
305 (deltaM-mu (deltaM-fmap tailDeltaM (tailDeltaM ( (deltaM (delta (mu mm (fmap fm headDeltaM x))
306 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))))))
307 ≡⟨ refl ⟩
308 deltaM-mu (deltaM (delta (mu mm (fmap fm headDeltaM x))
309 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
310 ≡⟨ refl ⟩
311 deltaM-mu (deltaM (deltaAppend (mono (mu mm (fmap fm headDeltaM x)))
312 (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
313 ≡⟨ refl ⟩
314 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
315 (deltaM (deconstruct {A = DeltaM M A (S (S n))} {mm = mm} (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))))
316 ≡⟨ cong (\de -> deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) de))
317 (deconstruct-id (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d)))) ⟩
318 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
319 (deltaM-mu (deltaM (delta-fmap (fmap fm tailDeltaM) d))))
320 ≡⟨ refl ⟩
243 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x)))) 321 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
244 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩ 322 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩
245 deltaM-mu (deltaM-mu (deltaM (delta x d))) 323 deltaM-mu (deltaM-mu (deltaM (delta x d)))
246 ∎ 324 ∎
247 325 -}
248 326
249 327
250 328
251 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} 329 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
252 {M : Set l -> Set l} 330 {M : Set l -> Set l}
259 return = deltaM-eta; 337 return = deltaM-eta;
260 bind = deltaM-bind; 338 bind = deltaM-bind;
261 association-law = (deltaM-association-law M functorM monadM) ; 339 association-law = (deltaM-association-law M functorM monadM) ;
262 left-unity-law = deltaM-left-unity-law; 340 left-unity-law = deltaM-left-unity-law;
263 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; 341 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ;
264 eta-is-nt = deltaM-eta-is-nt } 342 eta-is-nt = deltaM-eta-is-nt;
265 343 mu-is-nt = {!!}}
266 344
345