Mercurial > hg > Members > atton > delta_monad
annotate agda/delta.agda @ 90:55d11ce7e223
Unify levels on data type. only use suc to proofs
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 19 Jan 2015 12:11:38 +0900 |
parents | 5411ce26d525 |
children | bcd4fe52a504 |
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) |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
42 eta : {l : Level} {A : Set l} -> 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
|
43 eta x = mono x |
27
742e62fc63e4
Define Monad-law 1-4
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
26
diff
changeset
|
44 |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
45 bind : {l : Level} {A B : Set l} -> (Delta A) -> (A -> Delta B) -> Delta B |
59
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
57
diff
changeset
|
46 bind (mono x) f = f x |
70
18a20a14c4b2
Change prove method. use Int ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
47 bind (delta x d) f = delta (headDelta (f x)) (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 |
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
57
diff
changeset
|
49 mu : {l : Level} {A : Set l} -> Delta (Delta A) -> Delta A |
65
6d0193011f89
Trying prove monad-law-1 by another pattern
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
64
diff
changeset
|
50 mu d = bind d id |
59
46b15f368905
Define bind and mu for Infinite Delta
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
57
diff
changeset
|
51 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
52 returnS : {l : Level} {A : Set l} -> 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
|
53 returnS x = mono x |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
55 returnSS : {l : Level} {A : Set l} -> A -> 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
|
56 returnSS x y = deltaAppend (returnS x) (returnS y) |
26
5ba82f107a95
Define Similar in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 |
33 | 58 |
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
|
59 -- Monad (Haskell) |
43
90b171e3a73e
Rename to Delta from Similar
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
42
diff
changeset
|
60 return : {l : Level} {A : Set l} -> A -> Delta A |
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
|
61 return = eta |
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 |
90
55d11ce7e223
Unify levels on data type. only use suc to proofs
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
89
diff
changeset
|
63 _>>=_ : {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
|
64 (x : Delta A) -> (f : A -> (Delta B)) -> (Delta B) |
57
dfcd72dc697e
ReDefine Delta used non-empty-list for infinite changes
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
56
diff
changeset
|
65 (mono x) >>= f = f x |
70
18a20a14c4b2
Change prove method. use Int ...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
66 (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
|
67 |
a7cd7740f33e
Add Haskell style Monad-laws and Proof Monad-laws-h-1
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
39
diff
changeset
|
68 |
38
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
69 |
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
70 -- proofs |
6ce83b2c9e59
Proof Functor-laws
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
36
diff
changeset
|
71 |
76 | 72 -- sub-proofs |
73 | |
74 n-tail-plus : {l : Level} {A : Set l} -> (n : Nat) -> ((n-tail {l} {A} n) ∙ tailDelta) ≡ n-tail (S n) | |
79 | 75 n-tail-plus O = refl |
76 | 76 n-tail-plus (S n) = begin |
77 n-tail (S n) ∙ tailDelta ≡⟨ refl ⟩ | |
78 (tailDelta ∙ (n-tail n)) ∙ tailDelta ≡⟨ refl ⟩ | |
79 tailDelta ∙ ((n-tail n) ∙ tailDelta) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-plus n) ⟩ | |
80 n-tail (S (S n)) | |
81 ∎ | |
82 | |
83 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) | |
84 n-tail-add O m = refl | |
85 n-tail-add (S n) O = begin | |
86 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
|
87 n-tail (S n) ≡⟨ cong (\n -> n-tail n) (nat-add-right-zero (S n))⟩ |
76 | 88 n-tail (S n + O) |
89 ∎ | |
90 n-tail-add {l} {A} {d} (S n) (S m) = begin | |
91 n-tail (S n) ∙ n-tail (S m) ≡⟨ refl ⟩ | |
92 (tailDelta ∙ (n-tail n)) ∙ n-tail (S m) ≡⟨ refl ⟩ | |
93 tailDelta ∙ ((n-tail n) ∙ n-tail (S m)) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-add {l} {A} {d} n (S m)) ⟩ | |
94 tailDelta ∙ (n-tail (n + (S m))) ≡⟨ refl ⟩ | |
95 n-tail (S (n + S m)) ≡⟨ refl ⟩ | |
96 n-tail (S n + S m) ∎ | |
97 | |
98 tail-delta-to-mono : {l : Level} {A : Set l} -> (n : Nat) -> (x : A) -> | |
99 (n-tail n) (mono x) ≡ (mono x) | |
79 | 100 tail-delta-to-mono O x = refl |
76 | 101 tail-delta-to-mono (S n) x = begin |
102 n-tail (S n) (mono x) ≡⟨ refl ⟩ | |
103 tailDelta (n-tail n (mono x)) ≡⟨ refl ⟩ | |
104 tailDelta (n-tail n (mono x)) ≡⟨ cong (\t -> tailDelta t) (tail-delta-to-mono n x) ⟩ | |
105 tailDelta (mono x) ≡⟨ refl ⟩ | |
106 mono x ∎ | |
107 | |
80 | 108 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
|
109 -> (f : A -> B) -> (d : Delta A) -> headDelta (delta-fmap f d) ≡ f (headDelta d) |
79 | 110 head-delta-natural-transformation f (mono x) = refl |
80 | 111 head-delta-natural-transformation f (delta x d) = refl |
79 | 112 |
113 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
|
114 -> (n : Nat) -> (f : A -> B) -> (d : Delta A) -> n-tail n (delta-fmap f d) ≡ delta-fmap f (n-tail n d) |
79 | 115 n-tail-natural-transformation O f d = refl |
116 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
|
117 n-tail (S n) (delta-fmap f (mono x)) ≡⟨ refl ⟩ |
79 | 118 n-tail (S n) (mono (f x)) ≡⟨ tail-delta-to-mono (S n) (f x) ⟩ |
119 (mono (f x)) ≡⟨ refl ⟩ | |
89
5411ce26d525
Defining DeltaM in Agda...
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
88
diff
changeset
|
120 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
|
121 delta-fmap f (n-tail (S n) (mono x)) ∎ |
79 | 122 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
|
123 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
|
124 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
|
125 ((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
|
126 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
|
127 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
|
128 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
|
129 delta-fmap f (n-tail (S n) (delta x d)) ∎ |