Mercurial > hg > Members > atton > delta_monad

annotate agda/delta/monad.agda @ 105:e6499a50ccbd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Retrying prove monad-laws for delta
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 27 Jan 2015 17:49:25 +0900
parents ebd0d6e2772c
children caaf364f45ac
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import basic
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import delta
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import delta.functor
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import nat
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import laws
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import Level
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Binary.PropositionalEquality
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open ≡-Reasoning
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 module delta.monad where
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
14 delta-eta-is-nt : {l : Level} {A B : Set l} -> {n : Nat}
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
15 (f : A -> B) -> (x : A) -> (delta-eta {n = n} ∙ f) x ≡ delta-fmap f (delta-eta x)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
16 delta-eta-is-nt {n = O} f x = refl
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
17 delta-eta-is-nt {n = S O} f x = refl
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
18 delta-eta-is-nt {n = S n} f x = begin
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
19 (delta-eta ∙ f) x ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
20 delta-eta (f x) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
21 delta (f x) (delta-eta (f x)) ≡⟨ cong (\de -> delta (f x) de) (delta-eta-is-nt f x) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
22 delta (f x) (delta-fmap f (delta-eta x)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
23 delta-fmap f (delta x (delta-eta x)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
24 delta-fmap f (delta-eta x) ∎
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
25
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
26 delta-mu-is-nt : {l : Level} {A B : Set l} {n : Nat} -> (f : A -> B) -> (d : Delta (Delta A (S n)) (S n))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
27 -> delta-mu (delta-fmap (delta-fmap f) d) ≡ delta-fmap f (delta-mu d)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
28 delta-mu-is-nt f d = {!!}
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
29
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
30 hoge : {l : Level} {A : Set l} {n : Nat} -> (ds : Delta (Delta A (S (S n))) (S (S n))) ->
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
31 (tailDelta {n = n} ∙ delta-mu {n = (S n)}) ds
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
32 ≡
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
33 (((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) ∙ tailDelta) ds
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
34 hoge (delta ds ds₁) = refl
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
35
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
36
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
37
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 -- Monad-laws (Category)
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
40 -- monad-law-1 : join . delta-fmap join = join . join
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
41 monad-law-1 : {l : Level} {A : Set l} {n : Nat} (d : Delta (Delta (Delta A (S n)) (S n)) (S n)) ->
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
42 ((delta-mu ∙ (delta-fmap delta-mu)) d) ≡ ((delta-mu ∙ delta-mu) d)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
43 monad-law-1 {n = O} (mono d) = refl
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
44 monad-law-1 {n = S O} (delta (delta (delta _ _) _) (mono (delta (delta _ (mono _)) (mono (delta _ (mono _)))))) = refl
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
45 monad-law-1 {n = S n} (delta (delta (delta x d) dd) ds) = begin
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
46 (delta-mu ∙ delta-fmap delta-mu) (delta (delta (delta x d) dd) ds) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
47 delta-mu (delta-fmap delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
48 delta-mu (delta (delta-mu (delta (delta x d) dd)) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
49 delta-mu (delta (delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta dd))) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
50 delta-mu (delta (delta x (delta-mu (delta-fmap tailDelta dd))) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
51 delta (headDelta (delta x (delta-mu (delta-fmap tailDelta dd)))) (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
52 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds)))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
53 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (functor-law-2 tailDelta delta-mu ds)) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
54 delta x (delta-mu (delta-fmap (tailDelta {n = n} ∙ delta-mu {n = (S n)}) ds))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
55 -- ≡⟨ cong (\ff -> delta x (delta-mu (delta-fmap ff ds))) hoge ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
56 ≡⟨ {!!} ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
57 delta x (delta-mu (delta-fmap (((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) ∙ tailDelta) ds))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
58 ≡⟨ cong (\de -> delta x (delta-mu de)) (functor-law-2 (delta-mu ∙ (delta-fmap tailDelta)) tailDelta ds ) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
59 delta x (delta-mu (delta-fmap ((delta-mu {n = n}) ∙ (delta-fmap tailDelta)) (delta-fmap tailDelta ds)))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
60 ≡⟨ cong (\de -> delta x (delta-mu de)) (functor-law-2 delta-mu (delta-fmap tailDelta) (delta-fmap tailDelta ds)) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
61 delta x (delta-mu (delta-fmap (delta-mu {n = n}) (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
62 ≡⟨ cong (\de -> delta x de) (monad-law-1 (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
63 delta x (delta-mu (delta-mu (delta-fmap (delta-fmap tailDelta) (delta-fmap tailDelta ds))))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
64 ≡⟨ cong (\de -> delta x (delta-mu de)) (delta-mu-is-nt tailDelta (delta-fmap tailDelta ds)) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
65 delta x (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
66 delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
67 delta-mu (delta (delta x d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
68 delta-mu (delta (headDelta (delta (delta x d) dd)) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
69 delta-mu (delta-mu (delta (delta (delta x d) dd) ds)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
70 (delta-mu ∙ delta-mu) (delta (delta (delta x d) dd) ds)
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 ∎
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
72 {-
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
73 begin
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
74 (delta-mu ∙ delta-fmap delta-mu) (delta d ds) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
75 delta-mu (delta-fmap delta-mu (delta d ds)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
76 delta-mu (delta (delta-mu d) (delta-fmap delta-mu ds)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
77 delta (headDelta (delta-mu d)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-mu ds))) ≡⟨ {!!} ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
78 delta (headDelta (headDelta d)) (delta-mu (delta-fmap tailDelta (delta-mu (delta-fmap tailDelta ds)))) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
79 delta-mu (delta (headDelta d) (delta-mu (delta-fmap tailDelta ds))) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
80 delta-mu (delta-mu (delta d ds)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
81 (delta-mu ∙ delta-mu) (delta d ds)
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 ∎
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
83 -}
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
88 delta-right-unity-law : {l : Level} {A : Set l} {n : Nat} (d : Delta A (S n)) -> (delta-mu ∙ delta-eta) d ≡ id d
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
89 delta-right-unity-law (mono x) = refl
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
90 delta-right-unity-law (delta x d) = begin
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
91 (delta-mu ∙ delta-eta) (delta x d)
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
92 ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
93 delta-mu (delta-eta (delta x d))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
94 ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
95 delta-mu (delta (delta x d) (delta-eta (delta x d)))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
96 ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
97 delta (headDelta (delta x d)) (delta-mu (delta-fmap tailDelta (delta-eta (delta x d))))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
98 ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
99 delta x (delta-mu (delta-fmap tailDelta (delta-eta (delta x d))))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
100 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (delta-eta-is-nt tailDelta (delta x d))) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
101 delta x (delta-mu (delta-eta (tailDelta (delta x d))))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
102 ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
103 delta x (delta-mu (delta-eta d))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
104 ≡⟨ cong (\de -> delta x de) (delta-right-unity-law d) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
105 delta x d
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
106 ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
107 id (delta x d) ∎
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
110 delta-left-unity-law : {l : Level} {A : Set l} {n : Nat} -> (d : Delta A (S n)) ->
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
111 (delta-mu ∙ (delta-fmap delta-eta)) d ≡ id d
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
112 delta-left-unity-law (mono x) = refl
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
113 delta-left-unity-law {n = (S n)} (delta x d) = begin
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
114 (delta-mu ∙ delta-fmap delta-eta) (delta x d) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
115 delta-mu ( delta-fmap delta-eta (delta x d)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
116 delta-mu (delta (delta-eta x) (delta-fmap delta-eta d)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
117 delta (headDelta {n = S n} (delta-eta x)) (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d))) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
118 delta x (delta-mu (delta-fmap tailDelta (delta-fmap delta-eta d)))
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
119 ≡⟨ cong (\de -> delta x (delta-mu de)) (sym (functor-law-2 tailDelta delta-eta d)) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
120 delta x (delta-mu (delta-fmap (tailDelta ∙ delta-eta {n = S n}) d)) ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
121 delta x (delta-mu (delta-fmap (delta-eta {n = n}) d)) ≡⟨ cong (\de -> delta x de) (delta-left-unity-law d) ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
122 delta x d ≡⟨ refl ⟩
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
123 id (delta x d) ∎
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
125
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
126
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
127 delta-is-monad : {l : Level} {n : Nat} -> Monad {l} (\A -> Delta A (S n)) delta-is-functor
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
128
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
129
94
bcd4fe52a504 Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 90
diff changeset
130 delta-is-monad = record { eta = delta-eta;
bcd4fe52a504 Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 90
diff changeset
131 mu = delta-mu;
bcd4fe52a504 Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 90
diff changeset
132 return = delta-eta;
bcd4fe52a504 Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 90
diff changeset
133 bind = delta-bind;
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
134 eta-is-nt = delta-eta-is-nt;
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
135 association-law = monad-law-1;
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
136 left-unity-law = delta-left-unity-law ;
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
137 right-unity-law = \x -> (sym (delta-right-unity-law x)) }
104
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
138
ebd0d6e2772c Trying redenition Delta with length constraints
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 103
diff changeset
139
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
140
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
141
96
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
142
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
143 {-
96
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
144
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
145 -- Monad-laws (Haskell)
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
146 -- monad-law-h-1 : return a >>= k = k a
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
147 monad-law-h-1 : {l : Level} {A B : Set l} ->
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
148 (a : A) -> (k : A -> (Delta B)) ->
96
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
149 (delta-return a >>= k) ≡ (k a)
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
150 monad-law-h-1 a k = refl
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
151
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
152
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
153
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 -- monad-law-h-2 : m >>= return = m
96
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
155 monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= delta-return) ≡ m
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
156 monad-law-h-2 (mono x) = refl
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
157 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d)
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
158
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
159
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160
96
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
161 -- monad-law-h-3 : m >>= (\x -> f x >>= g) = (m >>= f) >>= g
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
162 monad-law-h-3 : {l : Level} {A B C : Set l} ->
96
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
163 (m : Delta A) -> (f : A -> (Delta B)) -> (g : B -> (Delta C)) ->
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
164 (delta-bind m (\x -> delta-bind (f x) g)) ≡ (delta-bind (delta-bind m f) g)
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
165 monad-law-h-3 (mono x) f g = refl
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
166 monad-law-h-3 (delta x d) f g = begin
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
167 (delta-bind (delta x d) (\x -> delta-bind (f x) g)) ≡⟨ {!!} ⟩
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
168 (delta-bind (delta-bind (delta x d) f) g) ∎
88
526186c4f298 Split monad-proofs into delta.monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
169
96
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
170
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
171
dfe8c67390bd Unify Levels in delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 94
diff changeset
172
105
e6499a50ccbd Retrying prove monad-laws for delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 104
diff changeset
173 -}