-
Notifications
You must be signed in to change notification settings - Fork 0
/
Assignment10_00.v
295 lines (243 loc) · 8.61 KB
/
Assignment10_00.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
291
292
293
294
Require Export Imp.
(* Important:
- You are NOT allowed to use the [admit] tactic.
- You are ALLOWED to use any tactics including:
[tauto], [intuition], [firstorder], [omega].
- Just leave [exact FILL_IN_HERE] for those problems that you fail to prove.
*)
Definition FILL_IN_HERE {T: Type} : T. Admitted.
Reserved Notation " t '==>' t' " (at level 40).
Inductive tm : Type :=
| C : nat -> tm (* Constant *)
| P : tm -> tm -> tm. (* Plus *)
Tactic Notation "tm_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "C" | Case_aux c "P" ].
Fixpoint evalF (t : tm) : nat :=
match t with
| C n => n
| P a1 a2 => evalF a1 + evalF a2
end.
Reserved Notation " t '||' n " (at level 50, left associativity).
Inductive eval : tm -> nat -> Prop :=
| E_Const : forall n,
C n || n
| E_Plus : forall t1 t2 n1 n2,
t1 || n1 ->
t2 || n2 ->
P t1 t2 || (n1 + n2)
where " t '||' n " := (eval t n).
Tactic Notation "eval_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "E_Const" | Case_aux c "E_Plus" ].
Definition relation (X: Type) := X->X->Prop.
Definition deterministic {X: Type} (R: relation X) :=
forall x y1 y2 : X, R x y1 -> R x y2 -> y1 = y2.
Inductive value : tm -> Prop :=
v_const : forall n, value (C n).
Reserved Notation " t '==>' t' " (at level 40).
Inductive step : tm -> tm -> Prop :=
| ST_PlusConstConst : forall n1 n2,
P (C n1) (C n2)
==> C (n1 + n2)
| ST_Plus1 : forall t1 t1' t2,
t1 ==> t1' ->
P t1 t2 ==> P t1' t2
| ST_Plus2 : forall v1 t2 t2',
value v1 -> (* <----- n.b. *)
t2 ==> t2' ->
P v1 t2 ==> P v1 t2'
where " t '==>' t' " := (step t t').
Tactic Notation "step_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "ST_PlusConstConst"
| Case_aux c "ST_Plus1" | Case_aux c "ST_Plus2" ].
Inductive multi {X:Type} (R: relation X) : relation X :=
| multi_refl : forall (x : X), multi R x x
| multi_step : forall (x y z : X),
R x y ->
multi R y z ->
multi R x z.
Tactic Notation "multi_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "multi_refl" | Case_aux c "multi_step" ].
Notation " t '==>*' t' " := (multi step t t') (at level 40).
Theorem multi_R : forall (X:Type) (R:relation X) (x y : X),
R x y -> (multi R) x y.
Proof.
intros X R x y H.
apply multi_step with y. apply H. apply multi_refl. Qed.
Theorem multi_trans :
forall (X:Type) (R: relation X) (x y z : X),
multi R x y ->
multi R y z ->
multi R x z.
Proof.
intros X R x y z G H.
multi_cases (induction G) Case.
Case "multi_refl". assumption.
Case "multi_step".
apply multi_step with y. assumption.
apply IHG. assumption.
Qed.
Definition normal_form {X:Type} (R:relation X) (t:X) : Prop :=
~ exists t', R t t'.
Definition step_normal_form := normal_form step.
Definition normal_form_of (t t' : tm) :=
(t ==>* t' /\ step_normal_form t').
(***
Concurrent Imp
***)
Inductive com : Type :=
| CSkip : com
| CAss : id -> aexp -> com
| CSeq : com -> com -> com
| CIf : bexp -> com -> com -> com
| CWhile : bexp -> com -> com
(* New: *)
| CPar : com -> com -> com.
Tactic Notation "com_cases" tactic(first) ident(c) :=
first;
[ Case_aux c "SKIP" | Case_aux c "::=" | Case_aux c ";"
| Case_aux c "IFB" | Case_aux c "WHILE" | Case_aux c "PAR" ].
Notation "'SKIP'" :=
CSkip.
Notation "x '::=' a" :=
(CAss x a) (at level 60).
Notation "c1 ;; c2" :=
(CSeq c1 c2) (at level 80, right associativity).
Notation "'WHILE' b 'DO' c 'END'" :=
(CWhile b c) (at level 80, right associativity).
Notation "'IFB' b 'THEN' c1 'ELSE' c2 'FI'" :=
(CIf b c1 c2) (at level 80, right associativity).
Notation "'PAR' c1 'WITH' c2 'END'" :=
(CPar c1 c2) (at level 80, right associativity).
Inductive aval : aexp -> Prop :=
av_num : forall n, aval (ANum n).
Hint Constructors aval.
Reserved Notation " t '/' st '==>a' t' " (at level 40, st at level 39).
Inductive astep : state -> aexp -> aexp -> Prop :=
| AS_Id : forall st i,
AId i / st ==>a ANum (st i)
| AS_Plus : forall st n1 n2,
APlus (ANum n1) (ANum n2) / st ==>a ANum (n1 + n2)
| AS_Plus1 : forall st a1 a1' a2,
a1 / st ==>a a1' ->
(APlus a1 a2) / st ==>a (APlus a1' a2)
| AS_Plus2 : forall st v1 a2 a2',
aval v1 ->
a2 / st ==>a a2' ->
(APlus v1 a2) / st ==>a (APlus v1 a2')
| AS_Minus : forall st n1 n2,
(AMinus (ANum n1) (ANum n2)) / st ==>a (ANum (minus n1 n2))
| AS_Minus1 : forall st a1 a1' a2,
a1 / st ==>a a1' ->
(AMinus a1 a2) / st ==>a (AMinus a1' a2)
| AS_Minus2 : forall st v1 a2 a2',
aval v1 ->
a2 / st ==>a a2' ->
(AMinus v1 a2) / st ==>a (AMinus v1 a2')
| AS_Mult : forall st n1 n2,
(AMult (ANum n1) (ANum n2)) / st ==>a (ANum (mult n1 n2))
| AS_Mult1 : forall st a1 a1' a2,
a1 / st ==>a a1' ->
(AMult (a1) (a2)) / st ==>a (AMult (a1') (a2))
| AS_Mult2 : forall st v1 a2 a2',
aval v1 ->
a2 / st ==>a a2' ->
(AMult v1 a2) / st ==>a (AMult v1 a2')
where " t '/' st '==>a' t' " := (astep st t t').
Hint Constructors astep.
Reserved Notation " t '/' st '==>b' t' " (at level 40, st at level 39).
Inductive bstep : state -> bexp -> bexp -> Prop :=
| BS_Eq : forall st n1 n2,
(BEq (ANum n1) (ANum n2)) / st ==>b
(if (beq_nat n1 n2) then BTrue else BFalse)
| BS_Eq1 : forall st a1 a1' a2,
a1 / st ==>a a1' ->
(BEq a1 a2) / st ==>b (BEq a1' a2)
| BS_Eq2 : forall st v1 a2 a2',
aval v1 ->
a2 / st ==>a a2' ->
(BEq v1 a2) / st ==>b (BEq v1 a2')
| BS_LtEq : forall st n1 n2,
(BLe (ANum n1) (ANum n2)) / st ==>b
(if (ble_nat n1 n2) then BTrue else BFalse)
| BS_LtEq1 : forall st a1 a1' a2,
a1 / st ==>a a1' ->
(BLe a1 a2) / st ==>b (BLe a1' a2)
| BS_LtEq2 : forall st v1 a2 a2',
aval v1 ->
a2 / st ==>a a2' ->
(BLe v1 a2) / st ==>b (BLe v1 (a2'))
| BS_NotTrue : forall st,
(BNot BTrue) / st ==>b BFalse
| BS_NotFalse : forall st,
(BNot BFalse) / st ==>b BTrue
| BS_NotStep : forall st b1 b1',
b1 / st ==>b b1' ->
(BNot b1) / st ==>b (BNot b1')
| BS_AndTrueTrue : forall st,
(BAnd BTrue BTrue) / st ==>b BTrue
| BS_AndTrueFalse : forall st,
(BAnd BTrue BFalse) / st ==>b BFalse
| BS_AndFalse : forall st b2,
(BAnd BFalse b2) / st ==>b BFalse
| BS_AndTrueStep : forall st b2 b2',
b2 / st ==>b b2' ->
(BAnd BTrue b2) / st ==>b (BAnd BTrue b2')
| BS_AndStep : forall st b1 b1' b2,
b1 / st ==>b b1' ->
(BAnd b1 b2) / st ==>b (BAnd b1' b2)
where " t '/' st '==>b' t' " := (bstep st t t').
Hint Constructors bstep.
Reserved Notation " t '/' st '==>c' t' '/' st' "
(at level 40, st at level 39, t' at level 39).
Inductive cstep : (com * state) -> (com * state) -> Prop :=
(* Old part *)
| CS_AssStep : forall st i a a',
a / st ==>a a' ->
(i ::= a) / st ==>c (i ::= a') / st
| CS_Ass : forall st i n,
(i ::= (ANum n)) / st ==>c SKIP / (update st i n)
| CS_SeqStep : forall st c1 c1' st' c2,
c1 / st ==>c c1' / st' ->
(c1 ;; c2) / st ==>c (c1' ;; c2) / st'
| CS_SeqFinish : forall st c2,
(SKIP ;; c2) / st ==>c c2 / st
| CS_IfTrue : forall st c1 c2,
(IFB BTrue THEN c1 ELSE c2 FI) / st ==>c c1 / st
| CS_IfFalse : forall st c1 c2,
(IFB BFalse THEN c1 ELSE c2 FI) / st ==>c c2 / st
| CS_IfStep : forall st b b' c1 c2,
b /st ==>b b' ->
(IFB b THEN c1 ELSE c2 FI) / st ==>c (IFB b' THEN c1 ELSE c2 FI) / st
| CS_While : forall st b c1,
(WHILE b DO c1 END) / st ==>c
(IFB b THEN (c1;; (WHILE b DO c1 END)) ELSE SKIP FI) / st
(* New part: *)
| CS_Par1 : forall st c1 c1' c2 st',
c1 / st ==>c c1' / st' ->
(PAR c1 WITH c2 END) / st ==>c (PAR c1' WITH c2 END) / st'
| CS_Par2 : forall st c1 c2 c2' st',
c2 / st ==>c c2' / st' ->
(PAR c1 WITH c2 END) / st ==>c (PAR c1 WITH c2' END) / st'
| CS_ParDone : forall st,
(PAR SKIP WITH SKIP END) / st ==>c SKIP / st
where " t '/' st '==>c' t' '/' st' " := (cstep (t,st) (t',st')).
Hint Constructors cstep.
Definition cmultistep := multi cstep.
Notation " t '/' st '==>c*' t' '/' st' " :=
(multi cstep (t,st) (t',st'))
(at level 40, st at level 39, t' at level 39).
(** Among the many interesting properties of this language is the fact
that the following program can terminate with the variable [X] set
to any value... *)
Definition par_loop : com :=
PAR
Y ::= ANum 1
WITH
WHILE BEq (AId Y) (ANum 0) DO
X ::= APlus (AId X) (ANum 1)
END
END.