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

5
6
Set Bullet Behavior "Strict Subproofs".

7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
(** 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
26
27
Definition loc := nat. (* Any countable type. *)

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

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
60
Definition Lam (e: {bind expr}) := Rec (e.[up ids]).
Ralf Jung's avatar
Ralf Jung committed
61
Definition LitUnit := Lit tt.
Ralf Jung's avatar
Ralf Jung committed
62
63
Definition LitTrue := Lit true.
Definition LitFalse := Lit false.
Ralf Jung's avatar
Ralf Jung committed
64

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

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

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

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

Ralf Jung's avatar
Ralf Jung committed
103
Section e2e. (* To get local tactics. *)
104
Lemma e2e e v:
105
  e2v e = Some v -> v2e v = e.
106
Proof.
Ralf Jung's avatar
Ralf Jung committed
107
108
109
110
111
112
113
114
115
116
117
118
119
120
  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.
121
  revert v2; induction v1=>v2; destruct v2; simpl; try discriminate;
Ralf Jung's avatar
Ralf Jung committed
122
    first [case_depeq1 | case]; eauto using f_equal, f_equal2.
123
Qed.
124

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

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

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

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

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

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

232
233
234
235
236
237
238
239
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
240
Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
Ralf Jung's avatar
Ralf Jung committed
241
| BetaS e1 e2 v2 σ (Hv2 : e2v e2 = Some v2):
Ralf Jung's avatar
Ralf Jung committed
242
    prim_step (App (Rec e1) e2) σ (e1.[e2.:(Rec e1).:ids]) σ None
243
244
245
246
| 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
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
254
255
| CaseRS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
    prim_step (Case (InjR e0) e1 e2) σ (e2.[e0/]) σ None
| ForkS e σ:
256
257
    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
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

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

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

280
281
282
283
284
285
286
287
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
288
289
290
  intros ?? Heq.
  edestruct (fill_value K) as [v' Hv'].
  { by rewrite <-Heq, v2v. }
291
292
  clear -Hv' => Hred. apply reducible_not_value in Hred.
  destruct (e2v e'); discriminate.
Ralf Jung's avatar
Ralf Jung committed
293
Qed.
294

Ralf Jung's avatar
Ralf Jung committed
295
Section step_by_value.
296
297
298
299
(* 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 *)
300
Lemma step_by_value {K K' e e'} :
301
302
303
304
305
  fill K e = fill K' e' ->
  reducible e' ->
  e2v e = None ->
  exists K'', K' = comp_ctx K K''.
Proof.
306
307
308
309
  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).
310
  Ltac bad_red   Hfill e' Hred := exfalso; destruct e'; try discriminate Hfill; [];
Ralf Jung's avatar
Ralf Jung committed
311
312
313
314
      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
315
        repeat match goal with [ H : e2v _ = _ |- _ ] => erewrite H; clear H; simpl end
Ralf Jung's avatar
Ralf Jung committed
316
      ); eassumption || done).
317
  Ltac good IH := intros; subst; 
Ralf Jung's avatar
Ralf Jung committed
318
319
320
321
    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. 
322
  Time revert K' Hfill; induction K=>K' /= Hfill;
323
    first (now eexists; reflexivity);
324
325
326
327
328
329
    (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.
330
331
332
333
334
335
336
337
338
339
340
341
342
         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
343
      end).
Ralf Jung's avatar
Ralf Jung committed
344
345
Qed.
End step_by_value.
346

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

357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
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
377
378
  destruct K; simpl; first reflexivity; unfold is_Some; intros Hatomic Hnval; exfalso; try assumption;
    try (destruct_conjs; eapply fill_not_value2; eassumption).
379
380
Qed.

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

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

  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.
403
End Tests.
404
405
406
407
408

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

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

412
  Instance heap_lang : Language expr value state := Build_Language v2e e2v atomic ectx_step.
413
414
415
416
  Proof.
    - exact v2v.
    - exact e2e.
    - intros e1 σ1 e2 σ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2.
417
418
419
420
421
422
423
      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.
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
  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.
441
  Qed.
442

443
End Language.