-
Notifications
You must be signed in to change notification settings - Fork 11
/
typed_store_lib.v
148 lines (117 loc) · 5.1 KB
/
typed_store_lib.v
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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later *)
Ltac typeof X := type of X.
Require Import ssrmatching Reals JMeq.
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
From infotheo Require Import Reals_ext.
Require Import preamble hierarchy.
(******************************************************************************)
(* Lemmas using the typed store monad *)
(* *)
(* cchk T (r : loc T) := cget r >> skip. *)
(* *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope monae_scope.
Section cchk.
Variables (MLU : ML_universe) (N : monad) (locT : eqType)
(M : typedStoreMonad MLU N locT).
Notation loc := (@loc MLU locT).
Definition cchk {T} (r : loc T) : M unit := cget r >> skip.
Lemma cnewchk T s (A : UU0) (k : loc T -> M A) :
cnew T s >>= (fun r => cchk r >> k r) = cnew T s >>= k.
Proof.
under eq_bind do rewrite bindA.
rewrite cnewget.
by under eq_bind do rewrite bindskipf.
Qed.
Lemma cchknewC T1 T2 (r : loc T1) s (A : UU0) (k : loc T2 -> M A) :
cchk r >> (cnew T2 s >>= fun r' => cchk r >> k r') =
cchk r >> (cnew T2 s >>= k).
Proof.
rewrite !(bindA,bindskipf).
under eq_bind do under eq_bind do rewrite bindA.
rewrite cgetnewD.
by under eq_bind do under eq_bind do rewrite bindskipf.
Qed.
Lemma cchkgetC T1 T2 (r1: loc T1) (r2: loc T2) (A: UU0)
(k: coq_type N T2 -> M A) :
cchk r1 >> (cget r2 >>= k) = cget r2 >>= (fun s => cchk r1 >> k s).
Proof.
under [in RHS]eq_bind do rewrite bindA bindskipf.
by rewrite !(bindA,bindskipf) cgetC.
Qed.
Lemma cchknewE T1 T2 (r1 : loc T1) s (A : UU0) (k1 k2 : loc T2 -> M A) :
(forall r2 : loc T2, loc_id r1 != loc_id r2 -> k1 r2 = k2 r2) ->
cchk r1 >> (cnew T2 s >>= k1) = cchk r1 >> (cnew T2 s >>= k2).
Proof. move=> Hk; rewrite !(bindA,bindskipf); exact: cgetnewE. Qed.
Lemma cchknewget T T' (r : loc T) s (A : UU0) k :
cchk r >> (cnew T' s >>= fun r' => cget r >>= k r') =
cget r >>= (fun u => cnew T' s >>= k ^~ u) :> M A.
Proof. by rewrite bindA bindskipf cgetnewD. Qed.
Lemma cchknewput T T' (r : loc T) s s' (A : UU0) k :
cchk r >> (cnew T' s' >>= fun r' => cput r s >> k r') =
cput r s >> (cnew T' s' >>= k) :> M A.
Proof. by rewrite bindA bindskipf cputnewC. Qed.
Lemma cchkget T (r : loc T) (A : UU0) (k : coq_type N T -> M A) :
cchk r >> (cget r >>= k) = cget r >>= k.
Proof. by rewrite bindA bindskipf cgetget. Qed.
Lemma cgetchk T (r : loc T) (A: UU0) (k : coq_type N T -> M A) :
cget r >>= (fun s => cchk r >> k s) = cget r >>= k.
Proof. under eq_bind do rewrite bindA bindskipf; by rewrite cgetget. Qed.
Lemma cchkputC T1 T2 (r1 : loc T1) (r2 : loc T2) (s : coq_type N T2) :
cchk r1 >> cput r2 s = cput r2 s >> cchk r1.
Proof. by rewrite bindA bindskipf cgetputC bindA. Qed.
Lemma cchkput T (r : loc T) (s : coq_type N T) :
cchk r >> cput r s = cput r s.
Proof. by rewrite bindA bindskipf cgetput. Qed.
Lemma cputchk T (r : loc T) (s : coq_type N T) :
cput r s >> cchk r = cput r s.
Proof. by rewrite cputget bindmskip. Qed.
Lemma cchkC T1 T2 (r1 : loc T1) (r2 : loc T2) :
cchk r1 >> cchk r2 = cchk r2 >> cchk r1.
Proof. by rewrite !(bindA,bindskipf) cgetC. Qed.
Lemma cchkdup T (r : loc T) : cchk r >> cchk r = cchk r.
Proof. by rewrite bindA bindskipf cgetget. Qed.
Lemma cgetret T (r : loc T) : cget r >>= Ret = cget r :> M _.
Proof. by rewrite bindmret. Qed.
Lemma cnewgetret T s : cnew T s >>= @cget _ _ _ _ _ = cnew T s >> Ret s :> M _.
Proof. under eq_bind do rewrite -cgetret; by rewrite cnewget. Qed.
End cchk.
Section crun.
Variables (MLU : ML_universe) (N : monad) (locT : eqType)
(M : typedStoreRunMonad MLU N locT).
Notation loc := (@loc MLU locT).
Local Notation cchk := (cchk M).
Lemma crunnew0 T s : crun (cnew T s : M _).
Proof. by rewrite -(bindskipf (cnew T s)) crunnew // crunskip. Qed.
Lemma crunchkget A T (m : M A) (r : A -> loc T) :
crun (m >>= fun x => cchk (r x)) = crun (m >>= fun x => cget (r x)) :> bool.
Proof. by rewrite /cchk -bindA crunmskip. Qed.
Lemma crunchkput A T (m : M A) (r : A -> loc T) s :
crun (m >>= fun x => cchk (r x)) ->
crun (m >>= fun x => cput (r x) (s x)).
Proof. rewrite crunchkget; exact: crungetput. Qed.
Lemma crunnewchkC A T1 T2 (m : M A) (r : A -> loc T1) s :
crun (m >>= fun x => cchk (r x)) ->
crun (m >>= fun x => cnew T2 (s x) >> cchk (r x)).
Proof.
rewrite crunchkget => Hck.
under eq_bind do rewrite -bindA.
rewrite -bindA crunmskip.
exact: crunnewgetC.
Qed.
Lemma crunnewchk A T (m : M A) s :
crun m -> crun (m >>= fun x => cnew T (s x) >>= cchk).
Proof.
under eq_bind do rewrite /cchk cnewget.
rewrite -bindA crunmskip.
exact: crunnew.
Qed.
Lemma crunnewchk0 T s : crun (cnew T s >>= fun r => cchk r : M _).
Proof. by rewrite -(bindskipf (_ >>= _)) crunnewchk // crunskip. Qed.
End crun.
Arguments cchk {MLU N locT M} [T].