### changeset 71:56da62d57c95

Change prove method. use Int ...
author Yasutaka Higa Thu, 27 Nov 2014 23:16:55 +0900 18a20a14c4b2 e95f15af3f8b agda/delta.agda 1 files changed, 83 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
```--- a/agda/delta.agda	Thu Nov 27 22:44:57 2014 +0900
+++ b/agda/delta.agda	Thu Nov 27 23:16:55 2014 +0900
@@ -100,6 +100,54 @@
mono x
∎

+monad-law-1-6 : {l : Level} {A : Set l} -> (n : Int) -> (ds : Delta (Delta A)) ->
+  ≡
+  headDelta (n-times-tail-delta n (bind ds (tailDelta ∙ tailDelta)))
+monad-law-1-6 one (mono ds) = refl
+monad-law-1-6 one (delta ds (mono ds₁)) = refl
+monad-law-1-6 one (delta ds (delta ds₁ ds₂)) = refl
+monad-law-1-6 (succ n) (mono (mono x)) = begin
+  headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta (n-times-tail-delta (succ n) (mono (mono x)))))
+  ≡⟨ cong (\d -> headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta d))) (tail-delta-to-mono (succ n) (mono x)) ⟩
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (bind (mono (mono x)) (tailDelta ∙ tailDelta)))
+ ∎
+monad-law-1-6 (succ n) (mono (delta x ds)) = begin
+  headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta (n-times-tail-delta (succ n) (mono (delta x ds)))))
+  ≡⟨ cong (\d -> headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta d))) (tail-delta-to-mono (succ n) (delta x ds)) ⟩
+  headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta (mono (delta x ds))))
+  ≡⟨ refl ⟩
+  headDelta(n-times-tail-delta (succ n) (bind (mono (delta x ds)) (tailDelta ∙ tailDelta)))
+ ∎
+monad-law-1-6 (succ n) (delta d (mono ds)) = begin
+  headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta (n-times-tail-delta (succ n) (delta d (mono ds)))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta (n-times-tail-delta n (mono ds))))
+  ≡⟨ cong (\d -> headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta d))) (tail-delta-to-mono n ds) ⟩
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (bind (delta d (mono ds)) (tailDelta ∙ tailDelta)))
+ ∎
+monad-law-1-6 (succ n) (delta d (delta dd ds)) = begin
+  headDelta (n-times-tail-delta (succ (succ (succ n))) (headDelta (n-times-tail-delta (succ n) (delta d (delta dd ds)))))
+  ≡⟨ {!!} ⟩
+  headDelta (n-times-tail-delta (succ n) (bind (delta d (delta dd ds)) (tailDelta ∙ tailDelta)))
+ ∎
+{-
+  ≡
+  headDelta (n-times-tail-delta n (bind ds (tailDelta ∙ tailDelta)))
+-}
+
+monad-law-1-5 : {l : Level} {A : Set l} -> (ds : Delta (Delta A)) ->
+  ≡
+  headDelta (bind ds (tailDelta ∙ tailDelta))
+monad-law-1-5 (delta ds ds₁) = refl
+
monad-law-1-4 : {l : Level} {A : Set l} -> (n : Int) (d : Delta (Delta A)) ->
@@ -134,7 +182,40 @@
≡⟨ refl ⟩
headDelta (n-times-tail-delta (succ n) (mu (delta d (mono ds))))
∎
-monad-law-1-4 (succ n) (delta d (delta dd ds)) = begin
+monad-law-1-4 (succ one) (delta d (delta dd ds)) = begin
+  headDelta (n-times-tail-delta (succ one) (headDelta (n-times-tail-delta (succ one) (delta d (delta dd ds)))))
+  ≡⟨ refl ⟩
+  ≡⟨ refl ⟩
+  headDelta (bind ds (tailDelta ∙ tailDelta))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta one (delta (headDelta (tailDelta dd)) (bind ds (tailDelta ∙ tailDelta ))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta one (bind (delta dd ds) (tailDelta)))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ one) (delta (headDelta d) (bind (delta dd ds) (tailDelta))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ one) (mu (delta d (delta dd ds))))
+  ∎
+monad-law-1-4 (succ (succ n)) (delta d (delta dd ds)) = begin
+  headDelta (n-times-tail-delta (succ (succ n)) (headDelta (n-times-tail-delta (succ (succ n)) (delta d (delta dd ds)))))
+  ≡⟨ refl ⟩
+  ≡⟨ monad-law-1-6 n ds ⟩
+  headDelta (n-times-tail-delta n (bind ds (tailDelta ∙ tailDelta)))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (delta (headDelta dd) (bind ds (tailDelta ∙ tailDelta))))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ n) (bind (delta dd ds) tailDelta))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ (succ n)) (delta (headDelta d) (bind (delta dd ds) tailDelta)))
+  ≡⟨ refl ⟩
+  headDelta (n-times-tail-delta (succ (succ n)) (mu (delta d (delta dd ds))))
+  ∎
+
+{-begin
headDelta (n-times-tail-delta (succ n) (headDelta (n-times-tail-delta (succ n) (delta d (delta dd ds)))))
≡⟨ refl ⟩