From 15058014515f9a23f83fce35d13577177a423204 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 01:56:41 +0100
Subject: [PATCH] Clean up heap_lang and remove some FIXMEs.

Notable changes:
* I am now using the same names for the fields of the language record and the
  instances in heap_lang. In order to deal with shadowing, I have put all
  definitions in heap_lang.v in a module.
* Instead of defining evaluation contexts recursively, these are now defined
  using lists. This way we can easily reuse operations on lists. For example,
  composition of evaluation contexts is just appending lists. Also, it allowed
  me to simplify the rather complicated proof of step_by_val as induction on
  the shape of contexts no longer results in a blow-up of the number of cases.
* Use better automation to prove all lemmas of heap_lang.
* I have introduced tactics to invert steps and to do steps. These tactics
  greatly helped simplifying boring parts of lifting lemmas.
---
 _CoqProject                 |   1 +
 barrier/heap_lang.v         | 648 ++++++++++++++----------------------
 barrier/heap_lang_tactics.v |  72 ++++
 barrier/lifting.v           | 349 +++++++------------
 barrier/sugar.v             |  62 ++--
 barrier/tests.v             |  61 ++--
 iris/hoare_lifting.v        |   2 +-
 iris/language.v             |  14 +-
 iris/weakestpre.v           |   8 +-
 9 files changed, 496 insertions(+), 721 deletions(-)
 create mode 100644 barrier/heap_lang_tactics.v

diff --git a/_CoqProject b/_CoqProject
index 3eaad9889..649a4017e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -64,6 +64,7 @@ iris/language.v
 iris/functor.v
 iris/tests.v
 barrier/heap_lang.v
+barrier/heap_lang_tactics.v
 barrier/lifting.v
 barrier/sugar.v
 barrier/tests.v
diff --git a/barrier/heap_lang.v b/barrier/heap_lang.v
index d579636ee..d2f508384 100644
--- a/barrier/heap_lang.v
+++ b/barrier/heap_lang.v
@@ -1,447 +1,301 @@
 Require Export Autosubst.Autosubst.
-Require Import prelude.option prelude.gmap iris.language.
+Require Export iris.language.
+Require Import prelude.gmap.
 
-(** Expressions and values. *)
+Module heap_lang.
+(** Expressions and vals. *)
 Definition loc := positive. (* Really, any countable type. *)
 
 Inductive expr :=
-(* Base lambda calculus *)
-| Var (x : var)
-| Rec (e : {bind 2 of expr}) (* These are recursive lambdas. The *inner* binder is the recursive call! *)
-| App (e1 e2 : expr)
-(* Natural numbers *)
-| LitNat (n : nat)
-| Plus (e1 e2 : expr)
-| Le (e1 e2 : expr)
-(* Unit *)
-| LitUnit
-(* Products *)
-| Pair (e1 e2 : expr)
-| Fst (e : expr)
-| Snd (e : expr)
-(* Sums *)
-| InjL (e : expr)
-| InjR (e : expr)
-| Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
-(* Concurrency *)
-| Fork (e : expr)
-(* Heap *)
-| Loc (l : loc)
-| Alloc (e : expr)
-| Load (e : expr)
-| Store (e1 : expr) (e2 : expr)
-| Cas (e0 : expr) (e1 : expr) (e2 : expr)
-.
+  (* Base lambda calculus *)
+  | Var (x : var)
+  | Rec (e : {bind 2 of expr}) (* These are recursive lambdas.
+                                  The *inner* binder is the recursive call! *)
+  | App (e1 e2 : expr)
+  (* Natural numbers *)
+  | LitNat (n : nat)
+  | Plus (e1 e2 : expr)
+  | Le (e1 e2 : expr)
+  (* Unit *)
+  | LitUnit
+  (* Products *)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
+  (* Sums *)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : {bind expr}) (e2 : {bind expr})
+  (* Concurrency *)
+  | Fork (e : expr)
+  (* Heap *)
+  | Loc (l : loc)
+  | Alloc (e : expr)
+  | Load (e : expr)
+  | Store (e1 : expr) (e2 : expr)
+  | Cas (e0 : expr) (e1 : expr) (e2 : expr).
 
 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.
 
-(* This sugar is used by primitive reduction riles (<=, CAS) and hence defined here. *)
-Definition LitTrue := InjL LitUnit.
-Definition LitFalse := InjR LitUnit.
-
-Inductive value :=
-| RecV (e : {bind 2 of expr})
-| LitNatV (n : nat) (* These are recursive lambdas. The *inner* binder is the recursive call! *)
-| LitUnitV
-| PairV (v1 v2 : value)
-| InjLV (v : value)
-| InjRV (v : value)
-| LocV (l : loc)
-.
+(* This sugar is used by primitive reduction riles (<=, CAS) and hence
+defined here. *)
+Notation LitTrue := (InjL LitUnit).
+Notation LitFalse := (InjR LitUnit).
+
+Inductive val :=
+  | RecV (e : {bind 2 of expr}) (* These are recursive lambdas.
+                                   The *inner* binder is the recursive call! *)
+  | LitNatV (n : nat)
+  | LitUnitV
+  | PairV (v1 v2 : val)
+  | InjLV (v : val)
+  | InjRV (v : val)
+  | LocV (l : loc).
 
 Definition LitTrueV := InjLV LitUnitV.
 Definition LitFalseV := InjRV LitUnitV.
 
-Fixpoint v2e (v : value) : expr :=
+Fixpoint of_val (v : val) : expr :=
   match v with
-  | RecV e   => Rec e
+  | RecV e => Rec e
   | LitNatV n => LitNat n
   | LitUnitV => LitUnit
-  | PairV v1 v2 => Pair (v2e v1) (v2e v2)
-  | InjLV v => InjL (v2e v)
-  | InjRV v => InjR (v2e v)
+  | 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
   end.
-
-Fixpoint e2v (e : expr) : option value :=
+Fixpoint to_val (e : expr) : option val :=
   match e with
   | Rec e => Some (RecV e)
   | LitNat n => Some (LitNatV n)
   | LitUnit => Some LitUnitV
-  | Pair e1 e2 => v1 â† e2v e1;
-                  v2 â† e2v e2;
-                  Some (PairV v1 v2)
-  | InjL e => InjLV <$> e2v e
-  | InjR e => InjRV <$> e2v e
+  | 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
   | Loc l => Some (LocV l)
   | _ => None
   end.
 
-Lemma v2v v:
-  e2v (v2e v) = Some v.
-Proof.
-  induction v; simpl; rewrite ?IHv ?IHv1 /= ?IHv2; reflexivity.
-Qed.
-
-Section e2e. (* To get local tactics. *)
-Lemma e2e e v:
-  e2v e = Some v â†’ v2e v = e.
-Proof.
-  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.
-  revert v2; induction v1=>v2; destruct v2; simpl; try done;
-    case; eauto using f_equal, f_equal2.
-Qed.
-
-(** The state: heaps of values. *)
-Definition state := gmap loc value.
+(** The state: heaps of vals. *)
+Definition state := gmap loc val.
 
 (** Evaluation contexts *)
-Inductive ectx :=
-| EmptyCtx
-| AppLCtx (K1 : ectx)  (e2 : expr)
-| AppRCtx (v1 : value) (K2 : ectx)
-| PlusLCtx (K1 : ectx)  (e2 : expr)
-| PlusRCtx (v1 : value) (K2 : ectx)
-| LeLCtx (K1 : ectx)  (e2 : expr)
-| LeRCtx (v1 : value) (K2 : ectx)
-| PairLCtx (K1 : ectx)  (e2 : expr)
-| PairRCtx (v1 : value) (K2 : ectx)
-| FstCtx (K : ectx)
-| SndCtx (K : ectx)
-| InjLCtx (K : ectx)
-| InjRCtx (K : ectx)
-| CaseCtx (K : ectx) (e1 : {bind expr}) (e2 : {bind expr})
-| AllocCtx (K : ectx)
-| 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)
-.
-
-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)
-  | PlusLCtx K1 e2 => Plus (fill K1 e) e2
-  | PlusRCtx v1 K2 => Plus (v2e v1) (fill K2 e)
-  | LeLCtx K1 e2 => Le (fill K1 e) e2
-  | LeRCtx v1 K2 => Le (v2e v1) (fill K2 e)
-  | 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
-  | AllocCtx K => Alloc (fill K e)
-  | LoadCtx K => Load (fill K e)
-  | 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)
-  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)
-  | PlusLCtx K1 e2 => PlusLCtx (comp_ctx K1 Ki) e2
-  | PlusRCtx v1 K2 => PlusRCtx v1 (comp_ctx K2 Ki)
-  | LeLCtx K1 e2 => LeLCtx (comp_ctx K1 Ki) e2
-  | LeRCtx v1 K2 => LeRCtx v1 (comp_ctx K2 Ki)
-  | 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
-  | AllocCtx K => AllocCtx (comp_ctx K Ki)
-  | LoadCtx K => LoadCtx (comp_ctx K Ki)
-  | 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)
+Inductive ectx_item :=
+  | AppLCtx (e2 : expr)
+  | AppRCtx (v1 : val)
+  | PlusLCtx (e2 : expr)
+  | PlusRCtx (v1 : val)
+  | LeLCtx (e2 : expr)
+  | LeRCtx (v1 : val)
+  | PairLCtx (e2 : expr)
+  | PairRCtx (v1 : val)
+  | FstCtx
+  | SndCtx
+  | InjLCtx
+  | InjRCtx
+  | CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
+  | AllocCtx
+  | LoadCtx
+  | StoreLCtx (e2 : expr)
+  | StoreRCtx (v1 : val)
+  | CasLCtx (e1 : expr)  (e2 : expr)
+  | CasMCtx (v0 : val) (e2 : expr)
+  | CasRCtx (v0 : val) (v1 : val).
+Notation ectx := (list ectx_item).
+Implicit Types Ki : ectx_item.
+Implicit Types K : ectx.
+
+Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
+  match Ki with
+  | AppLCtx e2 => App e e2
+  | AppRCtx v1 => App (of_val v1) e
+  | PlusLCtx e2 => Plus e e2
+  | PlusRCtx v1 => Plus (of_val v1) e
+  | LeLCtx e2 => Le e e2
+  | LeRCtx v1 => Le (of_val v1) e
+  | PairLCtx e2 => Pair e e2
+  | PairRCtx v1 => Pair (of_val v1) e
+  | FstCtx => Fst e
+  | SndCtx => Snd e
+  | InjLCtx => InjL e
+  | InjRCtx => InjR e
+  | 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
+  | 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.
+Instance ectx_fill : Fill ectx expr :=
+  fix go K e := let _ : Fill _ _ := @go in
+  match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) 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.
-  revert K2 e; induction K1 => K2 e /=; rewrite ?IHK1 ?IHK2; reflexivity.
-Qed.
-
-Lemma fill_inj_r K e1 e2 :
-  fill K e1 = fill K e2 â†’ e1 = e2.
-Proof.
-  revert e1 e2; induction K => el er /=;
-     (move=><-; reflexivity) || (case => /IHK <-; reflexivity).
-Qed.
-
-Lemma fill_value K e v':
-  e2v (fill K e) = Some v' â†’ is_Some (e2v e).
-Proof.
-  revert v'; induction K => v' /=; try discriminate;
-    try destruct (e2v (fill K e)); rewrite ?v2v; eauto.
-Qed.
+(** The stepping relation *)
+Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
+  | BetaS e1 e2 v2 Ïƒ :
+     to_val e2 = Some v2 â†’
+     head_step (App (Rec e1) e2) Ïƒ e1.[(Rec e1),e2/] Ïƒ None
+  | PlusS n1 n2 Ïƒ:
+     head_step (Plus (LitNat n1) (LitNat n2)) Ïƒ (LitNat (n1 + n2)) Ïƒ None
+  | LeTrueS n1 n2 Ïƒ :
+     n1 â‰¤ n2 â†’
+     head_step (Le (LitNat n1) (LitNat n2)) Ïƒ LitTrue Ïƒ None
+  | LeFalseS n1 n2 Ïƒ :
+     n1 > n2 â†’
+     head_step (Le (LitNat n1) (LitNat n2)) Ïƒ LitFalse Ïƒ 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 e1 e2 Ïƒ :
+     to_val e0 = Some v0 â†’
+     head_step (Case (InjL e0) e1 e2) Ïƒ e1.[e0/] Ïƒ None
+  | CaseRS e0 v0 e1 e2 Ïƒ :
+     to_val e0 = Some v0 â†’
+     head_step (Case (InjR e0) e1 e2) Ïƒ e2.[e0/] Ïƒ None
+  | ForkS e Ïƒ:
+     head_step (Fork e) Ïƒ LitUnit Ïƒ (Some e)
+  | 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) â†’
+     head_step (Store (Loc l) e) Ïƒ 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) Ïƒ LitFalse Ïƒ 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) Ïƒ LitTrue (<[l:=v2]>Ïƒ) None.
 
-Lemma fill_not_value e K :
-  e2v e = None â†’ e2v (fill K e) = None.
-Proof.
-  intros Hnval.  induction K =>/=; by rewrite ?v2v /= ?IHK /=.
-Qed.
+(** Atomic expressions *)
+Definition atomic (e: expr) :=
+  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)
+  | _ => False
+  end.
 
-Lemma fill_not_value2 e K v :
-  e2v e = None â†’ e2v (fill K e) = Some v -> False.
+(** 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 :=
+  Ectx_step (K : ectx) e1' e2' :
+    e1 = fill K e1' â†’ e2 = fill K e2' â†’
+    head_step e1' Ïƒ1 e2' Ïƒ2 ef â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 ef.
+
+(** Basic properties about the language *)
+Lemma to_of_val v : to_val (of_val v) = Some v.
+Proof. by induction v; simplify_option_equality. Qed.
+Lemma of_to_val e v : to_val e = Some v â†’ of_val v = e.
 Proof.
-  intros Hnval Hval. erewrite fill_not_value in Hval by assumption. discriminate.
+  revert v; induction e; intros; simplify_option_equality; auto with f_equal.
 Qed.
-
-Lemma comp_empty K K' :
-  EmptyCtx = comp_ctx K K' â†’
-  K = EmptyCtx âˆ§ K' = EmptyCtx.
+Instance: Injective (=) (=) of_val.
+Proof. by intros ?? Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
+Instance ectx_item_fill_inj Ki : Injective (=) (=) (ectx_item_fill Ki).
+Proof. destruct Ki; intros ???; simplify_equality'; auto with f_equal. Qed.
+Instance ectx_fill_inj K : Injective (=) (=) (fill K).
+Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
+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.
+Lemma fill_val K e : is_Some (to_val (fill K e)) â†’ is_Some (to_val e).
 Proof.
-  destruct K; try discriminate.
-  destruct K'; try discriminate.
-  done.
+  intros [v' Hv']; revert v' Hv'.
+  induction K as [|[]]; intros; simplify_option_equality; eauto.
 Qed.
-
-(** The stepping relation *)
-Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
-| BetaS e1 e2 v2 Ïƒ (Hv2 : e2v e2 = Some v2):
-    prim_step (App (Rec e1) e2) Ïƒ e1.[(Rec e1),e2/] Ïƒ None
-| PlusS n1 n2 Ïƒ:
-    prim_step (Plus (LitNat n1) (LitNat n2)) Ïƒ (LitNat (n1 + n2)) Ïƒ None
-| LeTrueS n1 n2 Ïƒ (Hle : n1 â‰¤ n2):
-    prim_step (Le (LitNat n1) (LitNat n2)) Ïƒ LitTrue Ïƒ None
-| LeFalseS n1 n2 Ïƒ (Hle : n1 > n2):
-    prim_step (Le (LitNat n1) (LitNat n2)) Ïƒ LitFalse Ïƒ None
-| 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
-| CaseLS e0 v0 e1 e2 Ïƒ (Hv0 : e2v e0 = Some v0):
-    prim_step (Case (InjL e0) e1 e2) Ïƒ e1.[e0/] Ïƒ None
-| CaseRS e0 v0 e1 e2 Ïƒ (Hv0 : e2v e0 = Some v0):
-    prim_step (Case (InjR e0) e1 e2) Ïƒ e2.[e0/] Ïƒ None
-| ForkS e Ïƒ:
-    prim_step (Fork e) Ïƒ LitUnit Ïƒ (Some e)
-| AllocS e v Ïƒ l (Hv : e2v e = Some v) (Hfresh : Ïƒ !! l = None):
-    prim_step (Alloc e) Ïƒ (Loc l) (<[l:=v]>Ïƒ) None
-| 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
-.
-
-Definition reducible e Ïƒ : Prop :=
-  âˆƒ e' Ïƒ' ef, prim_step e Ïƒ e' Ïƒ' ef.
-
-Lemma reducible_not_value e Ïƒ :
-  reducible e Ïƒ â†’ e2v e = None.
+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.
+Lemma values_head_stuck e1 Ïƒ1 e2 Ïƒ2 ef :
+  head_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ to_val e1 = None.
+Proof. destruct 1; naive_solver. Qed.
+Lemma values_stuck e1 Ïƒ1 e2 Ïƒ2 ef : prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ to_val e1 = None.
+Proof. intros [??? -> -> ?]; eauto using fill_not_val, values_head_stuck. Qed.
+Lemma atomic_not_val e : atomic e â†’ to_val e = None.
+Proof. destruct e; naive_solver. Qed.
+Lemma atomic_fill K e : atomic (fill K e) â†’ to_val e = None â†’ K = [].
 Proof.
-  intros (e' & Ïƒ' & ef & Hstep). destruct Hstep; simpl in *; reflexivity.
+  rewrite eq_None_not_Some.
+  destruct K as [|[]]; naive_solver eauto using fill_val.
 Qed.
-
-Definition stuck (e : expr) Ïƒ : Prop :=
-  âˆ€ K e', e = fill K e' â†’ ~reducible e' Ïƒ.
-
-Lemma values_stuck v Ïƒ :
-  stuck (v2e v) Ïƒ.
+Lemma atomic_head_step e1 Ïƒ1 e2 Ïƒ2 ef :
+  atomic e1 â†’ head_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ is_Some (to_val e2).
+Proof. destruct 2; simpl; rewrite ?to_of_val; naive_solver. Qed.
+Lemma atomic_step e1 Ïƒ1 e2 Ïƒ2 ef :
+  atomic e1 â†’ prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ is_Some (to_val e2).
 Proof.
-  intros ?? Heq.
-  edestruct (fill_value K) as [v' Hv'].
-  { by rewrite <-Heq, v2v. }
-  clear -Hv' => Hred. apply reducible_not_value in Hred.
-  destruct (e2v e'); discriminate.
+  intros Hatomic [K e1' e2' -> -> Hstep].
+  assert (K = []) as -> by eauto 10 using atomic_fill, values_head_stuck.
+  naive_solver eauto using atomic_head_step.
 Qed.
-
-Section step_by_value.
-(* 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 *)
-Lemma step_by_value {K K' e e' Ïƒ} :
-  fill K e = fill K' e' â†’
-  reducible e' Ïƒ â†’
-  e2v e = None â†’
-  âˆƒ K'', K' = comp_ctx K K''.
+Lemma head_ctx_step_val Ki e Ïƒ1 e2 Ïƒ2 ef :
+  head_step (ectx_item_fill Ki e) Ïƒ1 e2 Ïƒ2 ef â†’ is_Some (to_val e).
+Proof. destruct Ki; inversion_clear 1; simplify_option_equality; eauto. Qed.
+Lemma fill_item_inj Ki1 Ki2 e1 e2 :
+  to_val e1 = None â†’ to_val e2 = None â†’
+  ectx_item_fill Ki1 e1 = ectx_item_fill Ki2 e2 â†’ Ki1 = Ki2.
 Proof.
-  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).
-  Ltac bad_red   Hfill e' Hred := exfalso; destruct e';
-      try discriminate Hfill; [];
-      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;
-        repeat match goal with [ H : e2v _ = _ |- _ ] =>
-          erewrite H; clear H; simpl
-        end
-      ); eassumption || done).
-  Ltac good IH := intros; subst; 
-    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. 
-  revert K' Hfill; induction K=>K' /= Hfill;
-    first (now eexists; reflexivity);
-    (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.
-         Test whether the context als has the same head, and use the appropriate
-         tactic. *)
-      by match goal with
-      | [ |- exists x, ?C _ = ?C _ ] =>
-        case: Hfill; good IHK
-      | [ |- exists x, ?C _ _ = ?C _ _ ] =>
-        case: Hfill; good IHK
-      | [ |- exists x, ?C _ _ _ = ?C _ _ _ ] =>
-        case: Hfill; good IHK
-      | _ => case: Hfill; bad_fill
-      end).
+  destruct Ki1, Ki2; intros; try discriminate; simplify_equality';
+    repeat match goal with
+    | H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
+    end; auto.
 Qed.
-End step_by_value.
-
-(** Atomic expressions *)
-Definition atomic (e: expr) :=
-  match e with
-  | Alloc e => is_Some (e2v e)
-  | Load e => is_Some (e2v e)
-  | 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)
-  | _ => False
-  end.
-
-Lemma atomic_not_value e :
-  atomic e -> e2v e = None.
+(* 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'.
 Proof.
-  destruct e; simpl; contradiction || reflexivity.
+  intros Hfill Hred Hnval; revert K' Hfill.
+  induction K as [|Ki K IH]; simpl; intros K' Hfill; auto using prefix_of_nil.
+  destruct K' as [|Ki' K']; simplify_equality'.
+  { destruct (proj1 (eq_None_not_Some (to_val (fill K e1))));
+      eauto using fill_not_val, head_ctx_step_val. }
+  cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
+  eauto using fill_item_inj, values_head_stuck, fill_not_val.
 Qed.
-
-Lemma atomic_step e1 Ïƒ1 e2 Ïƒ2 ef :
-  atomic e1 â†’
-  prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
-  is_Some (e2v e2).
+Lemma alloc_fresh e v Ïƒ :
+  let l := fresh (dom _ Ïƒ) in
+  to_val e = Some v â†’ head_step (Alloc e) Ïƒ (Loc l) (<[l:=v]>Ïƒ) None.
 Proof.
-  destruct e1; simpl; intros Hatomic Hstep; inversion Hstep;
-    try contradiction Hatomic; rewrite ?v2v /=; eexists; reflexivity.
+  by intros; apply AllocS, (not_elem_of_dom (D:=gset positive)), is_fresh.
 Qed.
-
-(* Atomics must not contain evaluation positions. *)
-Lemma atomic_fill e K :
-  atomic (fill K e) â†’
-  e2v e = None â†’
-  K = EmptyCtx.
+End heap_lang.
+
+(** Language *)
+Program Canonical Structure heap_lang : language := {|
+  expr := heap_lang.expr; val := heap_lang.val; state := heap_lang.state;
+  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,
+  heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
+Global Instance heap_lang_ctx : CtxLanguage heap_lang heap_lang.ectx.
 Proof.
-  destruct K; simpl; first reflexivity; unfold is_Some; intros Hatomic Hnval;
-    exfalso; try assumption;
-    try (destruct_conjs; eapply fill_not_value2; eassumption).
+  split.
+  * eauto using heap_lang.fill_not_val.
+  * intros K ????? [K' e1' e2' Heq1 Heq2 Hstep].
+    by exists (K ++ K') e1' e2'; rewrite ?heap_lang.fill_app ?Heq1 ?Heq2.
+  * intros K e1 Ïƒ1 e2 Ïƒ2 ? Hnval [K'' e1'' e2'' Heq1 -> Hstep].
+    destruct (heap_lang.step_by_val
+      K K'' e1 e1'' Ïƒ1 e2'' Ïƒ2 ef) as [K' ->]; eauto.
+    rewrite heap_lang.fill_app in Heq1; apply (injective _) in Heq1.
+    exists (fill K' e2''); rewrite heap_lang.fill_app; split; auto.
+    econstructor; eauto.
 Qed.
-
-(** Instantiate the Iris language interface. This closes reduction under
-    evaluation contexts.
-    We could potentially make this a generic construction. *)
-Section Language.
-
-  Definition ectx_step e1 Ïƒ1 e2 Ïƒ2 (ef: option expr) :=
-    âˆƒ K e1' e2', e1 = fill K e1' âˆ§ e2 = fill K e2' âˆ§
-                 prim_step e1' Ïƒ1 e2' Ïƒ2 ef.
-  Program Canonical Structure heap_lang : language := {|
-    language.expr := expr;
-    language.val := value;
-    language.state := state;
-    of_val := v2e;
-    to_val := e2v;
-    language.atomic := atomic;
-    language.prim_step := ectx_step;
-    to_of_val := v2v;
-    of_to_val := e2e;
-    language.atomic_not_value := atomic_not_value
-  |}.
-  Next Obligation.
-    intros e1 Ïƒ1 e2 Ïƒ2 ef (K & e1' & e2' & He1 & He2 & Hstep). subst e1 e2.
-    eapply fill_not_value. eapply reducible_not_value. do 3 eexists; eassumption.
-  Qed.
-  Next Obligation.
-    intros ? ? ? ? ? Hatomic (K & e1' & e2' & Heq1 & Heq2 & Hstep).
-    subst. move: (Hatomic). rewrite (atomic_fill e1' K).
-    - rewrite !fill_empty. eauto using atomic_step.
-    - assumption.
-    - clear Hatomic. eapply reducible_not_value. do 3 eexists; eassumption.
-  Qed.
-
-  Global Instance heap_lang_fill : Fill ectx expr := fill.
-  Global Instance heap_lang_ctx : CtxLanguage heap_lang ectx.
-  Proof.
-    split.
-    - intros K ? Hnval. by eapply fill_not_value.
-    - intros K ? ? ? ? ? (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
-      exists (comp_ctx K K'), e1', e2'. rewrite -!fill_comp Heq1 Heq2.
-      split; last split; reflexivity || assumption.
-    - intros K ? ? ? ? ? Hnval (K'' & e1'' & e2'' & Heq1 & Heq2 & Hstep).
-      destruct (step_by_value (Ïƒ:=Ïƒ1) Heq1) as [K' HeqK].
-      + do 3 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.
-  Qed.
-
-  Lemma prim_ectx_step e1 Ïƒ1 e2 Ïƒ2 ef :
-    reducible e1 Ïƒ1 â†’
-    ectx_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
-    prim_step e1 Ïƒ1 e2 Ïƒ2 ef.
-  Proof.
-    intros Hred (K' & e1' & e2' & Heq1 & Heq2 & Hstep).
-    destruct (@step_by_value K' EmptyCtx e1' e1 Ïƒ1) as [K'' [HK' HK'']%comp_empty].
-    - by rewrite fill_empty.
-    - done.
-    - eapply reducible_not_value. do 3 eexists; eassumption.
-    - subst K' K'' e1 e2. by rewrite !fill_empty.
-  Qed.
-
-End Language.
diff --git a/barrier/heap_lang_tactics.v b/barrier/heap_lang_tactics.v
new file mode 100644
index 000000000..5a3f3d081
--- /dev/null
+++ b/barrier/heap_lang_tactics.v
@@ -0,0 +1,72 @@
+Require Export barrier.heap_lang.
+Require Import prelude.fin_maps.
+Import heap_lang.
+
+Ltac inv_step :=
+  repeat match goal with
+  | _ => progress simplify_map_equality' (* simplify memory stuff *)
+  | H : to_val _ = Some _ |- _ => apply of_to_val in H
+  | H : context [to_val (of_val _)] |- _ => rewrite to_of_val in H
+  | H : prim_step _ _ _ _ _ |- _ => destruct H; subst
+  | H : _ = fill ?K ?e |- _ =>
+     destruct K as [|[]];
+     simpl in H; first [subst e|discriminate H|injection' H]
+     (* ensure that we make progress for each subgoal *)
+  | H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
+    apply values_head_stuck, (fill_not_val K) in H;
+    by rewrite -Hv to_of_val in H (* maybe use a helper lemma here? *)
+  | 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.
+
+Ltac reshape_expr e tac :=
+  let rec go K e :=
+  match e with
+  | _ => tac (reverse K) e
+  | App ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (AppRCtx v1 :: K) e2 | _ => go (AppLCtx e2 :: K) e1
+     end
+  | Plus ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (PlusRCtx v1 :: K) e2 | _ => go (PlusLCtx e2 :: K) e1
+     end
+  | Le ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (LeRCtx v1 :: K) e2 | _ => go (LeLCtx e2 :: K) e1
+     end
+  | Pair ?e1 ?e2 =>
+     lazymatch e1 with
+     | of_val ?v1 => go (PairRCtx v1 :: K) e2 | _ => go (PairLCtx e2 :: K) e1
+     end
+  | Fst ?e => go (FstCtx :: K) e
+  | Snd ?e => go (SndCtx :: K) e
+  | InjL ?e => go (InjLCtx :: K) e
+  | InjR ?e => go (InjRCtx :: K) e
+  | Case ?e0 ?e1 ?e2 => go (CaseCtx e1 e2 :: K) e0
+  | Alloc ?e => go (AllocCtx :: K) e
+  | Load ?e => go (LoadCtx :: K) e
+  | Store ?e1 ?e2 => go (StoreLCtx e2 :: K) e1 || go (StoreRCtx e1 :: K) e2
+  | Cas ?e0 ?e1 ?e2 =>
+     lazymatch e0 with
+     | of_val ?v0 =>
+        lazymatch e1 with
+        | of_val ?v1 => go (CasRCtx v0 v1 :: K) e2
+        | _ => go (CasMCtx v0 e2 :: K) e1
+        end
+     | _ => go (CasLCtx e1 e2 :: K) e0
+     end
+  end in go (@nil ectx_item) e.
+
+Ltac do_step tac :=
+  try match goal with |- reducible _ _ => eexists _, _, _ end;
+  simpl;
+  match goal with
+  | |- prim_step ?e1 ?Ïƒ1 ?e2 ?Ïƒ2 ?ef =>
+     reshape_expr e1 ltac:(fun K e1' =>
+       eapply Ectx_step with K e1' _); [reflexivity|reflexivity|];
+       first [apply alloc_fresh|econstructor];
+       rewrite ?to_of_val; tac; fail
+  end.
diff --git a/barrier/lifting.v b/barrier/lifting.v
index 44bb7d593..5faa56d5b 100644
--- a/barrier/lifting.v
+++ b/barrier/lifting.v
@@ -1,19 +1,21 @@
 Require Import prelude.gmap iris.lifting.
-Require Export iris.weakestpre barrier.heap_lang.
+Require Export iris.weakestpre barrier.heap_lang_tactics.
 Import uPred.
+Import heap_lang.
+Local Hint Extern 0 (reducible _ _) => do_step ltac:(eauto 2).
 
 Section lifting.
 Context {Î£ : iFunctor}.
 Implicit Types P : iProp heap_lang Î£.
-Implicit Types Q : val heap_lang â†’ iProp heap_lang Î£.
+Implicit Types Q : val â†’ iProp heap_lang Î£.
+Implicit Types K : ectx.
 
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
-  wp E e (Î» v, wp E (fill K (v2e v)) Q) âŠ‘ wp E (fill K e) Q.
+  wp E e (Î» v, wp E (fill K (of_val v)) Q) âŠ‘ wp E (fill K e) Q.
 Proof. apply wp_bind. Qed.
 
 (** Base axioms for core primitives of the language: Stateful reductions. *)
-
 Lemma wp_lift_step E1 E2 (Ï† : expr â†’ state â†’ Prop) Q e1 Ïƒ1 :
   E1 âŠ† E2 â†’ to_val e1 = None â†’
   reducible e1 Ïƒ1 â†’
@@ -23,303 +25,176 @@ Lemma wp_lift_step E1 E2 (Ï† : expr â†’ state â†’ Prop) Q e1 Ïƒ1 :
   âŠ‘ wp E2 e1 Q.
 Proof.
   intros ? He Hsafe Hstep.
-  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
-  etransitivity; last eapply wp_lift_step with (Ïƒ2 := Ïƒ1)
-    (Ï†0 := Î» e' Ïƒ' ef, ef = None âˆ§ Ï† e' Ïƒ'); last first.
-  - intros e2 Ïƒ2 ef Hstep'%prim_ectx_step; last done.
-    by apply Hstep.
-  - destruct Hsafe as (e' & Ïƒ' & ? & ?).
-    do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); eassumption.
-  - done.
-  - eassumption.
-  - apply pvs_mono. apply sep_mono; first done.
-    apply later_mono. apply forall_mono=>e2. apply forall_mono=>Ïƒ2.
-    apply forall_intro=>ef. apply wand_intro_l.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l; move=>[-> HÏ†]. eapply const_intro_l; first eexact HÏ†.
-    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
-    apply pvs_mono. rewrite right_id. done.
+  rewrite -(wp_lift_step E1 E2 (Î» e' Ïƒ' ef, ef = None âˆ§ Ï† e' Ïƒ') _ _ Ïƒ1) //.
+  apply pvs_mono, sep_mono, later_mono; first done.
+  apply forall_mono=>e2; apply forall_mono=>Ïƒ2.
+  apply forall_intro=>ef; apply wand_intro_l.
+  rewrite always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ?] /=.
+  by rewrite const_equiv // left_id wand_elim_r right_id.
 Qed.
 
 (* TODO RJ: Figure out some better way to make the
    postcondition a predicate over a *location* *)
 Lemma wp_alloc_pst E Ïƒ e v Q :
-  e2v e = Some v â†’
-  (ownP Ïƒ â˜… â–·(âˆ€ l, â– (Ïƒ !! l = None) âˆ§ ownP (<[l:=v]>Ïƒ) -â˜… Q (LocV l)))
+  to_val e = Some v â†’
+  (ownP Ïƒ â˜… â–· (âˆ€ l, â– (Ïƒ !! l = None) âˆ§ ownP (<[l:=v]>Ïƒ) -â˜… Q (LocV l)))
        âŠ‘ wp E (Alloc e) Q.
 Proof.
-  (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
-  intros Hvl. etransitivity; last eapply wp_lift_step with (Ïƒ1 := Ïƒ)
-    (Ï† := Î» e' Ïƒ', âˆƒ l, e' = Loc l âˆ§ Ïƒ' = <[l:=v]>Ïƒ âˆ§ Ïƒ !! l = None);
-    last first.
-  - intros e2 Ïƒ2 ef Hstep. inversion_clear Hstep. split; first done.
-    rewrite Hv in Hvl. inversion_clear Hvl.
-    eexists; split_ands; done.
-  - set (l := fresh $ dom (gset loc) Ïƒ).
-    exists (Loc l), ((<[l:=v]>)Ïƒ), None. eapply AllocS; first done.
-    apply (not_elem_of_dom (D := gset loc)). apply is_fresh.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro. apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>Ïƒ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [l [-> [-> Hl]]].
-    rewrite (forall_elim l). eapply const_intro_l; first eexact Hl.
-    rewrite always_and_sep_l' associative -always_and_sep_l' wand_elim_r.
-    rewrite -wp_value'; done.
+  intros; set (Ï† e' Ïƒ' := âˆƒ l, e' = Loc l âˆ§ Ïƒ' = <[l:=v]>Ïƒ âˆ§ Ïƒ !! l = None).
+  rewrite -(wp_lift_step E E Ï† _ _  Ïƒ) // /Ï†; last by intros; inv_step; eauto.
+  rewrite -pvs_intro. apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2; apply forall_intro=>Ïƒ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[l [-> [-> ?]]].
+  by rewrite (forall_elim l) const_equiv // left_id wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_load_pst E Ïƒ l v Q :
   Ïƒ !! l = Some v â†’
-  (ownP Ïƒ â˜… â–·(ownP Ïƒ -â˜… Q v)) âŠ‘ wp E (Load (Loc l)) Q.
+  (ownP Ïƒ â˜… â–· (ownP Ïƒ -â˜… Q v)) âŠ‘ wp E (Load (Loc l)) Q.
 Proof.
-  intros Hl. etransitivity; last eapply wp_lift_step with (Ïƒ1 := Ïƒ)
-    (Ï† := Î» e' Ïƒ', e' = v2e v âˆ§ Ïƒ' = Ïƒ); last first.
-  - intros e2 Ïƒ2 ef Hstep. move: Hl. inversion_clear Hstep=>{Ïƒ}.
-    rewrite Hlookup. case=>->. done.
-  - do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>Ïƒ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value.
+  intros; rewrite -(wp_lift_step E E (Î» e' Ïƒ', e' = of_val v âˆ§ Ïƒ' = Ïƒ)) //;
+    last by intros; inv_step; eauto.
+  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2; apply forall_intro=>Ïƒ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value.
 Qed.
-
 Lemma wp_store_pst E Ïƒ l e v v' Q :
-  e2v e = Some v â†’
-  Ïƒ !! l = Some v' â†’
-  (ownP Ïƒ â˜… â–·(ownP (<[l:=v]>Ïƒ) -â˜… Q LitUnitV)) âŠ‘ wp E (Store (Loc l) e) Q.
+  to_val e = Some v â†’ Ïƒ !! l = Some v' â†’
+  (ownP Ïƒ â˜… â–· (ownP (<[l:=v]>Ïƒ) -â˜… Q LitUnitV)) âŠ‘ wp E (Store (Loc l) e) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (Ïƒ1 := Ïƒ)
-    (Ï† := Î» e' Ïƒ', e' = LitUnit âˆ§ Ïƒ' = <[l:=v]>Ïƒ); last first.
-  - intros e2 Ïƒ2 ef Hstep. move: Hl. inversion_clear Hstep=>{Ïƒ2}.
-    rewrite Hvl in Hv. inversion_clear Hv. done.
-  - do 3 eexists. eapply StoreS; last (eexists; eassumption). eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2. apply forall_intro=>Ïƒ2.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros.
+  rewrite -(wp_lift_step E E (Î» e' Ïƒ', e' = LitUnit âˆ§ Ïƒ' = <[l:=v]>Ïƒ)) //;
+    last by intros; inv_step; eauto.
+  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2; apply forall_intro=>Ïƒ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_cas_fail_pst E Ïƒ l e1 v1 e2 v2 v' Q :
-  e2v e1 = Some v1 â†’ e2v e2 = Some v2 â†’
-  Ïƒ !! l = Some v' â†’ v' <> v1 â†’
-  (ownP Ïƒ â˜… â–·(ownP Ïƒ -â˜… Q LitFalseV)) âŠ‘ wp E (Cas (Loc l) e1 e2) Q.
+  to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’ Ïƒ !! l = Some v' â†’ v' â‰  v1 â†’
+  (ownP Ïƒ â˜… â–· (ownP Ïƒ -â˜… Q LitFalseV)) âŠ‘ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (Ïƒ1 := Ïƒ)
-    (Ï† := Î» e' Ïƒ', e' = LitFalse âˆ§ Ïƒ' = Ïƒ) (E1:=E); auto; last first.
-  - by inversion_clear 1; simplify_map_equality.
-  - do 3 eexists; econstructor; eauto.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2'. apply forall_intro=>Ïƒ2'.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros; rewrite -(wp_lift_step E E (Î» e' Ïƒ', e' = LitFalse âˆ§ Ïƒ' = Ïƒ)) //;
+    last by intros; inv_step; eauto.
+  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2'; apply forall_intro=>Ïƒ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
-
 Lemma wp_cas_suc_pst E Ïƒ l e1 v1 e2 v2 Q :
-  e2v e1 = Some v1 â†’ e2v e2 = Some v2 â†’
-  Ïƒ !! l = Some v1 â†’
-  (ownP Ïƒ â˜… â–·(ownP (<[l:=v2]>Ïƒ) -â˜… Q LitTrueV)) âŠ‘ wp E (Cas (Loc l) e1 e2) Q.
+  to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’ Ïƒ !! l = Some v1 â†’
+  (ownP Ïƒ â˜… â–· (ownP (<[l:=v2]>Ïƒ) -â˜… Q LitTrueV)) âŠ‘ wp E (Cas (Loc l) e1 e2) Q.
 Proof.
-  intros Hvl Hl. etransitivity; last eapply wp_lift_step with (Ïƒ1 := Ïƒ)
-    (Ï† := Î» e' Ïƒ', e' = LitTrue âˆ§ Ïƒ' = <[l:=v2]>Ïƒ); last first.
-  - intros e2' Ïƒ2' ef Hstep. move:H. inversion_clear Hstep=>H.
-    (* FIXME this rewriting is rather ugly. *)
-    + exfalso. rewrite H in Hlookup. case:Hlookup=>?; subst vl.
-      rewrite Hvl in Hv1. case:Hv1=>?; subst v1. done.
-    + rewrite H in Hlookup. case:Hlookup=>?; subst v1.
-      rewrite Hl in Hv2. case:Hv2=>?; subst v2. done.
-  - do 3 eexists. eapply CasSucS; eassumption.
-  - reflexivity.
-  - reflexivity.
-  - rewrite -pvs_intro.
-    apply sep_mono; first done. apply later_mono.
-    apply forall_intro=>e2'. apply forall_intro=>Ïƒ2'.
-    apply wand_intro_l. rewrite -pvs_intro.
-    rewrite always_and_sep_l' -associative -always_and_sep_l'.
-    apply const_elim_l. intros [-> ->].
-    by rewrite wand_elim_r -wp_value'.
+  intros.
+  rewrite -(wp_lift_step E E (Î» e' Ïƒ', e' = LitTrue âˆ§ Ïƒ' = <[l:=v2]>Ïƒ)) //;
+    last by intros; inv_step; eauto.
+  rewrite -pvs_intro; apply sep_mono, later_mono; first done.
+  apply forall_intro=>e2'; apply forall_intro=>Ïƒ2; apply wand_intro_l.
+  rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
+  apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
-
 Lemma wp_fork E e :
-  â–· wp coPset_all e (Î» _, True : iProp heap_lang Î£)
-  âŠ‘ wp E (Fork e) (Î» v, â– (v = LitUnitV)).
+  â–· wp (Î£:=Î£) coPset_all e (Î» _, True) âŠ‘ wp E (Fork e) (Î» v, â– (v = LitUnitV)).
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e' ef, e' = LitUnit âˆ§ ef = Some e);
-    last first.
-  - intros Ïƒ1 e2 Ïƒ2 ef Hstep%prim_ectx_step; last first.
-    { do 3 eexists. eapply ForkS. }
-    inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); [].
-    eapply ForkS.
-  - reflexivity.
-  - apply later_mono.
-    apply forall_intro=>e2; apply forall_intro=>ef.
-    apply impl_intro_l, const_elim_l=>-[-> ->] /=; apply sep_intro_True_l; auto.
-    by rewrite -wp_value' //; apply const_intro.
+  rewrite -(wp_lift_pure_step E (Î» e' ef, e' = LitUnit âˆ§ ef = Some e)) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2; apply forall_intro=>ef.
+  apply impl_intro_l, const_elim_l=>-[-> ->] /=.
+  apply sep_intro_True_l; last done.
+  by rewrite -wp_value' //; apply const_intro.
 Qed.
-
 Lemma wp_lift_pure_step E (Ï† : expr â†’ Prop) Q e1 :
   to_val e1 = None â†’
   (âˆ€ Ïƒ1, reducible e1 Ïƒ1) â†’
   (âˆ€ Ïƒ1 e2 Ïƒ2 ef, prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’ Ïƒ1 = Ïƒ2 âˆ§ ef = None âˆ§ Ï† e2) â†’
   (â–· âˆ€ e2, â–  Ï† e2 â†’ wp E e2 Q) âŠ‘ wp E e1 Q.
 Proof.
-  intros He Hsafe Hstep.
-  (* RJ: working around https://coq.inria.fr/bugs/show_bug.cgi?id=4536 *)
-  etransitivity; last eapply wp_lift_pure_step with
-    (Ï†0 := Î» e' ef, ef = None âˆ§ Ï† e'); last first.
-  - intros Ïƒ1 e2 Ïƒ2 ef Hstep'%prim_ectx_step; last done.
-    by apply Hstep.
-  - intros Ïƒ1. destruct (Hsafe Ïƒ1) as (e' & Ïƒ' & ? & ?).
-    do 3 eexists. exists EmptyCtx. do 2 eexists.
-    split_ands; try (by rewrite fill_empty); eassumption.
-  - done.
-  - apply later_mono. apply forall_mono=>e2. apply forall_intro=>ef.
-    apply impl_intro_l. apply const_elim_l; move=>[-> HÏ†].
-    eapply const_intro_l; first eexact HÏ†. rewrite impl_elim_r.
-    rewrite right_id. done.
+  intros; rewrite -(wp_lift_pure_step E (Î» e' ef, ef = None âˆ§ Ï† e')) //=.
+  apply later_mono, forall_mono=>e2; apply forall_intro=>ef.
+  apply impl_intro_l, const_elim_l=>-[-> ?] /=.
+  by rewrite const_equiv // left_id right_id.
 Qed.
-
 Lemma wp_rec E ef e v Q :
-  e2v e = Some v â†’
-  â–·wp E ef.[Rec ef, e /] Q âŠ‘ wp E (App (Rec ef) e) Q.
+  to_val e = Some v â†’
+  â–· wp E ef.[Rec ef, e /] Q âŠ‘ wp E (App (Rec ef) e) Q.
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e', e' = ef.[Rec ef, e /]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. eapply BetaS; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->. done.
+  intros; rewrite -(wp_lift_pure_step E (Î» e', e' = ef.[Rec ef, e /])
+    Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto.
+  by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
 Qed.
-
 Lemma wp_plus n1 n2 E Q :
-  â–·Q (LitNatV (n1 + n2)) âŠ‘ wp E (Plus (LitNat n1) (LitNat n2)) Q.
+  â–· Q (LitNatV (n1 + n2)) âŠ‘ wp E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
-  etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e', e' = LitNat (n1 + n2)); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  rewrite -(wp_lift_pure_step E (Î» e', e' = LitNat (n1 + n2))) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
 Lemma wp_le_true n1 n2 E Q :
   n1 â‰¤ n2 â†’
-  â–·Q LitTrueV âŠ‘ wp E (Le (LitNat n1) (LitNat n2)) Q.
+  â–· Q LitTrueV âŠ‘ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros Hle. etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e', e' = LitTrue); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; first done.
-    exfalso. eapply le_not_gt with (n := n1); eassumption.
-  - intros ?. do 3 eexists. econstructor; done.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  intros; rewrite -(wp_lift_pure_step E (Î» e', e' = LitTrue)) //=;
+    last by intros; inv_step; eauto with lia.
+  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
 Lemma wp_le_false n1 n2 E Q :
   n1 > n2 â†’
-  â–·Q LitFalseV âŠ‘ wp E (Le (LitNat n1) (LitNat n2)) Q.
+  â–· Q LitFalseV âŠ‘ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros Hle. etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e', e' = LitFalse); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; last done.
-    exfalso. eapply le_not_gt with (n := n1); eassumption.
-  - intros ?. do 3 eexists. econstructor; done.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last reflexivity; done.
+  intros; rewrite -(wp_lift_pure_step E (Î» e', e' = LitFalse)) //=;
+    last by intros; inv_step; eauto with lia.
+  apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
 Lemma wp_fst e1 v1 e2 v2 E Q :
-  e2v e1 = Some v1 â†’ e2v e2 = Some v2 â†’
+  to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
   â–·Q v1 âŠ‘ wp E (Fst (Pair e1 e2)) Q.
 Proof.
-  intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e', e' = e1); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last eassumption; done.
+  intros; rewrite -(wp_lift_pure_step E (Î» e', e' = e1)) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
 Lemma wp_snd e1 v1 e2 v2 E Q :
-  e2v e1 = Some v1 â†’ e2v e2 = Some v2 â†’
-  â–·Q v2 âŠ‘ wp E (Snd (Pair e1 e2)) Q.
+  to_val e1 = Some v1 â†’ to_val e2 = Some v2 â†’
+  â–· Q v2 âŠ‘ wp E (Snd (Pair e1 e2)) Q.
 Proof.
-  intros Hv1 Hv2. etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e', e' = e2); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    apply const_elim_l=>->.
-    rewrite -wp_value'; last eassumption; done.
+  intros; rewrite -(wp_lift_pure_step E (Î» e', e' = e2)) //=;
+    last by intros; inv_step; eauto.
+  apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
+  by rewrite -wp_value'.
 Qed.
-
 Lemma wp_case_inl e0 v0 e1 e2 E Q :
-  e2v e0 = Some v0 â†’
-  â–·wp E e1.[e0/] Q âŠ‘ wp E (Case (InjL e0) e1 e2) Q.
+  to_val e0 = Some v0 â†’
+  â–· wp E e1.[e0/] Q âŠ‘ wp E (Case (InjL e0) e1 e2) Q.
 Proof.
-  intros Hv0. etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e', e' = e1.[e0/]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e1'. apply impl_intro_l.
-    by apply const_elim_l=>->.
+  intros; rewrite -(wp_lift_pure_step E (Î» e', e' = e1.[e0/]) _
+    (Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto.
+  by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
 Qed.
-
 Lemma wp_case_inr e0 v0 e1 e2 E Q :
-  e2v e0 = Some v0 â†’
-  â–·wp E e2.[e0/] Q âŠ‘ wp E (Case (InjR e0) e1 e2) Q.
+  to_val e0 = Some v0 â†’
+  â–· wp E e2.[e0/] Q âŠ‘ wp E (Case (InjR e0) e1 e2) Q.
 Proof.
-  intros Hv0. etransitivity; last eapply wp_lift_pure_step with
-    (Ï† := Î» e', e' = e2.[e0/]); last first.
-  - intros ? ? ? ? Hstep. inversion_clear Hstep; done.
-  - intros ?. do 3 eexists. econstructor; eassumption.
-  - reflexivity.
-  - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
-    by apply const_elim_l=>->.
+  intros; rewrite -(wp_lift_pure_step E (Î» e', e' = e2.[e0/]) _
+    (Case (InjR e0) e1 e2)) //=; last by intros; inv_step; eauto.
+  by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
 Qed.
 
 (** Some derived stateless axioms *)
-
 Lemma wp_le n1 n2 E P Q :
-  (n1 â‰¤ n2 â†’ P âŠ‘ â–·Q LitTrueV) â†’
-  (n1 > n2 â†’ P âŠ‘ â–·Q LitFalseV) â†’
+  (n1 â‰¤ n2 â†’ P âŠ‘ â–· Q LitTrueV) â†’
+  (n1 > n2 â†’ P âŠ‘ â–· Q LitFalseV) â†’
   P âŠ‘ wp E (Le (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros HPle HPgt.
-  assert (Decision (n1 â‰¤ n2)) as Hn12 by apply _.
-  destruct Hn12 as [Hle|Hgt].
-  - rewrite -wp_le_true; auto.
-  - assert (n1 > n2) by omega. rewrite -wp_le_false; auto.
+  intros; destruct (decide (n1 â‰¤ n2)).
+  * rewrite -wp_le_true; auto.
+  * rewrite -wp_le_false; auto with lia.
 Qed.
 End lifting.
diff --git a/barrier/sugar.v b/barrier/sugar.v
index d8fe3920f..6c39d0c19 100644
--- a/barrier/sugar.v
+++ b/barrier/sugar.v
@@ -1,5 +1,6 @@
 Require Export barrier.heap_lang barrier.lifting.
 Import uPred.
+Import heap_lang.
 
 (** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
 Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
@@ -13,67 +14,52 @@ Definition Eq e1 e2 :=
 
 Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
 
-Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1.
-Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]).
+Definition LetCtx (e2 : {bind expr}) := AppRCtx (LamV e2).
+Definition SeqCtx (e2 : expr) := LetCtx (e2.[ren(+1)]).
 
 Section suger.
 Context {Î£ : iFunctor}.
 Implicit Types P : iProp heap_lang Î£.
-Implicit Types Q : val heap_lang â†’ iProp heap_lang Î£.
+Implicit Types Q : val â†’ iProp heap_lang Î£.
 
 (** Proof rules for the sugar *)
 Lemma wp_lam E ef e v Q :
-  e2v e = Some v â†’ â–·wp E ef.[e/] Q âŠ‘ wp E (App (Lam ef) e) Q.
+  to_val e = Some v â†’ â–· wp E ef.[e/] Q âŠ‘ wp E (App (Lam ef) e) Q.
 Proof.
   intros Hv. rewrite -wp_rec; last eassumption.
   (* RJ: This pulls in functional extensionality. If that bothers us, we have
      to talk to the Autosubst guys. *)
   by asimpl.
 Qed.
-
 Lemma wp_let e1 e2 E Q :
-  wp E e1 (Î» v, â–·wp E (e2.[v2e v/]) Q) âŠ‘ wp E (Let e1 e2) Q.
+  wp E e1 (Î» v, â–·wp E (e2.[of_val v/]) Q) âŠ‘ wp E (Let e1 e2) Q.
 Proof.
-  rewrite -(wp_bind (LetCtx EmptyCtx e2)). apply wp_mono=>v.
-  rewrite -wp_lam //. by rewrite v2v.
+  rewrite -(wp_bind [LetCtx e2]). apply wp_mono=>v.
+  by rewrite -wp_lam //= to_of_val.
 Qed.
-
-Lemma wp_if_true e1 e2 E Q :
-  â–·wp E e1 Q âŠ‘ wp E (If LitTrue e1 e2) Q.
-Proof.
-  rewrite -wp_case_inl //. by asimpl.
-Qed.
-
-Lemma wp_if_false e1 e2 E Q :
-  â–·wp E e2 Q âŠ‘ wp E (If LitFalse e1 e2) Q.
-Proof.
-  rewrite -wp_case_inr //. by asimpl.
-Qed.
-
+Lemma wp_if_true e1 e2 E Q : â–· wp E e1 Q âŠ‘ wp E (If LitTrue e1 e2) Q.
+Proof. rewrite -wp_case_inl //. by asimpl. Qed.
+Lemma wp_if_false e1 e2 E Q : â–· wp E e2 Q âŠ‘ wp E (If LitFalse e1 e2) Q.
+Proof. rewrite -wp_case_inr //. by asimpl. Qed.
 Lemma wp_lt n1 n2 E P Q :
-  (n1 < n2 â†’ P âŠ‘ â–·Q LitTrueV) â†’
-  (n1 â‰¥ n2 â†’ P âŠ‘ â–·Q LitFalseV) â†’
+  (n1 < n2 â†’ P âŠ‘ â–· Q LitTrueV) â†’
+  (n1 â‰¥ n2 â†’ P âŠ‘ â–· Q LitFalseV) â†’
   P âŠ‘ wp E (Lt (LitNat n1) (LitNat n2)) Q.
 Proof.
-  intros HPlt HPge.
-  rewrite -(wp_bind (LeLCtx EmptyCtx _)) -wp_plus -later_intro. simpl.
-  apply wp_le; intros; [apply HPlt|apply HPge]; omega.
+  intros; rewrite -(wp_bind [LeLCtx _]) -wp_plus -later_intro /=.
+  auto using wp_le with lia.
 Qed.
-
 Lemma wp_eq n1 n2 E P Q :
-  (n1 = n2 â†’ P âŠ‘ â–·Q LitTrueV) â†’
-  (n1 â‰  n2 â†’ P âŠ‘ â–·Q LitFalseV) â†’
+  (n1 = n2 â†’ P âŠ‘ â–· Q LitTrueV) â†’
+  (n1 â‰  n2 â†’ P âŠ‘ â–· Q LitFalseV) â†’
   P âŠ‘ wp E (Eq (LitNat n1) (LitNat n2)) Q.
 Proof.
   intros HPeq HPne.
-  rewrite -wp_let -wp_value' // -later_intro. asimpl.
-  rewrite -wp_rec //. asimpl.
-  rewrite -(wp_bind (CaseCtx EmptyCtx _ _)) -later_intro.
-  apply wp_le; intros Hn12.
-  - asimpl. rewrite -wp_case_inl // -!later_intro. apply wp_le; intros Hn12'.
-    + apply HPeq; omega.
-    + apply HPne; omega.
-  - asimpl. rewrite -wp_case_inr // -later_intro -wp_value' //.
-    apply HPne; omega.
+  rewrite -wp_let -wp_value' // -later_intro; asimpl.
+  rewrite -wp_rec //; asimpl.
+  rewrite -(wp_bind [CaseCtx _ _]) -later_intro; asimpl.
+  apply wp_le; intros; asimpl.
+  * rewrite -wp_case_inl // -!later_intro. apply wp_le; auto with lia.
+  * rewrite -wp_case_inr // -later_intro -wp_value' //; auto with lia.
 Qed.
 End suger.
diff --git a/barrier/tests.v b/barrier/tests.v
index fa6c63b04..3a33c7505 100644
--- a/barrier/tests.v
+++ b/barrier/tests.v
@@ -1,34 +1,26 @@
 (** This file is essentially a bunch of testcases. *)
 Require Import modures.logic.
 Require Import barrier.lifting barrier.sugar.
+Import heap_lang.
 Import uPred.
 
 Module LangTests.
-  Definition add :=  Plus (LitNat 21) (LitNat 21).
+  Definition add := Plus (LitNat 21) (LitNat 21).
   Goal âˆ€ Ïƒ, prim_step add Ïƒ (LitNat 42) Ïƒ None.
-  Proof.
-    constructor.
-  Qed.
-
+  Proof. intros; do_step done. Qed.
   Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
   Definition rec_app := App rec (LitNat 0).
   Goal âˆ€ Ïƒ, prim_step rec_app Ïƒ rec_app Ïƒ None.
-  Proof.
-    move=>?. eapply BetaS.
-    reflexivity.
-  Qed.
-
+  Proof. intros; do_step done. Qed.
   Definition lam := Lam (Plus (Var 0) (LitNat 21)).
   Goal âˆ€ Ïƒ, prim_step (App lam (LitNat 21)) Ïƒ add Ïƒ None.
-  Proof.
-    move=>?. eapply BetaS. reflexivity.
-  Qed.
+  Proof. intros; do_step done. Qed.
 End LangTests.
 
 Module LiftingTests.
   Context {Î£ : iFunctor}.
   Implicit Types P : iProp heap_lang Î£.
-  Implicit Types Q : val heap_lang â†’ iProp heap_lang Î£.
+  Implicit Types Q : val â†’ iProp heap_lang Î£.
 
   (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
   Definition e3 := Load (Var 0).
@@ -42,26 +34,24 @@ Module LiftingTests.
     rewrite -later_intro. apply forall_intro=>l.
     apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
     rewrite -later_intro. asimpl.
-    rewrite -(wp_bind (SeqCtx EmptyCtx (Load (Loc _)))).
-    rewrite -(wp_bind (StoreRCtx (LocV _) EmptyCtx)).
-    rewrite -(wp_bind (PlusLCtx EmptyCtx _)).
+    rewrite -(wp_bind [SeqCtx (Load (Loc _))]).
+    rewrite -(wp_bind [StoreRCtx (LocV _)]).
+    rewrite -(wp_bind [PlusLCtx _]).
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
+    { by rewrite lookup_insert. } (* RJ TODO: figure out why apply and eapply fail. *)
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -wp_plus -later_intro.
     rewrite -wp_store_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. }
-    { reflexivity. }
+    { by rewrite lookup_insert. }
+    { done. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     rewrite -wp_lam // -later_intro. asimpl.
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
-    { apply: lookup_insert. }
+    { by rewrite lookup_insert. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     by apply const_intro.
   Qed.
 
-  Import Nat.
-
   Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2)
                                       (App f Sn1)
                                       n1.
@@ -85,10 +75,10 @@ Module LiftingTests.
     (* Go on. *)
     rewrite -(wp_let _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
     rewrite -wp_plus. asimpl.
-    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
-    rewrite -!later_intro. simpl.
+    rewrite -(wp_bind [CaseCtx _ _]).
+    rewrite -!later_intro /=.
     apply wp_lt; intros Hn12.
-    - (* TODO RJ: It would be better if we could use wp_if_true here
+    * (* TODO RJ: It would be better if we could use wp_if_true here
          (and below). But we cannot, because the substitutions in there
          got already unfolded. *)
       rewrite -wp_case_inl //.
@@ -97,30 +87,29 @@ Module LiftingTests.
       eapply impl_elim; first by eapply and_elim_l. apply and_intro.
       + apply const_intro; omega.
       + by rewrite !and_elim_r.
-    - rewrite -wp_case_inr //.
+    * rewrite -wp_case_inr //.
       rewrite -!later_intro -wp_value' //.
       rewrite and_elim_r. apply const_elim_l=>Hle.
-      assert (Heq: n1 = pred n2) by omega. by subst n1.
+      by replace n1 with (pred n2) by lia.
   Qed.
 
   Lemma Pred_spec n E Q :
     â–·Q (LitNatV $ pred n) âŠ‘ wp E (App Pred (LitNat n)) Q.
   Proof.
     rewrite -wp_lam //. asimpl.
-    rewrite -(wp_bind (CaseCtx EmptyCtx _ _)).
-    apply later_mono, wp_le; intros Hn.
+    rewrite -(wp_bind [CaseCtx _ _]).
+    apply later_mono, wp_le=> Hn.
     - rewrite -wp_case_inl //.
       rewrite -!later_intro -wp_value' //.
-      assert (Heq: n = 0) by omega. by subst n.
+      by replace n with 0 by lia.
     - rewrite -wp_case_inr //.
-      rewrite -!later_intro -FindPred_spec. apply and_intro.
-      + by apply const_intro; omega.
-      + done.
+      rewrite -!later_intro -FindPred_spec.
+      auto using and_intro, const_intro with lia.
   Qed.
 
   Goal âˆ€ E,
-    (True : iProp heap_lang Î£)
-    âŠ‘ wp E (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (Î» v, â– (v = LitNatV 40)).
+    True âŠ‘ wp (Î£:=Î£) E
+      (Let (App Pred (LitNat 42)) (App Pred (Var 0))) (Î» v, â– (v = LitNatV 40)).
   Proof.
     intros E. rewrite -wp_let. rewrite -Pred_spec -!later_intro.
     asimpl. (* TODO RJ: Can we somehow make it so that Pred gets folded again? *)
diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index 5e5467f1b..7bfd02e27 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -55,7 +55,7 @@ Proof.
   rewrite -(ht_lift_step E E Ï†'  _ P
     (Î» e2 Ïƒ2 ef, ownP Ïƒ2 â˜… â–  (Ï†' e2 Ïƒ2 ef))%I
     (Î» e2 Ïƒ2 ef, â–  Ï† e2 Ïƒ2 ef â˜… P)%I);
-    try by (rewrite /Ï†'; eauto using atomic_not_value, atomic_step).
+    try by (rewrite /Ï†'; eauto using atomic_not_val, atomic_step).
   apply and_intro; [by rewrite -vs_reflexive; apply const_intro|].
   apply forall_mono=>e2; apply forall_mono=>Ïƒ2; apply forall_mono=>ef.
   apply and_intro; [|apply and_intro; [|done]].
diff --git a/iris/language.v b/iris/language.v
index d9c9ef1e8..035062d93 100644
--- a/iris/language.v
+++ b/iris/language.v
@@ -11,7 +11,7 @@ Structure language := Language {
   to_of_val v : to_val (of_val v) = Some v;
   of_to_val e v : to_val e = Some v â†’ of_val v = e;
   values_stuck e Ïƒ e' Ïƒ' ef : prim_step e Ïƒ e' Ïƒ' ef â†’ to_val e = None;
-  atomic_not_value e : atomic e â†’ to_val e = None;
+  atomic_not_val e : atomic e â†’ to_val e = None;
   atomic_step e1 Ïƒ1 e2 Ïƒ2 ef :
     atomic e1 â†’
     prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
@@ -24,7 +24,7 @@ Arguments prim_step {_} _ _ _ _ _.
 Arguments to_of_val {_} _.
 Arguments of_to_val {_} _ _ _.
 Arguments values_stuck {_} _ _ _ _ _ _.
-Arguments atomic_not_value {_} _ _.
+Arguments atomic_not_val {_} _ _.
 Arguments atomic_step {_} _ _ _ _ _ _ _.
 
 Canonical Structure istateC Î£ := leibnizC (state Î£).
@@ -47,9 +47,7 @@ Section language.
   Lemma reducible_not_val e Ïƒ : reducible e Ïƒ â†’ to_val e = None.
   Proof. intros (?&?&?&?); eauto using values_stuck. Qed.
   Lemma atomic_of_val v : Â¬atomic (of_val v).
-  Proof.
-    by intros Hat; apply atomic_not_value in Hat; rewrite to_of_val in Hat.
-  Qed.
+  Proof. by intros Hat%atomic_not_val; rewrite to_of_val in Hat. Qed.
   Global Instance: Injective (=) (=) (@of_val Î›).
   Proof. by intros v v' Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
 End language.
@@ -59,12 +57,12 @@ Instance: Params (@fill) 3.
 Arguments fill {_ _ _} !_ _ / : simpl nomatch.
 
 Class CtxLanguage (Î› : language) (C : Type) `{Fill C (expr Î›)} := {
-  is_ctx_value K e :
+  fill_not_val K e :
     to_val e = None â†’ to_val (fill K e) = None;
-  is_ctx_step_preserved K e1 Ïƒ1 e2 Ïƒ2 ef :
+  fill_step K e1 Ïƒ1 e2 Ïƒ2 ef :
     prim_step e1 Ïƒ1 e2 Ïƒ2 ef â†’
     prim_step (fill K e1) Ïƒ1 (fill K e2) Ïƒ2 ef;
-  is_ctx_step K e1' Ïƒ1 e2 Ïƒ2 ef :
+  fill_step_inv K e1' Ïƒ1 e2 Ïƒ2 ef :
     to_val e1' = None â†’ prim_step (fill K e1') Ïƒ1 e2 Ïƒ2 ef â†’
     âˆƒ e2', e2 = fill K e2' âˆ§ prim_step e1' Ïƒ1 e2' Ïƒ2 ef
 }.
diff --git a/iris/weakestpre.v b/iris/weakestpre.v
index af6ea2e3b..a396c92fd 100644
--- a/iris/weakestpre.v
+++ b/iris/weakestpre.v
@@ -117,7 +117,7 @@ Qed.
 Lemma wp_atomic E1 E2 e Q :
   E2 âŠ† E1 â†’ atomic e â†’ pvs E1 E2 (wp E2 e (Î» v, pvs E2 E1 (Q v))) âŠ‘ wp E1 e Q.
 Proof.
-  intros ? He r n ? Hvs; constructor; eauto using atomic_not_value.
+  intros ? He r n ? Hvs; constructor; eauto using atomic_not_val.
   intros rf k Ef Ïƒ1 ???.
   destruct (Hvs rf (S k) Ef Ïƒ1) as (r'&Hwp&?); auto.
   inversion Hwp as [|???? Hgo]; subst; [by destruct (atomic_of_val v)|].
@@ -165,13 +165,13 @@ Lemma wp_bind `{CtxLanguage Î› C} E K e Q :
   wp E e (Î» v, wp E (fill K (of_val v)) Q) âŠ‘ wp E (fill K e) Q.
 Proof.
   intros r n; revert e r; induction n as [n IH] using lt_wf_ind; intros e r ?.
-  destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using is_ctx_value.
+  destruct 1 as [|n r e ? Hgo]; [|constructor]; auto using fill_not_val.
   intros rf k Ef Ïƒ1 ???; destruct (Hgo rf k Ef Ïƒ1) as [Hsafe Hstep]; auto.
   split.
   { destruct Hsafe as (e2&Ïƒ2&ef&?).
-    by exists (fill K e2), Ïƒ2, ef; apply is_ctx_step_preserved. }
+    by exists (fill K e2), Ïƒ2, ef; apply fill_step. }
   intros e2 Ïƒ2 ef ?.
-  destruct (is_ctx_step K e Ïƒ1 e2 Ïƒ2 ef) as (e2'&->&?); auto.
+  destruct (fill_step_inv K e Ïƒ1 e2 Ïƒ2 ef) as (e2'&->&?); auto.
   destruct (Hstep e2' Ïƒ2 ef) as (r2&r2'&?&?&?); auto.
   exists r2, r2'; split_ands; try eapply IH; eauto.
 Qed.
-- 
GitLab