heap_lang.v 15.3 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
Require Import Autosubst.Autosubst.
2
Require Import prelude.option prelude.gmap iris.language.
Ralf Jung's avatar
Ralf Jung committed
3

4
5
Set Bullet Behavior "Strict Subproofs".

6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
(** Some tactics useful when dealing with equality of sigma-like types: existT T0 t0 = existT T1 t1.
    They all assume such an equality is the first thing on the "stack" (goal). *)
Ltac case_depeq1 := let Heq := fresh "Heq" in
  case=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,<-).
Ltac case_depeq2 := let Heq := fresh "Heq" in
  case=>_ _ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,Heq);
  case:Heq=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,<-).
Ltac case_depeq3 := let Heq := fresh "Heq" in
  case=>_ _ _ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,Heq);
  case:Heq=>_ _ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,Heq);
  case:Heq=>_ /EqdepFacts.eq_sigT_sig_eq=>Heq;
  destruct Heq as (->,<-).

(** Expressions and values. *)
Ralf Jung's avatar
Ralf Jung committed
25
26
Definition loc := nat. (* Any countable type. *)

Ralf Jung's avatar
Ralf Jung committed
27
Inductive expr :=
28
(* Base lambda calculus *)
Ralf Jung's avatar
Ralf Jung committed
29
| Var (x : var)
Ralf Jung's avatar
Ralf Jung committed
30
| Rec (e : {bind 2 of expr}) (* These are recursive lambdas. *)
31
| App (e1 e2 : expr)
32
(* Embedding of Coq values and operations *)
33
34
35
| Lit {T : Type} (t: T)  (* arbitrary Coq values become literals *)
| Op1  {T1 To : Type} (f : T1 -> To) (e1 : expr)
| Op2  {T1 T2 To : Type} (f : T1 -> T2 -> To) (e1 : expr) (e2 : expr)
36
(* Products *)
Ralf Jung's avatar
Ralf Jung committed
37
38
39
| Pair (e1 e2 : expr)
| Fst (e : expr)
| Snd (e : expr)
40
(* Sums *)
Ralf Jung's avatar
Ralf Jung committed
41
42
| InjL (e : expr)
| InjR (e : expr)
Ralf Jung's avatar
Ralf Jung committed
43
| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
44
45
46
47
(* Concurrency *)
| Fork (e : expr)
(* Heap *)
| Loc (l : loc)
Ralf Jung's avatar
Ralf Jung committed
48
| Alloc (e : expr)
Ralf Jung's avatar
Ralf Jung committed
49
50
51
52
| Load (e : expr)
| Store (e1 : expr) (e2 : expr)
| Cas (e0 : expr) (e1 : expr) (e2 : expr)
.
Ralf Jung's avatar
Ralf Jung committed
53
54
55
56
57
58

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.

Ralf Jung's avatar
Ralf Jung committed
59
Definition Lam (e: {bind expr}) := Rec (e.[up ids]).
Ralf Jung's avatar
Ralf Jung committed
60
Definition LitUnit := Lit tt.
Ralf Jung's avatar
Ralf Jung committed
61
62
Definition LitTrue := Lit true.
Definition LitFalse := Lit false.
Ralf Jung's avatar
Ralf Jung committed
63

Ralf Jung's avatar
Ralf Jung committed
64
Inductive value :=
Ralf Jung's avatar
Ralf Jung committed
65
| RecV (e : {bind 2 of expr})
Ralf Jung's avatar
Ralf Jung committed
66
| LitV (T : Type) (t : T)  (* arbitrary Coq values become literal values *)
Ralf Jung's avatar
Ralf Jung committed
67
68
| PairV (v1 v2 : value)
| InjLV (v : value)
69
| InjRV (v : value)
Ralf Jung's avatar
Ralf Jung committed
70
71
| LocV (l : loc)
.
Ralf Jung's avatar
Ralf Jung committed
72

73
Fixpoint v2e (v : value) : expr :=
Ralf Jung's avatar
Ralf Jung committed
74
  match v with
75
  | LitV _ t => Lit t
Ralf Jung's avatar
Ralf Jung committed
76
  | RecV e   => Rec e
Ralf Jung's avatar
Ralf Jung committed
77
78
79
  | PairV v1 v2 => Pair (v2e v1) (v2e v2)
  | InjLV v => InjL (v2e v)
  | InjRV v => InjR (v2e v)
80
  | LocV l => Loc l
Ralf Jung's avatar
Ralf Jung committed
81
82
  end.

83
84
Fixpoint e2v (e : expr) : option value :=
  match e with
Ralf Jung's avatar
Ralf Jung committed
85
  | Rec e => Some (RecV e)
86
  | Lit T t => Some (LitV T t)
87
88
89
90
91
  | Pair e1 e2 => v1  e2v e1;
                  v2  e2v e2;
                  Some (PairV v1 v2)
  | InjL e => InjLV <$> e2v e
  | InjR e => InjRV <$> e2v e
92
  | Loc l => Some (LocV l)
Ralf Jung's avatar
Ralf Jung committed
93
  | _ => None
94
95
96
97
98
  end.

Lemma v2v v:
  e2v (v2e v) = Some v.
Proof.
99
  induction v; simpl; rewrite ?IHv ?IHv1 /= ?IHv2; reflexivity.
100
101
Qed.

Ralf Jung's avatar
Ralf Jung committed
102
Section e2e. (* To get local tactics. *)
103
Lemma e2e e v:
104
  e2v e = Some v -> v2e v = e.
105
Proof.
Ralf Jung's avatar
Ralf Jung committed
106
107
108
109
110
111
112
113
114
115
116
117
118
119
  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.

  revert v; induction e; intros v; simpl; try discriminate; by (case2 e1 e2 || case1 e || case0).
Qed.
End e2e.

Lemma v2e_inj v1 v2:
  v2e v1 = v2e v2 -> v1 = v2.
Proof.
120
  revert v2; induction v1=>v2; destruct v2; simpl; try discriminate;
Ralf Jung's avatar
Ralf Jung committed
121
    first [case_depeq1 | case]; eauto using f_equal, f_equal2.
122
Qed.
123

124
125
(** The state: heaps of values. *)
Definition state := gmap loc value.
Ralf Jung's avatar
Ralf Jung committed
126

127
(** Evaluation contexts *)
Ralf Jung's avatar
Ralf Jung committed
128
129
Inductive ectx :=
| EmptyCtx
Ralf Jung's avatar
Ralf Jung committed
130
| AppLCtx (K1 : ectx)  (e2 : expr)
Ralf Jung's avatar
Ralf Jung committed
131
| AppRCtx (v1 : value) (K2 : ectx)
132
| Op1Ctx {T1 To : Type} (f : T1 -> To) (K : ectx)
Ralf Jung's avatar
Ralf Jung committed
133
| Op2LCtx {T1 T2 To : Type} (f : T1 -> T2 -> To) (K1 : ectx)  (e2 : expr)
134
| Op2RCtx {T1 T2 To : Type} (f : T1 -> T2 -> To) (v1 : value) (K2 : ectx)
Ralf Jung's avatar
Ralf Jung committed
135
| PairLCtx (K1 : ectx)  (e2 : expr)
Ralf Jung's avatar
Ralf Jung committed
136
137
138
139
140
| PairRCtx (v1 : value) (K2 : ectx)
| FstCtx (K : ectx)
| SndCtx (K : ectx)
| InjLCtx (K : ectx)
| InjRCtx (K : ectx)
141
| CaseCtx (K : ectx) (e1 : {bind expr}) (e2 : {bind expr})
Ralf Jung's avatar
Ralf Jung committed
142
| AllocCtx (K : ectx)
Ralf Jung's avatar
Ralf Jung committed
143
144
145
146
147
148
149
| 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
150
151
152
153
154
155

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)
156
157
158
  | Op1Ctx _ _ f K => Op1 f (fill K e)
  | Op2LCtx _ _ _ f K1 e2 => Op2 f (fill K1 e) e2
  | Op2RCtx _ _ _ f v1 K2 => Op2 f (v2e v1) (fill K2 e)
Ralf Jung's avatar
Ralf Jung committed
159
160
161
162
163
164
165
  | 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
166
  | AllocCtx K => Alloc (fill K e)
167
  | LoadCtx K => Load (fill K e)
Ralf Jung's avatar
Ralf Jung committed
168
169
170
171
172
  | 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
173
174
175
176
177
178
179
  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)
180
181
182
  | Op1Ctx _ _ f K => Op1Ctx f (comp_ctx K Ki)
  | Op2LCtx _ _ _ f K1 e2 => Op2LCtx f (comp_ctx K1 Ki) e2
  | Op2RCtx _ _ _ f v1 K2 => Op2RCtx f v1 (comp_ctx K2 Ki)
Ralf Jung's avatar
Ralf Jung committed
183
184
185
186
187
188
189
  | 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
190
  | AllocCtx K => AllocCtx (comp_ctx K Ki)
191
  | LoadCtx K => LoadCtx (comp_ctx K Ki)
Ralf Jung's avatar
Ralf Jung committed
192
193
194
195
196
  | 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
197
198
199
200
201
202
203
204
205
206
207
  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.
208
  revert K2 e; induction K1 => K2 e /=; rewrite ?IHK1 ?IHK2; reflexivity.
Ralf Jung's avatar
Ralf Jung committed
209
210
211
212
213
Qed.

Lemma fill_inj_r K e1 e2 :
  fill K e1 = fill K e2 -> e1 = e2.
Proof.
214
215
  revert e1 e2; induction K => el er /=;
     (move=><-; reflexivity) || (case => /IHK <-; reflexivity).
Ralf Jung's avatar
Ralf Jung committed
216
217
Qed.

Ralf Jung's avatar
Ralf Jung committed
218
Lemma fill_value K e v':
219
  e2v (fill K e) = Some v' -> is_Some (e2v e).
Ralf Jung's avatar
Ralf Jung committed
220
Proof.
221
  revert v'; induction K => v' /=; try discriminate;
Ralf Jung's avatar
Ralf Jung committed
222
223
224
    try destruct (e2v (fill K e)); rewrite ?v2v; eauto.
Qed.

225
226
227
Lemma fill_not_value e K :
  e2v e = None -> e2v (fill K e) = None.
Proof.
228
  intros Hnval.  induction K =>/=; by rewrite ?v2v /= ?IHK /=.
229
Qed.
230

231
232
233
234
235
236
237
238
Lemma fill_not_value2 e K v :
  e2v e = None -> e2v (fill K e) = Some v -> False.
Proof.
  intros Hnval Hval. erewrite fill_not_value in Hval by assumption. discriminate.
Qed.


(** The stepping relation *)
Ralf Jung's avatar
Ralf Jung committed
239
Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
Ralf Jung's avatar
Ralf Jung committed
240
| BetaS e1 e2 v2 σ (Hv2 : e2v e2 = Some v2):
Ralf Jung's avatar
Ralf Jung committed
241
    prim_step (App (Rec e1) e2) σ (e1.[e2.:(Rec e1).:ids]) σ None
242
243
244
245
| Op1S T1 To (f : T1 -> To) t σ:
    prim_step (Op1 f (Lit t)) σ (Lit (f t)) σ None
| Op2S T1 T2 To (f : T1 -> T2 -> To) t1 t2 σ:
    prim_step (Op2 f (Lit t1) (Lit t2)) σ (Lit (f t1 t2)) σ None
246
247
248
249
| 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
250
| CaseLS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
251
    prim_step (Case (InjL e0) e1 e2) σ (e1.[e0/]) σ None
Ralf Jung's avatar
Ralf Jung committed
252
253
254
| CaseRS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
    prim_step (Case (InjR e0) e1 e2) σ (e2.[e0/]) σ None
| ForkS e σ:
255
256
    prim_step (Fork e) σ LitUnit σ (Some e)
| RefS e v σ l (Hv : e2v e = Some v) (Hfresh : σ !! l = None):
Ralf Jung's avatar
Ralf Jung committed
257
    prim_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
Ralf Jung's avatar
Ralf Jung committed
258
259
260
261
262
263
264
265
266
267
268
| 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
.
269
270

Definition reducible e: Prop :=
Ralf Jung's avatar
Ralf Jung committed
271
  exists σ e' σ' ef, prim_step e σ e' σ' ef.
272

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

279
280
281
282
283
284
285
286
Definition stuck (e : expr) : Prop :=
  forall K e',
    e = fill K e' ->
    ~reducible e'.

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

Ralf Jung's avatar
Ralf Jung committed
294
Section step_by_value.
295
296
297
298
(* 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 *)
299
Lemma step_by_value {K K' e e'} :
300
301
302
303
304
  fill K e = fill K' e' ->
  reducible e' ->
  e2v e = None ->
  exists K'', K' = comp_ctx K K''.
Proof.
305
306
307
308
  Ltac bad_fill := intros; exfalso; subst;
                   (eapply values_stuck; eassumption) || (eapply fill_not_value2; first eassumption;
                    try match goal with [ H : fill _ _ = _ |- _ ] => erewrite ->H end;
                    by erewrite ?v2v).
309
  Ltac bad_red   Hfill e' Hred := exfalso; destruct e'; try discriminate Hfill; [];
Ralf Jung's avatar
Ralf Jung committed
310
311
312
313
      case: Hfill; intros; subst; destruct Hred as (σ' & e'' & σ'' & ef & Hstep);
      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
314
        repeat match goal with [ H : e2v _ = _ |- _ ] => erewrite H; clear H; simpl end
Ralf Jung's avatar
Ralf Jung committed
315
      ); eassumption || done).
316
  Ltac good IH := intros; subst; 
Ralf Jung's avatar
Ralf Jung committed
317
318
319
320
    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. 
321
  Time revert K' Hfill; induction K=>K' /= Hfill;
322
    first (now eexists; reflexivity);
323
324
325
326
327
328
    (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;
      (* The remaining cases are "compatible" contexts - that result in the same head symbol of the expression.
329
330
331
332
333
334
335
336
337
338
339
340
341
         Test whether the context als has the same head, and use the appropriate tactic.
         Furthermore, the Op* contexts need special treatment due to the inhomogenuous equalities
         they induce. *)
      by match goal with
      | [ |- exists x, Op1Ctx _ _ = Op1Ctx _ _ ] => move: Hfill; case_depeq2; good IHK
      | [ |- exists x, Op2LCtx _ _ _ = Op2LCtx _ _ _ ] => move: Hfill; case_depeq3; good IHK
      | [ |- exists x, Op2RCtx _ _ _ = Op2RCtx _ _ _ ] => move: Hfill; case_depeq3; good IHK
      | [ |- exists x, ?C _ = ?C _ ] => case: Hfill; good IHK
      | [ |- exists x, ?C _ _ = ?C _ _ ] => case: Hfill; good IHK
      | [ |- exists x, ?C _ _ _ = ?C _ _ _ ] => case: Hfill; good IHK
      | [ |- exists x, Op2LCtx _ _ _ = Op2RCtx _ _ _ ] => move: Hfill; case_depeq3; bad_fill
      | [ |- exists x, Op2RCtx _ _ _ = Op2LCtx _ _ _ ] => move: Hfill; case_depeq3; bad_fill
      | _ => case: Hfill; bad_fill
342
      end).
Ralf Jung's avatar
Ralf Jung committed
343
344
Qed.
End step_by_value.
345

346
347
348
(** Atomic expressions *)
Definition atomic (e: expr) :=
  match e with
Ralf Jung's avatar
Ralf Jung committed
349
  | Alloc e => is_Some (e2v e)
350
  | Load e => is_Some (e2v e)
Ralf Jung's avatar
Ralf Jung committed
351
352
  | 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)
353
354
355
  | _ => False
  end.

356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
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 :
  atomic e1 ->
  prim_step e1 σ1 e2 σ2 ef ->
  is_Some (e2v e2).
Proof.
  destruct e1; simpl; intros Hatomic Hstep; inversion Hstep; try contradiction Hatomic; rewrite ?v2v /=; eexists; reflexivity.
Qed.

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

380
(** Tests, making sure that stuff works. *)
381
Module Tests.
Ralf Jung's avatar
Ralf Jung committed
382
  Definition add := Op2 plus (Lit 21) (Lit 21).
383

Ralf Jung's avatar
Ralf Jung committed
384
  Goal forall σ, prim_step add σ (Lit 42) σ None.
385
386
387
  Proof.
    apply Op2S.
  Qed.
Ralf Jung's avatar
Ralf Jung committed
388
389
390
391
392
393
394
395
396
397
398
399
400
401

  Definition rec := Rec (App (Var 1) (Var 0)). (* fix f x => f x *)
  Definition rec_app := App rec (Lit 0).
  Goal forall σ, prim_step rec_app σ rec_app σ None.
  Proof.
    move=>?. eapply BetaS. (* Honestly, I have no idea why this works. *)
    reflexivity.
  Qed.

  Definition lam := Lam (Op2 plus (Var 0) (Lit 21)).
  Goal forall σ, prim_step (App lam (Lit 21)) σ add σ None.
  Proof.
    move=>?. eapply BetaS. reflexivity.
  Qed.
402
End Tests.
403
404
405
406
407

(** Instantiate the Iris language interface. This closes reduction under evaluation contexts.
    We could potentially make this a generic construction. *)
Section Language.

408
  Definition ectx_step e1 σ1 e2 σ2 (ef: option expr) :=
409
410
    exists K e1' e2', e1 = fill K e1' /\ e2 = fill K e2' /\ prim_step e1' σ1 e2' σ2 ef.

411
  Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ectx_step.
412
413
414
415
  Proof.
    - exact v2v.
    - exact e2e.
    - intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2.
416
417
418
419
420
421
422
      eapply fill_not_value. eapply reducible_not_value. do 4 eexists; eassumption.
    - exact atomic_not_value.
    - intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep).
      subst. move: (Hatomic). rewrite (atomic_fill e1' K). (* RJ: this is kind of annoying. *)
      + rewrite !fill_empty. eauto using atomic_step.
      + assumption.
      + clear Hatomic. eapply reducible_not_value. do 4 eexists; eassumption.
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
  Defined.

  (** We can have bind with arbitrary evaluation contexts **)
  Lemma fill_is_ctx K: is_ctx (fill K).
  Proof.
    split; last split.
    - intros ? [v Hval]. eapply fill_value. eassumption.
    - intros ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
      exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
      split; last split; reflexivity || assumption.
    - intros ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep).
      destruct (step_by_value Heq1) as [K' HeqK].
      + do 4 eexists. eassumption.
      + assumption.
      + 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.
        do 3 eexists. split; last split; eassumption || reflexivity.
440
  Qed.
441

442
End Language.