Members/atton/delta_monad: agda/delta.agda annotate

annotate agda/delta.agda @ 77:4b16b485a4b2

Split nat definition

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Mon, 01 Dec 2014 11:58:35 +0900
parents	c7076f9bbaed
children	f02391a7402f

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 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	3 open import nat
29 e0ba1bf564dd Apply level to some functions Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 28 diff changeset	4
e0ba1bf564dd Apply level to some functions Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 28 diff changeset	5 open import Level
27 742e62fc63e4 Define Monad-law 1-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 26 diff changeset	6 open import Relation.Binary.PropositionalEquality
742e62fc63e4 Define Monad-law 1-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 26 diff changeset	7 open ≡-Reasoning
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	8
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	9 module delta where
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	10
54 9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	11
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	12 data Delta {l : Level} (A : Set l) : (Set (suc 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	13 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	14 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	15
9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	16 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	17 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	18 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	19
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	20 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	21 headDelta (mono x) = x
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	22 headDelta (delta x _) = x
54 9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	23
9bb7c9bee94f Trying redefine delta for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 43 diff changeset	24 tailDelta : {l : Level} {A : Set l} -> 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	25 tailDelta (mono x) = mono x
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	26 tailDelta (delta _ d) = d
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	27
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	28 n-tail : {l : Level} {A : Set l} -> Nat -> ((Delta A) -> (Delta A))
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	29 n-tail O = id
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	30 n-tail (S n) = tailDelta ∙ (n-tail n)
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	31
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	32
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	33 -- Functor
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	34 fmap : {l ll : Level} {A : Set l} {B : Set ll} -> (A -> B) -> (Delta A) -> (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	35 fmap f (mono x) = mono (f x)
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	36 fmap f (delta x d) = delta (f x) (fmap f d)
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	37
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	38
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	39
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	40 -- Monad (Category)
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	41 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	42 eta x = mono x
27 742e62fc63e4 Define Monad-law 1-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 26 diff changeset	43
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	44 bind : {l ll : Level} {A : Set l} {B : Set ll} -> (Delta A) -> (A -> Delta B) -> Delta B
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	45 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	46 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	47
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	48 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	49 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	50
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	51 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	52 returnS x = mono x
26 5ba82f107a95 Define Similar in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: diff changeset	53
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	54 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	55 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	56
33 0bc402f970b3 Proof Monad-law 1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 32 diff changeset	57
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	58 -- Monad (Haskell)
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	59 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	60 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	61
41 23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	62 _>>=_ : {l ll : Level} {A : Set l} {B : Set ll} ->
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	63 (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	64 (mono x) >>= f = f x
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	65 (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	66
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
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	68
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	69 -- proofs
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	70
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	71 -- sub-proofs
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	72
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	73 n-tail-plus : {l : Level} {A : Set l} -> (n : Nat) -> ((n-tail {l} {A} n) ∙ tailDelta) ≡ n-tail (S n)
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	74 n-tail-plus O = refl
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	75 n-tail-plus (S n) = begin
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	76 n-tail (S n) ∙ tailDelta ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	77 (tailDelta ∙ (n-tail n)) ∙ tailDelta ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	78 tailDelta ∙ ((n-tail n) ∙ tailDelta) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-plus n) ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	79 n-tail (S (S n))
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	80 ∎
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	81
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	82 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)
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	83 n-tail-add O m = refl
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	84 n-tail-add (S n) O = begin
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	85 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	86 n-tail (S n) ≡⟨ cong (\n -> n-tail n) (nat-add-right-zero (S n))⟩
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	87 n-tail (S n + O)
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	88 ∎
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	89 n-tail-add {l} {A} {d} (S n) (S m) = begin
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	90 n-tail (S n) ∙ n-tail (S m) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	91 (tailDelta ∙ (n-tail n)) ∙ n-tail (S m) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	92 tailDelta ∙ ((n-tail n) ∙ n-tail (S m)) ≡⟨ cong (\t -> tailDelta ∙ t) (n-tail-add {l} {A} {d} n (S m)) ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	93 tailDelta ∙ (n-tail (n + (S m))) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	94 n-tail (S (n + S m)) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	95 n-tail (S n + S m) ∎
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	96
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	97 tail-delta-to-mono : {l : Level} {A : Set l} -> (n : Nat) -> (x : A) ->
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	98 (n-tail n) (mono x) ≡ (mono x)
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	99 tail-delta-to-mono O x = refl
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	100 tail-delta-to-mono (S n) x = begin
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	101 n-tail (S n) (mono x) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	102 tailDelta (n-tail n (mono x)) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	103 tailDelta (n-tail n (mono x)) ≡⟨ cong (\t -> tailDelta t) (tail-delta-to-mono n x) ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	104 tailDelta (mono x) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	105 mono x ∎
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	106
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	107 -- Functor-laws
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	108
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	109 -- Functor-law-1 : T(id) = id'
55 9c8c09334e32 Redefine Delta for infinite changes in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 54 diff changeset	110 functor-law-1 : {l : Level} {A : Set l} -> (d : Delta A) -> (fmap id) d ≡ id d
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	111 functor-law-1 (mono x) = refl
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	112 functor-law-1 (delta x d) = cong (delta x) (functor-law-1 d)
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	113
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	114 -- Functor-law-2 : T(f . g) = T(f) . T(g)
6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	115 functor-law-2 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
55 9c8c09334e32 Redefine Delta for infinite changes in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 54 diff changeset	116 (f : B -> C) -> (g : A -> B) -> (d : Delta A) ->
9c8c09334e32 Redefine Delta for infinite changes in Agda Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 54 diff changeset	117 (fmap (f ∙ g)) d ≡ ((fmap f) ∙ (fmap g)) d
57 dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	118 functor-law-2 f g (mono x) = refl
dfcd72dc697e ReDefine Delta used non-empty-list for infinite changes Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 56 diff changeset	119 functor-law-2 f g (delta x d) = cong (delta (f (g x))) (functor-law-2 f g d)
38 6ce83b2c9e59 Proof Functor-laws Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 36 diff changeset	120
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	121
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	122 -- Monad-laws (Category)
63 474ed34e4f02 proving monad-law-1 ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 62 diff changeset	123
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	124
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	125 monad-law-1-5 : {l : Level} {A : Set l} -> (m : Nat) (n : Nat) -> (ds : Delta (Delta A)) ->
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	126 n-tail n (bind ds (n-tail m)) ≡ bind (n-tail n ds) (n-tail (m + n))
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	127 monad-law-1-5 O O ds = refl
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	128 monad-law-1-5 O (S n) (mono ds) = begin
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	129 n-tail (S n) (bind (mono ds) (n-tail O)) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	130 n-tail (S n) ds ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	131 bind (mono ds) (n-tail (S n)) ≡⟨ cong (\de -> bind de (n-tail (S n))) (sym (tail-delta-to-mono (S n) ds)) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	132 bind (n-tail (S n) (mono ds)) (n-tail (S n)) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	133 bind (n-tail (S n) (mono ds)) (n-tail (O + S n))
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	134 ∎
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	135 monad-law-1-5 O (S n) (delta d ds) = begin
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	136 n-tail (S n) (bind (delta d ds) (n-tail O)) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	137 n-tail (S n) (delta (headDelta d) (bind ds tailDelta )) ≡⟨ cong (\t -> t (delta (headDelta d) (bind ds tailDelta ))) (sym (n-tail-plus n)) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	138 ((n-tail n) ∙ tailDelta) (delta (headDelta d) (bind ds tailDelta )) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	139 (n-tail n) (bind ds tailDelta) ≡⟨ monad-law-1-5 (S O) n ds ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	140 bind (n-tail n ds) (n-tail (S n)) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	141 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) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	142 bind (n-tail (S n) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	143 bind (n-tail (S n) (delta d ds)) (n-tail (O + S n))
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	144 ∎
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	145 monad-law-1-5 (S m) n (mono (mono x)) = begin
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	146 n-tail n (bind (mono (mono x)) (n-tail (S m))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	147 n-tail n (n-tail (S m) (mono x)) ≡⟨ cong (\de -> n-tail n de) (tail-delta-to-mono (S m) x)⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	148 n-tail n (mono x) ≡⟨ tail-delta-to-mono n x ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	149 mono x ≡⟨ sym (tail-delta-to-mono (S m + n) x) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	150 (n-tail (S m + n)) (mono x) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	151 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))) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	152 bind (n-tail n (mono (mono x))) (n-tail (S m + n))
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	153 ∎
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	154 monad-law-1-5 (S m) n (mono (delta x ds)) = begin
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	155 n-tail n (bind (mono (delta x ds)) (n-tail (S m))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	156 n-tail n (n-tail (S m) (delta x ds)) ≡⟨ cong (\t -> n-tail n (t (delta x ds))) (sym (n-tail-plus m)) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	157 n-tail n (((n-tail m) ∙ tailDelta) (delta x ds)) ≡⟨ refl ⟩
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	158 n-tail n ((n-tail m) ds) ≡⟨ cong (\t -> t ds) (n-tail-add {d = ds} n m) ⟩
77 4b16b485a4b2 Split nat definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 76 diff changeset	159 n-tail (n + m) ds ≡⟨ cong (\n -> n-tail n ds) (nat-add-sym n m) ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	160 n-tail (m + n) ds ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	161 ((n-tail (m + n)) ∙ tailDelta) (delta x ds) ≡⟨ cong (\t -> t (delta x ds)) (n-tail-plus (m + n))⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	162 n-tail (S (m + n)) (delta x ds) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	163 n-tail (S m + n) (delta x ds) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	164 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))) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	165 bind (n-tail n (mono (delta x ds))) (n-tail (S m + n))
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	166 ∎
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	167 monad-law-1-5 (S m) O (delta d ds) = begin
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	168 n-tail O (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	169 (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	170 delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m)))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	171 bind (delta d ds) (n-tail (S m)) ≡⟨ refl ⟩
77 4b16b485a4b2 Split nat definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 76 diff changeset	172 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)) ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	173 bind (n-tail O (delta d ds)) (n-tail (S m + O))
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	174 ∎
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	175 monad-law-1-5 (S m) (S n) (delta d ds) = begin
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	176 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)) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	177 ((n-tail n) ∙ tailDelta) (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	178 ((n-tail n) ∙ tailDelta) (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	179 (n-tail n) (bind ds (tailDelta ∙ (n-tail (S m)))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	180 (n-tail n) (bind ds (n-tail (S (S m)))) ≡⟨ monad-law-1-5 (S (S m)) n ds ⟩
77 4b16b485a4b2 Split nat definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 76 diff changeset	181 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)) ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	182 bind ((n-tail n) ds) (n-tail (S m + S n)) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	183 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) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	184 bind (n-tail (S n) (delta d ds)) (n-tail (S m + S n))
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	185 ∎
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	186
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	187 monad-law-1-4 : {l : Level} {A : Set l} -> (m n : Nat) -> (dd : Delta (Delta A)) ->
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	188 headDelta ((n-tail n) (bind dd (n-tail m))) ≡ headDelta ((n-tail (m + n)) (headDelta (n-tail n dd)))
74 1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	189 monad-law-1-4 O O (mono dd) = refl
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	190 monad-law-1-4 O O (delta dd dd₁) = refl
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	191 monad-law-1-4 O (S n) (mono dd) = begin
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	192 headDelta (n-tail (S n) (bind (mono dd) (n-tail O))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	193 headDelta (n-tail (S n) dd) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	194 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)) ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	195 headDelta (n-tail (S n) (headDelta (n-tail (S n) (mono dd)))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	196 headDelta (n-tail (O + S n) (headDelta (n-tail (S n) (mono dd))))
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	197 ∎
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	198 monad-law-1-4 O (S n) (delta d ds) = begin
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	199 headDelta (n-tail (S n) (bind (delta d ds) (n-tail O))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	200 headDelta (n-tail (S n) (bind (delta d ds) id)) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	201 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)) ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	202 headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta d) (bind ds tailDelta))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	203 headDelta (n-tail n (bind ds tailDelta)) ≡⟨ monad-law-1-4 (S O) n ds ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	204 headDelta (n-tail (S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	205 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) ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	206 headDelta (n-tail (S n) (headDelta (n-tail (S n) (delta d ds)))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	207 headDelta (n-tail (O + S n) (headDelta (n-tail (S n) (delta d ds))))
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	208 ∎
74 1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	209 monad-law-1-4 (S m) n (mono dd) = begin
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	210 headDelta (n-tail n (bind (mono dd) (n-tail (S m)))) ≡⟨ refl ⟩
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	211 headDelta (n-tail n ((n-tail (S m)) dd))≡⟨ cong (\t -> headDelta (t dd)) (n-tail-add {d = dd} n (S m)) ⟩
77 4b16b485a4b2 Split nat definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 76 diff changeset	212 headDelta (n-tail (n + S m) dd) ≡⟨ cong (\n -> headDelta ((n-tail n) dd)) (nat-add-sym n (S m)) ⟩
74 1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	213 headDelta (n-tail (S m + n) dd) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	214 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)) ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	215 headDelta (n-tail (S m + n) (headDelta (n-tail n (mono dd))))
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	216 ∎
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	217 monad-law-1-4 (S m) O (delta d ds) = begin
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	218 headDelta (n-tail O (bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	219 headDelta (bind (delta d ds) (n-tail (S m))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	220 headDelta (delta (headDelta ((n-tail (S m) d))) (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩
77 4b16b485a4b2 Split nat definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 76 diff changeset	221 headDelta (n-tail (S m) d) ≡⟨ cong (\n -> headDelta ((n-tail n) d)) (nat-add-right-zero (S m)) ⟩
74 1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	222 headDelta (n-tail (S m + O) d) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	223 headDelta (n-tail (S m + O) (headDelta (delta d ds))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	224 headDelta (n-tail (S m + O) (headDelta (n-tail O (delta d ds))))
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	225 ∎
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	226 monad-law-1-4 (S m) (S n) (delta d ds) = begin
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	227 headDelta (n-tail (S n) (bind (delta d ds) (n-tail (S m)))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	228 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)) ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	229 headDelta ((((n-tail n) ∙ tailDelta) (delta (headDelta ((n-tail (S m)) d)) (bind ds (tailDelta ∙ (n-tail (S m))))))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	230 headDelta (n-tail n (bind ds (tailDelta ∙ (n-tail (S m))))) ≡⟨ refl ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	231 headDelta (n-tail n (bind ds (n-tail (S (S m))))) ≡⟨ monad-law-1-4 (S (S m)) n ds ⟩
77 4b16b485a4b2 Split nat definition Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 76 diff changeset	232 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)) ⟩
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	233 headDelta (n-tail (S m + S n) (headDelta (n-tail n ds))) ≡⟨ refl ⟩
74 1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	234 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) ⟩
1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	235 headDelta (n-tail (S m + S n) (headDelta (n-tail (S n) (delta d ds))))
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	236 ∎
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	237
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	238 monad-law-1-2 : {l : Level} {A : Set l} -> (d : Delta (Delta A)) -> headDelta (mu d) ≡ (headDelta (headDelta d))
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	239 monad-law-1-2 (mono _) = refl
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	240 monad-law-1-2 (delta _ _) = refl
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	241
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	242 monad-law-1-3 : {l : Level} {A : Set l} -> (n : Nat) -> (d : Delta (Delta (Delta A))) ->
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	243 bind (fmap mu d) (n-tail n) ≡ bind (bind d (n-tail n)) (n-tail n)
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	244 monad-law-1-3 O (mono d) = refl
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	245 monad-law-1-3 O (delta d ds) = begin
76 c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	246 bind (fmap mu (delta d ds)) (n-tail O) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	247 bind (delta (mu d) (fmap mu ds)) (n-tail O) ≡⟨ refl ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	248 delta (headDelta (mu d)) (bind (fmap mu ds) tailDelta) ≡⟨ cong (\dx -> delta dx (bind (fmap mu ds) tailDelta)) (monad-law-1-2 d) ⟩
c7076f9bbaed Refactors Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 75 diff changeset	249 delta (headDelta (headDelta d)) (bind (fmap mu ds) tailDelta) ≡⟨ cong (\dx -> delta (headDelta (headDelta d)) dx) (monad-law-1-3 (S O) ds) ⟩
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	250 delta (headDelta (headDelta d)) (bind (bind ds tailDelta) tailDelta) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	251 bind (delta (headDelta d) (bind ds tailDelta)) (n-tail O) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	252 bind (bind (delta d ds) (n-tail O)) (n-tail O)
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	253 ∎
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	254 monad-law-1-3 (S n) (mono (mono d)) = begin
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	255 bind (fmap mu (mono (mono d))) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	256 bind (mono d) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	257 (n-tail (S n)) d ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	258 bind (mono d) (n-tail (S n)) ≡⟨ cong (\t -> bind t (n-tail (S n))) (sym (tail-delta-to-mono (S n) d))⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	259 bind (n-tail (S n) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	260 bind (n-tail (S n) (mono d)) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	261 bind (bind (mono (mono d)) (n-tail (S n))) (n-tail (S n))
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	262 ∎
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	263 monad-law-1-3 (S n) (mono (delta d ds)) = begin
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	264 bind (fmap mu (mono (delta d ds))) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	265 bind (mono (mu (delta d ds))) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	266 n-tail (S n) (mu (delta d ds)) ≡⟨ refl ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	267 n-tail (S n) (delta (headDelta d) (bind ds tailDelta)) ≡⟨ cong (\t -> t (delta (headDelta d) (bind ds tailDelta))) (sym (n-tail-plus n)) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	268 (n-tail n ∙ tailDelta) (delta (headDelta d) (bind ds tailDelta)) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	269 n-tail n (bind ds tailDelta) ≡⟨ monad-law-1-5 (S O) n ds ⟩
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	270 bind (n-tail n ds) (n-tail (S n)) ≡⟨ refl ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	271 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) ⟩
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	272 bind (n-tail (S n) (delta d ds)) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	273 bind (bind (mono (delta d ds)) (n-tail (S n))) (n-tail (S n))
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	274 ∎
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	275 monad-law-1-3 (S n) (delta (mono d) ds) = begin
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	276 bind (fmap mu (delta (mono d) ds)) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	277 bind (delta (mu (mono d)) (fmap mu ds)) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	278 bind (delta d (fmap mu ds)) (n-tail (S n)) ≡⟨ refl ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	279 delta (headDelta ((n-tail (S n)) d)) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	280 delta (headDelta ((n-tail (S n)) d)) (bind (fmap mu ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta ((n-tail (S n)) d)) de) (monad-law-1-3 (S (S n)) ds) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	281 delta (headDelta ((n-tail (S n)) d)) (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	282 delta (headDelta ((n-tail (S n)) d)) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (n-tail (S (S n)))) ≡⟨ refl ⟩
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	283 delta (headDelta ((n-tail (S n)) d)) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	284 delta (headDelta ((n-tail (S n)) (headDelta (mono d)))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\de -> delta (headDelta ((n-tail (S n)) (headDelta de))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n))))) (sym (tail-delta-to-mono (S n) d)) ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	285 delta (headDelta ((n-tail (S n)) (headDelta ((n-tail (S n)) (mono d))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	286 bind (delta (headDelta ((n-tail (S n)) (mono d))) (bind ds (tailDelta ∙ (n-tail (S n))))) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	287 bind (bind (delta (mono d) ds) (n-tail (S n))) (n-tail (S n))
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	288 ∎
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	289 monad-law-1-3 (S n) (delta (delta d dd) ds) = begin
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	290 bind (fmap mu (delta (delta d dd) ds)) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	291 bind (delta (mu (delta d dd)) (fmap mu ds)) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	292 delta (headDelta ((n-tail (S n)) (mu (delta d dd)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	293 delta (headDelta ((n-tail (S n)) (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\t -> delta (headDelta (t (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))))(sym (n-tail-plus n)) ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	294 delta (headDelta (((n-tail n) ∙ tailDelta) (delta (headDelta d) (bind dd tailDelta)))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	295 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (fmap mu ds) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	296 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (fmap mu ds) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta (headDelta ((n-tail n) (bind dd tailDelta))) de) (monad-law-1-3 (S (S n)) ds) ⟩
74 1f4ea5cb153d Prove monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 73 diff changeset	297 delta (headDelta ((n-tail n) (bind dd tailDelta))) (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ cong (\de -> delta de ( (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))))) (monad-law-1-4 (S O) n dd) ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	298 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (n-tail (S (S n)))) (n-tail (S (S n)))) ≡⟨ refl ⟩
0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	299 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (n-tail (S (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	300 delta (headDelta ((n-tail (S n)) (headDelta (n-tail n dd)))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
73 0ad0ae7a3cbe Proving monad-law-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 72 diff changeset	301 delta (headDelta ((n-tail (S n)) (headDelta (((n-tail n) ∙ tailDelta) (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ cong (\t -> delta (headDelta ((n-tail (S n)) (headDelta (t (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n))))) (n-tail-plus n) ⟩
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	302 delta (headDelta ((n-tail (S n)) (headDelta ((n-tail (S n)) (delta d dd))))) (bind (bind ds (tailDelta ∙ (n-tail (S n)))) (tailDelta ∙ (n-tail (S n)))) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	303 bind (delta (headDelta ((n-tail (S n)) (delta d dd))) (bind ds (tailDelta ∙ (n-tail (S n))))) (n-tail (S n)) ≡⟨ refl ⟩
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	304 bind (bind (delta (delta d dd) ds) (n-tail (S n))) (n-tail (S n))
e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	305 ∎
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	306
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	307
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	308 -- monad-law-1 : join . fmap join = join . join
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	309 monad-law-1 : {l : Level} {A : Set l} -> (d : Delta (Delta (Delta A))) -> ((mu ∙ (fmap mu)) d) ≡ ((mu ∙ mu) d)
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	310 monad-law-1 (mono d) = refl
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	311 monad-law-1 (delta x d) = begin
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	312 (mu ∙ fmap mu) (delta x d)
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	313 ≡⟨ refl ⟩
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	314 mu (fmap mu (delta x d))
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	315 ≡⟨ refl ⟩
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	316 mu (delta (mu x) (fmap mu d))
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	317 ≡⟨ refl ⟩
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	318 delta (headDelta (mu x)) (bind (fmap mu d) tailDelta)
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	319 ≡⟨ cong (\x -> delta x (bind (fmap mu d) tailDelta)) (monad-law-1-2 x) ⟩
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	320 delta (headDelta (headDelta x)) (bind (fmap mu d) tailDelta)
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	321 ≡⟨ cong (\d -> delta (headDelta (headDelta x)) d) (monad-law-1-3 (S O) d) ⟩
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	322 delta (headDelta (headDelta x)) (bind (bind d tailDelta) tailDelta)
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	323 ≡⟨ refl ⟩
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	324 mu (delta (headDelta x) (bind d tailDelta))
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	325 ≡⟨ refl ⟩
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	326 mu (mu (delta x d))
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	327 ≡⟨ refl ⟩
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	328 (mu ∙ mu) (delta x d)
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	329 ∎
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	330
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	331
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	332
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	333 {-
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	334 -- monad-law-2 : join . fmap return = join . return = id
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	335 -- monad-law-2-1 join . fmap return = join . return
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	336 monad-law-2-1 : {l : Level} {A : Set l} -> (d : Delta A) ->
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	337 (mu ∙ fmap eta) d ≡ (mu ∙ eta) d
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	338 monad-law-2-1 (mono x) = refl
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	339 monad-law-2-1 (delta x d) = {!!}
63 474ed34e4f02 proving monad-law-1 ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 62 diff changeset	340
474ed34e4f02 proving monad-law-1 ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 62 diff changeset	341
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	342 -- monad-law-2-2 : join . return = id
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	343 monad-law-2-2 : {l : Level} {A : Set l } -> (d : Delta A) -> (mu ∙ eta) d ≡ id d
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	344 monad-law-2-2 d = refl
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	345
35 c5cdbedc68ad Proof Monad-law-2-2 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 34 diff changeset	346
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	347 -- monad-law-3 : return . f = fmap f . return
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	348 monad-law-3 : {l : Level} {A B : Set l} (f : A -> B) (x : A) -> (eta ∙ f) x ≡ (fmap f ∙ eta) x
36 169ec60fcd36 Proof Monad-law-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 35 diff changeset	349 monad-law-3 f x = refl
27 742e62fc63e4 Define Monad-law 1-4 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 26 diff changeset	350
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	351
39 b9b26b470cc2 Add Comments Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 38 diff changeset	352 -- monad-law-4 : join . fmap (fmap f) = fmap f . join
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	353 monad-law-4 : {l ll : Level} {A : Set l} {B : Set ll} (f : A -> B) (d : Delta (Delta A)) ->
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	354 (mu ∙ fmap (fmap f)) d ≡ (fmap f ∙ mu) d
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	355 monad-law-4 f d = {!!}
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	356
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	357
18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	358
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	359
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	360 -- Monad-laws (Haskell)
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	361 -- monad-law-h-1 : return a >>= k = k a
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	362 monad-law-h-1 : {l ll : Level} {A : Set l} {B : Set ll} ->
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	363 (a : A) -> (k : A -> (Delta B)) ->
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	364 (return a >>= k) ≡ (k a)
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	365 monad-law-h-1 a k = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	366
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	367
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	368
a7cd7740f33e Add Haskell style Monad-laws and Proof Monad-laws-h-1 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 39 diff changeset	369 -- monad-law-h-2 : m >>= return = m
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	370 monad-law-h-2 : {l : Level}{A : Set l} -> (m : Delta A) -> (m >>= return) ≡ m
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	371 monad-law-h-2 (mono x) = refl
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	372 monad-law-h-2 (delta x d) = cong (delta x) (monad-law-h-2 d)
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	373
46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	374
41 23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	375 -- monad-law-h-3 : m >>= (\x -> k x >>= h) = (m >>= k) >>= h
23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	376 monad-law-h-3 : {l ll lll : Level} {A : Set l} {B : Set ll} {C : Set lll} ->
43 90b171e3a73e Rename to Delta from Similar Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 42 diff changeset	377 (m : Delta A) -> (k : A -> (Delta B)) -> (h : B -> (Delta C)) ->
41 23474bf242c6 Proof monad-law-h-2, trying monad-law-h-3 Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 40 diff changeset	378 (m >>= (\x -> k x >>= h)) ≡ ((m >>= k) >>= h)
59 46b15f368905 Define bind and mu for Infinite Delta Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 57 diff changeset	379 monad-law-h-3 (mono x) k h = refl
70 18a20a14c4b2 Change prove method. use Int ... Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 69 diff changeset	380 monad-law-h-3 (delta x d) k h = {!!}
69 295e8ed39c0c Change headDelta definition. return non-delta value Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 68 diff changeset	381
72 e95f15af3f8b Trying prove infinite-delta. but I think this definition was missed. Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> parents: 71 diff changeset	382 -}

Mercurial > hg > Members > atton > delta_monad

annotate agda/delta.agda @ 77:4b16b485a4b2