# HG changeset patch # User Yasutaka Higa # Date 1417422649 -32400 # Node ID fc5cd8c5031299fb4c5090528d2ac9a8e62e4d0a # Parent 7307e43a3c768694896f63145b53e40c52d05cd8 Adjust proofs diff -r 7307e43a3c76 -r fc5cd8c50312 agda/delta.agda --- a/agda/delta.agda Mon Dec 01 17:25:59 2014 +0900 +++ b/agda/delta.agda Mon Dec 01 17:30:49 2014 +0900 @@ -104,10 +104,10 @@ tailDelta (mono x) ≡⟨ refl ⟩ mono x ∎ -head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} +head-delta-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} -> (f : A -> B) -> (d : Delta A) -> headDelta (fmap f d) ≡ f (headDelta d) head-delta-natural-transformation f (mono x) = refl -head-delta-natural-transformation f (delta x d) = refl +head-delta-natural-transformation f (delta x d) = refl n-tail-natural-transformation : {l ll : Level} {A : Set l} {B : Set ll} -> (n : Nat) -> (f : A -> B) -> (d : Delta A) -> n-tail n (fmap f d) ≡ fmap f (n-tail n d) @@ -146,67 +146,66 @@ -- Monad-laws (Category) -{- monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) -> n-tail n (bind ds (n-tail m)) ≡ bind (n-tail n ds) (n-tail (m + n)) monad-law-1-5 O O ds = refl monad-law-1-5 O (S n) (mono ds) = begin - n-tail (S n) (bind (mono ds) (n-tail O)) ≡⟨ refl ⟩ - n-tail (S n) ds ≡⟨ refl ⟩ - bind (mono ds) (n-tail (S n)) ≡⟨ cong (\de -> bind de (n-tail (S n))) (sym (tail-delta-to-mono (S n) ds)) ⟩ + n-tail (S n) (bind (mono ds) (n-tail O)) ≡⟨ refl ⟩ + n-tail (S n) ds ≡⟨ refl ⟩ + bind (mono ds) (n-tail (S n)) ≡⟨ cong (\de -> bind de (n-tail (S n))) (sym (tail-delta-to-mono (S n) ds)) ⟩ bind (n-tail (S n) (mono ds)) (n-tail (S n)) ≡⟨ refl ⟩ bind (n-tail (S n) (mono ds)) (n-tail (O + S n)) ∎ monad-law-1-5 O (S n) (delta d ds) = begin - n-tail (S n) (bind (delta d ds) (n-tail O)) ≡⟨ refl ⟩ - n-tail (S n) (delta (headDelta d) (bind ds tailDelta )) ≡⟨ cong (\t -> t (delta (headDelta d) (bind ds tailDelta ))) (sym (n-tail-plus n)) ⟩ + n-tail (S n) (bind (delta d ds) (n-tail O)) ≡⟨ refl ⟩ + n-tail (S n) (delta (headDelta d) (bind ds tailDelta )) ≡⟨ cong (\t -> t (delta (headDelta d) (bind ds tailDelta ))) (sym (n-tail-plus n)) ⟩ ((n-tail n) ∙ tailDelta) (delta (headDelta d) (bind ds tailDelta )) ≡⟨ refl ⟩ - (n-tail n) (bind ds tailDelta) ≡⟨ monad-law-1-5 (S O) n ds ⟩ - bind (n-tail n ds) (n-tail (S n)) ≡⟨ refl ⟩ - bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S n)) ≡⟨ cong (\t -> bind (t (delta d ds)) (n-tail (S n))) (n-tail-plus n) ⟩ - bind (n-tail (S n) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩ + (n-tail n) (bind ds tailDelta) ≡⟨ monad-law-1-5 (S O) n ds ⟩ + bind (n-tail n ds) (n-tail (S n)) ≡⟨ refl ⟩ + bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S n)) ≡⟨ cong (\t -> bind (t (delta d ds)) (n-tail (S n))) (n-tail-plus n) ⟩ + bind (n-tail (S n) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩ bind (n-tail (S n) (delta d ds)) (n-tail (O + S n)) ∎ monad-law-1-5 (S m) n (mono (mono x)) = begin n-tail n (bind (mono (mono x)) (n-tail (S m))) ≡⟨ refl ⟩ - n-tail n (n-tail (S m) (mono x)) ≡⟨ cong (\de -> n-tail n de) (tail-delta-to-mono (S m) x)⟩ - n-tail n (mono x) ≡⟨ tail-delta-to-mono n x ⟩ - mono x ≡⟨ sym (tail-delta-to-mono (S m + n) x) ⟩ - (n-tail (S m + n)) (mono x) ≡⟨ refl ⟩ - bind (mono (mono x)) (n-tail (S m + n)) ≡⟨ cong (\de -> bind de (n-tail (S m + n))) (sym (tail-delta-to-mono n (mono x))) ⟩ + n-tail n (n-tail (S m) (mono x)) ≡⟨ cong (\de -> n-tail n de) (tail-delta-to-mono (S m) x)⟩ + n-tail n (mono x) ≡⟨ tail-delta-to-mono n x ⟩ + mono x ≡⟨ sym (tail-delta-to-mono (S m + n) x) ⟩ + (n-tail (S m + n)) (mono x) ≡⟨ refl ⟩ + bind (mono (mono x)) (n-tail (S m + n)) ≡⟨ cong (\de -> bind de (n-tail (S m + n))) (sym (tail-delta-to-mono n (mono x))) ⟩ bind (n-tail n (mono (mono x))) (n-tail (S m + n)) ∎ monad-law-1-5 (S m) n (mono (delta x ds)) = begin n-tail n (bind (mono (delta x ds)) (n-tail (S m))) ≡⟨ refl ⟩ - n-tail n (n-tail (S m) (delta x ds)) ≡⟨ cong (\t -> n-tail n (t (delta x ds))) (sym (n-tail-plus m)) ⟩ - n-tail n (((n-tail m) ∙ tailDelta) (delta x ds)) ≡⟨ refl ⟩ - n-tail n ((n-tail m) ds) ≡⟨ cong (\t -> t ds) (n-tail-add {d = ds} n m) ⟩ - n-tail (n + m) ds ≡⟨ cong (\n -> n-tail n ds) (nat-add-sym n m) ⟩ - n-tail (m + n) ds ≡⟨ refl ⟩ - ((n-tail (m + n)) ∙ tailDelta) (delta x ds) ≡⟨ cong (\t -> t (delta x ds)) (n-tail-plus (m + n))⟩ - n-tail (S (m + n)) (delta x ds) ≡⟨ refl ⟩ - n-tail (S m + n) (delta x ds) ≡⟨ refl ⟩ - bind (mono (delta x ds)) (n-tail (S m + n)) ≡⟨ cong (\de -> bind de (n-tail (S m + n))) (sym (tail-delta-to-mono n (delta x ds))) ⟩ + n-tail n (n-tail (S m) (delta x ds)) ≡⟨ cong (\t -> n-tail n (t (delta x ds))) (sym (n-tail-plus m)) ⟩ + n-tail n (((n-tail m) ∙ tailDelta) (delta x ds)) ≡⟨ refl ⟩ + n-tail n ((n-tail m) ds) ≡⟨ cong (\t -> t ds) (n-tail-add {d = ds} n m) ⟩ + n-tail (n + m) ds ≡⟨ cong (\n -> n-tail n ds) (nat-add-sym n m) ⟩ + n-tail (m + n) ds ≡⟨ refl ⟩ + ((n-tail (m + n)) ∙ tailDelta) (delta x ds) ≡⟨ cong (\t -> t (delta x ds)) (n-tail-plus (m + n))⟩ + n-tail (S (m + n)) (delta x ds) ≡⟨ refl ⟩ + n-tail (S m + n) (delta x ds) ≡⟨ refl ⟩ + bind (mono (delta x ds)) (n-tail (S m + n)) ≡⟨ cong (\de -> bind de (n-tail (S m + n))) (sym (tail-delta-to-mono n (delta x ds))) ⟩ bind (n-tail n (mono (delta x ds))) (n-tail (S m + n)) ∎ monad-law-1-5 (S m) O (delta d ds) = begin - n-tail O (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩ - (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩ + n-tail O (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩ + (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩ delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m)))) ≡⟨ refl ⟩ - bind (delta d ds) (n-tail (S m)) ≡⟨ refl ⟩ - bind (n-tail O (delta d ds)) (n-tail (S m)) ≡⟨ cong (\n -> bind (n-tail O (delta d ds)) (n-tail n)) (nat-add-right-zero (S m)) ⟩ + bind (delta d ds) (n-tail (S m)) ≡⟨ refl ⟩ + bind (n-tail O (delta d ds)) (n-tail (S m)) ≡⟨ cong (\n -> bind (n-tail O (delta d ds)) (n-tail n)) (nat-add-right-zero (S m)) ⟩ bind (n-tail O (delta d ds)) (n-tail (S m + O)) ∎ monad-law-1-5 (S m) (S n) (delta d ds) = begin - n-tail (S n) (bind (delta d ds) (n-tail (S m))) ≡⟨ cong (\t -> t ((bind (delta d ds) (n-tail (S m))))) (sym (n-tail-plus n)) ⟩ - ((n-tail n) ∙ tailDelta) (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩ + n-tail (S n) (bind (delta d ds) (n-tail (S m))) ≡⟨ cong (\t -> t ((bind (delta d ds) (n-tail (S m))))) (sym (n-tail-plus n)) ⟩ + ((n-tail n) ∙ tailDelta) (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩ ((n-tail n) ∙ tailDelta) (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩ - (n-tail n) (bind ds (tailDelta ∙ (n-tail (S m)))) ≡⟨ refl ⟩ - (n-tail n) (bind ds (n-tail (S (S m)))) ≡⟨ monad-law-1-5 (S (S m)) n ds ⟩ - bind ((n-tail n) ds) (n-tail (S (S (m + n)))) ≡⟨ cong (\nm -> bind ((n-tail n) ds) (n-tail nm)) (sym (nat-right-increment (S m) n)) ⟩ - bind ((n-tail n) ds) (n-tail (S m + S n)) ≡⟨ refl ⟩ - bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S m + S n)) ≡⟨ cong (\t -> bind (t (delta d ds)) (n-tail (S m + S n))) (n-tail-plus n) ⟩ + (n-tail n) (bind ds (tailDelta ∙ (n-tail (S m)))) ≡⟨ refl ⟩ + (n-tail n) (bind ds (n-tail (S (S m)))) ≡⟨ monad-law-1-5 (S (S m)) n ds ⟩ + bind ((n-tail n) ds) (n-tail (S (S (m + n)))) ≡⟨ cong (\nm -> bind ((n-tail n) ds) (n-tail nm)) (sym (nat-right-increment (S m) n)) ⟩ + bind ((n-tail n) ds) (n-tail (S m + S n)) ≡⟨ refl ⟩ + bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S m + S n)) ≡⟨ cong (\t -> bind (t (delta d ds)) (n-tail (S m + S n))) (n-tail-plus n) ⟩ bind (n-tail (S n) (delta d ds)) (n-tail (S m + S n)) ∎ @@ -215,49 +214,49 @@ monad-law-1-4 O O (mono dd) = refl monad-law-1-4 O O (delta dd dd₁) = refl monad-law-1-4 O (S n) (mono dd) = begin - headDelta (n-tail (S n) (bind (mono dd) (n-tail O))) ≡⟨ refl ⟩ - headDelta (n-tail (S n) dd) ≡⟨ refl ⟩ - headDelta (n-tail (S n) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S n) (headDelta de))) (sym (tail-delta-to-mono (S n) dd)) ⟩ + headDelta (n-tail (S n) (bind (mono dd) (n-tail O))) ≡⟨ refl ⟩ + headDelta (n-tail (S n) dd) ≡⟨ refl ⟩ + headDelta (n-tail (S n) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S n) (headDelta de))) (sym (tail-delta-to-mono (S n) dd)) ⟩ headDelta (n-tail (S n) (headDelta (n-tail (S n) (mono dd)))) ≡⟨ refl ⟩ headDelta (n-tail (O + S n) (headDelta (n-tail (S n) (mono dd)))) ∎ monad-law-1-4 O (S n) (delta d ds) = begin - headDelta (n-tail (S n) (bind (delta d ds) (n-tail O))) ≡⟨ refl ⟩ - headDelta (n-tail (S n) (bind (delta d ds) id)) ≡⟨ refl ⟩ - headDelta (n-tail (S n) (delta (headDelta d) (bind ds tailDelta))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta d) (bind ds tailDelta)))) (sym (n-tail-plus n)) ⟩ + headDelta (n-tail (S n) (bind (delta d ds) (n-tail O))) ≡⟨ refl ⟩ + headDelta (n-tail (S n) (bind (delta d ds) id)) ≡⟨ refl ⟩ + headDelta (n-tail (S n) (delta (headDelta d) (bind ds tailDelta))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta d) (bind ds tailDelta)))) (sym (n-tail-plus n)) ⟩ headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta d) (bind ds tailDelta))) ≡⟨ refl ⟩ - headDelta (n-tail n (bind ds tailDelta)) ≡⟨ monad-law-1-4 (S O) n ds ⟩ - headDelta (n-tail (S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩ - headDelta (n-tail (S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩ - headDelta (n-tail (S n) (headDelta (n-tail (S n) (delta d ds)))) ≡⟨ refl ⟩ + headDelta (n-tail n (bind ds tailDelta)) ≡⟨ monad-law-1-4 (S O) n ds ⟩ + headDelta (n-tail (S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩ + headDelta (n-tail (S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩ + headDelta (n-tail (S n) (headDelta (n-tail (S n) (delta d ds)))) ≡⟨ refl ⟩ headDelta (n-tail (O + S n) (headDelta (n-tail (S n) (delta d ds)))) ∎ monad-law-1-4 (S m) n (mono dd) = begin headDelta (n-tail n (bind (mono dd) (n-tail (S m)))) ≡⟨ refl ⟩ - headDelta (n-tail n ((n-tail (S m)) dd))≡⟨ cong (\t -> headDelta (t dd)) (n-tail-add {d = dd} n (S m)) ⟩ - headDelta (n-tail (n + S m) dd) ≡⟨ cong (\n -> headDelta ((n-tail n) dd)) (nat-add-sym n (S m)) ⟩ - headDelta (n-tail (S m + n) dd) ≡⟨ refl ⟩ - headDelta (n-tail (S m + n) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S m + n) (headDelta de))) (sym (tail-delta-to-mono n dd)) ⟩ + headDelta (n-tail n ((n-tail (S m)) dd)) ≡⟨ cong (\t -> headDelta (t dd)) (n-tail-add {d = dd} n (S m)) ⟩ + headDelta (n-tail (n + S m) dd) ≡⟨ cong (\n -> headDelta ((n-tail n) dd)) (nat-add-sym n (S m)) ⟩ + headDelta (n-tail (S m + n) dd) ≡⟨ refl ⟩ + headDelta (n-tail (S m + n) (headDelta (mono dd))) ≡⟨ cong (\de -> headDelta (n-tail (S m + n) (headDelta de))) (sym (tail-delta-to-mono n dd)) ⟩ headDelta (n-tail (S m + n) (headDelta (n-tail n (mono dd)))) ∎ monad-law-1-4 (S m) O (delta d ds) = begin - headDelta (n-tail O (bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩ - headDelta (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩ + headDelta (n-tail O (bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩ + headDelta (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩ headDelta (delta (headDelta ((n-tail (S m) d))) (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩ - headDelta (n-tail (S m) d) ≡⟨ cong (\n -> headDelta ((n-tail n) d)) (nat-add-right-zero (S m)) ⟩ - headDelta (n-tail (S m + O) d) ≡⟨ refl ⟩ - headDelta (n-tail (S m + O) (headDelta (delta d ds))) ≡⟨ refl ⟩ + headDelta (n-tail (S m) d) ≡⟨ cong (\n -> headDelta ((n-tail n) d)) (nat-add-right-zero (S m)) ⟩ + headDelta (n-tail (S m + O) d) ≡⟨ refl ⟩ + headDelta (n-tail (S m + O) (headDelta (delta d ds))) ≡⟨ refl ⟩ headDelta (n-tail (S m + O) (headDelta (n-tail O (delta d ds)))) ∎ monad-law-1-4 (S m) (S n) (delta d ds) = begin - headDelta (n-tail (S n) (bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩ - headDelta (n-tail (S n) (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m)))))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m))))))) (sym (n-tail-plus n)) ⟩ + headDelta (n-tail (S n) (bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩ + headDelta (n-tail (S n) (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m)))))) ≡⟨ cong (\t -> headDelta (t (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m))))))) (sym (n-tail-plus n)) ⟩ headDelta ((((n-tail n) ∙ tailDelta) (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m))))))) ≡⟨ refl ⟩ - headDelta (n-tail n (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩ - headDelta (n-tail n (bind ds (n-tail (S (S m))))) ≡⟨ monad-law-1-4 (S (S m)) n ds ⟩ - headDelta (n-tail ((S (S m) + n)) (headDelta (n-tail n ds))) ≡⟨ cong (\nm -> headDelta ((n-tail nm) (headDelta (n-tail n ds)))) (sym (nat-right-increment (S m) n)) ⟩ - headDelta (n-tail (S m + S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩ - headDelta (n-tail (S m + S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S m + S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩ + headDelta (n-tail n (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩ + headDelta (n-tail n (bind ds (n-tail (S (S m))))) ≡⟨ monad-law-1-4 (S (S m)) n ds ⟩ + headDelta (n-tail ((S (S m) + n)) (headDelta (n-tail n ds))) ≡⟨ cong (\nm -> headDelta ((n-tail nm) (headDelta (n-tail n ds)))) (sym (nat-right-increment (S m) n)) ⟩ + headDelta (n-tail (S m + S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩ + headDelta (n-tail (S m + S n) (headDelta (((n-tail n) ∙ tailDelta) (delta d ds)))) ≡⟨ cong (\t -> headDelta (n-tail (S m + S n) (headDelta (t (delta d ds))))) (n-tail-plus n) ⟩ headDelta (n-tail (S m + S n) (headDelta (n-tail (S n) (delta d ds)))) ∎ @@ -269,33 +268,33 @@ bind (fmap mu d) (n-tail n) ≡ bind (bind d (n-tail n)) (n-tail n) monad-law-1-3 O (mono d) = refl monad-law-1-3 O (delta d ds) = begin - bind (fmap mu (delta d ds)) (n-tail O) ≡⟨ refl ⟩ - bind (delta (mu d) (fmap mu ds)) (n-tail O) ≡⟨ refl ⟩ - delta (headDelta (mu d)) (bind (fmap mu ds) tailDelta) ≡⟨ cong (\dx -> delta dx (bind (fmap mu ds) tailDelta)) (monad-law-1-2 d) ⟩ - delta (headDelta (headDelta d)) (bind (fmap mu ds) tailDelta) ≡⟨ cong (\dx -> delta (headDelta (headDelta d)) dx) (monad-law-1-3 (S O) ds) ⟩ + bind (fmap mu (delta d ds)) (n-tail O) ≡⟨ refl ⟩ + bind (delta (mu d) (fmap mu ds)) (n-tail O) ≡⟨ refl ⟩ + delta (headDelta (mu d)) (bind (fmap mu ds) tailDelta) ≡⟨ cong (\dx -> delta dx (bind (fmap mu ds) tailDelta)) (monad-law-1-2 d) ⟩ + delta (headDelta (headDelta d)) (bind (fmap mu ds) tailDelta) ≡⟨ cong (\dx -> delta (headDelta (headDelta d)) dx) (monad-law-1-3 (S O) ds) ⟩ delta (headDelta (headDelta d)) (bind (bind ds tailDelta) tailDelta) ≡⟨ refl ⟩ - bind (delta (headDelta d) (bind ds tailDelta)) (n-tail O) ≡⟨ refl ⟩ + bind (delta (headDelta d) (bind ds tailDelta)) (n-tail O) ≡⟨ refl ⟩ bind (bind (delta d ds) (n-tail O)) (n-tail O) ∎ monad-law-1-3 (S n) (mono (mono d)) = begin bind (fmap mu (mono (mono d))) (n-tail (S n)) ≡⟨ refl ⟩ - bind (mono d) (n-tail (S n)) ≡⟨ refl ⟩ - (n-tail (S n)) d ≡⟨ refl ⟩ - bind (mono d) (n-tail (S n)) ≡⟨ cong (\t -> bind t (n-tail (S n))) (sym (tail-delta-to-mono (S n) d))⟩ - bind (n-tail (S n) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩ - bind (n-tail (S n) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩ + bind (mono d) (n-tail (S n)) ≡⟨ refl ⟩ + (n-tail (S n)) d ≡⟨ refl ⟩ + bind (mono d) (n-tail (S n)) ≡⟨ cong (\t -> bind t (n-tail (S n))) (sym (tail-delta-to-mono (S n) d))⟩ + bind (n-tail (S n) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩ + bind (n-tail (S n) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩ bind (bind (mono (mono d)) (n-tail (S n))) (n-tail (S n)) ∎ monad-law-1-3 (S n) (mono (delta d ds)) = begin - bind (fmap mu (mono (delta d ds))) (n-tail (S n)) ≡⟨ refl ⟩ - bind (mono (mu (delta d ds))) (n-tail (S n)) ≡⟨ refl ⟩ - n-tail (S n) (mu (delta d ds)) ≡⟨ refl ⟩ - n-tail (S n) (delta (headDelta d) (bind ds tailDelta)) ≡⟨ cong (\t -> t (delta (headDelta d) (bind ds tailDelta))) (sym (n-tail-plus n)) ⟩ - (n-tail n ∙ tailDelta) (delta (headDelta d) (bind ds tailDelta)) ≡⟨ refl ⟩ - n-tail n (bind ds tailDelta) ≡⟨ monad-law-1-5 (S O) n ds ⟩ - bind (n-tail n ds) (n-tail (S n)) ≡⟨ refl ⟩ - bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S n)) ≡⟨ cong (\t -> (bind (t (delta d ds)) (n-tail (S n)))) (n-tail-plus n) ⟩ - bind (n-tail (S n) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩ + bind (fmap mu (mono (delta d ds))) (n-tail (S n)) ≡⟨ refl ⟩ + bind (mono (mu (delta d ds))) (n-tail (S n)) ≡⟨ refl ⟩ + n-tail (S n) (mu (delta d ds)) ≡⟨ refl ⟩ + n-tail (S n) (delta (headDelta d) (bind ds tailDelta)) ≡⟨ cong (\t -> t (delta (headDelta d) (bind ds tailDelta))) (sym (n-tail-plus n)) ⟩ + (n-tail n ∙ tailDelta) (delta (headDelta d) (bind ds tailDelta)) ≡⟨ refl ⟩ + n-tail n (bind ds tailDelta) ≡⟨ monad-law-1-5 (S O) n ds ⟩ + bind (n-tail n ds) (n-tail (S n)) ≡⟨ refl ⟩ + bind (((n-tail n) ∙ tailDelta) (delta d ds)) (n-tail (S n)) ≡⟨ cong (\t -> (bind (t (delta d ds)) (n-tail (S n)))) (n-tail-plus n) ⟩ + bind (n-tail (S n) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩ bind (bind (mono (delta d ds)) (n-tail (S n))) (n-tail (S n)) ∎ monad-law-1-3 (S n) (delta (mono d) ds) = begin @@ -335,28 +334,18 @@ monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d) monad-law-1 (mono d) = refl monad-law-1 (delta x d) = begin - (mu ∙ fmap mu) (delta x d) - ≡⟨ refl ⟩ - mu (fmap mu (delta x d)) - ≡⟨ refl ⟩ - mu (delta (mu x) (fmap mu d)) - ≡⟨ refl ⟩ - delta (headDelta (mu x)) (bind (fmap mu d) tailDelta) - ≡⟨ cong (\x -> delta x (bind (fmap mu d) tailDelta)) (monad-law-1-2 x) ⟩ - delta (headDelta (headDelta x)) (bind (fmap mu d) tailDelta) - ≡⟨ cong (\d -> delta (headDelta (headDelta x)) d) (monad-law-1-3 (S O) d) ⟩ - delta (headDelta (headDelta x)) (bind (bind d tailDelta) tailDelta) - ≡⟨ refl ⟩ - mu (delta (headDelta x) (bind d tailDelta)) - ≡⟨ refl ⟩ - mu (mu (delta x d)) - ≡⟨ refl ⟩ + (mu ∙ fmap mu) (delta x d) ≡⟨ refl ⟩ + mu (fmap mu (delta x d)) ≡⟨ refl ⟩ + mu (delta (mu x) (fmap mu d)) ≡⟨ refl ⟩ + delta (headDelta (mu x)) (bind (fmap mu d) tailDelta) ≡⟨ cong (\x -> delta x (bind (fmap mu d) tailDelta)) (monad-law-1-2 x) ⟩ + delta (headDelta (headDelta x)) (bind (fmap mu d) tailDelta) ≡⟨ cong (\d -> delta (headDelta (headDelta x)) d) (monad-law-1-3 (S O) d) ⟩ + delta (headDelta (headDelta x)) (bind (bind d tailDelta) tailDelta) ≡⟨ refl ⟩ + mu (delta (headDelta x) (bind d tailDelta)) ≡⟨ refl ⟩ + mu (mu (delta x d)) ≡⟨ refl ⟩ (mu ∙ mu) (delta x d) ∎ --} - monad-law-2-1 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta A) -> (bind (fmap eta d) (n-tail n)) ≡ d monad-law-2-1 O (mono x) = refl monad-law-2-1 O (delta x d) = begin