Mercurial > hg > Members > atton > delta_monad
annotate agda/delta.agda @ 95:cf372fbcebd8
Fix implicit values in deltaM-mu
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jan 2015 17:47:55 +0900 |
parents | bcd4fe52a504 |
children | dfe8c67390bd |
rev | line source |
---|---|
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import list |
28
6e6d646d7722
Split basic functions to file
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
27
diff
changeset
|
2 open import basic |
76 | 3 open import nat |
87
6789c65a75bc
Split functor-proofs into delta.functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
4 open import laws |
29
e0ba1bf564dd
Apply level to some functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
5 |
e0ba1bf564dd
Apply level to some functions
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
28
diff
changeset
|
6 open import Level |
27
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
7 open import Relation.Binary.PropositionalEquality |
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
8 open ≡-Reasoning |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
10 module delta where |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 |
54
9bb7c9bee94f
Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
43
diff
changeset
|
12 |
87
6789c65a75bc
Split functor-proofs into delta.functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
80
diff
changeset
|
13 data Delta {l : Level} (A : Set l) : (Set l) where |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
14 mono : A -> Delta A |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
15 delta : A -> Delta A -> Delta A |
54
9bb7c9bee94f
Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
43
diff
changeset
|
16 |
9bb7c9bee94f
Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
43
diff
changeset
|
17 deltaAppend : {l : Level} {A : Set l} -> Delta A -> Delta A -> Delta A |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
18 deltaAppend (mono x) d = delta x d |
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
19 deltaAppend (delta x d) ds = delta x (deltaAppend d ds) |
54
9bb7c9bee94f
Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
43
diff
changeset
|
20 |
70
18a20a14c4b2
Change prove method. use Int ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
21 headDelta : {l : Level} {A : Set l} -> Delta A -> A |
18a20a14c4b2
Change prove method. use Int ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
22 headDelta (mono x) = x |
18a20a14c4b2
Change prove method. use Int ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
23 headDelta (delta x _) = x |
54
9bb7c9bee94f
Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
43
diff
changeset
|
24 |
9bb7c9bee94f
Trying redefine delta for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
43
diff
changeset
|
25 tailDelta : {l : Level} {A : Set l} -> Delta A -> Delta A |
79 | 26 tailDelta (mono x) = mono x |
27 tailDelta (delta _ d) = d | |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 |
76 | 29 n-tail : {l : Level} {A : Set l} -> Nat -> ((Delta A) -> (Delta A)) |
30 n-tail O = id | |
31 n-tail (S n) = tailDelta ∙ (n-tail n) | |
32 | |
38
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
33 |
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
34 -- Functor |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
35 delta-fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (Delta B) |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
36 delta-fmap f (mono x) = mono (f x) |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
37 delta-fmap f (delta x d) = delta (f x) (delta-fmap f d) |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
38 |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
38
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
40 |
40
a7cd7740f33e
Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
41 -- Monad (Category) |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
42 delta-eta : {l : Level} {A : Set l} -> A -> Delta A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
43 delta-eta x = mono x |
59
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
57
diff
changeset
|
44 |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
45 delta-bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
46 delta-bind (mono x) f = f x |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
47 delta-bind (delta x d) f = delta (headDelta (f x)) (delta-bind d (tailDelta ∙ f)) |
59
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
57
diff
changeset
|
48 |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
49 delta-mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
50 delta-mu d = delta-bind d id |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 |
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 |
33 | 53 |
40
a7cd7740f33e
Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
54 -- Monad (Haskell) |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
55 delta-return : {l : Level} {A : Set l} -> A -> Delta A |
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
56 delta-return = delta-eta |
40
a7cd7740f33e
Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
57 |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
58 _>>=_ : {l : Level} {A B : Set l} -> |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
59 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) |
94
bcd4fe52a504
Rewrite monad definitions for delta/deltaM
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
90
diff
changeset
|
60 (mono x) >>= f = f x |
70
18a20a14c4b2
Change prove method. use Int ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
61 (delta x d) >>= f = delta (headDelta (f x)) (d >>= (tailDelta ∙ f)) |
40
a7cd7740f33e
Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
62 |
a7cd7740f33e
Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
63 |
38
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
64 |
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
65 -- proofs |
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
66 |
76 | 67 -- sub-proofs |
68 | |
69 n-tail-plus : {l : Level} {A : Set l} -> (n : Nat) -> ((n-tail {l} {A} n) ∙ tailDelta) ≡ n-tail (S n) | |
79 | 70 n-tail-plus O = refl |
76 | 71 n-tail-plus (S n) = begin |
72 n-tail (S n) ∙ tailDelta ≡⟨ refl ⟩ | |
73 (tailDelta ∙ (n-tail n)) ∙ tailDelta ≡⟨ refl ⟩ | |
74 tailDelta ∙ ((n-tail n) ∙ tailDelta) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-plus n) ⟩ | |
75 n-tail (S (S n)) | |
76 ∎ | |
77 | |
78 n-tail-add : {l : Level} {A : Set l} {d : Delta A} -> (n m : Nat) -> (n-tail {l} {A} n) ∙ (n-tail m) ≡ n-tail (n + m) | |
79 n-tail-add O m = refl | |
80 n-tail-add (S n) O = begin | |
81 n-tail (S n) ∙ n-tail O ≡⟨ refl ⟩ | |
77
4b16b485a4b2
Split nat definition
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
76
diff
changeset
|
82 n-tail (S n) ≡⟨ cong (\n -> n-tail n) (nat-add-right-zero (S n))⟩ |
76 | 83 n-tail (S n + O) |
84 ∎ | |
85 n-tail-add {l} {A} {d} (S n) (S m) = begin | |
86 n-tail (S n) ∙ n-tail (S m) ≡⟨ refl ⟩ | |
87 (tailDelta ∙ (n-tail n)) ∙ n-tail (S m) ≡⟨ refl ⟩ | |
88 tailDelta ∙ ((n-tail n) ∙ n-tail (S m)) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-add {l} {A} {d} n (S m)) ⟩ | |
89 tailDelta ∙ (n-tail (n + (S m))) ≡⟨ refl ⟩ | |
90 n-tail (S (n + S m)) ≡⟨ refl ⟩ | |
91 n-tail (S n + S m) ∎ | |
92 | |
93 tail-delta-to-mono : {l : Level} {A : Set l} -> (n : Nat) -> (x : A) -> | |
94 (n-tail n) (mono x) ≡ (mono x) | |
79 | 95 tail-delta-to-mono O x = refl |
76 | 96 tail-delta-to-mono (S n) x = begin |
97 n-tail (S n) (mono x) ≡⟨ refl ⟩ | |
98 tailDelta (n-tail n (mono x)) ≡⟨ refl ⟩ | |
99 tailDelta (n-tail n (mono x)) ≡⟨ cong (\t -> tailDelta t) (tail-delta-to-mono n x) ⟩ | |
100 tailDelta (mono x) ≡⟨ refl ⟩ | |
101 mono x ∎ | |
102 | |
80 | 103 head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
104 -> (f : A -> B) -> (d : Delta A) -> headDelta (delta-fmap f d) ≡ f (headDelta d) |
79 | 105 head-delta-natural-transformation f (mono x) = refl |
80 | 106 head-delta-natural-transformation f (delta x d) = refl |
79 | 107 |
108 n-tail-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} | |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
109 -> (n : Nat) -> (f : A -> B) -> (d : Delta A) -> n-tail n (delta-fmap f d) ≡ delta-fmap f (n-tail n d) |
79 | 110 n-tail-natural-transformation O f d = refl |
111 n-tail-natural-transformation (S n) f (mono x) = begin | |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
112 n-tail (S n) (delta-fmap f (mono x)) ≡⟨ refl ⟩ |
79 | 113 n-tail (S n) (mono (f x)) ≡⟨ tail-delta-to-mono (S n) (f x) ⟩ |
114 (mono (f x)) ≡⟨ refl ⟩ | |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
115 delta-fmap f (mono x) ≡⟨ cong (\d -> delta-fmap f d) (sym (tail-delta-to-mono (S n) x)) ⟩ |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
116 delta-fmap f (n-tail (S n) (mono x)) ∎ |
79 | 117 n-tail-natural-transformation (S n) f (delta x d) = begin |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
118 n-tail (S n) (delta-fmap f (delta x d)) ≡⟨ refl ⟩ |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
119 n-tail (S n) (delta (f x) (delta-fmap f d)) ≡⟨ cong (\t -> t (delta (f x) (delta-fmap f d))) (sym (n-tail-plus n)) ⟩ |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
120 ((n-tail n) ∙ tailDelta) (delta (f x) (delta-fmap f d)) ≡⟨ refl ⟩ |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
121 n-tail n (delta-fmap f d) ≡⟨ n-tail-natural-transformation n f d ⟩ |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
122 delta-fmap f (n-tail n d) ≡⟨ refl ⟩ |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
123 delta-fmap f (((n-tail n) ∙ tailDelta) (delta x d)) ≡⟨ cong (\t -> delta-fmap f (t (delta x d))) (n-tail-plus n) ⟩ |
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
124 delta-fmap f (n-tail (S n) (delta x d)) ∎ |