Mercurial > hg > Members > atton > delta_monad
comparison agda/delta.agda @ 131:d205ff1e406f InfiniteDeltaWithMonad
Cleanup proofs
author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 03 Feb 2015 12:57:13 +0900 |
parents | e6499a50ccbd |
children | 2bf1fa6d2006 |
comparison
equal
deleted
inserted
replaced
130:ac45d065cbf2 | 131:d205ff1e406f |
---|---|
1 open import Level | |
2 open import Relation.Binary.PropositionalEquality | |
3 open ≡-Reasoning | |
4 | |
1 open import list | 5 open import list |
2 open import basic | 6 open import basic |
3 open import nat | 7 open import nat |
4 open import laws | 8 open import laws |
5 | |
6 open import Level | |
7 open import Relation.Binary.PropositionalEquality | |
8 open ≡-Reasoning | |
9 | 9 |
10 module delta where | 10 module delta where |
11 | 11 |
12 data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where | 12 data Delta {l : Level} (A : Set l) : (Nat -> (Set l)) where |
13 mono : A -> Delta A (S O) | 13 mono : A -> Delta A (S O) |
36 -- Monad (Category) | 36 -- Monad (Category) |
37 delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n) | 37 delta-eta : {l : Level} {A : Set l} {n : Nat} -> A -> Delta A (S n) |
38 delta-eta {n = O} x = mono x | 38 delta-eta {n = O} x = mono x |
39 delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x) | 39 delta-eta {n = (S n)} x = delta x (delta-eta {n = n} x) |
40 | 40 |
41 | |
42 | |
43 | |
44 delta-mu : {l : Level} {A : Set l} {n : Nat} -> (Delta (Delta A (S n)) (S n)) -> Delta A (S n) | 41 delta-mu : {l : Level} {A : Set l} {n : Nat} -> (Delta (Delta A (S n)) (S n)) -> Delta A (S n) |
45 delta-mu (mono x) = x | 42 delta-mu (mono x) = x |
46 delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d)) | 43 delta-mu (delta x d) = delta (headDelta x) (delta-mu (delta-fmap tailDelta d)) |
47 | 44 |
48 delta-bind : {l : Level} {A B : Set l} {n : Nat} -> (Delta A (S n)) -> (A -> Delta B (S n)) -> Delta B (S n) | 45 delta-bind : {l : Level} {A B : Set l} {n : Nat} -> (Delta A (S n)) -> (A -> Delta B (S n)) -> Delta B (S n) |
49 delta-bind d f = delta-mu (delta-fmap f d) | 46 delta-bind d f = delta-mu (delta-fmap f d) |
50 | |
51 --delta-bind (mono x) f = f x | |
52 --delta-bind (delta x d) f = delta (headDelta (f x)) (tailDelta (f x)) | |
53 | |
54 | 47 |
55 {- | 48 {- |
56 -- Monad (Haskell) | 49 -- Monad (Haskell) |
57 delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O) | 50 delta-return : {l : Level} {A : Set l} -> A -> Delta A (S O) |
58 delta-return = delta-eta | 51 delta-return = delta-eta |
60 _>>=_ : {l : Level} {A B : Set l} {n : Nat} -> | 53 _>>=_ : {l : Level} {A B : Set l} {n : Nat} -> |
61 (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n) | 54 (x : Delta A n) -> (f : A -> (Delta B n)) -> (Delta B n) |
62 d >>= f = delta-bind d f | 55 d >>= f = delta-bind d f |
63 | 56 |
64 -} | 57 -} |
65 | |
66 {- | |
67 -- proofs | |
68 | |
69 -- sub-proofs | |
70 | |
71 n-tail-plus : {l : Level} {A : Set l} -> (n : Nat) -> ((n-tail {l} {A} n) ∙ tailDelta) ≡ n-tail (S n) | |
72 n-tail-plus O = refl | |
73 n-tail-plus (S n) = begin | |
74 n-tail (S n) ∙ tailDelta ≡⟨ refl ⟩ | |
75 (tailDelta ∙ (n-tail n)) ∙ tailDelta ≡⟨ refl ⟩ | |
76 tailDelta ∙ ((n-tail n) ∙ tailDelta) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-plus n) ⟩ | |
77 n-tail (S (S n)) | |
78 ∎ | |
79 | |
80 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) | |
81 n-tail-add O m = refl | |
82 n-tail-add (S n) O = begin | |
83 n-tail (S n) ∙ n-tail O ≡⟨ refl ⟩ | |
84 n-tail (S n) ≡⟨ cong (\n -> n-tail n) (nat-add-right-zero (S n))⟩ | |
85 n-tail (S n + O) | |
86 ∎ | |
87 n-tail-add {l} {A} {d} (S n) (S m) = begin | |
88 n-tail (S n) ∙ n-tail (S m) ≡⟨ refl ⟩ | |
89 (tailDelta ∙ (n-tail n)) ∙ n-tail (S m) ≡⟨ refl ⟩ | |
90 tailDelta ∙ ((n-tail n) ∙ n-tail (S m)) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-add {l} {A} {d} n (S m)) ⟩ | |
91 tailDelta ∙ (n-tail (n + (S m))) ≡⟨ refl ⟩ | |
92 n-tail (S (n + S m)) ≡⟨ refl ⟩ | |
93 n-tail (S n + S m) ∎ | |
94 | |
95 tail-delta-to-mono : {l : Level} {A : Set l} -> (n : Nat) -> (x : A) -> | |
96 (n-tail n) (mono x) ≡ (mono x) | |
97 tail-delta-to-mono O x = refl | |
98 tail-delta-to-mono (S n) x = begin | |
99 n-tail (S n) (mono x) ≡⟨ refl ⟩ | |
100 tailDelta (n-tail n (mono x)) ≡⟨ refl ⟩ | |
101 tailDelta (n-tail n (mono x)) ≡⟨ cong (\t -> tailDelta t) (tail-delta-to-mono n x) ⟩ | |
102 tailDelta (mono x) ≡⟨ refl ⟩ | |
103 mono x ∎ | |
104 | |
105 head-delta-natural-transformation : {l : Level} {A B : Set l} | |
106 -> (f : A -> B) -> (d : Delta A) -> headDelta (delta-fmap f d) ≡ f (headDelta d) | |
107 head-delta-natural-transformation f (mono x) = refl | |
108 head-delta-natural-transformation f (delta x d) = refl | |
109 | |
110 n-tail-natural-transformation : {l : Level} {A B : Set l} | |
111 -> (n : Nat) -> (f : A -> B) -> (d : Delta A) -> n-tail n (delta-fmap f d) ≡ delta-fmap f (n-tail n d) | |
112 n-tail-natural-transformation O f d = refl | |
113 n-tail-natural-transformation (S n) f (mono x) = begin | |
114 n-tail (S n) (delta-fmap f (mono x)) ≡⟨ refl ⟩ | |
115 n-tail (S n) (mono (f x)) ≡⟨ tail-delta-to-mono (S n) (f x) ⟩ | |
116 (mono (f x)) ≡⟨ refl ⟩ | |
117 delta-fmap f (mono x) ≡⟨ cong (\d -> delta-fmap f d) (sym (tail-delta-to-mono (S n) x)) ⟩ | |
118 delta-fmap f (n-tail (S n) (mono x)) ∎ | |
119 n-tail-natural-transformation (S n) f (delta x d) = begin | |
120 n-tail (S n) (delta-fmap f (delta x d)) ≡⟨ refl ⟩ | |
121 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)) ⟩ | |
122 ((n-tail n) ∙ tailDelta) (delta (f x) (delta-fmap f d)) ≡⟨ refl ⟩ | |
123 n-tail n (delta-fmap f d) ≡⟨ n-tail-natural-transformation n f d ⟩ | |
124 delta-fmap f (n-tail n d) ≡⟨ refl ⟩ | |
125 delta-fmap f (((n-tail n) ∙ tailDelta) (delta x d)) ≡⟨ cong (\t -> delta-fmap f (t (delta x d))) (n-tail-plus n) ⟩ | |
126 delta-fmap f (n-tail (S n) (delta x d)) ∎ | |
127 -} |