Mercurial > hg > Members > atton > delta_monad
comparison agda/delta.agda @ 56:bfb6be9a689d
Trying redefine monad-laws-1
| author | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 19 Nov 2014 21:09:45 +0900 |
| parents | 9c8c09334e32 |
| children | dfcd72dc697e |
comparison
equal
deleted
inserted
replaced
| 55:9c8c09334e32 | 56:bfb6be9a689d |
|---|---|
| 62 x >>= f = mu (fmap f x) | 62 x >>= f = mu (fmap f x) |
| 63 | 63 |
| 64 | 64 |
| 65 | 65 |
| 66 -- proofs | 66 -- proofs |
| 67 | |
| 68 -- sub proofs | |
| 69 twice-log-append : {l : Level} {A : Set l} -> (l : List String) -> (ll : List String) -> (d : Delta A) -> | |
| 70 logAppend l (logAppend ll d) ≡ logAppend (l ++ ll) d | |
| 71 twice-log-append l ll (mono lx x) = begin | |
| 72 mono (l ++ (ll ++ lx)) x | |
| 73 ≡⟨ cong (\l -> mono l x) (list-associative l ll lx) ⟩ | |
| 74 mono (l ++ ll ++ lx) x | |
| 75 ∎ | |
| 76 twice-log-append l ll (delta lx x d) = begin | |
| 77 delta (l ++ (ll ++ lx)) x (logAppend l (logAppend ll d)) | |
| 78 ≡⟨ cong (\lx -> delta lx x (logAppend l (logAppend ll d))) (list-associative l ll lx) ⟩ | |
| 79 delta (l ++ ll ++ lx) x (logAppend l (logAppend ll d)) | |
| 80 ≡⟨ cong (delta (l ++ ll ++ lx) x) (twice-log-append l ll d) ⟩ | |
| 81 delta (l ++ ll ++ lx) x (logAppend (l ++ ll) d) | |
| 82 ∎ | |
| 67 | 83 |
| 68 | 84 |
| 69 -- Functor-laws | 85 -- Functor-laws |
| 70 | 86 |
| 71 -- Functor-law-1 : T(id) = id' | 87 -- Functor-law-1 : T(id) = id' |
| 79 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d | 95 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d |
| 80 functor-law-2 f g (mono lx x) = refl | 96 functor-law-2 f g (mono lx x) = refl |
| 81 functor-law-2 f g (delta lx x d) = cong (delta lx (f (g x))) (functor-law-2 f g d) | 97 functor-law-2 f g (delta lx x d) = cong (delta lx (f (g x))) (functor-law-2 f g d) |
| 82 | 98 |
| 83 | 99 |
| 100 | |
| 101 -- Monad-laws (Category) | |
| 102 | |
| 103 -- monad-law-1 : join . fmap join = join . join | |
| 104 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d) | |
| 105 monad-law-1 (mono lx (mono llx (mono lllx x))) = begin | |
| 106 mono (lx ++ (llx ++ lllx)) x | |
| 107 ≡⟨ cong (\l -> mono l x) (list-associative lx llx lllx) ⟩ | |
| 108 mono (lx ++ llx ++ lllx) x | |
| 109 ∎ | |
| 110 monad-law-1 (mono lx (mono llx (delta lllx x d))) = begin | |
| 111 delta (lx ++ (llx ++ lllx)) x (logAppend lx (logAppend llx d)) | |
| 112 ≡⟨ cong (\l -> delta l x (logAppend lx (logAppend llx d))) (list-associative lx llx lllx) ⟩ | |
| 113 delta (lx ++ llx ++ lllx) x (logAppend lx (logAppend llx d)) | |
| 114 ≡⟨ cong (\d -> delta (lx ++ llx ++ lllx) x d) (twice-log-append lx llx d) ⟩ | |
| 115 delta (lx ++ llx ++ lllx) x (logAppend (lx ++ llx) d) | |
| 116 ∎ | |
| 117 monad-law-1 (mono lx (delta ld (mono x x₁) (mono x₂ (mono x₃ x₄)))) = begin | |
| 118 delta (lx ++ (ld ++ x)) x₁ (mono (lx ++ (x₂ ++ x₃)) x₄) | |
| 119 ≡⟨ cong (\l -> delta l x₁(mono (lx ++ (x₂ ++ x₃)) x₄)) (list-associative lx ld x) ⟩ | |
| 120 delta (lx ++ ld ++ x) x₁ (mono (lx ++ (x₂ ++ x₃)) x₄) | |
| 121 ≡⟨ cong (\l -> delta (lx ++ ld ++ x) x₁ (mono l x₄)) (list-associative lx x₂ x₃) ⟩ | |
| 122 delta (lx ++ ld ++ x) x₁ (mono (lx ++ x₂ ++ x₃) x₄) | |
| 123 ∎ | |
| 124 monad-law-1 (mono lx (delta ld (mono x x₁) (mono x₂ (delta x₃ x₄ ds)))) = begin | |
| 125 delta (lx ++ (ld ++ x)) x₁ (logAppend lx (logAppend x₂ ds)) | |
| 126 ≡⟨ cong (\l -> delta l x₁ (logAppend lx (logAppend x₂ ds))) (list-associative lx ld x) ⟩ | |
| 127 delta (lx ++ ld ++ x) x₁ (logAppend lx (logAppend x₂ ds)) | |
| 128 ≡⟨ cong (\d -> delta (lx ++ ld ++ x) x₁ d) (twice-log-append lx x₂ ds) ⟩ | |
| 129 delta (lx ++ ld ++ x) x₁ (logAppend (lx ++ x₂) ds) | |
| 130 ∎ | |
| 131 monad-law-1 (mono lx (delta ld (delta x x₁ (mono x₂ x₃)) (mono x₄ (mono x₅ x₆)))) = begin | |
| 132 delta (lx ++ (ld ++ x)) x₁ (mono (lx ++ (x₄ ++ x₅)) x₆) | |
| 133 ≡⟨ cong (\l -> delta l x₁ (mono (lx ++ (x₄ ++ x₅)) x₆)) (list-associative lx ld x ) ⟩ | |
| 134 delta (lx ++ ld ++ x) x₁ (mono (lx ++ (x₄ ++ x₅)) x₆) | |
| 135 ≡⟨ cong (\l -> delta (lx ++ ld ++ x) x₁ (mono l x₆)) (list-associative lx x₄ x₅)⟩ | |
| 136 delta (lx ++ ld ++ x) x₁ (mono (lx ++ x₄ ++ x₅) x₆) | |
| 137 ∎ | |
| 138 monad-law-1 (mono lx (delta ld (delta x x₁ (mono x₂ x₃)) (mono x₄ (delta x₅ x₆ ds)))) = begin | |
| 139 delta (lx ++ (ld ++ x)) x₁ (logAppend lx (logAppend x₄ ds)) | |
| 140 ≡⟨ cong (\l -> delta l x₁(logAppend lx (logAppend x₄ ds))) (list-associative lx ld x ) ⟩ | |
| 141 delta (lx ++ ld ++ x) x₁ (logAppend lx (logAppend x₄ ds)) | |
| 142 ≡⟨ cong (\d -> delta (lx ++ ld ++ x) x₁ d) (twice-log-append lx x₄ ds ) ⟩ | |
| 143 delta (lx ++ ld ++ x) x₁ (logAppend (lx ++ x₄) ds) | |
| 144 ∎ | |
| 145 | |
| 146 monad-law-1 (mono lx (delta ld (delta x x₁ (delta ly y (mono x₂ x₃))) (mono x₄ (mono x₅ x₆)))) = begin | |
| 147 delta (lx ++ (ld ++ x)) x₁ (mono (lx ++ (x₄ ++ x₅)) x₆) | |
| 148 ≡⟨ {!!} ⟩ | |
| 149 delta (lx ++ ld ++ x) x₁ (mono (lx ++ x₄ ++ x₅) x₆) | |
| 150 ∎ | |
| 151 monad-law-1 (mono lx (delta ld (delta x x₁ (delta ly y (mono x₂ x₃))) (mono x₄ (delta x₅ x₆ ds)))) = begin | |
| 152 delta (lx ++ (ld ++ x)) x₁ (logAppend lx (logAppend x₄ ds)) | |
| 153 ≡⟨ {!!} ⟩ | |
| 154 delta (lx ++ ld ++ x) x₁ (logAppend (lx ++ x₄) ds) | |
| 155 ∎ | |
| 156 monad-law-1 (mono lx (delta ld (delta x x₁ (delta ly y (delta x₂ x₃ d))) (mono x₄ (mono x₅ x₆)))) = begin | |
| 157 delta (lx ++ (ld ++ x)) x₁ (mono (lx ++ (x₄ ++ x₅)) x₆) | |
| 158 ≡⟨ {!!} ⟩ | |
| 159 delta (lx ++ ld ++ x) x₁ (mono (lx ++ x₄ ++ x₅) x₆) | |
| 160 ∎ | |
| 161 monad-law-1 (mono lx (delta ld (delta x x₁ (delta ly y (delta x₂ x₃ d))) (mono x₄ (delta x₅ x₆ ds)))) = begin | |
| 162 delta (lx ++ (ld ++ x)) x₁ (logAppend lx (logAppend x₄ ds)) | |
| 163 ≡⟨ {!!} ⟩ | |
| 164 delta (lx ++ ld ++ x) x₁ (logAppend (lx ++ x₄) ds) | |
| 165 ∎ | |
| 166 | |
| 167 | |
| 168 | |
| 169 | |
| 170 monad-law-1 (mono lx (delta ld d (delta x ds ds₁))) = {!!} | |
| 171 | |
| 172 | |
| 173 | |
| 174 monad-law-1 (delta lx x d) = {!!} | |
| 175 | |
| 84 {- | 176 {- |
| 85 -- Monad-laws (Category) | |
| 86 | |
| 87 -- monad-law-1 : join . fmap join = join . join | |
| 88 monad-law-1 : {l : Level} {A : Set l} -> (s : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s) | |
| 89 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _)) | |
| 90 ly (similar _ (similar _ _ _ _) lly (similar _ _ llly y))) = begin | |
| 91 similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y | |
| 92 ≡⟨ cong (\left-list -> similar left-list x (ly ++ (lly ++ llly)) y) (list-associative lx llx lllx) ⟩ | |
| 93 similar (lx ++ llx ++ lllx) x (ly ++ (lly ++ llly)) y | |
| 94 ≡⟨ cong (\right-list -> similar (lx ++ llx ++ lllx) x right-list y ) (list-associative ly lly llly) ⟩ | |
| 95 similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y | |
| 96 ∎ | |
| 97 | |
| 98 | |
| 99 -- monad-law-2 : join . fmap return = join . return = id | 177 -- monad-law-2 : join . fmap return = join . return = id |
| 100 -- monad-law-2-1 join . fmap return = join . return | 178 -- monad-law-2-1 join . fmap return = join . return |
| 101 monad-law-2-1 : {l : Level} {A : Set l} -> (s : Delta A) -> | 179 monad-law-2-1 : {l : Level} {A : Set l} -> (s : Delta A) -> |
| 102 (mu ∙ fmap eta) s ≡ (mu ∙ eta) s | 180 (mu ∙ fmap eta) s ≡ (mu ∙ eta) s |
| 103 monad-law-2-1 (similar lx x ly y) = begin | 181 monad-law-2-1 (similar lx x ly y) = begin |