lang.v 22.8 KB
Newer Older
1
2
3
From iris.program_logic Require Export language.
From iris.prelude Require Export strings.
From iris.prelude Require Import gmap.
4

5
Module heap_lang.
6
7
Open Scope Z_scope.

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

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

18
Inductive binder := BAnon | BNamed : string  binder.
Ralf Jung's avatar
Ralf Jung committed
19
20
Delimit Scope binder_scope with bind.
Bind Scope binder_scope with binder.
21

22
23
24
25
26
27
28
29
30
31
32
33
34
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).
Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
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.

Ralf Jung's avatar
Ralf Jung committed
35
36
37
38
39
40
(** A typeclass for whether a variable is bound in a given
   context. Making this a typeclass means we can use tpeclass search
   to program solving these constraints, so this becomes extensible.
   Also, since typeclass search runs *after* unification, Coq has already
   inferred the X for us; if we were to go for embedded proof terms ot
   tactics, Coq would do things in the wrong order. *)
41
42
Class VarBound (x : string) (X : list string) :=
  var_bound : bool_decide (x  X).
43
44
(* There is no need to restrict this hint to terms without evars, [vm_compute]
will fail in case evars are arround. *)
45
46
47
48
49
50
51
52
53
Hint Extern 0 (VarBound _ _) => vm_compute; exact I : typeclass_instances. 

Instance var_bound_proof_irrel x X : ProofIrrel (VarBound x X).
Proof. rewrite /VarBound. apply _. Qed.
Instance set_unfold_var_bound x X P :
  SetUnfold (x  X) P  SetUnfold (VarBound x X) P.
Proof.
  constructor. by rewrite /VarBound bool_decide_spec (set_unfold (x  X) P).
Qed.
54

55
Inductive expr (X : list string) :=
56
  (* Base lambda calculus *)
Ralf Jung's avatar
Ralf Jung committed
57
58
59
60
61
62
63
      (* Var is the only place where the terms contain a proof. The fact that they
       contain a proof at all is suboptimal, since this means two seeminlgy
       convertible terms could differ in their proofs. However, this also has
       some advantages:
       * We can make the [X] an index, so we can do non-dependent match.
       * In expr_weaken, we can push the proof all the way into Var, making
         sure that proofs never block computation. *)
64
65
66
  | Var (x : string) `{VarBound x X}
  | Rec (f x : binder) (e : expr (f :b: x :b: X))
  | App (e1 e2 : expr X)
67
68
  (* Base types and their operations *)
  | Lit (l : base_lit)
69
70
71
  | UnOp (op : un_op) (e : expr X)
  | BinOp (op : bin_op) (e1 e2 : expr X)
  | If (e0 e1 e2 : expr X)
72
  (* Products *)
73
74
75
  | Pair (e1 e2 : expr X)
  | Fst (e : expr X)
  | Snd (e : expr X)
76
  (* Sums *)
77
78
79
  | InjL (e : expr X)
  | InjR (e : expr X)
  | Case (e0 : expr X) (e1 : expr X) (e2 : expr X)
80
  (* Concurrency *)
81
  | Fork (e : expr X)
82
83
  (* Heap *)
  | Loc (l : loc)
84
85
86
  | Alloc (e : expr X)
  | Load (e : expr X)
  | Store (e1 : expr X) (e2 : expr X)
87
  | CAS (e0 : expr X) (e1 : expr X) (e2 : expr X).
Ralf Jung's avatar
Ralf Jung committed
88

89
90
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with E.
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
Arguments Var {_} _ {_}.
Arguments Rec {_} _ _ _%E.
Arguments App {_} _%E _%E.
Arguments Lit {_} _.
Arguments UnOp {_} _ _%E.
Arguments BinOp {_} _ _%E _%E.
Arguments If {_} _%E _%E _%E.
Arguments Pair {_} _%E _%E.
Arguments Fst {_} _%E.
Arguments Snd {_} _%E.
Arguments InjL {_} _%E.
Arguments InjR {_} _%E.
Arguments Case {_} _%E _%E _%E.
Arguments Fork {_} _%E.
Arguments Loc {_} _.
Arguments Alloc {_} _%E.
Arguments Load {_} _%E.
Arguments Store {_} _%E _%E.
109
Arguments CAS {_} _%E _%E _%E.
110

111
Inductive val :=
112
  | RecV (f x : binder) (e : expr (f :b: x :b: []))
113
  | LitV (l : base_lit)
114
115
116
117
  | PairV (v1 v2 : val)
  | InjLV (v : val)
  | InjRV (v : val)
  | LocV (l : loc).
Ralf Jung's avatar
Ralf Jung committed
118

119
120
Bind Scope val_scope with val.
Delimit Scope val_scope with V.
121
122
123
Arguments PairV _%V _%V.
Arguments InjLV _%V.
Arguments InjRV _%V.
124

125
Definition signal : val := RecV BAnon (BNamed "x") (Store (Var "x") (Lit (LitInt 1))).
126

127
Fixpoint of_val (v : val) : expr [] :=
Ralf Jung's avatar
Ralf Jung committed
128
  match v with
129
  | RecV f x e => Rec f x e
130
  | LitV l => Lit l
131
132
133
  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
  | InjLV v => InjL (of_val v)
  | InjRV v => InjR (of_val v)
134
  | LocV l => Loc l
Ralf Jung's avatar
Ralf Jung committed
135
  end.
136
137

Fixpoint to_val (e : expr []) : option val :=
138
  match e with
139
  | Rec f x e => Some (RecV f x e)
140
  | Lit l => Some (LitV l)
141
142
143
  | 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
144
  | Loc l => Some (LocV l)
Ralf Jung's avatar
Ralf Jung committed
145
  | _ => None
146
147
  end.

148
149
(** The state: heaps of vals. *)
Definition state := gmap loc val.
Ralf Jung's avatar
Ralf Jung committed
150

151
(** Evaluation contexts *)
152
Inductive ectx_item :=
153
  | AppLCtx (e2 : expr [])
154
  | AppRCtx (v1 : val)
155
  | UnOpCtx (op : un_op)
156
  | BinOpLCtx (op : bin_op) (e2 : expr [])
157
  | BinOpRCtx (op : bin_op) (v1 : val)
158
159
  | IfCtx (e1 e2 : expr [])
  | PairLCtx (e2 : expr [])
160
161
162
163
164
  | PairRCtx (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
165
  | CaseCtx (e1 : expr []) (e2 : expr [])
166
167
  | AllocCtx
  | LoadCtx
168
  | StoreLCtx (e2 : expr [])
169
  | StoreRCtx (v1 : val)
170
171
  | CasLCtx (e1 : expr [])  (e2 : expr [])
  | CasMCtx (v0 : val) (e2 : expr [])
172
  | CasRCtx (v0 : val) (v1 : val).
173

174
Notation ectx := (list ectx_item).
175

176
Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
177
178
179
  match Ki with
  | AppLCtx e2 => App e e2
  | AppRCtx v1 => App (of_val v1) e
180
181
182
183
  | 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
184
185
186
187
188
189
  | PairLCtx e2 => Pair e e2
  | PairRCtx v1 => Pair (of_val v1) e
  | FstCtx => Fst e
  | SndCtx => Snd e
  | InjLCtx => InjL e
  | InjRCtx => InjR e
190
  | CaseCtx e1 e2 => Case e e1 e2
191
192
193
194
  | AllocCtx => Alloc e
  | LoadCtx => Load e
  | StoreLCtx e2 => Store e e2
  | StoreRCtx v1 => Store (of_val v1) e
195
196
197
  | 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
Ralf Jung's avatar
Ralf Jung committed
198
  end.
199
Definition fill (K : ectx) (e : expr []) : expr [] := fold_right fill_item e K.
Ralf Jung's avatar
Ralf Jung committed
200

201
(** Substitution *)
202
(** We have [subst' e BAnon v = e] to deal with anonymous binders *)
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
Lemma wexpr_rec_prf {X Y} (H : X `included` Y) {f x} :
  f :b: x :b: X `included` f :b: x :b: Y.
Proof. set_solver. Qed.

Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
  match e return expr Y with
  | Var x _ => @Var _ x _
  | Rec f x e => Rec f x (wexpr (wexpr_rec_prf H) e)
  | App e1 e2 => App (wexpr H e1) (wexpr H e2)
  | Lit l => Lit l
  | UnOp op e => UnOp op (wexpr H e)
  | BinOp op e1 e2 => BinOp op (wexpr H e1) (wexpr H e2)
  | If e0 e1 e2 => If (wexpr H e0) (wexpr H e1) (wexpr H e2)
  | Pair e1 e2 => Pair (wexpr H e1) (wexpr H e2)
  | Fst e => Fst (wexpr H e)
  | Snd e => Snd (wexpr H e)
  | InjL e => InjL (wexpr H e)
  | InjR e => InjR (wexpr H e)
  | Case e0 e1 e2 => Case (wexpr H e0) (wexpr H e1) (wexpr H e2)
  | Fork e => Fork (wexpr H e)
  | Loc l => Loc l
  | Alloc e => Alloc (wexpr H e)
  | Load  e => Load (wexpr H e)
  | Store e1 e2 => Store (wexpr H e1) (wexpr H e2)
227
  | CAS e0 e1 e2 => CAS (wexpr H e0) (wexpr H e1) (wexpr H e2)
228
229
230
  end.
Solve Obligations with set_solver.

231
232
233
234
Program Definition wexpr' {X} (e : expr []) : expr X :=
  wexpr _ e.
Solve Obligations with set_solver.

235
236
237
238
239
240
241
242
243
244
245
246
247
248
Definition of_val' {X} (v : val) : expr X := wexpr (included_nil _) (of_val v).

Lemma wsubst_rec_true_prf {X Y x} (H : X `included` x :: Y) {f y}
    (Hfy :BNamed x  f  BNamed x  y) :
  f :b: y :b: X `included` x :: f :b: y :b: Y.
Proof. set_solver. Qed.
Lemma wsubst_rec_false_prf {X Y x} (H : X `included` x :: Y) {f y}
    (Hfy : ¬(BNamed x  f  BNamed x  y)) :
  f :b: y :b: X `included` f :b: y :b: Y.
Proof. move: Hfy=>/not_and_l [/dec_stable|/dec_stable]; set_solver. Qed.

Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
    (H : X `included` x :: Y) (e : expr X)  : expr Y :=
  match e return expr Y with
249
  | Var y _ => if decide (x = y) then wexpr' es else @Var _ y _
250
  | Rec f y e =>
251
252
253
254
255
     Rec f y $ match decide (BNamed x  f  BNamed x  y) return _ with
               | left Hfy => wsubst x es (wsubst_rec_true_prf H Hfy) e
               | right Hfy => wexpr (wsubst_rec_false_prf H Hfy) e
               end
  | App e1 e2 => App (wsubst x es H e1) (wsubst x es H e2)
256
  | Lit l => Lit l
257
258
259
260
261
262
263
264
  | UnOp op e => UnOp op (wsubst x es H e)
  | BinOp op e1 e2 => BinOp op (wsubst x es H e1) (wsubst x es H e2)
  | If e0 e1 e2 => If (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
  | Pair e1 e2 => Pair (wsubst x es H e1) (wsubst x es H e2)
  | Fst e => Fst (wsubst x es H e)
  | Snd e => Snd (wsubst x es H e)
  | InjL e => InjL (wsubst x es H e)
  | InjR e => InjR (wsubst x es H e)
265
  | Case e0 e1 e2 =>
266
267
     Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
  | Fork e => Fork (wsubst x es H e)
268
  | Loc l => Loc l
269
270
271
  | Alloc e => Alloc (wsubst x es H e)
  | Load e => Load (wsubst x es H e)
  | Store e1 e2 => Store (wsubst x es H e1) (wsubst x es H e2)
272
  | CAS e0 e1 e2 => CAS (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
273
  end.
274
275
276
277
278
279
Solve Obligations with set_solver.

Definition subst {X} (x : string) (es : expr []) (e : expr (x :: X)) : expr X :=
  wsubst x es (λ z, id) e.
Definition subst' {X} (mx : binder) (es : expr []) : expr (mx :b: X)  expr X :=
  match mx with BNamed x => subst x es | BAnon => id end.
280

281
(** The stepping relation *)
282
283
Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
  match op, l with
284
  | NegOp, LitBool b => Some (LitBool (negb b))
285
  | MinusUnOp, LitInt n => Some (LitInt (- n))
286
287
288
289
290
  | _, _ => None
  end.

Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
  match op, l1, l2 with
291
292
293
294
295
  | PlusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 + n2)
  | MinusOp, LitInt n1, LitInt n2 => Some $ LitInt (n1 - n2)
  | LeOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1  n2)
  | LtOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 < n2)
  | EqOp, LitInt n1, LitInt n2 => Some $ LitBool $ bool_decide (n1 = n2)
296
297
298
  | _, _, _ => None
  end.

299
300
Inductive head_step : expr []  state  expr []  state  option (expr [])  Prop :=
  | BetaS f x e1 e2 v2 e' σ :
301
     to_val e2 = Some v2 
302
303
     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) 
     head_step (App (Rec f x e1) e2) σ e' σ None
304
  | UnOpS op l l' σ :
305
306
     un_op_eval op l = Some l'  
     head_step (UnOp op (Lit l)) σ (Lit l') σ None
307
  | BinOpS op l1 l2 l' σ :
308
309
310
     bin_op_eval op l1 l2 = Some l'  
     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
  | IfTrueS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
311
     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
312
  | IfFalseS e1 e2 σ :
Ralf Jung's avatar
Ralf Jung committed
313
     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
314
315
316
317
318
319
  | FstS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Fst (Pair e1 e2)) σ e1 σ None
  | SndS e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     head_step (Snd (Pair e1 e2)) σ e2 σ None
320
  | CaseLS e0 v0 e1 e2 σ :
321
     to_val e0 = Some v0 
322
323
     head_step (Case (InjL e0) e1 e2) σ (App e1 e0) σ None
  | CaseRS e0 v0 e1 e2 σ :
324
     to_val e0 = Some v0 
325
     head_step (Case (InjR e0) e1 e2) σ (App e2 e0) σ None
326
  | ForkS e σ:
327
     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
328
329
330
331
332
333
334
335
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
     head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None
  | LoadS l v σ :
     σ !! l = Some v 
     head_step (Load (Loc l)) σ (of_val v) σ None
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
336
     head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
337
338
339
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
340
     head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
341
342
343
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
344
     head_step (CAS (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
Ralf Jung's avatar
Ralf Jung committed
345

346
(** Atomic expressions *)
347
Definition atomic (e: expr []) : Prop :=
348
349
350
351
  match e with
  | Alloc e => is_Some (to_val e)
  | Load e => is_Some (to_val e)
  | Store e1 e2 => is_Some (to_val e1)  is_Some (to_val e2)
352
  | CAS e0 e1 e2 => is_Some (to_val e0)  is_Some (to_val e1)  is_Some (to_val e2)
Ralf Jung's avatar
Ralf Jung committed
353
354
  (* Make "skip" atomic *)
  | App (Rec _ _ (Lit _)) (Lit _) => True
355
356
  | _ => False
  end.
357

358
359
(** Close reduction under evaluation contexts.
We could potentially make this a generic construction. *)
360
361
Inductive prim_step (e1 : expr []) (σ1 : state)
    (e2 : expr []) (σ2: state) (ef: option (expr [])) : Prop :=
362
  Ectx_step K e1' e2' :
363
364
365
    e1 = fill K e1'  e2 = fill K e2' 
    head_step e1' σ1 e2' σ2 ef  prim_step e1 σ1 e2 σ2 ef.

366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
(** Substitution *)
Lemma var_proof_irrel X x H1 H2 : @Var X x H1 = @Var X x H2.
Proof. f_equal. by apply (proof_irrel _). Qed.

Lemma wexpr_id X (H : X `included` X) e : wexpr H e = e.
Proof. induction e; f_equal/=; auto. by apply (proof_irrel _). Qed.
Lemma wexpr_proof_irrel X Y (H1 H2 : X `included` Y) e : wexpr H1 e = wexpr H2 e.
Proof.
  revert Y H1 H2; induction e; simpl; auto using var_proof_irrel with f_equal.
Qed.
Lemma wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) H3 e :
  wexpr H2 (wexpr H1 e) = wexpr H3 e.
Proof.
  revert Y Z H1 H2 H3.
  induction e; simpl; auto using var_proof_irrel with f_equal.
Qed.
Lemma wexpr_wexpr' X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e :
  wexpr H2 (wexpr H1 e) = wexpr (transitivity H1 H2) e.
Proof. apply wexpr_wexpr. Qed.

Lemma wsubst_proof_irrel X Y x es (H1 H2 : X `included` x :: Y) e :
  wsubst x es H1 e = wsubst x es H2 e.
Proof.
  revert Y H1 H2; induction e; simpl; intros; repeat case_decide;
    auto using var_proof_irrel, wexpr_proof_irrel with f_equal.
Qed.
Lemma wexpr_wsubst X Y Z x es (H1: X `included` x::Y) (H2: Y `included` Z) H3 e:
  wexpr H2 (wsubst x es H1 e) = wsubst x es H3 e.
Proof.
  revert Y Z H1 H2 H3.
  induction e; intros; repeat (case_decide || simplify_eq/=);
397
    unfold wexpr'; auto using var_proof_irrel, wexpr_wexpr with f_equal.
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
Qed.
Lemma wsubst_wexpr X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) H3 e:
  wsubst x es H2 (wexpr H1 e) = wsubst x es H3 e.
Proof.
  revert Y Z H1 H2 H3.
  induction e; intros; repeat (case_decide || simplify_eq/=);
    auto using var_proof_irrel, wexpr_wexpr with f_equal.
Qed.
Lemma wsubst_wexpr' X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) e:
  wsubst x es H2 (wexpr H1 e) = wsubst x es (transitivity H1 H2) e.
Proof. apply wsubst_wexpr. Qed.

Lemma wsubst_closed X Y x es (H1 : X `included` x :: Y) H2 (e : expr X) :
  x  X  wsubst x es H1 e = wexpr H2 e.
Proof.
  revert Y H1 H2.
  induction e; intros; repeat (case_decide || simplify_eq/=);
    auto using var_proof_irrel, wexpr_proof_irrel with f_equal set_solver.
  exfalso; set_solver.
Qed.
Lemma wsubst_closed_nil x es H (e : expr []) : wsubst x es H e = e.
Proof.
  rewrite -{2}(wexpr_id _ (reflexivity []) e).
  apply wsubst_closed, not_elem_of_nil.
Qed.

Ralf Jung's avatar
Ralf Jung committed
424
425
426
427
Lemma of_val'_closed (v : val) :
  of_val' v = of_val v.
Proof. by rewrite /of_val' wexpr_id. Qed.

Ralf Jung's avatar
Ralf Jung committed
428
429
430
431
432
433
434
435
436
437
438
(** to_val propagation.
    TODO: automatically appliy in wp_tactics? *)
Lemma to_val_InjL e v : to_val e = Some v  to_val (InjL e) = Some (InjLV v).
Proof. move=>H. simpl. by rewrite H. Qed.
Lemma to_val_InjR e v : to_val e = Some v  to_val (InjR e) = Some (InjRV v).
Proof. move=>H. simpl. by rewrite H. Qed.
Lemma to_val_Pair e1 e2 v1 v2 :
  to_val e1 = Some v1  to_val e2 = Some v2 
  to_val (Pair e1 e2) = Some (PairV v1 v2).
Proof. move=>H1 H2. simpl. by rewrite H1 H2. Qed.

439
440
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
441
Proof. by induction v; simplify_option_eq. Qed.
442

443
Lemma of_to_val e v : to_val e = Some v  of_val v = e.
444
Proof.
445
446
447
448
449
450
451
  revert e v. cut ( X (e : expr X) (H : X = ) v,
    to_val (eq_rect _ expr e _ H) = Some v  of_val v = eq_rect _ expr e _ H).
  { intros help e v. apply (help  e eq_refl). }
  intros X e; induction e; intros HX ??; simplify_option_eq;
    repeat match goal with
    | IH :  _ :  = , _ |- _ => specialize (IH eq_refl); simpl in IH
    end; auto with f_equal.
452
Qed.
453

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

457
Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
458
Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
459

460
Instance ectx_fill_inj K : Inj (=) (=) (fill K).
461
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
462

463
464
Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
Proof. revert e; induction K1; simpl; auto with f_equal. Qed.
465

466
Lemma fill_val K e : is_Some (to_val (fill K e))  is_Some (to_val e).
467
Proof.
468
  intros [v' Hv']; revert v' Hv'.
469
  induction K as [|[]]; intros; simplify_option_eq; eauto.
470
Qed.
471

472
473
Lemma fill_not_val K e : to_val e = None  to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
474

475
Lemma val_head_stuck e1 σ1 e2 σ2 ef :
476
477
  head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
478

479
480
Lemma val_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef  to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, val_head_stuck. Qed.
481

482
483
Lemma atomic_not_val e : atomic e  to_val e = None.
Proof. destruct e; naive_solver. Qed.
484

485
486
Lemma atomic_fill_item Ki e : atomic (fill_item Ki e)  is_Some (to_val e).
Proof.
487
  intros. destruct Ki; simplify_eq/=; destruct_and?;
488
489
490
    repeat (case_match || contradiction); eauto.
Qed.

491
Lemma atomic_fill K e : atomic (fill K e)  to_val e = None  K = [].
492
Proof.
493
494
  destruct K as [|Ki K]; [done|].
  rewrite eq_None_not_Some=> /= ? []; eauto using atomic_fill_item, fill_val.
495
Qed.
496

497
498
Lemma atomic_head_step e1 σ1 e2 σ2 ef :
  atomic e1  head_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
Ralf Jung's avatar
Ralf Jung committed
499
Proof.
500
  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
501
  unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
Ralf Jung's avatar
Ralf Jung committed
502
Qed.
503

504
505
Lemma atomic_step e1 σ1 e2 σ2 ef :
  atomic e1  prim_step e1 σ1 e2 σ2 ef  is_Some (to_val e2).
506
Proof.
507
  intros Hatomic [K e1' e2' -> -> Hstep].
508
  assert (K = []) as -> by eauto 10 using atomic_fill, val_head_stuck.
509
  naive_solver eauto using atomic_head_step.
Ralf Jung's avatar
Ralf Jung committed
510
Qed.
511

512
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
513
  head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
514
Proof. destruct Ki; inversion_clear 1; simplify_option_eq; eauto. Qed.
515

516
Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
517
  to_val e1 = None  to_val e2 = None 
518
  fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
519
Proof.
520
  destruct Ki1, Ki2; intros; try discriminate; simplify_eq/=;
521
    repeat match goal with
522
523
    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
    end; auto.
Ralf Jung's avatar
Ralf Jung committed
524
Qed.
525

526
527
528
529
530
531
(* When something does a step, and another decomposition of the same expression
has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
other words, [e] also contains the reducible expression *)
Lemma step_by_val K K' e1 e1' σ1 e2 σ2 ef :
  fill K e1 = fill K' e1'  to_val e1 = None  head_step e1' σ1 e2 σ2 ef 
  K `prefix_of` K'.
532
Proof.
533
534
  intros Hfill Hred Hnval; revert K' Hfill.
  induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil.
535
  destruct K' as [|Ki' K']; simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
536
  { exfalso; apply (eq_None_not_Some (to_val (fill K e1)));
537
538
      eauto using fill_not_val, head_ctx_step_val. }
  cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
539
  eauto using fill_item_no_val_inj, val_head_stuck, fill_not_val.
540
Qed.
541

542
543
544
Lemma alloc_fresh e v σ :
  let l := fresh (dom _ σ) in
  to_val e = Some v  head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
545
Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
546

Ralf Jung's avatar
Ralf Jung committed
547
(** Equality and other typeclass stuff *)
548
549
550
551
552
553
Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
Proof. solve_decision. Defined.
Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
Proof. solve_decision. Defined.
554

555
556
557
558
559
560
561
562
563
564
565
566
Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
  match e, e' with
  | Var x _, Var x' _ => bool_decide (x = x')
  | Rec f x e, Rec f' x' e' =>
     bool_decide (f = f') && bool_decide (x = x') && expr_beq e e'
  | App e1 e2, App e1' e2' | Pair e1 e2, Pair e1' e2' |
    Store e1 e2, Store e1' e2' => expr_beq e1 e1' && expr_beq e2 e2'
  | Lit l, Lit l' => bool_decide (l = l')
  | UnOp op e, UnOp op' e' => bool_decide (op = op') && expr_beq e e'
  | BinOp op e1 e2, BinOp op' e1' e2' =>
     bool_decide (op = op') && expr_beq e1 e1' && expr_beq e2 e2'
  | If e0 e1 e2, If e0' e1' e2' | Case e0 e1 e2, Case e0' e1' e2' |
567
    CAS e0 e1 e2, CAS e0' e1' e2' =>
568
569
570
571
572
     expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
  | Fst e, Fst e' | Snd e, Snd e' | InjL e, InjL e' | InjR e, InjR e' |
    Fork e, Fork e' | Alloc e, Alloc e' | Load e, Load e' => expr_beq e e'
  | Loc l, Loc l' => bool_decide (l = l')
  | _, _ => false
573
  end.
574
Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2  e1 = e2.
575
Proof.
576
577
578
579
  split.
  * revert e2; induction e1; intros [] * ?; simpl in *;
      destruct_and?; subst; repeat f_equal/=; auto; try apply proof_irrel.
  * intros ->. induction e2; naive_solver.
580
Qed.
581
Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
582
Proof.
583
584
585
 refine (cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
Defined.
Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
586
Proof.
587
588
 refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
Defined.
Ralf Jung's avatar
Ralf Jung committed
589
590
591

Instance expr_inhabited X : Inhabited (expr X) := populate (Lit LitUnit).
Instance val_inhabited : Inhabited val := populate (LitV LitUnit).
592
593
594
595
End heap_lang.

(** Language *)
Program Canonical Structure heap_lang : language := {|
596
  expr := heap_lang.expr []; val := heap_lang.val; state := heap_lang.state;
597
598
599
600
  of_val := heap_lang.of_val; to_val := heap_lang.to_val;
  atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
|}.
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
601
  heap_lang.val_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
602

603
Global Instance heap_lang_ctx K : LanguageCtx heap_lang (heap_lang.fill K).
604
Proof.
605
  split.
606
607
  - eauto using heap_lang.fill_not_val.
  - intros ????? [K' e1' e2' Heq1 Heq2 Hstep].
608
    by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
609
  - intros e1 σ1 e2 σ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
610
611
    destruct (heap_lang.step_by_val
      K K'' e1 e1'' σ1 e2'' σ2 ef) as [K' ->]; eauto.
612
    rewrite heap_lang.fill_app in Heq1; apply (inj _) in Heq1.
Ralf Jung's avatar
Ralf Jung committed
613
    exists (heap_lang.fill K' e2''); rewrite heap_lang.fill_app; split; auto.
614
    econstructor; eauto.
615
Qed.
616
617
618

Global Instance heap_lang_ctx_item Ki :
  LanguageCtx heap_lang (heap_lang.fill_item Ki).
619
Proof. change (LanguageCtx heap_lang (heap_lang.fill [Ki])). apply _. Qed.
620
621
622

(* Prefer heap_lang names over language names. *)
Export heap_lang.