lang.v 18.2 KB
Newer Older
1
From iris.program_logic Require Export language ectx_language ectxi_language.
2
From iris.algebra Require Export ofe.
Ralf Jung's avatar
Ralf Jung committed
3
4
From stdpp Require Export strings.
From stdpp Require Import gmap.
5
Set Default Proof Using "Type".
6

7
Module heap_lang.
8
9
Open Scope Z_scope.

10
(** Expressions and vals. *)
11
Definition loc := positive. (* Really, any countable type. *)
Ralf Jung's avatar
Ralf Jung committed
12

13
Inductive base_lit : Set :=
14
  | LitInt (n : Z) | LitBool (b : bool) | LitUnit | LitLoc (l : loc).
15
Inductive un_op : Set :=
16
  | NegOp | MinusUnOp.
17
18
19
Inductive bin_op : Set :=
  | PlusOp | MinusOp | LeOp | LtOp | EqOp.

20
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
21
22
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
23
24
25
Definition cons_binder (mx : binder) (X : list string) : list string :=
  match mx with BAnon => X | BNamed x => x :: X end.
Infix ":b:" := cons_binder (at level 60, right associativity).
26
Instance binder_eq_dec_eq : EqDecision binder.
27
28
29
30
31
32
33
34
35
Proof. solve_decision. Defined.

Instance set_unfold_cons_binder x mx X P :
  SetUnfold (x  X) P  SetUnfold (x  mx :b: X) (BNamed x = mx  P).
Proof.
  constructor. rewrite -(set_unfold (x  X) P).
  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
Qed.

36
Inductive expr :=
37
  (* Base lambda calculus *)
38
39
40
  | Var (x : string)
  | Rec (f x : binder) (e : expr)
  | App (e1 e2 : expr)
41
42
  (* Base types and their operations *)
  | Lit (l : base_lit)
43
44
45
  | UnOp (op : un_op) (e : expr)
  | BinOp (op : bin_op) (e1 e2 : expr)
  | If (e0 e1 e2 : expr)
46
  (* Products *)
47
48
49
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
50
  (* Sums *)
51
52
53
  | InjL (e : expr)
  | InjR (e : expr)
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
54
  (* Concurrency *)
55
  | Fork (e : expr)
56
  (* Heap *)
57
58
59
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
60
61
  | CAS (e0 : expr) (e1 : expr) (e2 : expr)
  | FAA (e1 : expr) (e2 : expr).
Ralf Jung's avatar
Ralf Jung committed
62

63
Bind Scope expr_scope with expr.
64
65
66
67
68
69
70
71

Fixpoint is_closed (X : list string) (e : expr) : bool :=
  match e with
  | Var x => bool_decide (x  X)
  | Rec f x e => is_closed (f :b: x :b: X) e
  | Lit _ => true
  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
     is_closed X e
72
  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 | FAA e1 e2 =>
73
74
75
76
77
     is_closed X e1 && is_closed X e2
  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
     is_closed X e0 && is_closed X e1 && is_closed X e2
  end.

Robbert Krebbers's avatar
Robbert Krebbers committed
78
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
79
Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
80
Proof. rewrite /Closed. apply _. Qed.
81
82
Instance closed_dec X e : Decision (Closed X e).
Proof. rewrite /Closed. apply _. Defined.
83

84
Inductive val :=
85
  | RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
86
  | LitV (l : base_lit)
87
88
  | PairV (v1 v2 : val)
  | InjLV (v : val)
89
  | InjRV (v : val).
Ralf Jung's avatar
Ralf Jung committed
90

91
Bind Scope val_scope with val.
92

93
Fixpoint of_val (v : val) : expr :=
Ralf Jung's avatar
Ralf Jung committed
94
  match v with
95
  | RecV f x e => Rec f x e
96
  | LitV l => Lit l
97
98
99
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
Ralf Jung's avatar
Ralf Jung committed
100
  end.
101

102
Fixpoint to_val (e : expr) : option val :=
103
  match e with
104
105
  | Rec f x e =>
     if decide (Closed (f :b: x :b: []) e) then Some (RecV f x e) else None
106
  | Lit l => Some (LitV l)
107
108
109
  | Pair e1 e2 => v1  to_val e1; v2  to_val e2; Some (PairV v1 v2)
  | InjL e => InjLV <$> to_val e
  | InjR e => InjRV <$> to_val e
Ralf Jung's avatar
Ralf Jung committed
110
  | _ => None
111
112
  end.

113
114
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
115

116
117
118
119
120
121
122
123
124
125
126
127
128
129
(** Equality and other typeclass stuff *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof.
  by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
Qed.

Lemma of_to_val e v : to_val e = Some v  of_val v = e.
Proof.
  revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
Qed.

Instance of_val_inj : Inj (=) (=) of_val.
Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.

130
Instance base_lit_eq_dec : EqDecision base_lit.
131
Proof. solve_decision. Defined.
132
Instance un_op_eq_dec : EqDecision un_op.
133
Proof. solve_decision. Defined.
134
Instance bin_op_eq_dec : EqDecision bin_op.
135
Proof. solve_decision. Defined.
136
Instance expr_eq_dec : EqDecision expr.
137
Proof. solve_decision. Defined.
138
Instance val_eq_dec : EqDecision val.
139
Proof.
140
 refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
141
142
Defined.

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
Instance base_lit_countable : Countable base_lit.
Proof.
 refine (inj_countable' (λ l, match l with
  | LitInt n => inl (inl n) | LitBool b => inl (inr b)
  | LitUnit => inr (inl ()) | LitLoc l => inr (inr l)
  end) (λ l, match l with
  | inl (inl n) => LitInt n | inl (inr b) => LitBool b
  | inr (inl ()) => LitUnit | inr (inr l) => LitLoc l
  end) _); by intros [].
Qed.
Instance un_op_finite : Countable un_op.
Proof.
 refine (inj_countable' (λ op, match op with NegOp => 0 | MinusUnOp => 1 end)
  (λ n, match n with 0 => NegOp | _ => MinusUnOp end) _); by intros [].
Qed.
Instance bin_op_countable : Countable bin_op.
Proof.
 refine (inj_countable' (λ op, match op with
  | PlusOp => 0 | MinusOp => 1 | LeOp => 2 | LtOp => 3 | EqOp => 4
  end) (λ n, match n with
  | 0 => PlusOp | 1 => MinusOp | 2 => LeOp | 3 => LtOp | _ => EqOp
  end) _); by intros [].
Qed.
Instance binder_countable : Countable binder.
Proof.
 refine (inj_countable' (λ b, match b with BNamed s => Some s | BAnon => None end)
  (λ b, match b with Some s => BNamed s | None => BAnon end) _); by intros [].
Qed.
Instance expr_countable : Countable expr.
Proof.
 set (enc := fix go e :=
  match e with
  | Var x => GenLeaf (inl (inl x))
  | Rec f x e => GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); go e]
  | App e1 e2 => GenNode 1 [go e1; go e2]
  | Lit l => GenLeaf (inr (inl l))
  | UnOp op e => GenNode 2 [GenLeaf (inr (inr (inl op))); go e]
  | BinOp op e1 e2 => GenNode 3 [GenLeaf (inr (inr (inr op))); go e1; go e2]
  | If e0 e1 e2 => GenNode 4 [go e0; go e1; go e2]
  | Pair e1 e2 => GenNode 5 [go e1; go e2]
  | Fst e => GenNode 6 [go e]
  | Snd e => GenNode 7 [go e]
  | InjL e => GenNode 8 [go e]
  | InjR e => GenNode 9 [go e]
  | Case e0 e1 e2 => GenNode 10 [go e0; go e1; go e2]
  | Fork e => GenNode 11 [go e]
  | Alloc e => GenNode 12 [go e]
  | Load e => GenNode 13 [go e]
  | Store e1 e2 => GenNode 14 [go e1; go e2]
  | CAS e0 e1 e2 => GenNode 15 [go e0; go e1; go e2]
193
  | FAA e1 e2 => GenNode 16 [go e1; go e2]
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
  end).
 set (dec := fix go e :=
  match e with
  | GenLeaf (inl (inl x)) => Var x
  | GenNode 0 [GenLeaf (inl (inr f)); GenLeaf (inl (inr x)); e] => Rec f x (go e)
  | GenNode 1 [e1; e2] => App (go e1) (go e2)
  | GenLeaf (inr (inl l)) => Lit l
  | GenNode 2 [GenLeaf (inr (inr (inl op))); e] => UnOp op (go e)
  | GenNode 3 [GenLeaf (inr (inr (inr op))); e1; e2] => BinOp op (go e1) (go e2)
  | GenNode 4 [e0; e1; e2] => If (go e0) (go e1) (go e2)
  | GenNode 5 [e1; e2] => Pair (go e1) (go e2)
  | GenNode 6 [e] => Fst (go e)
  | GenNode 7 [e] => Snd (go e)
  | GenNode 8 [e] => InjL (go e)
  | GenNode 9 [e] => InjR (go e)
  | GenNode 10 [e0; e1; e2] => Case (go e0) (go e1) (go e2)
  | GenNode 11 [e] => Fork (go e)
  | GenNode 12 [e] => Alloc (go e)
  | GenNode 13 [e] => Load (go e)
  | GenNode 14 [e1; e2] => Store (go e1) (go e2)
  | GenNode 15 [e0; e1; e2] => CAS (go e0) (go e1) (go e2)
215
  | GenNode 16 [e1; e2] => FAA (go e1) (go e2)
216
217
218
219
220
221
222
  | _ => Lit LitUnit (* dummy *)
  end).
 refine (inj_countable' enc dec _). intros e. induction e; f_equal/=; auto.
Qed.
Instance val_countable : Countable val.
Proof. refine (inj_countable of_val to_val _); auto using to_of_val. Qed.

223
224
225
226
227
228
229
Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).

Canonical Structure stateC := leibnizC state.
Canonical Structure valC := leibnizC val.
Canonical Structure exprC := leibnizC expr.

230
(** Evaluation contexts *)
231
Inductive ectx_item :=
232
  | AppLCtx (e2 : expr)
233
  | AppRCtx (v1 : val)
234
  | UnOpCtx (op : un_op)
235
  | BinOpLCtx (op : bin_op) (e2 : expr)
236
  | BinOpRCtx (op : bin_op) (v1 : val)
237
238
  | IfCtx (e1 e2 : expr)
  | PairLCtx (e2 : expr)
239
240
241
242
243
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
244
  | CaseCtx (e1 : expr) (e2 : expr)
245
246
  | AllocCtx
  | LoadCtx
247
  | StoreLCtx (e2 : expr)
248
  | StoreRCtx (v1 : val)
249
  | CasLCtx (e1 : expr) (e2 : expr)
250
  | CasMCtx (v0 : val) (e2 : expr)
251
252
253
  | CasRCtx (v0 : val) (v1 : val)
  | FaaLCtx (e2 : expr)
  | FaaRCtx (v1 : val).
254

255
Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
256
257
258
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
259
260
261
262
  | UnOpCtx op => UnOp op e
  | BinOpLCtx op e2 => BinOp op e e2
  | BinOpRCtx op v1 => BinOp op (of_val v1) e
  | IfCtx e1 e2 => If e e1 e2
263
264
265
266
267
268
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
269
  | CaseCtx e1 e2 => Case e e1 e2
270
271
  | AllocCtx => Alloc e
  | LoadCtx => Load e
272
  | StoreLCtx e2 => Store e e2 
273
  | StoreRCtx v1 => Store (of_val v1) e
274
275
276
  | CasLCtx e1 e2 => CAS e e1 e2
  | CasMCtx v0 e2 => CAS (of_val v0) e e2
  | CasRCtx v0 v1 => CAS (of_val v0) (of_val v1) e
277
278
  | FaaLCtx e2 => FAA e e2
  | FaaRCtx v1 => FAA (of_val v1) e
Ralf Jung's avatar
Ralf Jung committed
279
280
  end.

281
(** Substitution *)
282
283
284
Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
  match e with
  | Var y => if decide (x = y) then es else Var y
285
  | Rec f y e =>
286
287
     Rec f y $ if decide (BNamed x  f  BNamed x  y) then subst x es e else e
  | App e1 e2 => App (subst x es e1) (subst x es e2)
288
  | Lit l => Lit l
289
290
291
292
293
294
295
296
297
298
299
300
301
302
  | UnOp op e => UnOp op (subst x es e)
  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
  | Fst e => Fst (subst x es e)
  | Snd e => Snd (subst x es e)
  | InjL e => InjL (subst x es e)
  | InjR e => InjR (subst x es e)
  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
  | Fork e => Fork (subst x es e)
  | Alloc e => Alloc (subst x es e)
  | Load e => Load (subst x es e)
  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
303
  | FAA e1 e2 => FAA (subst x es e1) (subst x es e2)
304
  end.
305

306
Definition subst' (mx : binder) (es : expr) : expr  expr :=
307
  match mx with BNamed x => subst x es | BAnon => id end.
308

309
(** The stepping relation *)
310
311
312
313
Definition un_op_eval (op : un_op) (v : val) : option val :=
  match op, v with
  | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
  | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
314
315
316
  | _, _ => None
  end.

317
318
319
320
321
322
323
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
  match op, v1, v2 with
  | PlusOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitInt (n1 + n2)
  | MinusOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitInt (n1 - n2)
  | LeOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitBool $ bool_decide (n1  n2)
  | LtOp, LitV (LitInt n1), LitV (LitInt n2) => Some $ LitV $ LitBool $ bool_decide (n1 < n2)
  | EqOp, v1, v2 => Some $ LitV $ LitBool $ bool_decide (v1 = v2)
324
325
326
  | _, _, _ => None
  end.

327
Inductive head_step : expr  state  expr  state  list (expr)  Prop :=
328
  | BetaS f x e1 e2 v2 e' σ :
329
     to_val e2 = Some v2 
330
     Closed (f :b: x :b: []) e1 
331
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
332
     head_step (App (Rec f x e1) e2) σ e' σ []
333
334
335
336
337
338
339
340
  | UnOpS op e v v' σ :
     to_val e = Some v 
     un_op_eval op v = Some v'  
     head_step (UnOp op e) σ (of_val v') σ []
  | BinOpS op e1 e2 v1 v2 v' σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     bin_op_eval op v1 v2 = Some v'  
     head_step (BinOp op e1 e2) σ (of_val v') σ []
341
  | IfTrueS e1 e2 σ :
342
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ []
343
  | IfFalseS e1 e2 σ :
344
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ []
345
346
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
347
     head_step (Fst (Pair e1 e2)) σ e1 σ []
348
349
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
350
     head_step (Snd (Pair e1 e2)) σ e2 σ []
351
  | CaseLS e0 v0 e1 e2 σ :
352
     to_val e0 = Some v0 
353
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ []
354
  | CaseRS e0 v0 e1 e2 σ :
355
     to_val e0 = Some v0 
356
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ []
357
  | ForkS e σ:
358
     head_step (Fork e) σ (Lit LitUnit) σ [e]
359
360
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
361
     head_step (Alloc e) σ (Lit $ LitLoc l) (<[l:=v]>σ) []
362
363
  | LoadS l v σ :
     σ !! l = Some v 
364
     head_step (Load (Lit $ LitLoc l)) σ (of_val v) σ []
365
366
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
367
     head_step (Store (Lit $ LitLoc l) e) σ (Lit LitUnit) (<[l:=v]>σ) []
368
369
370
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
371
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool false) σ []
372
373
374
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
375
376
377
378
379
380
     head_step (CAS (Lit $ LitLoc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) []
   | FaaS l i1 e2 i2 σ :
     to_val e2 = Some (LitV (LitInt i2)) 
     σ !! l = Some (LitV (LitInt i1)) 
     head_step (FAA (Lit $ LitLoc l) e2) σ (Lit $ LitInt i1) (<[l:=LitV (LitInt (i1 + i2))]>σ) [].

Ralf Jung's avatar
Ralf Jung committed
381

382
(** Basic properties about the language *)
383
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
384
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
385

386
387
388
Lemma fill_item_val Ki e :
  is_Some (to_val (fill_item Ki e))  is_Some (to_val e).
Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.
389

390
Lemma val_head_stuck e1 σ1 e2 σ2 efs : head_step e1 σ1 e2 σ2 efs  to_val e1 = None.
391
Proof. destruct 1; naive_solver. Qed.
392

393
394
Lemma head_ctx_step_val Ki e σ1 e2 σ2 efs :
  head_step (fill_item Ki e) σ1 e2 σ2 efs  is_Some (to_val e).
395
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
396

397
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
398
  to_val e1 = None  to_val e2 = None 
399
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
400
Proof.
401
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
402
    repeat match goal with
403
404
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
405
Qed.
406

407
Lemma alloc_fresh e v σ :
408
  let l := fresh (dom (gset loc) σ) in
409
  to_val e = Some v  head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) [].
Robbert Krebbers's avatar
Robbert Krebbers committed
410
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
411

412
413
414
415
416
(* Misc *)
Lemma to_val_rec f x e `{!Closed (f :b: x :b: []) e} :
  to_val (Rec f x e) = Some (RecV f x e).
Proof. rewrite /to_val. case_decide=> //. do 2 f_equal; apply proof_irrel. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
417
(** Closed expressions *)
418
Lemma is_closed_weaken X Y e : is_closed X e  X  Y  is_closed Y e.
Robbert Krebbers's avatar
Robbert Krebbers committed
419
420
Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.

421
Lemma is_closed_weaken_nil X e : is_closed [] e  is_closed X e.
422
Proof. intros. by apply is_closed_weaken with [], list_subseteq_nil. Qed.
423

424
425
426
Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.

427
Lemma is_closed_to_val X e v : to_val e = Some v  is_closed X e.
Robbert Krebbers's avatar
Robbert Krebbers committed
428
Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
429

430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
Lemma is_closed_subst X e x es :
  is_closed [] es  is_closed (x :: X) e  is_closed X (subst x es e).
Proof.
  intros ?. revert X.
  induction e=> X /= ?; destruct_and?; split_and?; simplify_option_eq;
    try match goal with
    | H : ¬(_  _) |- _ => apply not_and_l in H as [?%dec_stable|?%dec_stable]
    end; eauto using is_closed_weaken with set_solver.
Qed.
Lemma is_closed_do_subst' X e x es :
  is_closed [] es  is_closed (x :b: X) e  is_closed X (subst' x es e).
Proof. destruct x; eauto using is_closed_subst. Qed.

(* Substitution *)
Lemma subst_is_closed X e x es : is_closed X e  x  X  subst x es e = e.
Robbert Krebbers's avatar
Robbert Krebbers committed
445
Proof.
446
  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
Robbert Krebbers's avatar
Robbert Krebbers committed
447
448
    repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
Qed.
449

450
451
Lemma subst_is_closed_nil e x es : is_closed [] e  subst x es e = e.
Proof. intros. apply subst_is_closed with []; set_solver. Qed.
452

453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
Lemma subst_subst e x es es' :
  Closed [] es'  subst x es (subst x es' e) = subst x es' e.
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst' e x es es' :
  Closed [] es'  subst' x es (subst' x es' e) = subst' x es' e.
Proof. destruct x; simpl; auto using subst_subst. Qed.

Lemma subst_subst_ne e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst x es (subst y es' e) = subst y es' (subst x es e).
Proof.
  intros. induction e; simpl; try (f_equal; by auto);
    simplify_option_eq; auto using eq_sym, subst_is_closed_nil with f_equal.
Qed.
Lemma subst_subst_ne' e x y es es' :
  Closed [] es  Closed [] es'  x  y 
  subst' x es (subst' y es' e) = subst' y es' (subst' x es e).
Proof. destruct x, y; simpl; auto using subst_subst_ne with congruence. Qed.

Lemma subst_rec' f y e x es :
  x = f  x = y  x = BAnon 
  subst' x es (Rec f y e) = Rec f y e.
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
Lemma subst_rec_ne' f y e x es :
  (x  f  f = BAnon)  (x  y  y = BAnon) 
  subst' x es (Rec f y e) = Rec f y (subst' x es e).
Proof. intros. destruct x; simplify_option_eq; naive_solver. Qed.
483
484
485
486
487
488

Lemma heap_lang_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
Proof.
  split; apply _ || eauto using to_of_val, of_to_val, val_head_stuck,
    fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
Qed.
489
490
491
End heap_lang.

(** Language *)
492
493
494
Canonical Structure heap_ectxi_lang := EctxiLanguage heap_lang.heap_lang_mixin.
Canonical Structure heap_ectx_lang := EctxLanguageOfEctxi heap_ectxi_lang.
Canonical Structure heap_lang := LanguageOfEctx heap_ectx_lang.
495

496
(* Prefer heap_lang names over ectx_language names. *)
497
Export heap_lang.
498
499
500
501
502
503
504
505
506
507

(** Define some derived forms *)
Notation Lam x e := (Rec BAnon x e).
Notation Let x e1 e2 := (App (Lam x e2) e1).
Notation Seq e1 e2 := (Let BAnon e1 e2).
Notation LamV x e := (RecV BAnon x e).
Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
Notation SeqCtx e2 := (LetCtx BAnon e2).
Notation Skip := (Seq (Lit LitUnit) (Lit LitUnit)).
Notation Match e0 x1 e1 x2 e2 := (Case e0 (Lam x1 e1) (Lam x2 e2)).