-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtriple.v
294 lines (238 loc) · 7.05 KB
/
triple.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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
Require Import Coq.Bool.Bool.
Require Import Coq.Arith.Arith.
Require Import Coq.Arith.EqNat.
Require Import language.
Require Import state.
Require Import util.
Require Import semantic.
Require Import assertion.
Require Import Coq.omega.Omega.
Require Import Coq.Lists.List.
Require Import Coq.Logic.FunctionalExtensionality.
Import ListNotations.
Definition triple
(P: assertion) (c:command) (Q:assertion) : Prop :=
forall st opst,
c / st \\ opst ->
P st ->
match opst with
| St st => Q st
| Abt => False
end.
Notation "{{ P }} c {{ Q }}" :=
(triple P c Q) (at level 90, c at next level).
Definition assn_sub (X: id) (a: aexp) P : assertion :=
fun st => P ((st_update (fst st) X (aeval (fst st) a)), (snd st)).
Notation "P [ X \ a ]" := (assn_sub X a P) (at level 10).
(* proof rules & soundness *)
(* assign *)
Theorem rule_asgn : forall Q X a,
{{Q [X \ a]}} (CAss X a) {{Q}}.
Proof.
intros.
unfold triple.
intros. unfold assn_sub in *.
inversion H. subst. assumption.
Qed.
(* consquence *)
Theorem rule_consequence_pre : forall (P P' Q : assertion) c,
{{P'}} c {{Q}} ->
P ==> P' ->
{{P}} c {{Q}}.
Proof.
intros.
unfold triple in *.
unfold strongerThan in *.
intros.
apply H0 in H2.
apply H in H1.
-apply H1. -apply H2.
Qed.
Theorem rule_consequence_post : forall (P Q Q' : assertion) c,
{{P}} c {{Q'}} ->
Q' ==> Q ->
{{P}} c {{Q}}.
Proof.
unfold triple in *.
unfold strongerThan in *.
intros. unfold s_imp in *.
assert (c / st \\ opst /\ P st). -auto.
-apply H in H1.
+destruct opst.
*apply H0. assumption.
*inversion H1.
+apply H2.
Qed.
Theorem rule_consequence : forall (P P' Q Q' : assertion) c,
{{P'}} c {{Q'}} ->
P ==> P' ->
Q' ==> Q ->
{{P}} c {{Q}}.
Proof.
intros.
apply rule_consequence_pre with P'.
-apply rule_consequence_post with Q'.
+assumption.
+assumption.
-assumption.
Qed.
Theorem rule_skip : forall P,
{{P}} CSkip {{P}}.
Proof.
unfold triple. intros.
inversion H. subst. assumption.
Qed.
(* Sequencing *)
Theorem rule_seq : forall P Q R c1 c2,
{{Q}} c2 {{R}} ->
{{P}} c1 {{Q}} ->
{{P}} (CSeq c1 c2) {{R}}.
Proof.
unfold triple.
intros.
inversion H1. subst.
apply H0 in H5. apply H in H8.
-assumption. -assumption. -assumption.
-subst. apply H0 in H7.
+inversion H7. +apply H2.
Qed.
(* Conditionals *)
(*
{{P ∧ b}} c1 {{Q}}
{{P ∧ ~b}} c2 {{Q}}
------------------------------------
{{P}} IFB b THEN c1 ELSE c2 FI {{Q}}
*)
Definition bassn b : assertion :=
fun st => (beval (fst st) b = true).
Lemma bexp_eval_true : forall b st,
beval (fst st) b = true -> (bassn b) st.
Proof.
intros.
unfold bassn. assumption.
Qed.
Lemma bexp_eval_false : forall b st,
beval (fst st) b = false -> not ((bassn b) st).
Proof.
unfold bassn, not.
intros. rewrite H in H0. inversion H0.
Qed.
Theorem rule_if : forall P Q b c1 c2,
{{fun st => P st /\ bassn b st}} c1 {{Q}} ->
{{fun st => P st /\ ~(bassn b st)}} c2 {{Q}} ->
{{P}} (CIf b c1 c2) {{Q}}.
Proof.
unfold triple, bassn, not.
intros. inversion H1. subst.
-apply H in H9. assumption.
+split. ++apply H2. ++apply H8.
-subst. apply H0 in H9.
+apply H9.
+split.
++apply H2.
++intros. simpl in H3.
rewrite H8 in H3. inversion H3.
Qed.
(* loops *)
Theorem rule_while : forall P b c,
{{fun st => P st /\ bassn b st}} c {{P}} ->
{{P}} (CWhile b c) {{fun st => P st /\ not (bassn b st)}}.
Proof.
intros P b c Hhoare st st' He HP.
remember (CWhile b c) as wcom eqn:Heqwcom.
induction He;
try (inversion Heqwcom); subst; clear Heqwcom.
- (* E_WhileEnd *)
split. assumption. apply bexp_eval_false. assumption.
- (* E_WhileLoop *)
apply IHHe2. reflexivity. unfold triple in *.
apply (Hhoare (sto, h) (St st)). assumption.
split. assumption. apply bexp_eval_true. assumption.
- unfold triple in *.
apply (Hhoare (sto, h) Abt).
+assumption. +split. *assumption.
*apply bexp_eval_true. simpl. assumption.
Qed.
(* allocation *)
Theorem rule_alloc : forall P X a,
{{fun st => forall loc, (((ANum loc) |-> a) --* P [X \ (ANum loc)]) st}}
(CCons X a)
{{P}}.
Proof.
intros. unfold triple. intros.
unfold sep_disj, assn_sub, point_to in *.
inversion H. subst.
simpl in *.
remember (h_update emp_heap l (aeval sto a)) as h'.
assert ((h_union h h') = (h_update h l (aeval sto a))).
-unfold h_union, h_update. apply functional_extensionality.
intros. destruct (in_not_in_dec x h) eqn:Hx.
+destruct (l =? x) eqn:Hxx.
*apply beq_nat_true in Hxx. unfold in_dom in i.
destruct i. subst. rewrite e in H6. inversion H6.
*reflexivity.
+destruct (l =? x) eqn:Hxx.
*apply beq_nat_true in Hxx. unfold not_in_dom in n.
subst. unfold h_update. destruct (x =? x) eqn:Fk.
++reflexivity.
++apply beq_nat_false in Fk. destruct Fk. reflexivity.
*apply beq_nat_false in Hxx. subst. unfold not_in_dom in n.
unfold h_update. destruct (l =? x) eqn:Fkk.
++apply beq_nat_true in Fkk. subst. destruct Hxx. reflexivity.
++unfold emp_heap. rewrite n. reflexivity.
-rewrite <- H1. apply H0.
+unfold disjoint. intros. destruct (l =? l0) eqn:Hx.
*apply beq_nat_true in Hx.
right. unfold not_in_dom. subst. assumption.
*left. unfold not_in_dom. subst. unfold h_update. rewrite Hx.
unfold emp_heap. reflexivity.
+subst. reflexivity.
Qed.
(* mutation *)
Theorem rule_mutate : forall P a1 a2,
{{fun st => exists loc, ((aeval (fst st) a1) = loc) /\
exists val, ((snd st) loc) = Some val /\
P ((fst st), (h_update (snd st) loc (aeval (fst st) a2))) }}
(CMutat a1 a2)
{{P}}.
Proof.
intros. unfold triple. intros. inversion H. subst.
-inversion H0. simpl in *. destruct H1. destruct H2.
destruct H2. rewrite H1. assumption.
-subst. destruct H0. destruct H0. destruct H1. destruct H1.
simpl in *. rewrite <- H0 in H1. rewrite H1 in H6.
inversion H6.
Qed.
(* look up *)
Theorem rule_lookup : forall P a x,
{{fun st => exists loc, ((aeval (fst st) a) = loc) /\
exists val, ((snd st) loc) = Some val /\
P ((st_update (fst st) x val), (snd st))
}}
(CLookup x a)
{{P}}.
Proof.
intros. unfold triple. intros. inversion H. subst.
-destruct H0. destruct H0. destruct H1. destruct H1.
simpl in *. rewrite <- H0 in H1. rewrite H1 in H6.
inversion H6. subst. assumption.
-subst. destruct H0. destruct H0. destruct H1.
destruct H1. simpl in *. rewrite H0 in H6.
rewrite H1 in H6. inversion H6.
Qed.
(* dispose *)
Theorem rule_dispose : forall P a,
{{fun st => exists loc, ((aeval (fst st) a) = loc) /\
exists val, ((snd st) loc) = Some val /\
P ((fst st),
(fun l => if (eq_nat_dec l loc) then None else (snd st) l))
}}
(CDispose a)
{{P}}.
Proof.
intros. unfold triple. intros. inversion H. subst.
-destruct H0. destruct H0. destruct H1. destruct H1.
simpl in *. rewrite H0. assumption.
-subst. destruct H0. destruct H0. destruct H1. destruct H1.
simpl in *. rewrite <- H0 in H1. rewrite H1 in H3. inversion H3.
Qed.