Mercurial > hg > Members > atton > delta_monad
comparison agda/deltaM/monad.agda @ 116:f02c5ad4a327
Prove association-law for DeltaM by (S O) pattern with definition changes
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 01 Feb 2015 17:55:39 +0900 |
parents | e6bcc7467335 |
children | 6f86b55bf8b4 |
comparison
equal
deleted
inserted
replaced
115:e6bcc7467335 | 116:f02c5ad4a327 |
---|---|
197 (M : Set l -> Set l) (fm : Functor M) (mm : Monad M fm) | 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)) -> | 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) | 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 | 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 ⟩ | 201 deltaM-mu (deltaM-fmap deltaM-mu (deltaM (mono x))) ≡⟨ refl ⟩ |
202 deltaM-mu (deltaM (mono (fmap fm deltaM-mu 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 ⟩ | 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 ⟩ |
204 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (\x -> (deltaM (mono (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩ | 204 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x)))) ≡⟨ refl ⟩ |
205 | 205 deltaM (mono (mu mm (fmap fm (headDeltaM {A = A} {monadM = mm}) (fmap fm |
206 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (\x -> (deltaM-mono (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) ≡⟨ refl ⟩ | 206 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) x)))) |
207 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm (deltaM-mono ∙ (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) ≡⟨ refl ⟩ | 207 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) |
208 deltaM (mono (mu mm (fmap fm headDeltaM (((fmap fm (deltaM-mono)) ∙ (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))))) x)))) ≡⟨ refl ⟩ | 208 (sym (covariant fm (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))))) headDeltaM x)) ⟩ |
209 deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mono (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))))) | 209 deltaM (mono (mu mm (fmap fm ((headDeltaM {A = A} {monadM = mm}) ∙ |
210 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (sym (covariant fm deltaM-mu headDeltaM x )) ⟩ | 210 (\d -> (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) x))) |
211 | 211 ≡⟨ refl ⟩ |
212 deltaM (mono (mu mm (fmap fm (headDeltaM ∙ deltaM-mono) ((fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x))))) x)))) | 212 deltaM (mono (mu mm (fmap fm (\d -> (headDeltaM {A = A} {monadM = mm} (deltaM (mono (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d))))))) 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)) ⟩ | 213 ≡⟨ refl ⟩ |
214 | 214 deltaM (mono (mu mm (fmap fm (\d -> (mu mm (fmap fm headDeltaM ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}) d)))) x))) |
215 deltaM (mono (mu mm (fmap fm (\x -> (mu mm (fmap fm headDeltaM (headDeltaM x)))) x))) ≡⟨ refl ⟩ | 215 ≡⟨ refl ⟩ |
216 | 216 deltaM (mono (mu mm (fmap fm ((mu mm) ∙ (((fmap fm headDeltaM)) ∙ ((headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x))) |
217 | 217 ≡⟨ cong (\de -> deltaM (mono (mu mm de))) (covariant fm ((fmap fm headDeltaM) ∙ (headDeltaM)) (mu mm) x )⟩ |
218 | 218 deltaM (mono (mu mm (((fmap fm (mu mm)) ∙ (fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm})))) x))) |
219 {- | 219 ≡⟨ refl ⟩ |
220 {!!} | 220 deltaM (mono (mu mm (fmap fm (mu mm) ((fmap fm ((fmap fm headDeltaM) ∙ (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x)))) |
221 | 221 ≡⟨ cong (\de -> deltaM (mono (mu mm (fmap fm (mu mm) de)))) (covariant fm headDeltaM (fmap fm headDeltaM) x) ⟩ |
222 | 222 deltaM (mono (mu mm (fmap fm (mu mm) (((fmap fm (fmap fm headDeltaM)) ∙ (fmap fm (headDeltaM {l} {DeltaM M A (S O)} {monadM = mm}))) x)))) |
223 | 223 ≡⟨ refl ⟩ |
224 deltaM (mono (mu mm (fmap fm (headDeltaM) (fmap fm | 224 deltaM (mono (mu mm (fmap fm (mu mm) (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))))) |
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 ⟩ | 225 ≡⟨ cong (\de -> deltaM (mono de)) (association-law mm (fmap fm (fmap fm headDeltaM) (fmap fm headDeltaM x))) ⟩ |
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))))) | 226 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)) ⟩ | 227 ≡⟨ 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 ⟩ | 228 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 ⟩ | |
248 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩ | 230 deltaM-mu (deltaM (mono (mu mm (fmap fm headDeltaM x)))) ≡⟨ refl ⟩ |
249 deltaM-mu (deltaM-mu (deltaM (mono x))) | 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 ⟩ |
250 ∎ | 232 deltaM-mu (deltaM-mu (deltaM (mono x))) ∎ |
233 | |
251 deltaM-association-law {n = S n} M fm mm (deltaM (delta x d)) = begin | 234 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 ⟩ | 235 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 ⟩ | 236 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 ⟩ | 237 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))))) | 238 appendDeltaM (deltaM (mono (mu mm (fmap fm headDeltaM (fmap fm deltaM-mu x))))) |