Mercurial > hg > Members > atton > agda-proofs

annotate state/state.agda @ 14:31b1b7cc43cd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prove state is functor
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 03 May 2016 16:31:56 +0900
parents 14c22339ce06
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
4
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Relation.Binary.PropositionalEquality
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 open import Level
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open ≡-Reasoning
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
14
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
5
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
6 module state where
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
7
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
8 record Product {l : Level} (A B : Set l) : Set (suc l) where
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
9 constructor <_,_>
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
10 field
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
11 first : A
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
12 second : B
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
13 open Product
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
14
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
15 id : {l : Level} {A : Set l} -> A -> A
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
16 id a = a
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
17
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
18
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
19 infixr 10 _∘_
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
20 _∘_ : {l : Level} {A B C : Set l} -> (B -> C) -> (A -> B) -> (A -> C)
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
21 g ∘ f = \a -> g (f a)
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
22
4
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 {-
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 Haskell Definition
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 newtype State s a = State { runState :: s -> (a, s) }
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 instance Monad (State s) where
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 return a = State $ \s -> (a, s)
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 m >>= k = State $ \s -> let
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 (a, s') = runState m s
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 in runState (k a) s'
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 -}
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
13
14c22339ce06 Define state in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
35 record State {l : Level} (S A : Set l) : Set (suc l) where
4
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 field
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 runState : S -> Product A S
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 open State
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39
13
14c22339ce06 Define state in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
40 state : {l : Level} {S A : Set l} -> (S -> Product A S) -> State S A
4
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 state f = record {runState = f}
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
14
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
43 return : {l : Level} {S A : Set l} -> A -> State S A
4
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 return a = state (\s -> < a , s > )
fe1cf97997b9 Start proof to State Monad
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
13
14c22339ce06 Define state in agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
46 _>>=_ : {l : Level} {S A B : Set l} -> State S A -> (A -> State S B) -> State S B
14
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
47 m >>= k = state (\s -> (runState (k (first (runState m s))) (second (runState m s))))
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
48
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
49 {- fmap definitions in Haskell
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
50 instance Functor (State s) where
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
51 fmap f m = State $ \s -> let
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
52 (a, s') = runState m s
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
53 in (f a, s')
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
54 -}
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
55
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
56 fmap : {l : Level} {S A B : Set l} -> (A -> B) -> (State S A) -> (State S B)
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
57 fmap f m = state (\s -> < (f (first ((runState m) s))), (second ((runState m) s)) >)
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
58
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
59 -- proofs
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
60
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
61 fmap-id : {l : Level} {A S : Set l} {s : State S A} -> fmap id s ≡ id s
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
62 fmap-id = refl
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
63
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
64 fmap-comp : {l : Level} {S A B C : Set l} {g : B -> C} {f : A -> B} {s : State S A} -> ((fmap g) ∘ (fmap f)) s ≡ fmap (g ∘ f) s
31b1b7cc43cd Prove state is functor
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
65 fmap-comp {_}{_}{_}{_}{_}{g}{f}{s} = refl