Mercurial > hg > Members > atton > delta_monad

comparison agda/deltaM/monad.agda @ 115:e6bcc7467335

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 Sun, 01 Feb 2015 17:06:55 +0900
parents 08403eb8db8b
children f02c5ad4a327
comparison
equal deleted inserted replaced
114:08403eb8db8b 115:e6bcc7467335
34 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl 34 fmap-tailDeltaM-with-deltaM-eta {n = S n} d = refl
35 35
36 36
37 -- main proofs 37 -- main proofs
38 38
39 deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat} 39 postulate deltaM-eta-is-nt : {l : Level} {A B : Set l} {n : Nat}
40 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} 40 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM}
41 (f : A -> B) -> (x : A) -> 41 (f : A -> B) -> (x : A) ->
42 ((deltaM-eta {l} {B} {n} {M} {functorM} {monadM} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x) 42 ((deltaM-eta {l} {B} {n} {M} {functorM} {monadM} )∙ f) x ≡ deltaM-fmap f (deltaM-eta x)
43 {-
43 deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin 44 deltaM-eta-is-nt {l} {A} {B} {O} {M} {fm} {mm} f x = begin
44 deltaM-eta {n = O} (f x) ≡⟨ refl ⟩ 45 deltaM-eta {n = O} (f x) ≡⟨ refl ⟩
45 deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩ 46 deltaM (mono (eta mm (f x))) ≡⟨ cong (\de -> deltaM (mono de)) (eta-is-nt mm f x) ⟩
46 deltaM (mono (fmap fm f (eta mm x))) ≡⟨ refl ⟩ 47 deltaM (mono (fmap fm f (eta mm x))) ≡⟨ refl ⟩
47 deltaM-fmap f (deltaM-eta {n = O} x) ∎ 48 deltaM-fmap f (deltaM-eta {n = O} x) ∎
54 ≡⟨ cong (\de -> deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩ 55 ≡⟨ cong (\de -> deltaM (delta (fmap fm f (eta mm x)) de)) (eta-is-nt delta-is-monad (fmap fm f) (eta mm x)) ⟩
55 deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x)))) 56 deltaM (delta (fmap fm f (eta mm x)) (delta-fmap (fmap fm f) (delta-eta (eta mm x))))
56 ≡⟨ refl ⟩ 57 ≡⟨ refl ⟩
57 deltaM-fmap f (deltaM-eta {n = S n} x) 58 deltaM-fmap f (deltaM-eta {n = S n} x)
58 ∎ 59 ∎
60 -}
59 61
60 postulate deltaM-right-unity-law : {l : Level} {A : Set l} 62 postulate deltaM-right-unity-law : {l : Level} {A : Set l}
61 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat} 63 {M : Set l -> Set l} {functorM : Functor M} {monadM : Monad M functorM} {n : Nat}
62 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d 64 (d : DeltaM M {functorM} {monadM} A (S n)) -> (deltaM-mu ∙ deltaM-eta) d ≡ id d
63 {- 65 {-
166 ∎ 168 ∎
167 169
168 -} 170 -}
169 171
170 172
173 fmap-headDeltaM-with-deltaM-mu : {l : Level} {A : Set l} {n : Nat}
174 {M : Set l -> Set l} {fm : Functor M} {mm : Monad M fm}
175 (x : M (DeltaM M {fm} {mm} (DeltaM M {fm} {mm} A (S n)) (S n))) ->
176 -- (fmap fm headDeltaM (fmap fm deltaM-mu x)) ≡ (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x)))
177 -- fmap fm (headDeltaM ∙ deltaM-mu) x ≡ fmap fm (fmap fm ((mu mm) ∙ (fmap fm headDeltaM))) x
178 headDeltaM (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡ deltaM (mono (mu mm (fmap fm headDeltaM x)))
179 fmap-headDeltaM-with-deltaM-mu {l} {A} {O} {M} {fm} {mm} x = {!!}
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
195
196 deltaM-association-law : {l : Level} {A : Set l} {n : Nat}
197 (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)) ->
199 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
201 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
202 deltaM-mu (deltaM (mono (fmap fm deltaM-mu x))) ≡⟨ refl ⟩
203 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩
204 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (\x -> (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩
205
206 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (\x -> (deltaM-mono (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) ≡⟨ refl ⟩
207 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (deltaM-mono ∙ (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) ≡⟨ refl ⟩
208 deltaM (mono (mu mm (fmap fm headDeltaM (((fmap fm (deltaM-mono)) ∙ (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩
209 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mono (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x)))))
210 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (covariant fm deltaM-mu headDeltaM x )) ⟩
211
212 deltaM (mono (mu mm (fmap fm (headDeltaM ∙ deltaM-mono) ((fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x))))
213 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-mono ((fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)) ⟩
214
215 deltaM (mono (mu mm (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))) ≡⟨ refl ⟩
216
217
218
219 {-
220 {!!}
221
222
223
224 deltaM (mono (mu mm (fmap fm (headDeltaM) (fmap fm
225 (\x -> ((deltaM (mono (mu mm (fmap fm (headDeltaM {l} {A} {O} {M} {fm} {mm} )(headDeltaM {l} {DeltaM M {fm} {mm} A (S O)} {O} {M} {fm} {mm} x))))))) x)))) ≡⟨ refl ⟩
226 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (\x -> ((deltaM-mono (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩
227
228 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (deltaM-mono ∙ (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) ≡⟨ refl ⟩
229 deltaM (mono (mu mm (fmap fm headDeltaM (((fmap fm deltaM-mono) ∙ (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩
230 deltaM (mono (mu mm (fmap fm headDeltaM (((fmap fm deltaM-mono (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))))))) ≡⟨ refl ⟩
231 deltaM (mono (mu mm (fmap fm (headDeltaM ∙ deltaM-mono) (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))))
232 ≡⟨ {!!} ⟩
233 -- ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (fmap-headDeltaM-with-deltaM-eta (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x)) ⟩
234 -}
235 deltaM (mono (mu mm (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))) ≡⟨ refl ⟩
236 deltaM (mono (mu mm (fmap fm ((mu mm) ∙ (\x -> (fmap fm headDeltaM (headDeltaM x)))) x))) ≡⟨ refl ⟩
237 deltaM (mono (mu mm (fmap fm ((mu mm) ∙ ((fmap fm headDeltaM) ∙ headDeltaM)) x)))
238 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (covariant fm ((fmap fm headDeltaM) ∙ headDeltaM) (mu mm) x) ⟩
239 deltaM (mono (mu mm (((fmap fm (mu mm)) ∙ (fmap fm ((fmap fm headDeltaM) ∙ headDeltaM))) x)))
240 ≡⟨ refl ⟩
241 deltaM (mono (mu mm (fmap fm (mu mm) ((fmap fm ((fmap fm headDeltaM) ∙ headDeltaM) x))) ))
242 ≡⟨ cong (\de -> deltaM (mono (mu mm (fmap fm (mu mm) de)))) (covariant fm headDeltaM (fmap fm headDeltaM) x) ⟩
243 deltaM (mono (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x)))))
244 ≡⟨ cong (\de -> deltaM (mono de)) (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩
245 deltaM (mono (mu mm (mu mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x)))))
246 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (mu-is-nt mm headDeltaM (fmap fm headDeltaM x)) ⟩
247 deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))) ≡⟨ refl ⟩
248 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩
249 deltaM-mu (deltaM-mu (deltaM (mono x)))
250 ∎
251 deltaM-association-law {n = S n} M fm mm (deltaM (delta x d)) = begin
252 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (delta x d))) ≡⟨ refl ⟩
253 deltaM-mu (deltaM (delta-fmap (fmap fm deltaM-mu) (delta x d))) ≡⟨ refl ⟩
254 deltaM-mu (deltaM (delta (fmap fm deltaM-mu x) (delta-fmap (fmap fm deltaM-mu) d))) ≡⟨ refl ⟩
255 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))))
256 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM (delta-fmap (fmap fm deltaM-mu) d)))) ≡⟨ {!!} ⟩
257
258 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (mu mm (fmap fm headDeltaM x))))))
259 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))) ≡⟨ {!!} ⟩
260 deltaM-mu (appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM x))))
261 (deltaM-mu (deltaM-fmap tailDeltaM (deltaM d))))≡⟨ refl ⟩
262 deltaM-mu (deltaM-mu (deltaM (delta x d)))
263 ∎
264
265
266
171 267
172 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat} 268 deltaM-is-monad : {l : Level} {A : Set l} {n : Nat}
173 {M : Set l -> Set l} 269 {M : Set l -> Set l}
174 (functorM : Functor M) 270 (functorM : Functor M)
175 (monadM : Monad M functorM) -> 271 (monadM : Monad M functorM) ->
176 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n}) 272 Monad {l} (\A -> DeltaM M {functorM} {monadM} A (S n)) (deltaM-is-functor {l} {n})
177 deltaM-is-monad functorM monadM = record 273 deltaM-is-monad {l} {A} {n} {M} functorM monadM =
178 { mu = deltaM-mu; 274 record { mu = deltaM-mu;
179 eta = deltaM-eta; 275 eta = deltaM-eta;
180 return = deltaM-eta; 276 return = deltaM-eta;
181 bind = deltaM-bind; 277 bind = deltaM-bind;
182 association-law = {!!}; 278 association-law = (deltaM-association-law M functorM monadM) ;
183 left-unity-law = deltaM-left-unity-law; 279 left-unity-law = deltaM-left-unity-law;
184 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ; 280 right-unity-law = (\x -> (sym (deltaM-right-unity-law x))) ;
185 eta-is-nt = deltaM-eta-is-nt 281 eta-is-nt = deltaM-eta-is-nt }
186 } 282
187 283
188
189
190
191
192
193 {-
194 deltaM-association-law : {l : Level} {A : Set l}
195 {M : {l' : Level} -> Set l' -> Set l'}
196 (functorM : {l' : Level} -> Functor {l'} M)
197 (monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM)
198 -> (d : DeltaM M (DeltaM M (DeltaM M {functorM} {monadM} A)))
199 -> ((deltaM-mu ∙ (deltaM-fmap deltaM-mu)) d) ≡ ((deltaM-mu ∙ deltaM-mu) d)
200 deltaM-association-law functorM monadM (deltaM (mono x)) = begin
201 (deltaM-mu ∙ deltaM-fmap deltaM-mu) (deltaM (mono x)) ≡⟨ refl ⟩
202 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
203 deltaM-mu (deltaM (delta-fmap (fmap functorM deltaM-mu) (mono x))) ≡⟨ {!!} ⟩
204 deltaM-mu (deltaM (mono (bind monadM x headDeltaM))) ≡⟨ refl ⟩
205 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
206 deltaM-mu (deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩
207 (deltaM-mu ∙ deltaM-mu) (deltaM (mono x)) ∎
208 deltaM-association-law functorM monadM (deltaM (delta x d)) = {!!}
209 -}
210
211 {-
212
213 nya : {l : Level} {A B C : Set l} ->
214 {M : {l' : Level} -> Set l' -> Set l'}
215 {functorM : {l' : Level} -> Functor {l'} M }
216 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
217 (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M {functorM} {monadM} B)) -> (g : B -> (DeltaM M C)) ->
218 (x : M A) ->
219 (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡
220 (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g)
221 nya = {!!}
222
223 deltaM-monad-law-h-3 : {l : Level} {A B C : Set l} ->
224 {M : {l' : Level} -> Set l' -> Set l'}
225 {functorM : {l' : Level} -> Functor {l'} M }
226 {monadM : {l' : Level} {A : Set l'} -> Monad {l'} {A} M functorM}
227 (m : DeltaM M {functorM} {monadM} A) -> (f : A -> (DeltaM M B)) -> (g : B -> (DeltaM M C)) ->
228 (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡ (deltaM-bind (deltaM-bind m f) g)
229 {-
230 deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin
231 (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩
232
233 (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩
234 (deltaM-bind (deltaM (fmap delta-is-functor (\x -> (bind {l} {A} monadM x (headDeltaM ∙ f))) (mono x))) g) ≡⟨ refl ⟩
235 (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩
236 (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g) ∎
237 -}
238
239 deltaM-monad-law-h-3 {l} {A} {B} {C} {M} {functorM} {monadM} (deltaM (mono x)) f g = begin
240 (deltaM-bind (deltaM (mono x)) (\x -> deltaM-bind (f x) g)) ≡⟨ refl ⟩
241 (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))))) ≡⟨ {!!} ⟩
242 -- (deltaM (fmap delta-is-functor (\x -> bind {l} {A} monadM x (headDeltaM ∙ (\x -> deltaM-bind (f x) g))) (mono x))) ≡⟨ {!!} ⟩
243 deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩
244 deltaM (mono (bind {l} {B} monadM (bind {_} {A} monadM x (headDeltaM ∙ f)) (headDeltaM ∙ g))) ≡⟨ {!!} ⟩
245 (deltaM-bind (deltaM (mono (bind {l} {A} monadM x (headDeltaM ∙ f)))) g) ≡⟨ refl ⟩
246 (deltaM-bind (deltaM-bind (deltaM (mono x)) f) g)
247 ∎
248 deltaM-monad-law-h-3 (deltaM (delta x d)) f g = {!!}
249 {-
250 begin
251 (deltaM-bind m (\x -> deltaM-bind (f x) g)) ≡⟨ {!!} ⟩
252 (deltaM-bind (deltaM-bind m f) g)
253 ∎
254 -}
255 -}