Mercurial > hg > Members > atton > delta_monad

comparison agda/delta.agda @ 74:1f4ea5cb153d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove monad-law-1
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Sun, 30 Nov 2014 23:05:42 +0900
parents 0ad0ae7a3cbe
children a4eb68476766
comparison
equal deleted inserted replaced
73:0ad0ae7a3cbe 74:1f4ea5cb153d
186 bind ((n-tail n) ds) (n-tail (S m + S n)) ≡⟨ refl ⟩ 186 bind ((n-tail n) ds) (n-tail (S m + S n)) ≡⟨ refl ⟩
187 bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S m + S n)) ≡⟨ cong (\t -> bind (t (delta d ds)) (n-tail (S m + S n))) (n-tail-plus n) ⟩ 187 bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S m + S n)) ≡⟨ cong (\t -> bind (t (delta d ds)) (n-tail (S m + S n))) (n-tail-plus n) ⟩
188 bind (n-tail (S n) (delta d ds)) (n-tail (S m + S n)) 188 bind (n-tail (S n) (delta d ds)) (n-tail (S m + S n))
189 ∎ 189 ∎
190 190
191 monad-law-1-4 : {l : Level} {A : Set l} -> (n : Int) -> (dd : Delta (Delta A)) -> 191 monad-law-1-4 : {l : Level} {A : Set l} -> (m n : Int) -> (dd : Delta (Delta A)) ->
192 headDelta ((n-tail n) (bind dd tailDelta)) ≡ headDelta ((n-tail (S n)) (headDelta (n-tail n dd))) 192 headDelta ((n-tail n) (bind dd (n-tail m))) ≡ headDelta ((n-tail (m + n)) (headDelta (n-tail n dd)))
193 monad-law-1-4 O (mono dd) = refl 193 monad-law-1-4 O O (mono dd) = refl
194 monad-law-1-4 O (delta dd dd₁) = refl 194 monad-law-1-4 O O (delta dd dd₁) = refl
195 monad-law-1-4 (S n) (mono dd) = begin 195 monad-law-1-4 O (S n) (mono dd) = begin
196 headDelta (n-tail (S n) (bind (mono dd) tailDelta)) ≡⟨ refl ⟩ 196 headDelta (n-tail (S n) (bind (mono dd) (n-tail O))) ≡⟨ refl ⟩
197 headDelta (n-tail (S n) (tailDelta dd)) ≡⟨ cong (\t -> headDelta (t dd)) (n-tail-plus (S n)) ⟩ 197 headDelta (n-tail (S n) dd) ≡⟨ refl ⟩
198 headDelta (n-tail (S (S n)) dd) ≡⟨ refl ⟩ 198 headDelta (n-tail (S n) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S n) (headDelta de))) (sym (tail-delta-to-mono (S n) dd)) ⟩
199 headDelta (n-tail (S (S n)) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S (S n)) (headDelta de))) (sym (tail-delta-to-mono (S n) dd)) ⟩ 199 headDelta (n-tail (S n) (headDelta (n-tail (S n) (mono dd)))) ≡⟨ refl ⟩
200 headDelta (n-tail (S (S n)) (headDelta (n-tail (S n) (mono dd)))) 200 headDelta (n-tail (O + S n) (headDelta (n-tail (S n) (mono dd))))
201 ∎ 201 ∎
202 monad-law-1-4 (S n) (delta d ds) = begin 202 monad-law-1-4 O (S n) (delta d ds) = begin
203 headDelta (n-tail (S n) (bind (delta d ds) tailDelta)) ≡⟨ refl ⟩ 203 headDelta (n-tail (S n) (bind (delta d ds) (n-tail O))) ≡⟨ refl ⟩
204 headDelta (n-tail (S n) (delta (headDelta (tailDelta d)) (bind ds (tailDelta ∙ tailDelta)))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta (tailDelta d)) (bind ds (tailDelta ∙ tailDelta))))) (sym (n-tail-plus n)) ⟩ 204 headDelta (n-tail (S n) (bind (delta d ds) id)) ≡⟨ refl ⟩
205 headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta (tailDelta d)) (bind ds (tailDelta ∙ tailDelta)))) ≡⟨ refl ⟩ 205 headDelta (n-tail (S n) (delta (headDelta d) (bind ds tailDelta))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta d) (bind ds tailDelta)))) (sym (n-tail-plus n)) ⟩
206 headDelta (n-tail n (bind ds (tailDelta ∙ tailDelta))) ≡⟨ {!!} ⟩ 206 headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta d) (bind ds tailDelta))) ≡⟨ refl ⟩
207 headDelta (n-tail (S (S n)) (headDelta ((n-tail n ds)))) ≡⟨ refl ⟩ 207 headDelta (n-tail n (bind ds tailDelta)) ≡⟨ monad-law-1-4 (S O) n ds ⟩
208 headDelta (n-tail (S (S n)) (headDelta ((n-tail n ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S (S n)) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩ 208 headDelta (n-tail (S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩
209 headDelta (n-tail (S (S n)) (headDelta (n-tail (S n) (delta d ds)))) 209 headDelta (n-tail (S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩
210 headDelta (n-tail (S n) (headDelta (n-tail (S n) (delta d ds)))) ≡⟨ refl ⟩
211 headDelta (n-tail (O + S n) (headDelta (n-tail (S n) (delta d ds))))
212 ∎
213 monad-law-1-4 (S m) n (mono dd) = begin
214 headDelta (n-tail n (bind (mono dd) (n-tail (S m)))) ≡⟨ refl ⟩
215 headDelta (n-tail n ((n-tail (S m)) dd))≡⟨ cong (\t -> headDelta (t dd)) (n-tail-add n (S m)) ⟩
216 headDelta (n-tail (n + S m) dd) ≡⟨ cong (\n -> headDelta ((n-tail n) dd)) (int-add-assoc n (S m)) ⟩
217 headDelta (n-tail (S m + n) dd) ≡⟨ refl ⟩
218 headDelta (n-tail (S m + n) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S m + n) (headDelta de))) (sym (tail-delta-to-mono n dd)) ⟩
219 headDelta (n-tail (S m + n) (headDelta (n-tail n (mono dd))))
220 ∎
221 monad-law-1-4 (S m) O (delta d ds) = begin
222 headDelta (n-tail O (bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩
223 headDelta (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
224 headDelta (delta (headDelta ((n-tail (S m) d))) (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩
225 headDelta (n-tail (S m) d) ≡⟨ cong (\n -> headDelta ((n-tail n) d)) (int-add-right-zero (S m)) ⟩
226 headDelta (n-tail (S m + O) d) ≡⟨ refl ⟩
227 headDelta (n-tail (S m + O) (headDelta (delta d ds))) ≡⟨ refl ⟩
228 headDelta (n-tail (S m + O) (headDelta (n-tail O (delta d ds))))
229 ∎
230 monad-law-1-4 (S m) (S n) (delta d ds) = begin
231 headDelta (n-tail (S n) (bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩
232 headDelta (n-tail (S n) (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m)))))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m))))))) (sym (n-tail-plus n)) ⟩
233 headDelta ((((n-tail n) ∙ tailDelta) (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m))))))) ≡⟨ refl ⟩
234 headDelta (n-tail n (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩
235 headDelta (n-tail n (bind ds (n-tail (S (S m))))) ≡⟨ monad-law-1-4 (S (S m)) n ds ⟩
236 headDelta (n-tail ((S (S m) + n)) (headDelta (n-tail n ds))) ≡⟨ cong (\nm -> headDelta ((n-tail nm) (headDelta (n-tail n ds)))) (sym (int-add-right m n)) ⟩
237 headDelta (n-tail (S m + S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩
238 headDelta (n-tail (S m + S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S m + S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩
239 headDelta (n-tail (S m + S n) (headDelta (n-tail (S n) (delta d ds))))
210 ∎ 240 ∎
211 241
212 monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (mu d) ≡ (headDelta (headDelta d)) 242 monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (mu d) ≡ (headDelta (headDelta d))
213 monad-law-1-2 (mono _) = refl 243 monad-law-1-2 (mono _) = refl
214 monad-law-1-2 (delta _ _) = refl 244 monad-law-1-2 (delta _ _) = refl
266 delta (headDelta ((n-tail (S n)) (mu (delta d dd)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩ 296 delta (headDelta ((n-tail (S n)) (mu (delta d dd)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
267 delta (headDelta ((n-tail (S n)) (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\t -> delta (headDelta (t (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))))(sym (n-tail-plus n)) ⟩ 297 delta (headDelta ((n-tail (S n)) (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\t -> delta (headDelta (t (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))))(sym (n-tail-plus n)) ⟩
268 delta (headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩ 298 delta (headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
269 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩ 299 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
270 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (fmap mu ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta ((n-tail n) (bind dd tailDelta))) de) (monad-law-1-3 (S (S n)) ds) ⟩ 300 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (fmap mu ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta ((n-tail n) (bind dd tailDelta))) de) (monad-law-1-3 (S (S n)) ds) ⟩
271 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta de ( (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))))) (monad-law-1-4 n dd) ⟩ 301 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta de ( (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))))) (monad-law-1-4 (S O) n dd) ⟩
272 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ refl ⟩ 302 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ refl ⟩
273 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (n-tail (S (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩ 303 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (n-tail (S (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
274 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩ 304 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
275 delta (headDelta ((n-tail (S n)) (headDelta (((n-tail n) ∙ tailDelta) (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\t -> delta (headDelta ((n-tail (S n)) (headDelta (t (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n))))) (n-tail-plus n) ⟩ 305 delta (headDelta ((n-tail (S n)) (headDelta (((n-tail n) ∙ tailDelta) (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\t -> delta (headDelta ((n-tail (S n)) (headDelta (t (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n))))) (n-tail-plus n) ⟩
276 delta (headDelta ((n-tail (S n)) (headDelta ((n-tail (S n)) (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩ 306 delta (headDelta ((n-tail (S n)) (headDelta ((n-tail (S n)) (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩