Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 70:18a20a14c4b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Change prove method. use Int ...
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Thu, 27 Nov 2014 22:44:57 +0900
parents 295e8ed39c0c
children 56da62d57c95
comparison
equal deleted inserted replaced
69:295e8ed39c0c 70:18a20a14c4b2
14 14
15 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A 15 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A
16 deltaAppend (mono x) d = delta x d 16 deltaAppend (mono x) d = delta x d
17 deltaAppend (delta x d) ds = delta x (deltaAppend d ds) 17 deltaAppend (delta x d) ds = delta x (deltaAppend d ds)
18 18
19 headDelta : {l : Level} {A : Set l} -> Delta A -> Delta A 19 headDelta : {l : Level} {A : Set l} -> Delta A -> A
20 headDelta (mono x) = mono x 20 headDelta (mono x) = x
21 headDelta (delta x _) = mono x 21 headDelta (delta x _) = x
22 22
23 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A 23 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A
24 tailDelta (mono x) = mono x 24 tailDelta (mono x) = mono x
25 tailDelta (delta _ d) = d 25 tailDelta (delta _ d) = d
26 26
36 eta : {l : Level} {A : Set l} -> A -> Delta A 36 eta : {l : Level} {A : Set l} -> A -> Delta A
37 eta x = mono x 37 eta x = mono x
38 38
39 bind : {l ll : Level} {A : Set l} {B : Set ll} -> (Delta A) -> (A -> Delta B) -> Delta B 39 bind : {l ll : Level} {A : Set l} {B : Set ll} -> (Delta A) -> (A -> Delta B) -> Delta B
40 bind (mono x) f = f x 40 bind (mono x) f = f x
41 bind (delta x d) f = deltaAppend (headDelta (f x)) (bind d (tailDelta ∙ f)) 41 bind (delta x d) f = delta (headDelta (f x)) (bind d (tailDelta ∙ f))
42 42
43 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A 43 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A
44 mu d = bind d id 44 mu d = bind d id
45
46 45
47 returnS : {l : Level} {A : Set l} -> A -> Delta A 46 returnS : {l : Level} {A : Set l} -> A -> Delta A
48 returnS x = mono x 47 returnS x = mono x
49 48
50 returnSS : {l : Level} {A : Set l} -> A -> A -> Delta A 49 returnSS : {l : Level} {A : Set l} -> A -> A -> Delta A
56 return = eta 55 return = eta
57 56
58 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} -> 57 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
59 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) 58 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B)
60 (mono x) >>= f = f x 59 (mono x) >>= f = f x
61 (delta x d) >>= f = deltaAppend (headDelta (f x)) (d >>= (tailDelta ∙ f)) 60 (delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f))
62 61
63 62
64 63
65 -- proofs 64 -- proofs
66 65
67 -- sub proofs
68
69 head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} ->
70 (f : A -> B) (d : Delta A) -> (headDelta (fmap f d)) ≡ fmap f (headDelta d)
71 head-delta-natural-transformation f (mono x) = refl
72 head-delta-natural-transformation f (delta x d) = refl
73
74 tail-delta-natural-transfomation : {l ll : Level} {A : Set l} {B : Set ll} ->
75 (f : A -> B) (d : Delta A) -> (tailDelta (fmap f d)) ≡ fmap f (tailDelta d)
76 tail-delta-natural-transfomation f (mono x) = refl
77 tail-delta-natural-transfomation f (delta x d) = refl
78
79 delta-append-natural-transfomation : {l ll : Level} {A : Set l} {B : Set ll} ->
80 (f : A -> B) (d : Delta A) (dd : Delta A) ->
81 deltaAppend (fmap f d) (fmap f dd) ≡ fmap f (deltaAppend d dd)
82 delta-append-natural-transfomation f (mono x) dd = refl
83 delta-append-natural-transfomation f (delta x d) dd = begin
84 deltaAppend (fmap f (delta x d)) (fmap f dd)
85 ≡⟨ refl ⟩
86 deltaAppend (delta (f x) (fmap f d)) (fmap f dd)
87 ≡⟨ refl ⟩
88 delta (f x) (deltaAppend (fmap f d) (fmap f dd))
89 ≡⟨ cong (\d -> delta (f x) d) (delta-append-natural-transfomation f d dd) ⟩
90 delta (f x) (fmap f (deltaAppend d dd))
91 ≡⟨ refl ⟩
92 fmap f (deltaAppend (delta x d) dd)
93 ∎
94 -- Functor-laws 66 -- Functor-laws
95 67
96 -- Functor-law-1 : T(id) = id' 68 -- Functor-law-1 : T(id) = id'
97 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d 69 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d
98 functor-law-1 (mono x) = refl 70 functor-law-1 (mono x) = refl
103 (f : B -> C) -> (g : A -> B) -> (d : Delta A) -> 75 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
104 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d 76 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d
105 functor-law-2 f g (mono x) = refl 77 functor-law-2 f g (mono x) = refl
106 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d) 78 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
107 79
108 {- 80
109 -- Monad-laws (Category) 81 -- Monad-laws (Category)
82
83
84 data Int : Set where
85 one : Int
86 succ : Int -> Int
87
88 n-times-tail-delta : {l : Level} {A : Set l} -> Int -> ((Delta A) -> (Delta A))
89 n-times-tail-delta one = tailDelta
90 n-times-tail-delta (succ n) = (n-times-tail-delta n) ∙ tailDelta
91
92 tail-delta-to-mono : {l : Level} {A : Set l} -> (n : Int) -> (x : A) ->
93 (n-times-tail-delta n) (mono x) ≡ (mono x)
94 tail-delta-to-mono one x = refl
95 tail-delta-to-mono (succ n) x = begin
96 n-times-tail-delta (succ n) (mono x)
97 ≡⟨ refl ⟩
98 n-times-tail-delta n (mono x)
99 ≡⟨ tail-delta-to-mono n x ⟩
100 mono x
101 ∎
102
103 monad-law-1-4 : {l : Level} {A : Set l} -> (n : Int) (d : Delta (Delta A)) ->
104 (headDelta ((n-times-tail-delta n) (headDelta ((n-times-tail-delta n) d)))) ≡
105 (headDelta ((n-times-tail-delta n) (mu d)))
106 monad-law-1-4 one (mono d) = refl
107 monad-law-1-4 one (delta d (mono ds)) = refl
108 monad-law-1-4 one (delta d (delta ds ds₁)) = refl
109 monad-law-1-4 (succ n) (mono d) = begin
110 headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta (succ n) (mono d))))
111 ≡⟨ refl ⟩
112 headDelta (n-times-tail-delta (succ n) (headDelta ((n-times-tail-delta n) (mono d))))
113 ≡⟨ cong (\d -> headDelta (n-times-tail-delta (succ n) (headDelta d))) (tail-delta-to-mono n d) ⟩
114 headDelta (n-times-tail-delta (succ n) (headDelta (mono d)))
115 ≡⟨ refl ⟩
116 headDelta (n-times-tail-delta (succ n) d)
117 ≡⟨ refl ⟩
118 headDelta (n-times-tail-delta (succ n) (mu (mono d)))
119 ∎
120 monad-law-1-4 (succ n) (delta d (mono ds)) = begin
121 headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta (succ n) (delta d (mono ds)))))
122 ≡⟨ refl ⟩
123 headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta n (mono ds))))
124 ≡⟨ cong (\d -> headDelta (n-times-tail-delta (succ n) (headDelta d))) (tail-delta-to-mono n ds) ⟩
125 headDelta (n-times-tail-delta (succ n) (headDelta (mono ds)))
126 ≡⟨ refl ⟩
127 headDelta (n-times-tail-delta (succ n) ds)
128 ≡⟨ refl ⟩
129 headDelta (n-times-tail-delta n (tailDelta ds))
130 ≡⟨ refl ⟩
131 headDelta (n-times-tail-delta n ((bind (mono ds) tailDelta)))
132 ≡⟨ refl ⟩
133 headDelta (n-times-tail-delta (succ n) (delta (headDelta d) (bind (mono ds) tailDelta)))
134 ≡⟨ refl ⟩
135 headDelta (n-times-tail-delta (succ n) (mu (delta d (mono ds))))
136 ∎
137 monad-law-1-4 (succ n) (delta d (delta dd ds)) = begin
138 headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta (succ n) (delta d (delta dd ds)))))
139 ≡⟨ refl ⟩
140 headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta n (delta dd ds))))
141 ≡⟨ {!!} ⟩ -- ?
142
143 headDelta (n-times-tail-delta n (delta (headDelta (tailDelta dd)) (bind ds (tailDelta ∙ tailDelta))))
144 ≡⟨ {!!} ⟩
145 headDelta (n-times-tail-delta n (delta (headDelta (tailDelta dd)) (bind ds (tailDelta ∙ tailDelta ))))
146 ≡⟨ refl ⟩
147 headDelta (n-times-tail-delta n (bind (delta dd ds) (tailDelta)))
148 ≡⟨ refl ⟩
149 headDelta (n-times-tail-delta (succ n) (delta (headDelta d) (bind (delta dd ds) (tailDelta))))
150 ≡⟨ refl ⟩
151 headDelta (n-times-tail-delta (succ n) (mu (delta d (delta dd ds))))
152 ∎
153
154
155
156
157 monad-law-1-3 : {l : Level} {A : Set l} -> (i : Int) -> (d : Delta (Delta (Delta A))) ->
158 (bind (fmap mu d) (n-times-tail-delta i) ≡ (bind (bind d (n-times-tail-delta i)) (n-times-tail-delta i)))
159 monad-law-1-3 one (mono (mono d)) = refl
160 monad-law-1-3 one (mono (delta d d₁)) = refl
161 monad-law-1-3 one (delta d ds) = begin
162 bind (fmap mu (delta d ds)) (n-times-tail-delta one)
163 ≡⟨ refl ⟩
164 bind (delta (mu d) (fmap mu ds)) (n-times-tail-delta one)
165 ≡⟨ refl ⟩
166 delta (headDelta ((n-times-tail-delta one) (mu d))) (bind (fmap mu ds) ((n-times-tail-delta one) ∙ tailDelta))
167 ≡⟨ refl ⟩
168 delta (headDelta ((n-times-tail-delta one) (mu d))) (bind (fmap mu ds) (n-times-tail-delta (succ one)))
169 ≡⟨ cong (\dx -> delta (headDelta ((n-times-tail-delta one) (mu d))) dx) (monad-law-1-3 (succ one) ds) ⟩
170 delta (headDelta ((n-times-tail-delta one) (mu d))) (bind (bind ds (n-times-tail-delta (succ one))) (n-times-tail-delta (succ one)))
171 ≡⟨ cong (\dx -> delta dx (bind (bind ds (n-times-tail-delta (succ one))) (n-times-tail-delta (succ one )))) (sym (monad-law-1-4 one d)) ⟩
172 delta (headDelta ((n-times-tail-delta one) (headDelta ((n-times-tail-delta one) d)))) (bind (bind ds (n-times-tail-delta (succ one))) (n-times-tail-delta (succ one)))
173 ≡⟨ refl ⟩
174 delta (headDelta ((n-times-tail-delta one) (headDelta ((n-times-tail-delta one) d)))) ((bind (bind ds (n-times-tail-delta (succ one)))) ((n-times-tail-delta one) ∙ tailDelta))
175 ≡⟨ refl ⟩
176 bind (delta (headDelta ((n-times-tail-delta one) d)) (bind ds (n-times-tail-delta (succ one)))) (n-times-tail-delta one)
177 ≡⟨ refl ⟩
178 bind (delta (headDelta ((n-times-tail-delta one) d)) (bind ds ((n-times-tail-delta one) ∙ tailDelta))) (n-times-tail-delta one)
179 ≡⟨ refl ⟩
180 bind (bind (delta d ds) (n-times-tail-delta one)) (n-times-tail-delta one)
181 ∎
182 monad-law-1-3 (succ i) d = {!!}
183
184
185 monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (mu d) ≡ (headDelta (headDelta d))
186 monad-law-1-2 (mono _) = refl
187 monad-law-1-2 (delta _ _) = refl
110 188
111 -- monad-law-1 : join . fmap join = join . join 189 -- monad-law-1 : join . fmap join = join . join
112 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d) 190 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
113 monad-law-1 d = ? 191 monad-law-1 (mono d) = refl
192 monad-law-1 (delta x d) = begin
193 (mu ∙ fmap mu) (delta x d)
194 ≡⟨ refl ⟩
195 mu (fmap mu (delta x d))
196 ≡⟨ refl ⟩
197 mu (delta (mu x) (fmap mu d))
198 ≡⟨ refl ⟩
199 delta (headDelta (mu x)) (bind (fmap mu d) tailDelta)
200 ≡⟨ cong (\x -> delta x (bind (fmap mu d) tailDelta)) (monad-law-1-2 x) ⟩
201 delta (headDelta (headDelta x)) (bind (fmap mu d) tailDelta)
202 ≡⟨ cong (\d -> delta (headDelta (headDelta x)) d) (monad-law-1-3 one d) ⟩
203 delta (headDelta (headDelta x)) (bind (bind d tailDelta) tailDelta)
204 ≡⟨ refl ⟩
205 mu (delta (headDelta x) (bind d tailDelta))
206 ≡⟨ refl ⟩
207 mu (mu (delta x d))
208 ≡⟨ refl ⟩
209 (mu ∙ mu) (delta x d)
210 ∎
211
212
213
214 {-
215 -- monad-law-2 : join . fmap return = join . return = id
216 -- monad-law-2-1 join . fmap return = join . return
217 monad-law-2-1 : {l : Level} {A : Set l} -> (d : Delta A) ->
218 (mu ∙ fmap eta) d ≡ (mu ∙ eta) d
219 monad-law-2-1 (mono x) = refl
220 monad-law-2-1 (delta x d) = {!!}
114 221
115 222
116 -- monad-law-2-2 : join . return = id 223 -- monad-law-2-2 : join . return = id
117 monad-law-2-2 : {l : Level} {A : Set l } -> (s : Delta A) -> (mu ∙ eta) s ≡ id s 224 monad-law-2-2 : {l : Level} {A : Set l } -> (d : Delta A) -> (mu ∙ eta) d ≡ id d
118 monad-law-2-2 (similar lx x ly y) = refl 225 monad-law-2-2 d = refl
226
119 227
120 -- monad-law-3 : return . f = fmap f . return 228 -- monad-law-3 : return . f = fmap f . return
121 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x 229 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x
122 monad-law-3 f x = refl 230 monad-law-3 f x = refl
123 231
232
124 -- monad-law-4 : join . fmap (fmap f) = fmap f . join 233 -- monad-law-4 : join . fmap (fmap f) = fmap f . join
125 monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (s : Delta (Delta A)) -> 234 monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (d : Delta (Delta A)) ->
126 (mu ∙ fmap (fmap f)) s ≡ (fmap f ∙ mu) s 235 (mu ∙ fmap (fmap f)) d ≡ (fmap f ∙ mu) d
127 monad-law-4 f (similar lx (similar llx x _ _) ly (similar _ _ lly y)) = refl 236 monad-law-4 f d = {!!}
128 -} 237
238
239
129 240
130 -- Monad-laws (Haskell) 241 -- Monad-laws (Haskell)
131 -- monad-law-h-1 : return a >>= k = k a 242 -- monad-law-h-1 : return a >>= k = k a
132 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} -> 243 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} ->
133 (a : A) -> (k : A -> (Delta B)) -> 244 (a : A) -> (k : A -> (Delta B)) ->
145 -- monad-law-h-3 : m >>= (\x -> k x >>= h) = (m >>= k) >>= h 256 -- monad-law-h-3 : m >>= (\x -> k x >>= h) = (m >>= k) >>= h
146 monad-law-h-3 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} -> 257 monad-law-h-3 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
147 (m : Delta A) -> (k : A -> (Delta B)) -> (h : B -> (Delta C)) -> 258 (m : Delta A) -> (k : A -> (Delta B)) -> (h : B -> (Delta C)) ->
148 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h) 259 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h)
149 monad-law-h-3 (mono x) k h = refl 260 monad-law-h-3 (mono x) k h = refl
150 monad-law-h-3 (delta x (mono xx)) k h = begin 261 monad-law-h-3 (delta x d) k h = {!!}
151 delta x (mono xx) >>= (\x → k x >>= h) 262
152 ≡⟨ refl ⟩ 263 -}
153 deltaAppend (headDelta ((\x -> k x >>= h) x)) ((mono xx) >>= (tailDelta ∙ ((\x → k x >>= h))))
154 ≡⟨ refl ⟩
155 deltaAppend (headDelta ((\x -> k x >>= h) x)) ((tailDelta ∙ (\x → k x >>= h)) xx)
156 ≡⟨ refl ⟩
157 deltaAppend (headDelta (k x >>= h)) (tailDelta (k xx >>= h))
158 ≡⟨ {!!} ⟩ -- ?
159 deltaAppend (headDelta (k x)) (tailDelta (k xx)) >>= h
160 ≡⟨ refl ⟩
161 (delta x (mono xx) >>= k) >>= h
162 ∎
163 monad-law-h-3 (delta x (delta xx d)) k h = {!!}
164