heap_lang/lang.v

 From program_logic Require Export language.
-From prelude Require Export strings.
+From prelude Require Export strings stringmap.
 From prelude Require Import gmap.
 
 Module heap_lang.
@@ -15,35 +15,45 @@ Inductive un_op : Set :=
 Inductive bin_op : Set :=
   | PlusOp | MinusOp | LeOp | LtOp | EqOp.
 
-Inductive expr :=
+(* expr X is the type of expressions with free variables bounded by X.
+   I removed the "empty binder" hack since it does not go well with
+   proof irrelevance of the proof required for [Var]. If we really want
+   that back, we should change the binders in [Rec] to "option string". *)
+Inductive expr {X : stringset} : Type :=
   (* Base lambda calculus *)
-  | Var (x : string)
-  | Rec (f x : string) (e : expr)
-  | App (e1 e2 : expr)
+  | Var (x : string) {H : x ∈ X} : @expr X
+  | Rec (f x : string) (e : @expr ((X ∪ {[ x ]}) ∪ {[ f ]})) : @expr X
+  | App (e1 e2 : @expr X) : @expr X
   (* Base types and their operations *)
-  | Lit (l : base_lit)
-  | UnOp (op : un_op) (e : expr)
-  | BinOp (op : bin_op) (e1 e2 : expr)
-  | If (e0 e1 e2 : expr)
+  | Lit (l : base_lit) : @expr X
+  | UnOp (op : un_op) (e : @expr X) : @expr X
+  | BinOp (op : bin_op) (e1 e2 : @expr X) : @expr X
+  | If (e0 e1 e2 : @expr X) : @expr X
   (* Products *)
-  | Pair (e1 e2 : expr)
-  | Fst (e : expr)
-  | Snd (e : expr)
+  | Pair (e1 e2 : @expr X) : @expr X
+  | Fst (e : @expr X) : @expr X
+  | Snd (e : @expr X) : @expr X
   (* Sums *)
-  | InjL (e : expr)
-  | InjR (e : expr)
-  | Case (e0 : expr) (x1 : string) (e1 : expr) (x2 : string) (e2 : expr)
+  | InjL (e : @expr X) : @expr X
+  | InjR (e : @expr X) : @expr X
+  | Case (e0 e1 e2 : @expr X) : @expr X
   (* Concurrency *)
-  | Fork (e : expr)
+  | Fork (e : @expr X) : @expr X
   (* Heap *)
-  | Loc (l : loc)
-  | Alloc (e : expr)
-  | Load (e : expr)
-  | Store (e1 : expr) (e2 : expr)
-  | Cas (e0 : expr) (e1 : expr) (e2 : expr).
+  | Loc (l : loc) : @expr X
+  | Alloc (e : @expr X) : @expr X
+  | Load (e : @expr X) : @expr X
+  | Store (e1 e2 : @expr X) : @expr X
+  | Cas (e0 e1 e2 : @expr X) : @expr X.
+(* X should be explicit for a few of them: Those that do not take an expr of the same X *)
+Arguments expr _ : clear implicits.
+Arguments Var _ _ {_} : clear implicits.
+Arguments Rec _ _ _ _ : clear implicits.
+Arguments Lit _ _ : clear implicits.
+Arguments Loc _ _ : clear implicits.
 
 Inductive val :=
-  | RecV (f x : string) (e : expr) (* e should be closed *)
+  | RecV (f x : string) (e : expr ((∅ ∪ {[ x ]}) ∪ {[ f ]}))
   | LitV (l : base_lit)
   | PairV (v1 v2 : val)
   | InjLV (v : val)
@@ -56,25 +66,56 @@ Global Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
 Proof. solve_decision. Defined.
 Global Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
 Proof. solve_decision. Defined.
-Global Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
+(*Global Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
 Proof. solve_decision. Defined.
 Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
-Proof. solve_decision. Defined.
+Proof. solve_decision. Defined.*)
 
 Delimit Scope lang_scope with L.
 Bind Scope lang_scope with expr val.
 
-Fixpoint of_val (v : val) : expr :=
-  match v with
-  | RecV f x e => Rec f x e
-  | LitV l => Lit l
-  | PairV v1 v2 => Pair (of_val v1) (of_val v2)
-  | InjLV v => InjL (of_val v)
-  | InjRV v => InjR (of_val v)
-  | LocV l => Loc l
+Definition expr_cast {X1 X2} {H : X1 = X2} (e : expr X1) : expr X2 :=
+  eq_rect _ (λ X, expr X) e _ H.
+
+Program Fixpoint expr_weaken {X1 X2 : stringset} {H : X1 ⊆ X2} (e : expr X1) : expr X2 :=
+  match e return _ with
+  | Var x Hx => Var X2 x
+  | Rec f x e => Rec X2 f x (expr_weaken e)
+  | App e1 e2 => App (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
+  | Lit l => Lit X2 l
+  | UnOp op e => UnOp op (expr_weaken (H:=H) e)
+  | BinOp op e1 e2 => BinOp op (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
+  | If e0 e1 e2 => If (expr_weaken (H:=H) e0) (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
+  | Pair e1 e2 => Pair (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
+  | Fst e => Fst (expr_weaken (H:=H) e)
+  | Snd e => Snd (expr_weaken (H:=H) e)
+  | InjL e => InjL (expr_weaken (H:=H) e)
+  | InjR e => InjR (expr_weaken (H:=H) e)
+  | Case e0 e1 e2 => Case (expr_weaken (H:=H) e0) (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
+  | Fork e => Fork (expr_weaken (H:=H) e)
+  | Loc l => Loc X2 l
+  | Alloc e => Alloc (expr_weaken (H:=H) e)
+  | Load  e => Load (expr_weaken (H:=H) e)
+  | Store e1 e2 => Store (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
+  | Cas e0 e1 e2 => Cas (expr_weaken (H:=H) e0) (expr_weaken (H:=H) e1) (expr_weaken (H:=H) e2)
   end.
-Fixpoint to_val (e : expr) : option val :=
-  match e with
+Solve Obligations with set_solver.
+
+Program Fixpoint of_val X (v : val) : expr X :=
+  match v return expr X with
+  | RecV f x e => Rec X f x (expr_weaken e)
+  | LitV l => Lit X l
+  | PairV v1 v2 => Pair (of_val X v1) (of_val X v2)
+  | InjLV v => InjL (of_val X v)
+  | InjRV v => InjR (of_val X v)
+  | LocV l => Loc X l
+  end.
+Solve Obligations with set_solver.
+
+Fixpoint to_val (e : expr ∅) : option val :=
+  match e return option val with
+    (* The LHS of thus ⊆ must be like the argument of Rec, the RHS
+       must be like the argument of RecV. *)
   | Rec f x e => Some (RecV f x e)
   | Lit l => Some (LitV l)
   | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
@@ -89,82 +130,94 @@ Definition state := gmap loc val.
 
 (** Evaluation contexts *)
 Inductive ectx_item :=
-  | AppLCtx (e2 : expr)
+  | AppLCtx (e2 : expr ∅)
   | AppRCtx (v1 : val)
   | UnOpCtx (op : un_op)
-  | BinOpLCtx (op : bin_op) (e2 : expr)
+  | BinOpLCtx (op : bin_op) (e2 : expr ∅)
   | BinOpRCtx (op : bin_op) (v1 : val)
-  | IfCtx (e1 e2 : expr)
-  | PairLCtx (e2 : expr)
+  | IfCtx (e1 e2 : expr ∅)
+  | PairLCtx (e2 : expr ∅)
   | PairRCtx (v1 : val)
   | FstCtx
   | SndCtx
   | InjLCtx
   | InjRCtx
-  | CaseCtx (x1 : string) (e1 : expr) (x2 : string) (e2 : expr)
+  | CaseCtx (e1 : expr ∅) (e2 : expr ∅)
   | AllocCtx
   | LoadCtx
-  | StoreLCtx (e2 : expr)
+  | StoreLCtx (e2 : expr ∅)
   | StoreRCtx (v1 : val)
-  | CasLCtx (e1 : expr)  (e2 : expr)
-  | CasMCtx (v0 : val) (e2 : expr)
+  | CasLCtx (e1 : expr ∅)  (e2 : expr ∅)
+  | CasMCtx (v0 : val) (e2 : expr ∅)
   | CasRCtx (v0 : val) (v1 : val).
 
 Notation ectx := (list ectx_item).
 
-Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
-  match Ki with
+Definition fill_item (Ki : ectx_item) (e : expr ∅) : expr ∅ :=
+  match Ki return expr ∅ with
   | AppLCtx e2 => App e e2
-  | AppRCtx v1 => App (of_val v1) e
+  | AppRCtx v1 => App (of_val ∅ v1) e
   | UnOpCtx op => UnOp op e
   | BinOpLCtx op e2 => BinOp op e e2
-  | BinOpRCtx op v1 => BinOp op (of_val v1) e
+  | BinOpRCtx op v1 => BinOp op (of_val ∅ v1) e
   | IfCtx e1 e2 => If e e1 e2
   | PairLCtx e2 => Pair e e2
-  | PairRCtx v1 => Pair (of_val v1) e
+  | PairRCtx v1 => Pair (of_val ∅ v1) e
   | FstCtx => Fst e
   | SndCtx => Snd e
   | InjLCtx => InjL e
   | InjRCtx => InjR e
-  | CaseCtx x1 e1 x2 e2 => Case e x1 e1 x2 e2
+  | CaseCtx e1 e2 => Case e e1 e2
   | AllocCtx => Alloc e
   | LoadCtx => Load e
   | StoreLCtx e2 => Store e e2
-  | StoreRCtx v1 => Store (of_val v1) e
+  | 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
+  | CasMCtx v0 e2 => Cas (of_val ∅ v0) e e2
+  | CasRCtx v0 v1 => Cas (of_val ∅ v0) (of_val ∅ v1) e
   end.
-Definition fill (K : ectx) (e : expr) : expr := fold_right fill_item e K.
+
+Definition fill (K : ectx) (e : expr ∅) : expr ∅ := fold_right fill_item e K.
 
 (** Substitution *)
-(** We have [subst e "" v = e] to deal with anonymous binders *)
-Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
-  match e with
-  | Var y => if decide (x = y ∧ x ≠ "") then of_val v else Var y
-  | Rec f y e => Rec f y (if decide (x ≠ f ∧ x ≠ y) then subst e x v else e)
-  | App e1 e2 => App (subst e1 x v) (subst e2 x v)
-  | Lit l => Lit l
-  | UnOp op e => UnOp op (subst e x v)
-  | BinOp op e1 e2 => BinOp op (subst e1 x v) (subst e2 x v)
-  | If e0 e1 e2 => If (subst e0 x v) (subst e1 x v) (subst e2 x v)
-  | Pair e1 e2 => Pair (subst e1 x v) (subst e2 x v)
-  | Fst e => Fst (subst e x v)
-  | Snd e => Snd (subst e x v)
-  | InjL e => InjL (subst e x v)
-  | InjR e => InjR (subst e x v)
-  | Case e0 x1 e1 x2 e2 =>
-     Case (subst e0 x v)
-       x1 (if decide (x ≠ x1) then subst e1 x v else e1)
-       x2 (if decide (x ≠ x2) then subst e2 x v else e2)
-  | Fork e => Fork (subst e x v)
-  | Loc l => Loc l
-  | Alloc e => Alloc (subst e x v)
-  | Load e => Load (subst e x v)
-  | Store e1 e2 => Store (subst e1 x v) (subst e2 x v)
-  | Cas e0 e1 e2 => Cas (subst e0 x v) (subst e1 x v) (subst e2 x v)
+Program Fixpoint subst X (x : string) (v : val) (e : expr (X ∪ {[ x ]})) :
+    expr X :=
+  match e return expr X with
+  | Var y Hx => if decide (x = y) then of_val X v
+                                   else Var X y
+  | Rec f y e => Rec X f y (if decide (x ≠ f ∧ x ≠ y)
+                            then subst ((X ∪ {[ y ]}) ∪ {[ f ]}) x v (expr_cast e)
+                            else expr_cast e)
+  | App e1 e2 => App (subst X x v e1) (subst X x v e2)
+  | Lit l => Lit X l
+  | UnOp op e => UnOp op (subst X x v e)
+  | BinOp op e1 e2 => BinOp op (subst X x v e1) (subst X x v e2)
+  | If e0 e1 e2 => If (subst X x v e0) (subst X x v e1) (subst X x v e2)
+  | Pair e1 e2 => Pair (subst X x v e1) (subst X x v e2)
+  | Fst e => Fst (subst X x v e)
+  | Snd e => Snd (subst X x v e)
+  | InjL e => InjL (subst X x v e)
+  | InjR e => InjR (subst X x v e)
+  | Case e0 e1 e2 =>
+     Case (subst X x v e0) (subst X x v e1) (subst X x v e2)
+  | Fork e => Fork (subst X x v e)
+  | Loc l => Loc X l
+  | Alloc e => Alloc (subst X x v e)
+  | Load e => Load (subst X x v e)
+  | Store e1 e2 => Store (subst X x v e1) (subst X x v e2)
+  | Cas e0 e1 e2 => Cas (subst X x v e0) (subst X x v e1) (subst X x v e2)
   end.
-
+Next Obligation. set_solver. Qed.
+Next Obligation. set_solver. Qed.
+(* FIXME fix this *)
+Next Obligation.
+  intros ??????? [H%dec_stable|H%dec_stable]%not_and_l; subst.
+  - apply elem_of_equiv_L=>x.
+    destruct (decide (x = f)); set_solver.
+  - apply elem_of_equiv_L=>x.
+    destruct (decide (x = y)); set_solver.
+Qed.
+                 
 (** The stepping relation *)
 Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
   match op, l with
@@ -183,55 +236,61 @@ Definition bin_op_eval (op : bin_op) (l1 l2 : base_lit) : option base_lit :=
   | _, _, _ => None
   end.
 
-Inductive head_step : expr → state → expr → state → option expr → Prop :=
-  | BetaS f x e1 e2 v2 σ :
+Inductive head_step : expr ∅ → state → expr ∅ → state → option (expr ∅) → Prop :=
+  (* The second "x" in the type of [e1] should be an "f". *)
+  | BetaS (f x : string) (e1 : expr ((∅ ∪ {[ x ]}) ∪ {[ x ]})) (e2 : expr ∅) v2 (σ : state) :
      to_val e2 = Some v2 →
-     head_step (App (Rec f x e1) e2) σ
-       (subst (subst e1 f (RecV f x e1)) x v2) σ None
+     head_step (App (Rec ∅ f x e1) e2) σ
+       (subst ∅ x v2 (subst (∅ ∪ {[ x ]}) f (RecV f x e1) e1)) σ None.
+
+Set Printing All.
+Print head_step.
+
+
   | UnOpS op l l' σ :
      un_op_eval op l = Some l' → 
-     head_step (UnOp op (Lit l)) σ (Lit l') σ None
+     head_step (UnOp op (Lit ∅ l)) σ (Lit ∅ l') σ None
   | BinOpS op l1 l2 l' σ :
      bin_op_eval op l1 l2 = Some l' → 
-     head_step (BinOp op (Lit l1) (Lit l2)) σ (Lit l') σ None
+     head_step (BinOp op (Lit ∅ l1) (Lit ∅ l2)) σ (Lit ∅ l') σ None
   | IfTrueS e1 e2 σ :
-     head_step (If (Lit $ LitBool true) e1 e2) σ e1 σ None
+     head_step (If (Lit ∅ $ LitBool true) e1 e2) σ e1 σ None
   | IfFalseS e1 e2 σ :
-     head_step (If (Lit $ LitBool false) e1 e2) σ e2 σ None
+     head_step (If (Lit ∅ $ LitBool false) e1 e2) σ e2 σ None
   | 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
-  | CaseLS e0 v0 x1 e1 x2 e2 σ :
+  | CaseLS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjL e0) x1 e1 x2 e2) σ (subst e1 x1 v0) σ None
-  | CaseRS e0 v0 x1 e1 x2 e2 σ :
+     head_step (Case (InjL e0) e1 e2) σ (App e1 (of_val ∅ v0)) σ None
+  | CaseRS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
-     head_step (Case (InjR e0) x1 e1 x2 e2) σ (subst e2 x2 v0) σ None
+     head_step (Case (InjR e0) e1 e2) σ (App e2 (of_val ∅ v0)) σ None
   | ForkS e σ:
-     head_step (Fork e) σ (Lit LitUnit) σ (Some e)
+     head_step (Fork e) σ (Lit ∅ LitUnit) σ (Some e)
   | AllocS e v σ l :
      to_val e = Some v → σ !! l = None →
-     head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) 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
+     head_step (Load (Loc ∅ l)) σ (of_val ∅ v) σ None
   | StoreS l e v σ :
      to_val e = Some v → is_Some (σ !! l) →
-     head_step (Store (Loc l) e) σ (Lit LitUnit) (<[l:=v]>σ) None
+     head_step (Store (Loc ∅ l) e) σ (Lit ∅ LitUnit) (<[l:=v]>σ) None
   | CasFailS l e1 v1 e2 v2 vl σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some vl → vl ≠ v1 →
-     head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool false) σ None
+     head_step (Cas (Loc ∅ l) e1 e2) σ (Lit ∅ $ LitBool false) σ None
   | CasSucS l e1 v1 e2 v2 σ :
      to_val e1 = Some v1 → to_val e2 = Some v2 →
      σ !! l = Some v1 →
-     head_step (Cas (Loc l) e1 e2) σ (Lit $ LitBool true) (<[l:=v2]>σ) None.
+     head_step (Cas (Loc ∅ l) e1 e2) σ (Lit ∅ $ LitBool true) (<[l:=v2]>σ) None.
 
 (** Atomic expressions *)
-Definition atomic (e: expr) : Prop :=
+Definition atomic (e: expr ∅) : Prop :=
   match e with
   | Alloc e => is_Some (to_val e)
   | Load e => is_Some (to_val e)
@@ -245,25 +304,71 @@ Definition atomic (e: expr) : Prop :=
 (** Close reduction under evaluation contexts.
 We could potentially make this a generic construction. *)
 Inductive prim_step
-    (e1 : expr) (σ1 : state) (e2 : expr) (σ2: state) (ef: option expr) : Prop :=
+    (e1 : expr ∅) (σ1 : state) (e2 : expr ∅) (σ2: state) (ef: option (expr ∅)) : Prop :=
   Ectx_step K e1' e2' :
     e1 = fill K e1' → e2 = fill K e2' →
     head_step e1' σ1 e2' σ2 ef → prim_step e1 σ1 e2 σ2 ef.
 
+(** The equalities we need for some lemmas. *)
+Lemma stringset_eq_1 {X : stringset} :
+  X = ∅ ∪ X.
+Proof. set_solver. Qed.
+Lemma stringset_eq_2 {f x : string} :
+  (({[f; x]} ∖ {[f]}) ∖ {[x]}) = (∅ : stringset).
+Proof. set_solver. Qed.
+Lemma stringset_subseteq_1 {X : stringset} :
+  ∅ ⊆ X.
+Proof. set_solver. Qed.
+
+
+
+(** Properties of the cast operators *)
+Lemma not_or_l {P Q : Prop} `{Decision P} : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q.
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_or_r {P Q : Prop} `{Decision Q} : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.
+
+Lemma expr_weaken_id {X : stringset} {H : X ⊆ X} (e : expr X) :
+  expr_weaken (H:=H) e = e.
+Proof.
+  induction e; simpl; by (f_equal; try apply proof_irrel; eauto).
+Qed.
+
+Lemma expr_weaken_cast_id {X Y : stringset} {H1 : Y ⊆ X} {H2 : X = Y} (e : expr X) :
+  expr_weaken (H:=H1) (expr_cast (H:=H2) e) = e.
+Proof.
+  destruct H2. by apply expr_weaken_id.
+Qed.
+
+Lemma expr_weaken_cast_weaken_id {X Y Z : stringset} {H1 : Z ⊆ X} {H2 : Y = Z} {H3 : X ⊆ Y} (e : expr X) :
+  expr_weaken (H:=H1) (expr_cast (H:=H2) (expr_weaken (H:=H3) e)) = e.
+Proof.
+  destruct H2. assert (X = Y) by set_solver. subst Y. by rewrite !expr_weaken_id.
+Qed.
+
+Lemma expr_cast_val {X Y : stringset} {H : X = Y} e:
+  to_val (expr_cast (H:=H) e) = to_val e.
+Proof. destruct H. done. Qed.
+
 (** Basic properties about the language *)
 Lemma to_of_val v : to_val (of_val v) = Some v.
-Proof. by induction v; simplify_option_eq. Qed.
+Proof.
+  induction v; simpl; try case_match; simplify_option_eq; try done.
+  - f_equiv. f_equiv. by rewrite expr_weaken_cast_id.
+  - exfalso. apply H. set_solver+.
+Qed.
 
-Lemma of_to_val e v : to_val e = Some v → of_val v = e.
+Lemma of_to_val' X (e : expr X) v : to_val e = Some v → expr_weaken (H:=stringset_subseteq_1) (of_val v) = e.
 Proof.
   revert v; induction e; intros; simplify_option_eq; auto with f_equal.
+  f_equiv. by rewrite expr_weaken_cast_weaken_id.
 Qed.
 
 Instance: Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
 Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
-Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
+Proof. destruct Ki; intros ?? H; simpl in *; inversion_clear H; done. Qed.
 
 Instance ectx_fill_inj K : Inj (=) (=) (fill K).
 Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
@@ -294,6 +399,7 @@ Lemma atomic_fill_item Ki e : atomic (fill_item Ki e) → is_Some (to_val e).
 Proof.
   intros. destruct Ki; simplify_eq/=; destruct_conjs;
     repeat (case_match || contradiction); eauto.
+  simpl. case_match; first by eauto. exfalso. apply n. set_solver+.
 Qed.
 
 Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
@@ -307,6 +413,7 @@ Lemma atomic_head_step e1 σ1 e2 σ2 ef :
 Proof.
   destruct 2; simpl; rewrite ?to_of_val; try by eauto.
   repeat (case_match || contradiction || simplify_eq/=); eauto.
+  rewrite expr_cast_val. 
 Qed.
 
 Lemma atomic_step e1 σ1 e2 σ2 ef :