1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
(* Proof StoreT forms a comonad -- Russell O'Connor *)
Set Implict Arguments.
Unset Strict Implicit.
Require Import FunctionalExtensionality.
Record Comonad (w : Type -> Type) : Type :=
{ extract : forall a, w a -> a
; extend : forall a b, (w a -> b) -> w a -> w b
; law1 : forall a x, extend _ _ (extract a) x = x
; law2 : forall a b f x, extract b (extend a _ f x) = f x
; law3 : forall a b c f g x, extend b c f (extend a b g x) = extend a c (fun y => f (extend a b g y)) x
}.
Section StoreT.
Variables (s : Type) (w:Type -> Type).
Hypothesis wH : Comonad w.
Definition map a b f x := extend _ wH a b (fun y => f (extract _ wH _ y)) x.
Lemma map_extend : forall a b c f g x, map b c f (extend _ wH a b g x) = extend _ wH _ _ (fun y => f (g y)) x.
Proof.
intros a b c f g x.
unfold map.
rewrite law3.
apply equal_f.
apply f_equal.
extensionality y.
rewrite law2.
reflexivity.
Qed.
Record StoreT (a:Type): Type := mkStoreT
{store : w (s -> a)
;loc : s}.
Definition extractST a (x:StoreT a) : a :=
extract _ wH _ (store _ x) (loc _ x).
Definition mapST a b (f:a -> b) (x:StoreT a) : StoreT b :=
mkStoreT _ (map _ _ (fun g x => f (g x)) (store _ x)) (loc _ x).
Definition duplicateST a (x:StoreT a) : StoreT (StoreT a) :=
mkStoreT _ (extend _ wH _ _ (mkStoreT _) (store _ x)) (loc _ x).
Let extendST := fun a b f x => mapST _ b f (duplicateST a x).
Lemma law1ST : forall a x, extendST _ _ (extractST a) x = x.
Proof.
intros a [v b].
unfold extractST, extendST, duplicateST, mapST.
simpl.
rewrite map_extend.
simpl.
replace (fun (y : w (s -> a)) (x : s) => extract w wH (s -> a) y x)
with (extract w wH (s -> a)).
rewrite law1.
reflexivity.
extensionality y.
extensionality x.
reflexivity.
Qed.
Lemma law2ST : forall a b f x, extractST b (extendST a _ f x) = f x.
Proof.
intros a b f [v c].
unfold extendST, mapST, extractST.
simpl.
rewrite map_extend.
rewrite law2.
reflexivity.
Qed.
Lemma law3ST : forall a b c f g x, extendST b c f (extendST a b g x) = extendST a c (fun y => f (extendST a b g y)) x.
Proof.
intros a b c f g [v d].
unfold extendST, mapST, extractST.
simpl.
repeat rewrite map_extend.
rewrite law3.
repeat (apply equal_f||apply f_equal).
extensionality y.
extensionality x.
rewrite map_extend.
reflexivity.
Qed.
Definition StoreTComonad : Comonad StoreT :=
Build_Comonad _ _ _ law1ST law2ST law3ST.
End StoreT.
Check StoreTComonad.
|
