heap_lang.v 14.4 KB
Newer Older
1
Require Export Autosubst.Autosubst.
2
Require Import prelude.option prelude.gmap iris.language.
3

4
(** Expressions and values. *)
5
Definition loc := positive. (* Really, any countable type. *)
Ralf Jung's avatar
Ralf Jung committed
6

Ralf Jung's avatar
Ralf Jung committed
7
Inductive expr :=
8
(* Base lambda calculus *)
Ralf Jung's avatar
Ralf Jung committed
9
| Var (x : var)
10
| Rec (e : {bind 2 of expr}) (* These are recursive lambdas. The *inner* binder is the recursive call! *)
11
| App (e1 e2 : expr)
Ralf Jung's avatar
Ralf Jung committed
12
(* Natural numbers *)
13
14
| LitNat (n : nat)
| Plus (e1 e2 : expr)
Ralf Jung's avatar
Ralf Jung committed
15
| Le (e1 e2 : expr)
16
17
(* Unit *)
| LitUnit
18
(* Products *)
Ralf Jung's avatar
Ralf Jung committed
19
20
21
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
22
(* Sums *)
Ralf Jung's avatar
Ralf Jung committed
23
24
| InjL (e : expr)
| InjR (e : expr)
Ralf Jung's avatar
Ralf Jung committed
25
| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
26
27
28
29
(* Concurrency *)
| Fork (e : expr)
(* Heap *)
| Loc (l : loc)
Ralf Jung's avatar
Ralf Jung committed
30
| Alloc (e : expr)
Ralf Jung's avatar
Ralf Jung committed
31
32
33
34
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| Cas (e0 : expr) (e1 : expr) (e2 : expr)
.
Ralf Jung's avatar
Ralf Jung committed
35
36
37
38
39
40

Instance Ids_expr : Ids expr. derive. Defined.
Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.

41
42
43
(* This sugar is used by primitive reduction riles (<=, CAS) and hence defined here. *)
Definition LitTrue := InjL LitUnit.
Definition LitFalse := InjR LitUnit.
44

Ralf Jung's avatar
Ralf Jung committed
45
Inductive value :=
Ralf Jung's avatar
Ralf Jung committed
46
| RecV (e : {bind 2 of expr})
47
48
| LitNatV (n : nat) (* These are recursive lambdas. The *inner* binder is the recursive call! *)
| LitUnitV
Ralf Jung's avatar
Ralf Jung committed
49
50
| PairV (v1 v2 : value)
| InjLV (v : value)
51
| InjRV (v : value)
Ralf Jung's avatar
Ralf Jung committed
52
53
| LocV (l : loc)
.
Ralf Jung's avatar
Ralf Jung committed
54

Ralf Jung's avatar
Ralf Jung committed
55
56
Definition LitTrueV := InjLV LitUnitV.
Definition LitFalseV := InjRV LitUnitV.
Ralf Jung's avatar
Ralf Jung committed
57

58
Fixpoint v2e (v : value) : expr :=
Ralf Jung's avatar
Ralf Jung committed
59
  match v with
Ralf Jung's avatar
Ralf Jung committed
60
  | RecV e   => Rec e
61
62
  | LitNatV n => LitNat n
  | LitUnitV => LitUnit
Ralf Jung's avatar
Ralf Jung committed
63
64
65
  | PairV v1 v2 => Pair (v2e v1) (v2e v2)
  | InjLV v => InjL (v2e v)
  | InjRV v => InjR (v2e v)
66
  | LocV l => Loc l
Ralf Jung's avatar
Ralf Jung committed
67
68
  end.

69
70
Fixpoint e2v (e : expr) : option value :=
  match e with
Ralf Jung's avatar
Ralf Jung committed
71
  | Rec e => Some (RecV e)
72
73
  | LitNat n => Some (LitNatV n)
  | LitUnit => Some LitUnitV
74
75
76
77
78
  | Pair e1 e2 => v1  e2v e1;
                  v2  e2v e2;
                  Some (PairV v1 v2)
  | InjL e => InjLV <$> e2v e
  | InjR e => InjRV <$> e2v e
79
  | Loc l => Some (LocV l)
Ralf Jung's avatar
Ralf Jung committed
80
  | _ => None
81
82
83
84
85
  end.

Lemma v2v v:
  e2v (v2e v) = Some v.
Proof.
86
  induction v; simpl; rewrite ?IHv ?IHv1 /= ?IHv2; reflexivity.
87
88
Qed.

Ralf Jung's avatar
Ralf Jung committed
89
Section e2e. (* To get local tactics. *)
90
Lemma e2e e v:
Ralf Jung's avatar
Ralf Jung committed
91
  e2v e = Some v  v2e v = e.
92
Proof.
Ralf Jung's avatar
Ralf Jung committed
93
94
95
96
97
98
99
  Ltac case0 := case =><-; simpl; eauto using f_equal, f_equal2.
  Ltac case1 e1 := destruct (e2v e1); simpl; [|discriminate];
                   case0.
  Ltac case2 e1 e2 := destruct (e2v e1); simpl; [|discriminate];
                      destruct (e2v e2); simpl; [|discriminate];
                      case0.

Ralf Jung's avatar
Ralf Jung committed
100
101
  revert v; induction e; intros v; simpl; try discriminate;
    by (case2 e1 e2 || case1 e || case0).
Ralf Jung's avatar
Ralf Jung committed
102
103
104
105
Qed.
End e2e.

Lemma v2e_inj v1 v2:
Ralf Jung's avatar
Ralf Jung committed
106
  v2e v1 = v2e v2  v1 = v2.
Ralf Jung's avatar
Ralf Jung committed
107
Proof.
108
109
  revert v2; induction v1=>v2; destruct v2; simpl; try done;
    case; eauto using f_equal, f_equal2.
110
Qed.
111

112
113
(** The state: heaps of values. *)
Definition state := gmap loc value.
Ralf Jung's avatar
Ralf Jung committed
114

115
(** Evaluation contexts *)
Ralf Jung's avatar
Ralf Jung committed
116
117
Inductive ectx :=
| EmptyCtx
Ralf Jung's avatar
Ralf Jung committed
118
| AppLCtx (K1 : ectx)  (e2 : expr)
Ralf Jung's avatar
Ralf Jung committed
119
| AppRCtx (v1 : value) (K2 : ectx)
120
121
| PlusLCtx (K1 : ectx)  (e2 : expr)
| PlusRCtx (v1 : value) (K2 : ectx)
Ralf Jung's avatar
Ralf Jung committed
122
123
| LeLCtx (K1 : ectx)  (e2 : expr)
| LeRCtx (v1 : value) (K2 : ectx)
Ralf Jung's avatar
Ralf Jung committed
124
| PairLCtx (K1 : ectx)  (e2 : expr)
Ralf Jung's avatar
Ralf Jung committed
125
126
127
128
129
| PairRCtx (v1 : value) (K2 : ectx)
| FstCtx (K : ectx)
| SndCtx (K : ectx)
| InjLCtx (K : ectx)
| InjRCtx (K : ectx)
130
| CaseCtx (K : ectx) (e1 : {bind expr}) (e2 : {bind expr})
Ralf Jung's avatar
Ralf Jung committed
131
| AllocCtx (K : ectx)
Ralf Jung's avatar
Ralf Jung committed
132
133
134
135
136
137
138
| LoadCtx (K : ectx)
| StoreLCtx (K1 : ectx)  (e2 : expr)
| StoreRCtx (v1 : value) (K2 : ectx)
| CasLCtx (K0 : ectx)  (e1 : expr)  (e2 : expr)
| CasMCtx (v0 : value) (K1 : ectx)  (e2 : expr)
| CasRCtx (v0 : value) (v1 : value) (K2 : ectx)
.
Ralf Jung's avatar
Ralf Jung committed
139
140
141
142
143
144

Fixpoint fill (K : ectx) (e : expr) :=
  match K with
  | EmptyCtx => e
  | AppLCtx K1 e2 => App (fill K1 e) e2
  | AppRCtx v1 K2 => App (v2e v1) (fill K2 e)
145
146
  | PlusLCtx K1 e2 => Plus (fill K1 e) e2
  | PlusRCtx v1 K2 => Plus (v2e v1) (fill K2 e)
Ralf Jung's avatar
Ralf Jung committed
147
148
  | LeLCtx K1 e2 => Le (fill K1 e) e2
  | LeRCtx v1 K2 => Le (v2e v1) (fill K2 e)
Ralf Jung's avatar
Ralf Jung committed
149
150
151
152
153
154
155
  | PairLCtx K1 e2 => Pair (fill K1 e) e2
  | PairRCtx v1 K2 => Pair (v2e v1) (fill K2 e)
  | FstCtx K => Fst (fill K e)
  | SndCtx K => Snd (fill K e)
  | InjLCtx K => InjL (fill K e)
  | InjRCtx K => InjR (fill K e)
  | CaseCtx K e1 e2 => Case (fill K e) e1 e2
Ralf Jung's avatar
Ralf Jung committed
156
  | AllocCtx K => Alloc (fill K e)
157
  | LoadCtx K => Load (fill K e)
Ralf Jung's avatar
Ralf Jung committed
158
159
160
161
162
  | StoreLCtx K1 e2 => Store (fill K1 e) e2
  | StoreRCtx v1 K2 => Store (v2e v1) (fill K2 e)
  | CasLCtx K0 e1 e2 => Cas (fill K0 e) e1 e2
  | CasMCtx v0 K1 e2 => Cas (v2e v0) (fill K1 e) e2
  | CasRCtx v0 v1 K2 => Cas (v2e v0) (v2e v1) (fill K2 e)
Ralf Jung's avatar
Ralf Jung committed
163
164
165
166
167
168
169
  end.

Fixpoint comp_ctx (Ko : ectx) (Ki : ectx) :=
  match Ko with
  | EmptyCtx => Ki
  | AppLCtx K1 e2 => AppLCtx (comp_ctx K1 Ki) e2
  | AppRCtx v1 K2 => AppRCtx v1 (comp_ctx K2 Ki)
170
171
  | PlusLCtx K1 e2 => PlusLCtx (comp_ctx K1 Ki) e2
  | PlusRCtx v1 K2 => PlusRCtx v1 (comp_ctx K2 Ki)
Ralf Jung's avatar
Ralf Jung committed
172
173
  | LeLCtx K1 e2 => LeLCtx (comp_ctx K1 Ki) e2
  | LeRCtx v1 K2 => LeRCtx v1 (comp_ctx K2 Ki)
Ralf Jung's avatar
Ralf Jung committed
174
175
176
177
178
179
180
  | PairLCtx K1 e2 => PairLCtx (comp_ctx K1 Ki) e2
  | PairRCtx v1 K2 => PairRCtx v1 (comp_ctx K2 Ki)
  | FstCtx K => FstCtx (comp_ctx K Ki)
  | SndCtx K => SndCtx (comp_ctx K Ki)
  | InjLCtx K => InjLCtx (comp_ctx K Ki)
  | InjRCtx K => InjRCtx (comp_ctx K Ki)
  | CaseCtx K e1 e2 => CaseCtx (comp_ctx K Ki) e1 e2
Ralf Jung's avatar
Ralf Jung committed
181
  | AllocCtx K => AllocCtx (comp_ctx K Ki)
182
  | LoadCtx K => LoadCtx (comp_ctx K Ki)
Ralf Jung's avatar
Ralf Jung committed
183
184
185
186
187
  | StoreLCtx K1 e2 => StoreLCtx (comp_ctx K1 Ki) e2
  | StoreRCtx v1 K2 => StoreRCtx v1 (comp_ctx K2 Ki)
  | CasLCtx K0 e1 e2 => CasLCtx (comp_ctx K0 Ki) e1 e2
  | CasMCtx v0 K1 e2 => CasMCtx v0 (comp_ctx K1 Ki) e2
  | CasRCtx v0 v1 K2 => CasRCtx v0 v1 (comp_ctx K2 Ki)
Ralf Jung's avatar
Ralf Jung committed
188
189
190
191
192
193
194
195
196
197
198
  end.

Lemma fill_empty e :
  fill EmptyCtx e = e.
Proof.
  reflexivity.
Qed.

Lemma fill_comp K1 K2 e :
  fill K1 (fill K2 e) = fill (comp_ctx K1 K2) e.
Proof.
199
  revert K2 e; induction K1 => K2 e /=; rewrite ?IHK1 ?IHK2; reflexivity.
Ralf Jung's avatar
Ralf Jung committed
200
201
202
Qed.

Lemma fill_inj_r K e1 e2 :
Ralf Jung's avatar
Ralf Jung committed
203
  fill K e1 = fill K e2  e1 = e2.
Ralf Jung's avatar
Ralf Jung committed
204
Proof.
205
206
  revert e1 e2; induction K => el er /=;
     (move=><-; reflexivity) || (case => /IHK <-; reflexivity).
Ralf Jung's avatar
Ralf Jung committed
207
208
Qed.

Ralf Jung's avatar
Ralf Jung committed
209
Lemma fill_value K e v':
Ralf Jung's avatar
Ralf Jung committed
210
  e2v (fill K e) = Some v'  is_Some (e2v e).
Ralf Jung's avatar
Ralf Jung committed
211
Proof.
212
  revert v'; induction K => v' /=; try discriminate;
Ralf Jung's avatar
Ralf Jung committed
213
214
215
    try destruct (e2v (fill K e)); rewrite ?v2v; eauto.
Qed.

216
Lemma fill_not_value e K :
Ralf Jung's avatar
Ralf Jung committed
217
  e2v e = None  e2v (fill K e) = None.
218
Proof.
219
  intros Hnval.  induction K =>/=; by rewrite ?v2v /= ?IHK /=.
220
Qed.
221

222
Lemma fill_not_value2 e K v :
Ralf Jung's avatar
Ralf Jung committed
223
  e2v e = None  e2v (fill K e) = Some v -> False.
224
225
226
227
Proof.
  intros Hnval Hval. erewrite fill_not_value in Hval by assumption. discriminate.
Qed.

228
229
230
231
232
233
234
235
Lemma comp_empty K K' :
  EmptyCtx = comp_ctx K K' 
  K = EmptyCtx  K' = EmptyCtx.
Proof.
  destruct K; try discriminate.
  destruct K'; try discriminate.
  done.
Qed.
236
237

(** The stepping relation *)
Ralf Jung's avatar
Ralf Jung committed
238
Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
Ralf Jung's avatar
Ralf Jung committed
239
| BetaS e1 e2 v2 σ (Hv2 : e2v e2 = Some v2):
240
    prim_step (App (Rec e1) e2) σ e1.[(Rec e1),e2/] σ None
241
242
| PlusS n1 n2 σ:
    prim_step (Plus (LitNat n1) (LitNat n2)) σ (LitNat (n1 + n2)) σ None
Ralf Jung's avatar
Ralf Jung committed
243
244
245
246
| LeTrueS n1 n2 σ (Hle : n1  n2):
    prim_step (Le (LitNat n1) (LitNat n2)) σ LitTrue σ None
| LeFalseS n1 n2 σ (Hle : n1 > n2):
    prim_step (Le (LitNat n1) (LitNat n2)) σ LitFalse σ None
247
248
249
250
| FstS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2):
    prim_step (Fst (Pair e1 e2)) σ e1 σ None
| SndS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2):
    prim_step (Snd (Pair e1 e2)) σ e2 σ None
Ralf Jung's avatar
Ralf Jung committed
251
| CaseLS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
252
    prim_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ None
Ralf Jung's avatar
Ralf Jung committed
253
| CaseRS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
254
    prim_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
Ralf Jung's avatar
Ralf Jung committed
255
| ForkS e σ:
256
    prim_step (Fork e) σ LitUnit σ (Some e)
257
| AllocS e v σ l (Hv : e2v e = Some v) (Hfresh : σ !! l = None):
Ralf Jung's avatar
Ralf Jung committed
258
    prim_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
Ralf Jung's avatar
Ralf Jung committed
259
260
261
262
263
264
265
266
267
268
269
| LoadS l v σ (Hlookup : σ !! l = Some v):
    prim_step (Load (Loc l)) σ (v2e v) σ None
| StoreS l e v σ (Hv : e2v e = Some v) (Halloc : is_Some (σ !! l)):
    prim_step (Store (Loc l) e) σ LitUnit (<[l:=v]>σ) None
| CasFailS l e1 v1 e2 v2 vl σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2)
  (Hlookup : σ !! l = Some vl) (Hne : vl <> v1):
    prim_step (Cas (Loc l) e1 e2) σ LitFalse σ None
| CasSucS l e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2)
  (Hlookup : σ !! l = Some v1):
    prim_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None
.
270

271
272
Definition reducible e σ : Prop :=
   e' σ' ef, prim_step e σ e' σ' ef.
273

274
275
Lemma reducible_not_value e σ :
  reducible e σ  e2v e = None.
276
Proof.
277
  intros (e' & σ' & ef & Hstep). destruct Hstep; simpl in *; reflexivity.
278
279
Qed.

280
281
Definition stuck (e : expr) σ : Prop :=
   K e', e = fill K e'  ~reducible e' σ.
282

283
284
Lemma values_stuck v σ :
  stuck (v2e v) σ.
285
Proof.
Ralf Jung's avatar
Ralf Jung committed
286
287
288
  intros ?? Heq.
  edestruct (fill_value K) as [v' Hv'].
  { by rewrite <-Heq, v2v. }
289
290
  clear -Hv' => Hred. apply reducible_not_value in Hred.
  destruct (e2v e'); discriminate.
Ralf Jung's avatar
Ralf Jung committed
291
Qed.
292

Ralf Jung's avatar
Ralf Jung committed
293
Section step_by_value.
294
295
296
297
(* When something does a step, and another decomposition of the same
     expression has a non-value e in the hole, then K is a left
     sub-context of K' - in other words, e also contains the reducible
     expression *)
298
Lemma step_by_value {K K' e e' σ} :
Ralf Jung's avatar
Ralf Jung committed
299
300
301
302
  fill K e = fill K' e' 
  reducible e' σ 
  e2v e = None 
   K'', K' = comp_ctx K K''.
303
Proof.
304
  Ltac bad_fill := intros; exfalso; subst;
Ralf Jung's avatar
Ralf Jung committed
305
306
307
308
309
310
311
312
                   (eapply values_stuck; eassumption) ||
                     (eapply fill_not_value2; first eassumption;
                      try match goal with
                        [ H : fill _ _ = _ |- _ ] => erewrite ->H
                      end;
                      by erewrite ?v2v).
  Ltac bad_red   Hfill e' Hred := exfalso; destruct e';
      try discriminate Hfill; [];
313
      case: Hfill; intros; subst; destruct Hred as (e'' & σ'' & ef & Hstep);
Ralf Jung's avatar
Ralf Jung committed
314
315
316
      inversion Hstep; done || (clear Hstep; subst;
      eapply fill_not_value2; last (
        try match goal with [ H : _ = fill _ _ |- _ ] => erewrite <-H end; simpl;
Ralf Jung's avatar
Ralf Jung committed
317
318
319
        repeat match goal with [ H : e2v _ = _ |- _ ] =>
          erewrite H; clear H; simpl
        end
Ralf Jung's avatar
Ralf Jung committed
320
      ); eassumption || done).
321
  Ltac good IH := intros; subst; 
Ralf Jung's avatar
Ralf Jung committed
322
323
324
325
    let K'' := fresh "K''" in edestruct IH as [K'' Hcomp]; first eassumption;
    exists K''; by eauto using f_equal, f_equal2, f_equal3, v2e_inj.

  intros Hfill Hred Hnval. 
326
  revert K' Hfill; induction K=>K' /= Hfill;
327
    first (now eexists; reflexivity);
328
329
330
331
332
    (destruct K'; simpl;
      (* The first case is: K' is EmpyCtx. *)
      first (by bad_red Hfill e' Hred);
      (* Many of the other cases result in contradicting equalities. *)
      try discriminate Hfill;
Ralf Jung's avatar
Ralf Jung committed
333
334
335
      (* The remaining cases are "compatible" contexts - that result in the same
         head symbol of the expression.
         Test whether the context als has the same head, and use the appropriate
336
         tactic. *)
337
      by match goal with
Ralf Jung's avatar
Ralf Jung committed
338
339
340
341
342
343
      | [ |- exists x, ?C _ = ?C _ ] =>
        case: Hfill; good IHK
      | [ |- exists x, ?C _ _ = ?C _ _ ] =>
        case: Hfill; good IHK
      | [ |- exists x, ?C _ _ _ = ?C _ _ _ ] =>
        case: Hfill; good IHK
344
      | _ => case: Hfill; bad_fill
345
      end).
Ralf Jung's avatar
Ralf Jung committed
346
347
Qed.
End step_by_value.
348

349
350
351
(** Atomic expressions *)
Definition atomic (e: expr) :=
  match e with
Ralf Jung's avatar
Ralf Jung committed
352
  | Alloc e => is_Some (e2v e)
353
  | Load e => is_Some (e2v e)
Ralf Jung's avatar
Ralf Jung committed
354
355
  | Store e1 e2 => is_Some (e2v e1)  is_Some (e2v e2)
  | Cas e0 e1 e2 => is_Some (e2v e0)  is_Some (e2v e1)  is_Some (e2v e2)
356
357
358
  | _ => False
  end.

359
360
361
362
363
364
365
Lemma atomic_not_value e :
  atomic e -> e2v e = None.
Proof.
  destruct e; simpl; contradiction || reflexivity.
Qed.

Lemma atomic_step e1 σ1 e2 σ2 ef :
Ralf Jung's avatar
Ralf Jung committed
366
367
  atomic e1 
  prim_step e1 σ1 e2 σ2 ef 
368
369
  is_Some (e2v e2).
Proof.
Ralf Jung's avatar
Ralf Jung committed
370
371
  destruct e1; simpl; intros Hatomic Hstep; inversion Hstep;
    try contradiction Hatomic; rewrite ?v2v /=; eexists; reflexivity.
372
373
374
375
Qed.

(* Atomics must not contain evaluation positions. *)
Lemma atomic_fill e K :
Ralf Jung's avatar
Ralf Jung committed
376
377
  atomic (fill K e) 
  e2v e = None 
378
379
  K = EmptyCtx.
Proof.
Ralf Jung's avatar
Ralf Jung committed
380
381
  destruct K; simpl; first reflexivity; unfold is_Some; intros Hatomic Hnval;
    exfalso; try assumption;
Ralf Jung's avatar
Ralf Jung committed
382
    try (destruct_conjs; eapply fill_not_value2; eassumption).
383
384
Qed.

Ralf Jung's avatar
Ralf Jung committed
385
386
(** Instantiate the Iris language interface. This closes reduction under
    evaluation contexts.
387
388
389
    We could potentially make this a generic construction. *)
Section Language.

390
  Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
Ralf Jung's avatar
Ralf Jung committed
391
392
     K e1' e2', e1 = fill K e1'  e2 = fill K e2' 
                 prim_step e1' σ1 e2' σ2 ef.
393
394
395
396
  Program Canonical Structure heap_lang : language := {|
    language.expr := expr;
    language.val := value;
    language.state := state;
397
398
399
400
401
402
403
404
405
406
    of_val := v2e;
    to_val := e2v;
    language.atomic := atomic;
    language.prim_step := ectx_step;
    to_of_val := v2v;
    of_to_val := e2e;
    language.atomic_not_value := atomic_not_value
  |}.
  Next Obligation.
    intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2.
407
    eapply fill_not_value. eapply reducible_not_value. do 3 eexists; eassumption.
408
409
410
411
412
413
  Qed.
  Next Obligation.
    intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep).
    subst. move: (Hatomic). rewrite (atomic_fill e1' K).
    - rewrite !fill_empty. eauto using atomic_step.
    - assumption.
414
    - clear Hatomic. eapply reducible_not_value. do 3 eexists; eassumption.
415
  Qed.
416

417
418
  Global Instance heap_lang_fill : Fill ectx expr := fill.
  Global Instance heap_lang_ctx : CtxLanguage heap_lang ectx.
419
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
420
    split.
421
422
    - intros K ? Hnval. by eapply fill_not_value.
    - intros K ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
423
424
      exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
      split; last split; reflexivity || assumption.
425
    - intros K ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep).
426
427
      destruct (step_by_value (σ:=σ1) Heq1) as [K' HeqK].
      + do 3 eexists. eassumption.
428
      + assumption.
Ralf Jung's avatar
Ralf Jung committed
429
430
      + subst e2 K''. rewrite -fill_comp in Heq1. apply fill_inj_r in Heq1.
        subst e1'. exists (fill K' e2''). split; first by rewrite -fill_comp.
431
        do 3 eexists. split; last split; eassumption || reflexivity.
432
  Qed.
433

434
  Lemma prim_ectx_step e1 σ1 e2 σ2 ef :
435
    reducible e1 σ1 
436
437
438
439
    ectx_step e1 σ1 e2 σ2 ef 
    prim_step e1 σ1 e2 σ2 ef.
  Proof.
    intros Hred (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
440
    destruct (@step_by_value K' EmptyCtx e1' e1 σ1) as [K'' [HK' HK'']%comp_empty].
441
442
    - by rewrite fill_empty.
    - done.
443
    - eapply reducible_not_value. do 3 eexists; eassumption.
444
445
    - subst K' K'' e1 e2. by rewrite !fill_empty.
  Qed.
446

447
End Language.