lang.v 18 KB
Newer Older
1 2
From iris.algebra Require Import ofe.
From iris.program_logic Require Export language.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
From iris.program_logic Require Export ectx_language ectxi_language.
Dan Frumin's avatar
Dan Frumin committed
4
From iris_logrel.prelude Require Export base.
5
From iris_logrel.F_mu_ref_conc Require Export binder.
6

7
Module lang.
8
  (** * Syntax and syntactic categories *)
9 10
  Definition loc := positive.

11
  Instance loc_dec_eq : EqDecision loc := _.
12

Dan Frumin's avatar
Dan Frumin committed
13
  (** ** Expressions *)
14
  Inductive binop := Mul | Add | Sub | Eq | Le | Lt | Xor.
Dan Frumin's avatar
Dan Frumin committed
15
  
16
  Instance binop_dec_eq : EqDecision binop.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  Proof. solve_decision. Defined.
18

19
  Inductive literal := LitUnit | Nat (n : nat) | Bool (b : bool) | Loc (l : loc).
20

21
  Inductive expr :=
22
  | Var (x : string)
23
  (* λ-rec *)
24
  | Rec (f x : binder) (e : expr)
25
  | App (e1 e2 : expr)
26
  (* Constants *)
27
  | Lit (l : literal)
28
  | BinOp (op : binop) (e1 e2 : expr)
29 30
  (* If then else *)
  | If (e0 e1 e2 : expr)
31 32 33 34 35 36 37
  (* Products *)
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
  | Snd (e : expr)
  (* Sums *)
  | InjL (e : expr)
  | InjR (e : expr)
38
  | Case (e0 : expr) (e1 : expr) (e2 : expr)
39 40 41 42 43 44
  (* Recursive Types *)
  | Fold (e : expr)
  | Unfold (e : expr)
  (* Polymorphic Types *)
  | TLam (e : expr)
  | TApp (e : expr)
45 46
  (* Existential types *)
  | Pack (e : expr)
47
  | Unpack (e : expr) (e' : expr)
48 49 50 51 52 53 54 55
  (* Concurrency *)
  | Fork (e : expr)
  (* Reference Types *)
  | Alloc (e : expr)
  | Load (e : expr)
  | Store (e1 : expr) (e2 : expr)
  (* Compare and swap used for fine-grained concurrency *)
  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
56
  Bind Scope expr_scope with expr.
57

58
  Instance literal_dec_eq : EqDecision literal.
59
  Proof. solve_decision. Defined.
60

61
  Instance expr_dec_eq : EqDecision expr.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
  Proof. solve_decision. Defined.
63

Dan Frumin's avatar
Dan Frumin committed
64
  (** ** Closed expressions *)
65
  Fixpoint is_closed (X : stringset) (e : expr) : bool :=
66 67 68
    match e with
    | Var x => bool_decide (x  X)
    | Rec f x e => is_closed (x :b: f :b: X) e
69
    | Lit _ => true
70 71 72 73 74 75 76 77 78 79 80 81
    | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e | Fold e | Unfold e | TLam e | TApp e | Pack e => 
      is_closed X e
    | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
      is_closed X e1 && is_closed X e2
    | If e0 e1 e2 | CAS e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 && is_closed X e2
    | Case e0 e1 e2 =>
      is_closed X e0 && is_closed X e1 
                     && is_closed X e2      
    | Unpack e e1 => is_closed X e && is_closed X e1
    end.

82
  Class Closed (X : stringset) (e : expr) := closed : is_closed X e.
83 84 85 86 87 88 89 90 91 92
  Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
  Proof. rewrite /Closed. apply _. Qed.
  Instance closed_decision env e : Decision (Closed env e).
  Proof. rewrite /Closed. apply _. Qed.
  Instance: Proper (() ==> (=) ==> (=)) is_closed.
  Proof.
    intros X Y HXY e e' Hee'. 
    fold_leibniz. by subst.
  Defined.  

Dan Frumin's avatar
Dan Frumin committed
93
  (** ** Values *)
94
  Inductive val :=
95
  | RecV (f x : binder) (e : expr) `{!Closed (x :b: f :b: ) e}
Dan Frumin's avatar
Dan Frumin committed
96
  | TLamV (e : expr) `{!Closed  e} (* only closed lambdas are values *)
97
  | LitV (l : literal)
98 99 100 101
  | PairV (v1 v2 : val)
  | InjLV (v : val)
  | InjRV (v : val)
  | FoldV (v : val)
102
  | PackV (v : val).
103 104
  Bind Scope val_scope with val.

105
  (* Notation for bool and nat *)
Dan Frumin's avatar
Dan Frumin committed
106 107
  Fixpoint binop_eval (op : binop) (v1 v2 : val) : option val :=
    match op,v1,v2 with
108
    | Mul, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a * b))
Robbert Krebbers's avatar
Robbert Krebbers committed
109 110
    | Add, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a + b))
    | Sub, LitV (Nat a), LitV (Nat b) => Some $ LitV (Nat (a - b))
111
    | Eq, LitV (Nat a), LitV (Nat b) => Some $ if decide (a = b) then LitV (Bool true) else LitV (Bool false)
Robbert Krebbers's avatar
Robbert Krebbers committed
112
    | Eq, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (eqb a b))
113
    | Eq, LitV (Loc l1), LitV (Loc l2) => Some $ if decide (l1 = l2) then LitV (Bool true) else LitV (Bool false)
Robbert Krebbers's avatar
Robbert Krebbers committed
114 115 116
    | Le, LitV (Nat a), LitV (Nat b) => Some $ if le_dec a b then LitV (Bool true) else LitV (Bool false)
    | Lt, LitV (Nat a), LitV (Nat b) => Some $ if lt_dec a b then LitV (Bool true) else LitV (Bool false)
    | Xor, LitV (Bool a), LitV (Bool b) => Some $ LitV (Bool (xorb a b))
Dan Frumin's avatar
Dan Frumin committed
117
    | _,_,_ => None
118
    end.
119
  Instance val_inh : Inhabited val := populate (LitV LitUnit).
120 121 122

  Fixpoint of_val (v : val) : expr :=
    match v with
Dan Frumin's avatar
Dan Frumin committed
123 124
    | RecV f x e => Rec f x e
    | TLamV e => TLam e
Dan Frumin's avatar
Dan Frumin committed
125
    | LitV l => Lit l
126 127 128 129
    | PairV v1 v2 => Pair (of_val v1) (of_val v2)
    | InjLV v => InjL (of_val v)
    | InjRV v => InjR (of_val v)
    | FoldV v => Fold (of_val v)
130
    | PackV v => Pack (of_val v)
131 132 133 134
    end.

  Fixpoint to_val (e : expr) : option val :=
    match e with
135 136 137 138 139 140 141 142
    | Rec f x e =>
      if decide (Closed (x :b: f :b: ) e)
      then Some (RecV f x e)
      else None
    | TLam e => 
      if decide (Closed  e)
      then Some (TLamV e)
      else None
Dan Frumin's avatar
Dan Frumin committed
143
    | Lit l => Some (LitV l)
144 145 146 147
    | 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
    | Fold e => v  to_val e; Some (FoldV v)
148
    | Pack e => v  to_val e; Some (PackV v)
149 150 151
    | _ => None
    end.

152
  Lemma to_of_val v : to_val (of_val v) = Some v.
153
  Proof.
154
      by induction v; simplify_option_eq; repeat f_equal; try apply (proof_irrel _).
155 156
  Qed.

157
  Lemma of_to_val e v : to_val e = Some v  of_val v = e.
158
  Proof.
159
    revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
160
  Qed.
161 162 163 164

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

165
  Instance val_dec_eq : EqDecision val.
166
  Proof.
167
    refine (fun v v' => cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
168
  Defined.
169 170 171 172 173

  Instance literal_countable : Countable literal.
  Proof.
    refine (inj_countable' (λ l, match l with
    | Nat n => inl (inl n) | Bool b => inl (inr b)
174
    | LitUnit => inr (inl ()) | Loc l => inr (inr l)
175 176
    end) (λ l, match l with
    | inl (inl n) => Nat n | inl (inr b) => Bool b
177
    | inr (inl ()) => LitUnit | inr (inr l) => Loc l
178 179 180 181 182 183
    end) _); by intros [].
  Qed.

  Instance binop_countable : Countable binop.
  Proof.
   refine (inj_countable' (λ op, match op with
184
    | Mul => 0 | Add => 1 | Sub => 2 | Eq => 3 | Le => 4 | Lt => 5 | Xor => 6
185
    end) (λ n, match n with
186
    | 0 => Mul | 1 => Add | 2 => Sub | 3 => Eq | 4 => Le | 5 => Lt | _ => Xor
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242
    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))
           | Fold e => GenNode 2 [go e]
           | BinOp op e1 e2 => GenNode 3 [GenLeaf (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]
           | Unfold e => GenNode 16 [go e]
           | TLam e => GenNode 17 [go e]
           | TApp e => GenNode 18 [go e]
           | Pack e => GenNode 19 [go e]
           | Unpack e1 e2 => GenNode 20 [go e1; go e2]
           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 [e] => Fold (go e)
           | GenNode 3 [GenLeaf (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)
           | GenNode 16 [e] => Unfold (go e)
           | GenNode 17 [e] => TLam (go e)
           | GenNode 18 [e] => TApp (go e)
           | GenNode 19 [e] => Pack (go e)
           | GenNode 20 [e1; e2] => Unpack (go e1) (go e2)
243
           | _ => Lit LitUnit (* dummy *)
244 245 246 247 248 249 250
           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.

Dan Frumin's avatar
Dan Frumin committed
251
  (** ** Evaluation contexts *)
252 253 254 255 256 257
  Inductive ectx_item :=
  | AppLCtx (e2 : expr)
  | AppRCtx (v1 : val)
  | TAppCtx
  | PairLCtx (e2 : expr)
  | PairRCtx (v1 : val)
258 259
  | BinOpLCtx (op : binop) (e2 : expr)
  | BinOpRCtx (op : binop) (v1 : val)
260 261 262 263
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
264 265
  | CaseCtx (e1 : expr) (e2 : expr)
  | IfCtx (e1 : expr) (e2 : expr)
266 267
  | FoldCtx
  | UnfoldCtx
268 269
  | PackCtx
  | UnpackLCtx (e2 : expr)
270 271 272 273 274 275 276 277 278 279 280 281 282 283 284
  | AllocCtx
  | LoadCtx
  | StoreLCtx (e2 : expr)
  | StoreRCtx (v1 : val)
  | CasLCtx (e1 : expr)  (e2 : expr)
  | CasMCtx (v0 : val) (e2 : expr)
  | CasRCtx (v0 : val) (v1 : val).

  Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
    match Ki with
    | AppLCtx e2 => App e e2
    | AppRCtx v1 => App (of_val v1) e
    | TAppCtx => TApp e
    | PairLCtx e2 => Pair e e2
    | PairRCtx v1 => Pair (of_val v1) e
285 286
    | BinOpLCtx op e2 => BinOp op e e2
    | BinOpRCtx op v1 => BinOp op (of_val v1) e
287 288 289 290 291
    | FstCtx => Fst e
    | SndCtx => Snd e
    | InjLCtx => InjL e
    | InjRCtx => InjR e
    | CaseCtx e1 e2 => Case e e1 e2
292
    | IfCtx e1 e2 => If e e1 e2
293 294
    | FoldCtx => Fold e
    | UnfoldCtx => Unfold e
295 296
    | PackCtx => Pack e
    | UnpackLCtx e2 => Unpack e e2  
297 298 299 300 301 302 303 304 305
    | AllocCtx => Alloc e
    | LoadCtx => Load e
    | StoreLCtx e2 => Store e e2
    | StoreRCtx v1 => Store (of_val v1) e
    | 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
    end.

306
  (** * Substitutions *)  
Dan Frumin's avatar
Dan Frumin committed
307
  (** Parallel substitutions and some properties are defined in [subst.v] *)
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338
  Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
    match e with
    | Var y => if decide (x = y) then es else Var y
    | Rec f y e =>
      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)
    | TLam e => TLam (subst x es e)
    | TApp e => TApp (subst x es e)
    | Lit l => Lit l
    | 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)
    | Fold e => Fold (subst x es e)
    | Unfold e => Unfold (subst x es e)
    | Pack e => Pack (subst x es e)                
    | Unpack e0 e => 
      Unpack (subst x es e0) (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)
  end.
339

340 341 342 343
  Definition subst' (mx : binder) (es : expr) : expr  expr :=
    match mx with BNamed x => subst x es | BAnon => id end.
 
  (** * Reduction semantics *)
344 345
  Definition state : Type := gmap loc val.

Robbert Krebbers's avatar
Robbert Krebbers committed
346
  Inductive head_step : expr  state  expr  state  list expr  Prop :=
347
  (* β *)
348
  | BetaS f x e1 e2 v2 σ e' :
349
      to_val e2 = Some v2 
350 351 352 353
      Closed (x :b: f :b: ) e1 
      (* e' = subst_p (<[x:=e2]>{[f:=(Rec f x e1)]}) e1  *)
      e' = subst' f (Rec f x e1) (subst' x e2 e1) 
      head_step (App (Rec f x e1) e2) σ e' σ []
354 355 356
  (* Products *)
  | FstS e1 v1 e2 v2 σ :
      to_val e1 = Some v1  to_val e2 = Some v2 
Robbert Krebbers's avatar
Robbert Krebbers committed
357
      head_step (Fst (Pair e1 e2)) σ e1 σ []
358 359
  | SndS e1 v1 e2 v2 σ :
      to_val e1 = Some v1  to_val e2 = Some v2 
Robbert Krebbers's avatar
Robbert Krebbers committed
360
      head_step (Snd (Pair e1 e2)) σ e2 σ []
361
  (* Sums *)
362
  | CaseLS e0 v0 e1 e2 σ e' :
363
      to_val e0 = Some v0 
364 365 366
      e' = App e1 e0 
      head_step (Case (InjL e0) e1 e2) σ e' σ []
  | CaseRS e0 v0 e1 e2 σ e' :
367
      to_val e0 = Some v0 
368 369
      e' = App e2 e0 
      head_step (Case (InjR e0) e1 e2) σ e' σ []
370
  (* bin op *)
Dan Frumin's avatar
Dan Frumin committed
371 372 373 374 375
  | BinOpS op e1 e2 v1 v2 v σ :
      to_val e1 = Some v1 
      to_val e2 = Some v2 
      binop_eval op v1 v2 = Some v 
      head_step (BinOp op e1 e2) σ (of_val v) σ []
376 377
  (* If then else *)
  | IfFalse e1 e2 σ :
Robbert Krebbers's avatar
Robbert Krebbers committed
378
      head_step (If (Lit (Bool false)) e1 e2) σ e2 σ []
379
  | IfTrue e1 e2 σ :
Robbert Krebbers's avatar
Robbert Krebbers committed
380
      head_step (If (Lit (Bool true)) e1 e2) σ e1 σ []
381 382 383
  (* Recursive Types *)
  | Unfold_Fold e v σ :
      to_val e = Some v 
Robbert Krebbers's avatar
Robbert Krebbers committed
384
      head_step (Unfold (Fold e)) σ e σ []
385 386
  (* Polymorphic Types *)
  | TBeta e σ :
387
      Closed  e 
Robbert Krebbers's avatar
Robbert Krebbers committed
388
      head_step (TApp (TLam e)) σ e σ []
389
  (* Existential types *)
390
  | Unpack_Pack e1 v e2 σ e' :
391
      to_val e1 = Some v 
392 393
      e' = App e2 e1 
      head_step (Unpack (Pack e1) e2) σ e' σ []
394 395
  (* Concurrency *)
  | ForkS e σ:
396
      head_step (Fork e) σ (Lit LitUnit) σ [e]
397 398 399
  (* Reference Types *)
  | AllocS e v σ l :
     to_val e = Some v  σ !! l = None 
400
     head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) []
401 402
  | LoadS l v σ :
     σ !! l = Some v 
403
     head_step (Load (Lit (Loc l))) σ (of_val v) σ []
404 405
  | StoreS l e v σ :
     to_val e = Some v  is_Some (σ !! l) 
406
     head_step (Store (Lit (Loc l)) e) σ (Lit LitUnit) (<[l:=v]>σ) []
407 408 409 410
  (* Compare and swap *)
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some vl  vl  v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
411
     head_step (CAS (Lit (Loc l)) e1 e2) σ (Lit (Bool false)) σ []
412 413 414
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1  to_val e2 = Some v2 
     σ !! l = Some v1 
Robbert Krebbers's avatar
Robbert Krebbers committed
415
     head_step (CAS (Lit (Loc l)) e1 e2) σ (Lit (Bool true)) (<[l:=v2]>σ) [].
416

417 418 419 420 421 422
  Definition is_atomic (e : expr) : Prop :=
    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)
    | CAS e0 e1 e2 => is_Some (to_val e0)  is_Some (to_val e1)  is_Some (to_val e2)
Dan Frumin's avatar
Dan Frumin committed
423
    | BinOp _ e1 e2 => is_Some (to_val e1)  is_Some (to_val e2)
424 425 426 427 428 429 430
    | Fork _ => True
    | _ => False
    end.

  Canonical Structure stateC := leibnizC state.
  Canonical Structure valC := leibnizC val.
  Canonical Structure exprC := leibnizC expr.
431 432
  Canonical Structure locC := leibnizC loc.
  Canonical Structure ectx_itemC := leibnizC ectx_item.
433

Robbert Krebbers's avatar
Robbert Krebbers committed
434 435 436 437
  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.

438 439 440
  Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
  Proof. destruct Ki; intros ???; simplify_eq; auto with f_equal. Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
441
  Lemma val_stuck e1 σ1 e2 σ2 ef :
442 443 444 445 446
    head_step e1 σ1 e2 σ2 ef  to_val e1 = None.
  Proof. destruct 1; naive_solver. Qed.

  Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
    head_step (fill_item Ki e) σ1 e2 σ2 ef  is_Some (to_val e).
447
  Proof. destruct Ki; inversion_clear 1; simplify_option_eq; by eauto. Qed.
448 449 450 451 452 453 454 455 456 457 458 459

  Lemma fill_item_no_val_inj Ki1 Ki2 e1 e2 :
    to_val e1 = None  to_val e2 = None 
    fill_item Ki1 e1 = fill_item Ki2 e2  Ki1 = Ki2.
  Proof.
    destruct Ki1, Ki2; intros; try discriminate; simplify_eq;
    repeat match goal with
           | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
           end; auto.
  Qed.

  Lemma alloc_fresh e v σ :
Dan Frumin's avatar
Dan Frumin committed
460
    let l := fresh (dom (gset loc) σ) in
461
    to_val e = Some v  head_step (Alloc e) σ (Lit (Loc l)) (<[l:=v]>σ) [].
Dan Frumin's avatar
Dan Frumin committed
462
  Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset loc)), is_fresh. Qed.
463

Dan Frumin's avatar
Dan Frumin committed
464 465 466 467 468 469 470
  Lemma F_mu_ref_conc_mixin : EctxiLanguageMixin of_val to_val fill_item head_step.
  Proof.
    split; apply _ || eauto using to_of_val, of_to_val, val_stuck,
           fill_item_val, fill_item_no_val_inj, head_ctx_step_val.
  Qed.

End lang.
471

Dan Frumin's avatar
Dan Frumin committed
472 473 474 475
(** Language *)
Canonical Structure F_mu_ref_conc_ectxi_lang := EctxiLanguage lang.F_mu_ref_conc_mixin.
Canonical Structure F_mu_ref_conc_ectx_lang := EctxLanguageOfEctxi F_mu_ref_conc_ectxi_lang.
Canonical Structure F_mu_ref_conc_lang := LanguageOfEctx F_mu_ref_conc_ectx_lang.
Robbert Krebbers's avatar
Robbert Krebbers committed
476 477 478

Export lang.

479 480 481
(* This lemma is helpful for tactics on locked values and for reifying locked values. *)
Lemma of_val_unlock v e : of_val v = e  of_val (locked v) = e.
Proof. by unlock. Qed.
Dan Frumin's avatar
Dan Frumin committed
482 483 484 485

Local Hint Resolve language.val_irreducible.
Local Hint Resolve to_of_val.
Local Hint Unfold language.irreducible.
486

Dan Frumin's avatar
Dan Frumin committed
487
Lemma is_atomic_correct e : is_atomic e  Atomic e.
488
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
489
  intros ?; apply ectx_language_atomic.
Dan Frumin's avatar
Dan Frumin committed
490
  - destruct 1; simpl; eauto.
Dan Frumin's avatar
Dan Frumin committed
491
  - apply ectxi_language_sub_redexes_are_values=> /= Ki e' Hfill.
492
    destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
493
                   naive_solver eauto using to_val_is_Some.
494 495
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
496 497 498
Ltac solve_atomic :=
  apply is_atomic_correct; simpl; repeat split;
    rewrite ?to_of_val; eapply mk_is_Some; fast_done.
499

Dan Frumin's avatar
Dan Frumin committed
500
Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
501

502 503 504 505 506 507 508 509 510 511 512 513
(* Some other useful tactics *)
Ltac inv_head_step :=
  repeat match goal with
  | _ => progress simplify_map_eq/= (* simplify memory stuff *)
  | H : to_val _ = Some _ |- _ => apply of_to_val in H
  | H : _ = of_val ?v |- _ =>
     is_var v; destruct v; first[discriminate H|injection H as H]
  | H : head_step ?e _ _ _ _ |- _ =>
     try (is_var e; fail 1); (* inversion yields many goals if [e] is a variable
     and can thus better be avoided. *)
     inversion H; subst; clear H
  end.