Mercurial > hg > Members > atton > delta_monad

comparison agda/delta/monad.agda @ 107:caaf364f45ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove monad-laws for length fixed infinite Delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 28 Jan 2015 22:21:27 +0900
parents e6499a50ccbd
children d47aea3f9246
comparison
equal deleted inserted replaced
106:2779a09e1526 107:caaf364f45ac
8 open import Level 8 open import Level
9 open import Relation.Binary.PropositionalEquality 9 open import Relation.Binary.PropositionalEquality
10 open ≡-Reasoning 10 open ≡-Reasoning
11 11
12 module delta.monad where 12 module delta.monad where
13
14 tailDelta-is-nt : {l : Level} {A B : Set l} {n : Nat}
15 (f : A -> B) -> (d : Delta A (S (S n))) ->
16 (tailDelta {n = n} ∙ (delta-fmap f)) d ≡ ((delta-fmap f) ∙ tailDelta {n = n}) d
17 tailDelta-is-nt f (delta x d) = refl
18
19 tailDelta-to-tail-nt : {l : Level} {A B : Set l} (n m : Nat)
20 (f : A -> B) (d : Delta (Delta A (S (S m))) (S n)) ->
21 delta-fmap tailDelta (delta-fmap (delta-fmap f) d) ≡ delta-fmap (delta-fmap f) (delta-fmap tailDelta d)
22 tailDelta-to-tail-nt O O f (mono (delta x d)) = refl
23 tailDelta-to-tail-nt O (S m) f (mono (delta x d)) = refl
24 tailDelta-to-tail-nt (S n) O f (delta (delta x (mono xx)) d) = begin
25 delta (mono (f xx))
26 (delta-fmap tailDelta (delta-fmap (delta-fmap f) d))
27 ≡⟨ cong (\de -> delta (mono (f xx)) de) (tailDelta-to-tail-nt n O f d) ⟩
28 delta (mono (f xx))
29 (delta-fmap (delta-fmap f) (delta-fmap tailDelta d))
30 ∎
31 tailDelta-to-tail-nt (S n) (S m) f (delta (delta x (delta xx d)) ds) = begin
32 delta (delta (f xx) (delta-fmap f d))
33 (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds))
34 ≡⟨ cong (\de -> delta (delta (f xx) (delta-fmap f d)) de) (tailDelta-to-tail-nt n (S m) f ds) ⟩
35 delta (delta (f xx) (delta-fmap f d))
36 (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds))
37 ∎
38
39
13 40
14 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat} 41 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
15 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x) 42 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
16 delta-eta-is-nt {n = O} f x = refl 43 delta-eta-is-nt {n = O} f x = refl
17 delta-eta-is-nt {n = S O} f x = refl 44 delta-eta-is-nt {n = S O} f x = refl
21 delta (f x) (delta-eta (f x)) ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩ 48 delta (f x) (delta-eta (f x)) ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩
22 delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩ 49 delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩
23 delta-fmap f (delta x (delta-eta x)) ≡⟨ refl ⟩ 50 delta-fmap f (delta x (delta-eta x)) ≡⟨ refl ⟩
24 delta-fmap f (delta-eta x) ∎ 51 delta-fmap f (delta-eta x) ∎
25 52
53
26 delta-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} -> (f : A -> B) -> (d : Delta (Delta A (S n)) (S n)) 54 delta-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} -> (f : A -> B) -> (d : Delta (Delta A (S n)) (S n))
27 -> delta-mu (delta-fmap (delta-fmap f) d) ≡ delta-fmap f (delta-mu d) 55 -> delta-mu (delta-fmap (delta-fmap f) d) ≡ delta-fmap f (delta-mu d)
28 delta-mu-is-nt f d = {!!} 56 delta-mu-is-nt {n = O} f (mono d) = refl
29 57 delta-mu-is-nt {n = S n} f (delta (delta x d) ds) = begin
30 hoge : {l : Level} {A : Set l} {n : Nat} -> (ds : Delta (Delta A (S (S n))) (S (S n))) -> 58 delta (f x) (delta-mu (delta-fmap tailDelta (delta-fmap (delta-fmap f) ds)))
31 (tailDelta {n = n} ∙ delta-mu {n = (S n)}) ds 59 ≡⟨ cong (\de -> delta (f x) (delta-mu de)) (tailDelta-to-tail-nt n n f ds ) ⟩
60 delta (f x) (delta-mu (delta-fmap (delta-fmap f) (delta-fmap tailDelta ds)))
61 ≡⟨ cong (\de -> delta (f x) de) (delta-mu-is-nt f (delta-fmap tailDelta ds)) ⟩
62 delta (f x) (delta-fmap f (delta-mu (delta-fmap tailDelta ds)))
63 ∎
64
65
66 delta-fmap-mu-to-tail : {l : Level} {A : Set l} (n m : Nat) (d : Delta (Delta (Delta A (S (S m))) (S (S m))) (S n)) ->
67 delta-fmap tailDelta (delta-fmap delta-mu d)
32 ≡ 68 ≡
33 (((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) ∙ tailDelta) ds 69 (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta d)))
34 hoge (delta ds ds₁) = refl 70 delta-fmap-mu-to-tail O O (mono (delta d ds)) = refl
35 71 delta-fmap-mu-to-tail O (S n) (mono (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds))) = refl
72 delta-fmap-mu-to-tail (S n) O (delta (delta (delta x (mono xx)) (mono (delta dx (mono dxx)))) ds) = begin
73 delta (mono dxx) (delta-fmap tailDelta (delta-fmap delta-mu ds))
74 ≡⟨ cong (\de -> delta (mono dxx) de) (delta-fmap-mu-to-tail n O ds) ⟩
75 delta (mono dxx)
76 (delta-fmap delta-mu
77 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds)))
78 ∎
79 delta-fmap-mu-to-tail (S n) (S n₁) (delta (delta (delta x (delta xx d)) (delta (delta dx (delta dxx dd)) ds)) dds) = begin
80 delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
81 (delta-fmap tailDelta (delta-fmap delta-mu dds))
82 ≡⟨ cong (\de -> delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds)))) de) (delta-fmap-mu-to-tail n (S n₁) dds) ⟩
83 delta (delta dxx (delta-mu (delta-fmap tailDelta (delta-fmap tailDelta ds))))
84 (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta dds)))
85 ∎
36 86
37 87
38 88
39 -- Monad-laws (Category) 89 -- Monad-laws (Category)
40 -- monad-law-1 : join . delta-fmap join = join . join 90 -- monad-law-1 : join . delta-fmap join = join . join
41 monad-law-1 : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) -> 91 monad-law-1 : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
42 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d) 92 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
43 monad-law-1 {n = O} (mono d) = refl 93 monad-law-1 {n = O} (mono d) = refl
94 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin
95 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
96 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-fmap-mu-to-tail n n ds) ⟩
97 delta x (delta-mu (delta-fmap delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
98 ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
99 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
100 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds) ) ⟩
101 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds))))
102 ∎
103
104
105 {-
106 begin
107 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ {!!} ⟩
108 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds))))
109 ∎
110 -}
111 {-
44 monad-law-1 {n = S O} (delta (delta (delta _ _) _) (mono (delta (delta _ (mono _)) (mono (delta _ (mono _)))))) = refl 112 monad-law-1 {n = S O} (delta (delta (delta _ _) _) (mono (delta (delta _ (mono _)) (mono (delta _ (mono _)))))) = refl
45 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin 113 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin
46 (delta-mu ∙ delta-fmap delta-mu) (delta (delta (delta x d) dd) ds) ≡⟨ refl ⟩ 114 (delta-mu ∙ delta-fmap delta-mu) (delta (delta (delta x d) dd) ds) ≡⟨ refl ⟩
47 delta-mu (delta-fmap delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩ 115 delta-mu (delta-fmap delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
48 delta-mu (delta (delta-mu (delta (delta x d) dd)) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩ 116 delta-mu (delta (delta-mu (delta (delta x d) dd)) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
67 delta-mu (delta (delta x d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩ 135 delta-mu (delta (delta x d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
68 delta-mu (delta (headDelta (delta (delta x d) dd)) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩ 136 delta-mu (delta (headDelta (delta (delta x d) dd)) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
69 delta-mu (delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩ 137 delta-mu (delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
70 (delta-mu ∙ delta-mu) (delta (delta (delta x d) dd) ds) 138 (delta-mu ∙ delta-mu) (delta (delta (delta x d) dd) ds)
71 ∎ 139 ∎
140 -}
72 {- 141 {-
73 begin 142 begin
74 (delta-mu ∙ delta-fmap delta-mu) (delta d ds) ≡⟨ refl ⟩ 143 (delta-mu ∙ delta-fmap delta-mu) (delta d ds) ≡⟨ refl ⟩
75 delta-mu (delta-fmap delta-mu (delta d ds)) ≡⟨ refl ⟩ 144 delta-mu (delta-fmap delta-mu (delta d ds)) ≡⟨ refl ⟩
76 delta-mu (delta (delta-mu d) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩ 145 delta-mu (delta (delta-mu d) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
123 id (delta x d) ∎ 192 id (delta x d) ∎
124 193
125 194
126 195
127 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor 196 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor
128
129
130 delta-is-monad = record { eta = delta-eta; 197 delta-is-monad = record { eta = delta-eta;
131 mu = delta-mu; 198 mu = delta-mu;
132 return = delta-eta; 199 return = delta-eta;
133 bind = delta-bind; 200 bind = delta-bind;
134 eta-is-nt = delta-eta-is-nt; 201 eta-is-nt = delta-eta-is-nt;