From 162c2f80c0527e167880615c327df9bd444072d6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Mar 2016 02:08:06 +0100
Subject: [PATCH] Expressions as dependent type.

---
 barrier/barrier.v        |  10 +-
 barrier/client.v         |  14 +-
 heap_lang/derived.v      |  16 +-
 heap_lang/lang.v         | 408 +++++++++++++++++++++++++--------------
 heap_lang/lifting.v      |  14 +-
 heap_lang/notation.v     |  44 ++---
 heap_lang/substitution.v | 250 ++++++++++++++++--------
 heap_lang/tactics.v      |   5 +-
 heap_lang/tests.v        |  33 ++--
 heap_lang/wp_tactics.v   |  35 ++--
 10 files changed, 506 insertions(+), 323 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index ec12db940..d9dd2b4e6 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -1,10 +1,6 @@
-From heap_lang Require Export substitution notation.
+From heap_lang Require Export notation.
 
 Definition newbarrier : val := λ: <>, ref #0.
-Definition signal : val := λ: "x", "x" <- #1.
+Definition signal : val := λ: "x", '"x" <- #1.
 Definition wait : val :=
-  rec: "wait" "x" := if: !"x" = #1 then #() else "wait" "x".
-
-Instance newbarrier_closed : Closed newbarrier. Proof. solve_closed. Qed.
-Instance signal_closed : Closed signal. Proof. solve_closed. Qed.
-Instance wait_closed : Closed wait. Proof. solve_closed. Qed.
+  rec: "wait" "x" := if: !'"x" = #1 then #() else '"wait" '"x".
diff --git a/barrier/client.v b/barrier/client.v
index 3a97f9598..34d2957ae 100644
--- a/barrier/client.v
+++ b/barrier/client.v
@@ -3,12 +3,12 @@ From program_logic Require Import auth sts saved_prop hoare ownership.
 Import uPred.
 
 Definition worker (n : Z) : val :=
-  λ: "b" "y", wait "b" ;; !"y" #n.
-Definition client : expr :=
+  λ: "b" "y", ^wait '"b" ;; !'"y" #n.
+Definition client : expr [] :=
   let: "y" := ref #0 in
-  let: "b" := newbarrier #() in
-  Fork (Fork (worker 12 "b" "y") ;; worker 17 "b" "y") ;;
-  "y" <- (λ: "z", "z" + #42) ;; signal "b".
+  let: "b" := ^newbarrier #() in
+  Fork (Fork (^(worker 12) '"b" '"y") ;; ^(worker 17) '"b" '"y") ;;
+  '"y" <- (λ: "z", '"z" + #42) ;; ^signal '"b".
 
 Section client.
   Context {Σ : rFunctorG} `{!heapG Σ, !barrierG Σ} (heapN N : namespace).
@@ -16,7 +16,7 @@ Section client.
 
   Definition y_inv q y : iProp :=
     (∃ f : val, y ↦{q} f ★ □ ∀ n : Z, || f #n {{ λ v, v = #(n + 42) }})%I.
-  
+
   Lemma y_inv_split q y :
     y_inv q y ⊑ (y_inv (q/2) y ★ y_inv (q/2) y).
   Proof.
@@ -56,7 +56,7 @@ Section client.
       wp_seq. (ewp eapply wp_store); eauto with I. strip_later.
       rewrite assoc [(_ ★ y ↦ _)%I]comm. apply sep_mono_r, wand_intro_l.
       wp_seq. rewrite -signal_spec right_id assoc sep_elim_l comm.
-      apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", "z" + #42)%V).
+      apply sep_mono_r. rewrite /y_inv -(exist_intro (λ: "z", '"z" + #42)%V).
       apply sep_intro_True_r; first done. apply: always_intro.
       apply forall_intro=>n. wp_let. wp_op. by apply const_intro. }
     (* The two spawned threads, the waiters. *)
diff --git a/heap_lang/derived.v b/heap_lang/derived.v
index d8957ece3..c5f9bc599 100644
--- a/heap_lang/derived.v
+++ b/heap_lang/derived.v
@@ -19,12 +19,12 @@ Implicit Types Φ : val → iProp heap_lang Σ.
 (** Proof rules for the sugar *)
 Lemma wp_lam E x ef e v Φ :
   to_val e = Some v →
-  ▷ || subst' ef x v @ E {{ Φ }} ⊑ || App (Lam x ef) e @ E {{ Φ }}.
+  ▷ || subst' x e ef @ E {{ Φ }} ⊑ || App (Lam x ef) e @ E {{ Φ }}.
 Proof. intros. by rewrite -wp_rec. Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
   to_val e1 = Some v →
-  ▷ || subst' e2 x v @ E {{ Φ }} ⊑ || Let x e1 e2 @ E {{ Φ }}.
+  ▷ || subst' x e1 e2 @ E {{ Φ }} ⊑ || Let x e1 e2 @ E {{ Φ }}.
 Proof. apply wp_lam. Qed.
 
 Lemma wp_seq E e1 e2 v Φ :
@@ -37,17 +37,13 @@ Proof. rewrite -wp_seq // -wp_value //. Qed.
 
 Lemma wp_match_inl E e0 v0 x1 e1 x2 e2 Φ :
   to_val e0 = Some v0 →
-  ▷ || subst' e1 x1 v0 @ E {{ Φ }} ⊑ || Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_case_inl // -[X in _ ⊑ X]later_intro. by apply wp_let.
-Qed.
+  ▷ || subst' x1 e0 e1 @ E {{ Φ }} ⊑ || Match (InjL e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_case_inl // -[X in _ ⊑ X]later_intro -wp_let. Qed.
 
 Lemma wp_match_inr E e0 v0 x1 e1 x2 e2 Φ :
   to_val e0 = Some v0 →
-  ▷ || subst' e2 x2 v0 @ E {{ Φ }} ⊑ || Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
-Proof.
-  intros. rewrite -wp_case_inr // -[X in _ ⊑ X]later_intro. by apply wp_let.
-Qed.
+  ▷ || subst' x2 e0 e2 @ E {{ Φ }} ⊑ || Match (InjR e0) x1 e1 x2 e2 @ E {{ Φ }}.
+Proof. intros. by rewrite -wp_case_inr // -[X in _ ⊑ X]later_intro -wp_let. Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Φ :
   (n1 ≤ n2 → P ⊑ ▷ Φ (LitV (LitBool true))) →
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 6d85546b6..ecc53ff13 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -1,5 +1,5 @@
 From program_logic Require Export language.
-From prelude Require Export stringmap.
+From prelude Require Export strings.
 From prelude Require Import gmap.
 
 Module heap_lang.
@@ -17,41 +17,84 @@ Inductive bin_op : Set :=
 
 Inductive binder := BAnon | BNamed : string → binder.
 
+Definition cons_binder (mx : binder) (X : list string) : list string :=
+  match mx with BAnon => X | BNamed x => x :: X end.
+Infix ":b:" := cons_binder (at level 60, right associativity).
 Delimit Scope binder_scope with binder.
 Bind Scope binder_scope with binder.
+Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
+Proof. solve_decision. Defined.
+
+Instance set_unfold_cons_binder x mx X P :
+  SetUnfold (x ∈ X) P → SetUnfold (x ∈ mx :b: X) (BNamed x = mx ∨ P).
+Proof.
+  constructor. rewrite -(set_unfold (x ∈ X) P).
+  destruct mx; rewrite /= ?elem_of_cons; naive_solver.
+Qed.
+
+Class VarBound (x : string) (X : list string) :=
+  var_bound : bool_decide (x ∈ X).
+Hint Extern 0 (VarBound _ _) => vm_compute; exact I : typeclass_instances. 
+
+Instance var_bound_proof_irrel x X : ProofIrrel (VarBound x X).
+Proof. rewrite /VarBound. apply _. Qed.
+Instance set_unfold_var_bound x X P :
+  SetUnfold (x ∈ X) P → SetUnfold (VarBound x X) P.
+Proof.
+  constructor. by rewrite /VarBound bool_decide_spec (set_unfold (x ∈ X) P).
+Qed.
 
-Inductive expr :=
+Inductive expr (X : list string) :=
   (* Base lambda calculus *)
-  | Var (x : string)
-  | Rec (f x : binder) (e : expr)
-  | App (e1 e2 : expr)
+  | Var (x : string) `{VarBound x X}
+  | Rec (f x : binder) (e : expr (f :b: x :b: X))
+  | App (e1 e2 : 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)
+  | UnOp (op : un_op) (e : expr X)
+  | BinOp (op : bin_op) (e1 e2 : expr X)
+  | If (e0 e1 e2 : expr X)
   (* Products *)
-  | Pair (e1 e2 : expr)
-  | Fst (e : expr)
-  | Snd (e : expr)
+  | Pair (e1 e2 : expr X)
+  | Fst (e : expr X)
+  | Snd (e : expr X)
   (* Sums *)
-  | InjL (e : expr)
-  | InjR (e : expr)
-  | Case (e0 : expr) (e1 : expr) (e2 : expr)
+  | InjL (e : expr X)
+  | InjR (e : expr X)
+  | Case (e0 : expr X) (e1 : expr X) (e2 : expr X)
   (* Concurrency *)
-  | Fork (e : expr)
+  | Fork (e : expr X)
   (* Heap *)
   | Loc (l : loc)
-  | Alloc (e : expr)
-  | Load (e : expr)
-  | Store (e1 : expr) (e2 : expr)
-  | Cas (e0 : expr) (e1 : expr) (e2 : expr).
+  | Alloc (e : expr X)
+  | Load (e : expr X)
+  | Store (e1 : expr X) (e2 : expr X)
+  | Cas (e0 : expr X) (e1 : expr X) (e2 : expr X).
 
 Bind Scope expr_scope with expr.
 Delimit Scope expr_scope with E.
+Arguments Var {_} _ {_}.
+Arguments Rec {_} _ _ _%E.
+Arguments App {_} _%E _%E.
+Arguments Lit {_} _.
+Arguments UnOp {_} _ _%E.
+Arguments BinOp {_} _ _%E _%E.
+Arguments If {_} _%E _%E _%E.
+Arguments Pair {_} _%E _%E.
+Arguments Fst {_} _%E.
+Arguments Snd {_} _%E.
+Arguments InjL {_} _%E.
+Arguments InjR {_} _%E.
+Arguments Case {_} _%E _%E _%E.
+Arguments Fork {_} _%E.
+Arguments Loc {_} _.
+Arguments Alloc {_} _%E.
+Arguments Load {_} _%E.
+Arguments Store {_} _%E _%E.
+Arguments Cas {_} _%E _%E _%E.
 
 Inductive val :=
-  | RecV (f x : binder) (e : expr) (* e should be closed *)
+  | RecV (f x : binder) (e : expr (f :b: x :b: []))
   | LitV (l : base_lit)
   | PairV (v1 v2 : val)
   | InjLV (v : val)
@@ -60,21 +103,13 @@ Inductive val :=
 
 Bind Scope val_scope with val.
 Delimit Scope val_scope with V.
+Arguments PairV _%V _%V.
+Arguments InjLV _%V.
+Arguments InjRV _%V.
 
-Global Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
-Proof. solve_decision. Defined.
-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 binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
-Proof. solve_decision. Defined.
-Global Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
-Proof. solve_decision. Defined.
-Global Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
-Proof. solve_decision. Defined.
+Definition signal : val := RecV BAnon (BNamed "x") (Store (Var "x") (Lit (LitInt 1))).
 
-Fixpoint of_val (v : val) : expr :=
+Fixpoint of_val (v : val) : expr [] :=
   match v with
   | RecV f x e => Rec f x e
   | LitV l => Lit l
@@ -83,7 +118,8 @@ Fixpoint of_val (v : val) : expr :=
   | InjRV v => InjR (of_val v)
   | LocV l => Loc l
   end.
-Fixpoint to_val (e : expr) : option val :=
+
+Fixpoint to_val (e : expr []) : option val :=
   match e with
   | Rec f x e => Some (RecV f x e)
   | Lit l => Some (LitV l)
@@ -99,30 +135,30 @@ 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 (e1 : expr) (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 :=
+Definition fill_item (Ki : ectx_item) (e : expr []) : expr [] :=
   match Ki with
   | AppLCtx e2 => App e e2
   | AppRCtx v1 => App (of_val v1) e
@@ -145,36 +181,83 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   | 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 BAnon 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) then of_val v else Var y
+Lemma wexpr_rec_prf {X Y} (H : X `included` Y) {f x} :
+  f :b: x :b: X `included` f :b: x :b: Y.
+Proof. set_solver. Qed.
+
+Program Fixpoint wexpr {X Y} (H : X `included` Y) (e : expr X) : expr Y :=
+  match e return expr Y with
+  | Var x _ => @Var _ x _
+  | Rec f x e => Rec f x (wexpr (wexpr_rec_prf H) e)
+  | App e1 e2 => App (wexpr H e1) (wexpr H e2)
+  | Lit l => Lit l
+  | UnOp op e => UnOp op (wexpr H e)
+  | BinOp op e1 e2 => BinOp op (wexpr H e1) (wexpr H e2)
+  | If e0 e1 e2 => If (wexpr H e0) (wexpr H e1) (wexpr H e2)
+  | Pair e1 e2 => Pair (wexpr H e1) (wexpr H e2)
+  | Fst e => Fst (wexpr H e)
+  | Snd e => Snd (wexpr H e)
+  | InjL e => InjL (wexpr H e)
+  | InjR e => InjR (wexpr H e)
+  | Case e0 e1 e2 => Case (wexpr H e0) (wexpr H e1) (wexpr H e2)
+  | Fork e => Fork (wexpr H e)
+  | Loc l => Loc l
+  | Alloc e => Alloc (wexpr H e)
+  | Load  e => Load (wexpr H e)
+  | Store e1 e2 => Store (wexpr H e1) (wexpr H e2)
+  | Cas e0 e1 e2 => Cas (wexpr H e0) (wexpr H e1) (wexpr H e2)
+  end.
+Solve Obligations with set_solver.
+
+Definition of_val' {X} (v : val) : expr X := wexpr (included_nil _) (of_val v).
+
+Lemma wsubst_rec_true_prf {X Y x} (H : X `included` x :: Y) {f y}
+    (Hfy :BNamed x ≠ f ∧ BNamed x ≠ y) :
+  f :b: y :b: X `included` x :: f :b: y :b: Y.
+Proof. set_solver. Qed.
+Lemma wsubst_rec_false_prf {X Y x} (H : X `included` x :: Y) {f y}
+    (Hfy : ¬(BNamed x ≠ f ∧ BNamed x ≠ y)) :
+  f :b: y :b: X `included` f :b: y :b: Y.
+Proof. move: Hfy=>/not_and_l [/dec_stable|/dec_stable]; set_solver. Qed.
+
+Program Fixpoint wsubst {X Y} (x : string) (es : expr [])
+    (H : X `included` x :: Y) (e : expr X)  : expr Y :=
+  match e return expr Y with
+  | Var y _ => if decide (x = y) then wexpr _ es else @Var _ y _
   | Rec f y e =>
-     Rec f y (if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst e x v else e)
-  | App e1 e2 => App (subst e1 x v) (subst e2 x v)
+     Rec f y $ match decide (BNamed x ≠ f ∧ BNamed x ≠ y) return _ with
+               | left Hfy => wsubst x es (wsubst_rec_true_prf H Hfy) e
+               | right Hfy => wexpr (wsubst_rec_false_prf H Hfy) e
+               end
+  | App e1 e2 => App (wsubst x es H e1) (wsubst x es H e2)
   | 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)
+  | UnOp op e => UnOp op (wsubst x es H e)
+  | BinOp op e1 e2 => BinOp op (wsubst x es H e1) (wsubst x es H e2)
+  | If e0 e1 e2 => If (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
+  | Pair e1 e2 => Pair (wsubst x es H e1) (wsubst x es H e2)
+  | Fst e => Fst (wsubst x es H e)
+  | Snd e => Snd (wsubst x es H e)
+  | InjL e => InjL (wsubst x es H e)
+  | InjR e => InjR (wsubst x es H e)
   | Case e0 e1 e2 =>
-     Case (subst e0 x v) (subst e1 x v) (subst e2 x v)
-  | Fork e => Fork (subst e x v)
+     Case (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
+  | Fork e => Fork (wsubst x es H e)
   | 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)
+  | Alloc e => Alloc (wsubst x es H e)
+  | Load e => Load (wsubst x es H e)
+  | Store e1 e2 => Store (wsubst x es H e1) (wsubst x es H e2)
+  | Cas e0 e1 e2 => Cas (wsubst x es H e0) (wsubst x es H e1) (wsubst x es H e2)
   end.
-Definition subst' (e : expr) (mx : binder) (v : val) : expr :=
-  match mx with BNamed x => subst e x v | BAnon => e end.
+Solve Obligations with set_solver.
+
+Definition subst {X} (x : string) (es : expr []) (e : expr (x :: X)) : expr X :=
+  wsubst x es (λ z, id) e.
+Definition subst' {X} (mx : binder) (es : expr []) : expr (mx :b: X) → expr X :=
+  match mx with BNamed x => subst x es | BAnon => id end.
 
 (** The stepping relation *)
 Definition un_op_eval (op : un_op) (l : base_lit) : option base_lit :=
@@ -194,11 +277,11 @@ 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 :=
+  | BetaS f x e1 e2 v2 e' σ :
      to_val e2 = Some v2 →
-     head_step (App (Rec f x e1) e2) σ
-       (subst' (subst' e1 f (RecV f x e1)) x v2) σ None
+     e' = subst' x (of_val v2) (subst' f (Rec f x e1) e1) →
+     head_step (App (Rec f x e1) e2) σ e' σ None
   | UnOpS op l l' σ :
      un_op_eval op l = Some l' → 
      head_step (UnOp op (Lit l)) σ (Lit l') σ None
@@ -242,7 +325,7 @@ Inductive head_step : expr → state → expr → state → option expr → Prop
      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)
@@ -255,19 +338,83 @@ 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 :=
+Inductive prim_step (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.
 
+(** Substitution *)
+Lemma var_proof_irrel X x H1 H2 : @Var X x H1 = @Var X x H2.
+Proof. f_equal. by apply (proof_irrel _). Qed.
+
+Lemma wexpr_id X (H : X `included` X) e : wexpr H e = e.
+Proof. induction e; f_equal/=; auto. by apply (proof_irrel _). Qed.
+Lemma wexpr_proof_irrel X Y (H1 H2 : X `included` Y) e : wexpr H1 e = wexpr H2 e.
+Proof.
+  revert Y H1 H2; induction e; simpl; auto using var_proof_irrel with f_equal.
+Qed.
+Lemma wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) H3 e :
+  wexpr H2 (wexpr H1 e) = wexpr H3 e.
+Proof.
+  revert Y Z H1 H2 H3.
+  induction e; simpl; auto using var_proof_irrel with f_equal.
+Qed.
+Lemma wexpr_wexpr' X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e :
+  wexpr H2 (wexpr H1 e) = wexpr (transitivity H1 H2) e.
+Proof. apply wexpr_wexpr. Qed.
+
+Lemma wsubst_proof_irrel X Y x es (H1 H2 : X `included` x :: Y) e :
+  wsubst x es H1 e = wsubst x es H2 e.
+Proof.
+  revert Y H1 H2; induction e; simpl; intros; repeat case_decide;
+    auto using var_proof_irrel, wexpr_proof_irrel with f_equal.
+Qed.
+Lemma wexpr_wsubst X Y Z x es (H1: X `included` x::Y) (H2: Y `included` Z) H3 e:
+  wexpr H2 (wsubst x es H1 e) = wsubst x es H3 e.
+Proof.
+  revert Y Z H1 H2 H3.
+  induction e; intros; repeat (case_decide || simplify_eq/=);
+    auto using var_proof_irrel, wexpr_wexpr with f_equal.
+Qed.
+Lemma wsubst_wexpr X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) H3 e:
+  wsubst x es H2 (wexpr H1 e) = wsubst x es H3 e.
+Proof.
+  revert Y Z H1 H2 H3.
+  induction e; intros; repeat (case_decide || simplify_eq/=);
+    auto using var_proof_irrel, wexpr_wexpr with f_equal.
+Qed.
+Lemma wsubst_wexpr' X Y Z x es (H1: X `included` Y) (H2: Y `included` x::Z) e:
+  wsubst x es H2 (wexpr H1 e) = wsubst x es (transitivity H1 H2) e.
+Proof. apply wsubst_wexpr. Qed.
+
+Lemma wsubst_closed X Y x es (H1 : X `included` x :: Y) H2 (e : expr X) :
+  x ∉ X → wsubst x es H1 e = wexpr H2 e.
+Proof.
+  revert Y H1 H2.
+  induction e; intros; repeat (case_decide || simplify_eq/=);
+    auto using var_proof_irrel, wexpr_proof_irrel with f_equal set_solver.
+  exfalso; set_solver.
+Qed.
+Lemma wsubst_closed_nil x es H (e : expr []) : wsubst x es H e = e.
+Proof.
+  rewrite -{2}(wexpr_id _ (reflexivity []) e).
+  apply wsubst_closed, not_elem_of_nil.
+Qed.
+
 (** 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.
 
 Lemma of_to_val e v : to_val e = Some v → of_val v = e.
 Proof.
-  revert v; induction e; intros; simplify_option_eq; auto with f_equal.
+  revert e v. cut (∀ X (e : expr X) (H : X = ∅) v,
+    to_val (eq_rect _ expr e _ H) = Some v → of_val v = eq_rect _ expr e _ H).
+  { intros help e v. apply (help ∅ e eq_refl). }
+  intros X e; induction e; intros HX ??; simplify_option_eq;
+    repeat match goal with
+    | IH : ∀ _ : ∅ = ∅, _ |- _ => specialize (IH eq_refl); simpl in IH
+    end; auto with f_equal.
 Qed.
 
 Instance: Inj (=) (=) of_val.
@@ -316,7 +463,7 @@ Qed.
 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; try by eauto.
+  destruct 2; simpl; rewrite ?to_of_val; try by eauto. subst.
   unfold subst'; repeat (case_match || contradiction || simplify_eq/=); eauto.
 Qed.
 
@@ -363,92 +510,53 @@ Lemma alloc_fresh e v σ :
   to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
-(** Closed expressions *)
-Definition of_binder (mx : binder) : stringset :=
-  match mx with BAnon => ∅ | BNamed x => {[ x ]} end.
-Lemma elem_of_of_binder x mx: x ∈ of_binder mx ↔ mx = BNamed x.
-Proof. destruct mx; set_solver. Qed.
-Global Instance set_unfold_of_binder (mx : binder) x :
-  SetUnfold (x ∈ of_binder mx) (mx = BNamed x).
-Proof. constructor; destruct mx; set_solver. Qed.
+(** Equality stuff *)
+Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
+Proof. solve_decision. Defined.
+Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
+Proof. solve_decision. Defined.
+Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
+Proof. solve_decision. Defined.
 
-Fixpoint is_closed (X : stringset) (e : expr) : bool :=
-  match e with
-  | Var x => bool_decide (x ∈ X)
-  | Rec f y e => is_closed (of_binder f ∪ of_binder y ∪ X) e
-  | App e1 e2 => is_closed X e1 && is_closed X e2
-  | Lit l => true
-  | UnOp _ e => is_closed X e
-  | BinOp _ e1 e2 => is_closed X e1 && is_closed X e2
-  | If e0 e1 e2 => is_closed X e0 && is_closed X e1 && is_closed X e2
-  | Pair e1 e2 => is_closed X e1 && is_closed X e2
-  | Fst e => is_closed X e
-  | Snd e => is_closed X e
-  | InjL e => is_closed X e
-  | InjR e => is_closed X e
-  | Case e0 e1 e2 => is_closed X e0 && is_closed X e1 && is_closed X e2
-  | Fork e => is_closed X e
-  | Loc l => true
-  | Alloc e => is_closed X e
-  | Load e => is_closed X e
-  | Store e1 e2 => is_closed X e1 && is_closed X e2
-  | Cas e0 e1 e2 => is_closed X e0 && is_closed X e1 && is_closed X e2
+Fixpoint expr_beq {X Y} (e : expr X) (e' : expr Y) : bool :=
+  match e, e' with
+  | Var x _, Var x' _ => bool_decide (x = x')
+  | Rec f x e, Rec f' x' e' =>
+     bool_decide (f = f') && bool_decide (x = x') && expr_beq e e'
+  | App e1 e2, App e1' e2' | Pair e1 e2, Pair e1' e2' |
+    Store e1 e2, Store e1' e2' => expr_beq e1 e1' && expr_beq e2 e2'
+  | Lit l, Lit l' => bool_decide (l = l')
+  | UnOp op e, UnOp op' e' => bool_decide (op = op') && expr_beq e e'
+  | BinOp op e1 e2, BinOp op' e1' e2' =>
+     bool_decide (op = op') && expr_beq e1 e1' && expr_beq e2 e2'
+  | If e0 e1 e2, If e0' e1' e2' | Case e0 e1 e2, Case e0' e1' e2' |
+    Cas e0 e1 e2, Cas e0' e1' e2' =>
+     expr_beq e0 e0' && expr_beq e1 e1' && expr_beq e2 e2'
+  | Fst e, Fst e' | Snd e, Snd e' | InjL e, InjL e' | InjR e, InjR e' |
+    Fork e, Fork e' | Alloc e, Alloc e' | Load e, Load e' => expr_beq e e'
+  | Loc l, Loc l' => bool_decide (l = l')
+  | _, _ => false
   end.
-Class Closed (e : expr) := closed : ∀ x v, subst e x v = e.
-
-Lemma is_closed_subst_same X e x v : is_closed X e → x ∉ X → subst e x v = e.
+Lemma expr_beq_correct {X} (e1 e2 : expr X) : expr_beq e1 e2 ↔ e1 = e2.
 Proof.
-  revert X. induction e; simpl;
-    repeat case_decide; naive_solver eauto with f_equal set_solver.
-Qed.
-Lemma is_closed_Closed e : is_closed ∅ e → Closed e.
-Proof. intros ? x v. by eapply is_closed_subst_same, not_elem_of_empty. Qed.
-
-Ltac solve_closed := apply is_closed_Closed; vm_compute; exact I.
-
-Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
-Proof.
-  revert X Y.
-  induction e; simpl; intros; naive_solver eauto with f_equal set_solver.
+  split.
+  * revert e2; induction e1; intros [] * ?; simpl in *;
+      destruct_and?; subst; repeat f_equal/=; auto; try apply proof_irrel.
+  * intros ->. induction e2; naive_solver.
 Qed.
-
-Lemma is_closed_fill_item X Ki e : is_closed X (fill_item Ki e) → is_closed X e.
-Proof. destruct Ki; rewrite /= ?andb_True; tauto. Qed.
-Lemma is_closed_fill X K e : is_closed X (fill K e) → is_closed X e.
-Proof. induction K; simpl; eauto using is_closed_fill_item. Qed.
-
-Lemma is_closed_subst X e x v :
-  is_closed ({[x]} ∪ X) e → is_closed ∅ (of_val v) → is_closed X (subst e x v).
+Instance expr_dec_eq {X} (e1 e2 : expr X) : Decision (e1 = e2).
 Proof.
-  revert X. elim: e; simpl; try by intros; destruct_and?; split_and?; auto.
-  - intros y X; rewrite bool_decide_spec=>??.
-    case_decide; subst; last set_solver.
-    eauto using is_closed_weaken with set_solver.
-  - intros f y e IH X ??. case_decide as Hx.
-    + apply IH; clear IH; eauto using is_closed_weaken with set_solver.
-    + clear IH; apply not_and_l in Hx;
-        destruct Hx as [Hx|Hx]; apply dec_stable in Hx; subst;
-        eauto using is_closed_weaken with set_solver.
-Qed.
-Lemma is_closed_subst' X e x v :
-  is_closed (of_binder x ∪ X) e → is_closed ∅ (of_val v) →
-  is_closed X (subst' e x v).
-Proof. destruct x; rewrite /= ?left_id_L; auto using is_closed_subst. Qed.
-Lemma is_closed_head_step e1 σ1 e2 σ2 ef :
-  (* for load, the state should be closed *)
-  match e1 with Load _ => False | _ => True end →
-  head_step e1 σ1 e2 σ2 ef → is_closed ∅ e1 → is_closed ∅ e2.
+ refine (cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
+Defined.
+Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
 Proof.
-  destruct 2; rewrite /= ?andb_True; try
-    match goal with H : to_val _ = _ |- _ => apply of_to_val in H; subst end;
-    try tauto.
-  intros [??]. repeat apply is_closed_subst'; rewrite /= ?assoc_L; auto.
-Qed.
+ refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
+Defined.
 End heap_lang.
 
 (** Language *)
 Program Canonical Structure heap_lang : language := {|
-  expr := heap_lang.expr; val := heap_lang.val; state := heap_lang.state;
+  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;
 |}.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 70200c1b3..f8e0d5fe5 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -12,7 +12,7 @@ Context {Σ : rFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
 Implicit Types K : ectx.
-Implicit Types ef : option expr.
+Implicit Types ef : option (expr []).
 
 (** Bind. *)
 Lemma wp_bind {E e} K Φ :
@@ -84,19 +84,19 @@ Qed.
 
 Lemma wp_rec E f x e1 e2 v Φ :
   to_val e2 = Some v →
-  ▷ || subst' (subst' e1 f (RecV f x e1)) x v @ E {{ Φ }}
+  ▷ || subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
   ⊑ || App (Rec f x e1) e2 @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (App _ _)
-    (subst' (subst' e1 f (RecV f x e1)) x v) None) ?right_id //=;
+    (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
     intros; inv_step; eauto.
 Qed.
 
-Lemma wp_rec' E f x erec v1 e2 v2 Φ :
-  v1 = RecV f x erec →
+Lemma wp_rec' E f x erec e1 e2 v2 Φ :
+  e1 = Rec f x erec →
   to_val e2 = Some v2 →
-  ▷ || subst' (subst' erec f v1) x v2 @ E {{ Φ }}
-  ⊑ || App (of_val v1) e2 @ E {{ Φ }}.
+  ▷ || subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
+  ⊑ || App e1 e2 @ E {{ Φ }}.
 Proof. intros ->. apply wp_rec. Qed.
 
 Lemma wp_un_op E op l l' Φ :
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index ad55bee90..36a041104 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -10,18 +10,22 @@ Notation "|| e {{ Φ } }" := (wp ⊤ e%E Φ)
 
 Coercion LitInt : Z >-> base_lit.
 Coercion LitBool : bool >-> base_lit.
-(** No coercion from base_lit to expr. This makes is slightly easier to tell
-   apart language and Coq expressions. *)
-Coercion Var : string >-> expr.
 Coercion App : expr >-> Funclass.
 Coercion of_val : val >-> expr.
 
 Coercion BNamed : string >-> binder.
 Notation "<>" := BAnon : binder_scope.
 
-(* No scope, does not conflict and scope is often not inferred properly. *)
+(* No scope for the values, does not conflict and scope is often not inferred properly. *)
 Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
 Notation "% l" := (LocV l) (at level 8, format "% l").
+Notation "# l" := (LitV l%Z%V) (at level 8, format "# l") : val_scope.
+Notation "% l" := (LocV l) (at level 8, format "% l") : val_scope.
+Notation "# l" := (Lit l%Z%V) (at level 8, format "# l") : expr_scope.
+Notation "% l" := (Loc l) (at level 8, format "% l") : expr_scope.
+
+Notation "' x" := (Var x) (at level 8, format "' x") : expr_scope.
+Notation "^ v" := (of_val' v%V) (at level 8, format "^ v") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
@@ -56,10 +60,23 @@ Notation "'if:' e1 'then' e2 'else' e3" := (If e1%E e2%E e3%E)
 are stated explicitly instead of relying on the Notations Let and Seq as
 defined above. This is needed because App is now a coercion, and these
 notations are otherwise not pretty printed back accordingly. *)
-Notation "λ: x , e" := (Lam x e%E)
+Notation "'rec:' f x y := e" := (Rec f x (Lam y e%E))
+  (at level 102, f, x, y at level 1, e at level 200) : expr_scope.
+Notation "'rec:' f x y := e" := (RecV f x (Lam y e%E))
+  (at level 102, f, x, y at level 1, e at level 200) : val_scope.
+Notation "'rec:' f x y .. z := e" := (Rec f x (Lam y .. (Lam z e%E) ..))
+  (at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
+Notation "'rec:' f x y .. z := e" := (RecV f x (Lam y .. (Lam z e%E) ..))
+  (at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
+
+Notation "λ: x , e" := (Lam x  e%E)
   (at level 102, x at level 1, e at level 200) : expr_scope.
+Notation "λ: x y .. z , e" := (Lam x (Lam y .. (Lam z e%E) ..))
+  (at level 102, x, y, z at level 1, e at level 200) : expr_scope.
 Notation "λ: x , e" := (LamV x e%E)
   (at level 102, x at level 1, e at level 200) : val_scope.
+Notation "λ: x y .. z , e" := (LamV x (Lam y .. (Lam z e%E) .. ))
+  (at level 102, x, y, z at level 1, e at level 200) : val_scope.
 
 Notation "'let:' x := e1 'in' e2" := (Lam x e2%E e1%E)
   (at level 102, x at level 1, e1, e2 at level 200) : expr_scope.
@@ -70,20 +87,3 @@ Notation "'let:' x := e1 'in' e2" := (LamV x e2%E e1%E)
   (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
 Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
   (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
-
-Notation "'rec:' f x y := e" := (Rec f x (Lam y e%E))
-  (at level 102, f, x, y at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f x y := e" := (RecV f x (Lam y e%E))
-  (at level 102, f, x, y at level 1, e at level 200) : val_scope.
-Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%E)))
-  (at level 102, f, x, y, z at level 1, e at level 200) : expr_scope.
-Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%E)))
-  (at level 102, f, x, y, z at level 1, e at level 200) : val_scope.
-Notation "λ: x y , e" := (Lam x (Lam y e%E))
-  (at level 102, x, y at level 1, e at level 200) : expr_scope.
-Notation "λ: x y , e" := (LamV x (Lam y e%E))
-  (at level 102, x, y at level 1, e at level 200) : val_scope.
-Notation "λ: x y z , e" := (Lam x (Lam y (Lam z e%E)))
-  (at level 102, x, y, z at level 1, e at level 200) : expr_scope.
-Notation "λ: x y z , e" := (LamV x (Lam y (Lam z e%E)))
-  (at level 102, x, y, z at level 1, e at level 200) : val_scope.
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
index b56d16bf4..0f1035b1f 100644
--- a/heap_lang/substitution.v
+++ b/heap_lang/substitution.v
@@ -1,112 +1,206 @@
 From heap_lang Require Export lang.
-From prelude Require Import stringmap.
 Import heap_lang.
 
 (** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
 can be tuned using instances of the type class [Closed e], which can be used
 to mark that expressions are closed, and should thus not be substituted into. *)
 
-Class Subst (e : expr) (x : string) (v : val) (er : expr) :=
-  do_subst : subst e x v = er.
-Hint Mode Subst + + + - : typeclass_instances.
+(** * Weakening *)
+Class WExpr {X Y} (H : X `included` Y) (e : expr X) (er : expr Y) :=
+  do_wexpr : wexpr H e = er.
+Hint Mode WExpr + + + + - : typeclass_instances.
 
-Ltac simpl_subst :=
-  repeat match goal with
-  | |- context [subst ?e ?x ?v] => progress rewrite (@do_subst e x v)
-  | |- _ => progress csimpl
-  end; fold of_val.
-
-Arguments of_val : simpl never.
-Hint Extern 10 (Subst (of_val _) _ _ _) => unfold of_val : typeclass_instances.
-Hint Extern 10 (Closed (of_val _)) => unfold of_val : typeclass_instances.
+(* Variables *)
+Hint Extern 0 (WExpr _ (Var ?y) _) =>
+  apply var_proof_irrel : typeclass_instances.
 
-Instance subst_fallthrough e x v : Subst e x v (subst e x v) | 1000.
-Proof. done. Qed.
-
-Class SubstIf (P : Prop) (e : expr) (x : string) (v : val) (er : expr) := {
-  subst_if_true : P → subst e x v = er;
-  subst_if_false : ¬P → e = er
-}.
-Hint Mode SubstIf + + + + - : typeclass_instances.
-Definition subst_if_mk_true (P : Prop) x v e er :
-  Subst e x v er → P → SubstIf P e x v er.
-Proof. by split. Qed.
-Definition subst_if_mk_false (P : Prop) x v e : ¬P → SubstIf P e x v e.
-Proof. by split. Qed.
+(* Rec *)
+Instance do_wexpr_rec_true {X Y f y e} {H : X `included` Y} er :
+  WExpr (wexpr_rec_prf H) e er → WExpr H (Rec f y e) (Rec f y er).
+Proof. intros; red; f_equal/=. by etrans; [apply wexpr_proof_irrel|]. Qed.
 
-Ltac bool_decide_no_check := apply (bool_decide_unpack _); vm_cast_no_check I.
-
-Hint Extern 0 (SubstIf ?P ?e ?x ?v _) =>
-  match eval vm_compute in (bool_decide P) with
-  | true => apply subst_if_mk_true; [|bool_decide_no_check]
-  | false => apply subst_if_mk_false; bool_decide_no_check
-  end : typeclass_instances.
+(* Values *)
+Instance do_wexpr_of_val_nil (H : [] `included` []) v :
+  WExpr H (of_val v) (of_val v) | 0.
+Proof. apply wexpr_id. Qed.
+Instance do_wexpr_of_val_nil' X (H : X `included` []) v :
+  WExpr H (of_val' v) (of_val v) | 0.
+Proof. by rewrite /WExpr /of_val' wexpr_wexpr' wexpr_id. Qed.
+Instance do_wexpr_of_val Y (H : [] `included` Y) v :
+  WExpr H (of_val v) (of_val' v) | 1.
+Proof. apply wexpr_proof_irrel. Qed.
+Instance do_wexpr_of_val' X Y (H : X `included` Y) v :
+  WExpr H (of_val' v) (of_val' v) | 1.
+Proof. apply wexpr_wexpr. Qed.
 
-Instance subst_closed e x v : Closed e → Subst e x v e | 0.
-Proof. intros He; apply He. Qed.
+(* Boring connectives *)
+Section do_wexpr.
+Context {X Y : list string} (H : X `included` Y).
+Notation W := (WExpr H).
 
-Instance lit_closed l : Closed (Lit l).
+(* Ground terms *)
+Global Instance do_wexpr_lit l : W (Lit l) (Lit l).
 Proof. done. Qed.
-Instance loc_closed l : Closed (Loc l).
+Global Instance do_wexpr_loc l : W (Loc l) (Loc l).
 Proof. done. Qed.
+Global Instance do_wexpr_app e1 e2 e1r e2r :
+  W e1 e1r → W e2 e2r → W (App e1 e2) (App e1r e2r).
+Proof. intros; red; f_equal/=; apply: do_wexpr. Qed.
+Global Instance do_wexpr_unop op e er : W e er → W (UnOp op e) (UnOp op er).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_binop op e1 e2 e1r e2r :
+  W e1 e1r → W e2 e2r → W (BinOp op e1 e2) (BinOp op e1r e2r).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_if e0 e1 e2 e0r e1r e2r :
+  W e0 e0r → W e1 e1r → W e2 e2r → W (If e0 e1 e2) (If e0r e1r e2r).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_pair e1 e2 e1r e2r :
+  W e1 e1r → W e2 e2r → W (Pair e1 e2) (Pair e1r e2r).
+Proof. by intros ??; red; f_equal/=. Qed.
+Global Instance do_wexpr_fst e er : W e er → W (Fst e) (Fst er).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_snd e er : W e er → W (Snd e) (Snd er).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_injL e er : W e er → W (InjL e) (InjL er).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_injR e er : W e er → W (InjR e) (InjR er).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_case e0 e1 e2 e0r e1r e2r :
+  W e0 e0r → W e1 e1r → W e2 e2r → W (Case e0 e1 e2) (Case e0r e1r e2r).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_fork e er : W e er → W (Fork e) (Fork er).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_alloc e er : W e er → W (Alloc e) (Alloc er).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_load e er : W e er → W (Load e) (Load er).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_store e1 e2 e1r e2r :
+  W e1 e1r → W e2 e2r → W (Store e1 e2) (Store e1r e2r).
+Proof. by intros; red; f_equal/=. Qed.
+Global Instance do_wexpr_cas e0 e1 e2 e0r e1r e2r :
+  W e0 e0r → W e1 e1r → W e2 e2r → W (Cas e0 e1 e2) (Cas e0r e1r e2r).
+Proof. by intros; red; f_equal/=. Qed.
+End do_wexpr.
 
-Definition subst_var_eq y x v : x = y → Subst (Var y) x v (of_val v).
-Proof. intros. by red; rewrite /= decide_True. Defined.
-Definition subst_var_ne y x v : x ≠ y → Subst (Var y) x v (Var y).
-Proof. intros. by red; rewrite /= decide_False. Defined.
+(** * WSubstitution *)
+Class WSubst {X Y} (x : string) (es : expr []) H (e : expr X) (er : expr Y) :=
+  do_wsubst : wsubst x es H e = er.
+Hint Mode WSubst + + + + + + - : typeclass_instances.
 
-Hint Extern 0 (Subst (Var ?y) ?x ?v _) =>
-  match eval vm_compute in (bool_decide (x = y)) with
-  | true => apply subst_var_eq; bool_decide_no_check
-  | false => apply subst_var_ne; bool_decide_no_check
+(* Variables *)
+Lemma do_wsubst_var_eq {X Y x es} {H : X `included` x :: Y} `{VarBound x X} er :
+  WExpr (included_nil _) es er → WSubst x es H (Var x) er.
+Proof.
+  intros; red; simpl. case_decide; last done.
+  by etrans; [apply wexpr_proof_irrel|].
+Qed.
+Hint Extern 0 (WSubst ?x ?v _ (Var ?y) _) => first
+  [ apply var_proof_irrel
+  | apply do_wsubst_var_eq ] : typeclass_instances.
+
+(** Rec *)
+Lemma do_wsubst_rec_true {X Y x es f y e} {H : X `included` x :: Y}
+    (Hfy : BNamed x ≠ f ∧ BNamed x ≠ y) er :
+  WSubst x es (wsubst_rec_true_prf H Hfy) e er →
+  WSubst x es H (Rec f y e) (Rec f y er).
+Proof.
+  intros ?; red; f_equal/=; case_decide; last done.
+  by etrans; [apply wsubst_proof_irrel|].
+Qed.
+Lemma do_wsubst_rec_false {X Y x es f y e} {H : X `included` x :: Y}
+    (Hfy : ¬(BNamed x ≠ f ∧ BNamed x ≠ y)) er :
+  WExpr (wsubst_rec_false_prf H Hfy) e er →
+  WSubst x es H (Rec f y e) (Rec f y er).
+Proof.
+  intros; red; f_equal/=; case_decide; first done.
+  by etrans; [apply wexpr_proof_irrel|].
+Qed.
+
+Ltac bool_decide_no_check := apply (bool_decide_unpack _); vm_cast_no_check I.
+Hint Extern 0 (WSubst ?x ?v _ (Rec ?f ?y ?e) _) =>
+  match eval vm_compute in (bool_decide (BNamed x ≠ f ∧ BNamed x ≠ y)) with
+  | true => eapply (do_wsubst_rec_true ltac:(bool_decide_no_check))
+  | false => eapply (do_wsubst_rec_false ltac:(bool_decide_no_check))
   end : typeclass_instances.
 
-Instance subst_rec f y e x v er :
-  SubstIf (BNamed x ≠ f ∧ BNamed x ≠ y) e x v er →
-  Subst (Rec f y e) x v (Rec f y er).
-Proof. intros [??]; red; f_equal/=; case_decide; auto. Qed.
+(* Values *)
+Instance do_wsubst_of_val_nil x es (H : [] `included` [x]) w :
+  WSubst x es H (of_val w) (of_val w) | 0.
+Proof. apply wsubst_closed_nil. Qed.
+Instance do_wsubst_of_val_nil' {X} x es (H : X `included` [x]) w :
+  WSubst x es H (of_val' w) (of_val w) | 0.
+Proof. by rewrite /WSubst /of_val' wsubst_wexpr' wsubst_closed_nil. Qed.
+Instance do_wsubst_of_val Y x es (H : [] `included` x :: Y) w :
+  WSubst x es H (of_val w) (of_val' w) | 1.
+Proof. apply wsubst_closed, not_elem_of_nil. Qed.
+Instance do_wsubst_of_val' X Y x es (H : X `included` x :: Y) w :
+  WSubst x es H (of_val' w) (of_val' w) | 1.
+Proof.
+  rewrite /WSubst /of_val' wsubst_wexpr'.
+  apply wsubst_closed, not_elem_of_nil.
+Qed.
 
-Instance subst_app e1 e2 x v e1r e2r :
-  Subst e1 x v e1r → Subst e2 x v e2r → Subst (App e1 e2) x v (App e1r e2r).
-Proof. by intros; red; f_equal/=. Qed.
-Instance subst_unop op e x v er :
-  Subst e x v er → Subst (UnOp op e) x v (UnOp op er).
+(* Boring connectives *)
+Section wsubst.
+Context {X Y} (x : string) (es : expr []) (H : X `included` x :: Y).
+Notation Sub := (WSubst x es H).
+
+(* Ground terms *)
+Global Instance do_wsubst_lit l : Sub (Lit l) (Lit l).
+Proof. done. Qed.
+Global Instance do_wsubst_loc l : Sub (Loc l) (Loc l).
+Proof. done. Qed.
+Global Instance do_wsubst_app e1 e2 e1r e2r :
+  Sub e1 e1r → Sub e2 e2r → Sub (App e1 e2) (App e1r e2r).
+Proof. intros; red; f_equal/=; apply: do_wsubst. Qed.
+Global Instance do_wsubst_unop op e er : Sub e er → Sub (UnOp op e) (UnOp op er).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_binop op e1 e2 x v e1r e2r :
-  Subst e1 x v e1r → Subst e2 x v e2r →
-  Subst (BinOp op e1 e2) x v (BinOp op e1r e2r).
+Global Instance do_wsubst_binop op e1 e2 e1r e2r :
+  Sub e1 e1r → Sub e2 e2r → Sub (BinOp op e1 e2) (BinOp op e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_if e0 e1 e2 x v e0r e1r e2r :
-  Subst e0 x v e0r → Subst e1 x v e1r → Subst e2 x v e2r →
-  Subst (If e0 e1 e2) x v (If e0r e1r e2r).
+Global Instance do_wsubst_if e0 e1 e2 e0r e1r e2r :
+  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (If e0 e1 e2) (If e0r e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_pair e1 e2 x v e1r e2r :
-  Subst e1 x v e1r → Subst e2 x v e2r → Subst (Pair e1 e2) x v (Pair e1r e2r).
+Global Instance do_wsubst_pair e1 e2 e1r e2r :
+  Sub e1 e1r → Sub e2 e2r → Sub (Pair e1 e2) (Pair e1r e2r).
 Proof. by intros ??; red; f_equal/=. Qed.
-Instance subst_fst e x v er : Subst e x v er → Subst (Fst e) x v (Fst er).
+Global Instance do_wsubst_fst e er : Sub e er → Sub (Fst e) (Fst er).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_snd e x v er : Subst e x v er → Subst (Snd e) x v (Snd er).
+Global Instance do_wsubst_snd e er : Sub e er → Sub (Snd e) (Snd er).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_injL e x v er : Subst e x v er → Subst (InjL e) x v (InjL er).
+Global Instance do_wsubst_injL e er : Sub e er → Sub (InjL e) (InjL er).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_injR e x v er : Subst e x v er → Subst (InjR e) x v (InjR er).
+Global Instance do_wsubst_injR e er : Sub e er → Sub (InjR e) (InjR er).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_case e0 e1 e2 x v e0r e1r e2r :
-  Subst e0 x v e0r → Subst e1 x v e1r → Subst e2 x v e2r →
-  Subst (Case e0 e1 e2) x v (Case e0r e1r e2r).
+Global Instance do_wsubst_case e0 e1 e2 e0r e1r e2r :
+  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (Case e0 e1 e2) (Case e0r e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_fork e x v er : Subst e x v er → Subst (Fork e) x v (Fork er).
+Global Instance do_wsubst_fork e er : Sub e er → Sub (Fork e) (Fork er).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_alloc e x v er : Subst e x v er → Subst (Alloc e) x v (Alloc er).
+Global Instance do_wsubst_alloc e er : Sub e er → Sub (Alloc e) (Alloc er).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_load e x v er : Subst e x v er → Subst (Load e) x v (Load er).
+Global Instance do_wsubst_load e er : Sub e er → Sub (Load e) (Load er).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_store e1 e2 x v e1r e2r :
-  Subst e1 x v e1r → Subst e2 x v e2r → Subst (Store e1 e2) x v (Store e1r e2r).
+Global Instance do_wsubst_store e1 e2 e1r e2r :
+  Sub e1 e1r → Sub e2 e2r → Sub (Store e1 e2) (Store e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
-Instance subst_cas e0 e1 e2 x v e0r e1r e2r :
-  Subst e0 x v e0r → Subst e1 x v e1r → Subst e2 x v e2r →
-  Subst (Cas e0 e1 e2) x v (Cas e0r e1r e2r).
+Global Instance do_wsubst_cas e0 e1 e2 e0r e1r e2r :
+  Sub e0 e0r → Sub e1 e1r → Sub e2 e2r → Sub (Cas e0 e1 e2) (Cas e0r e1r e2r).
 Proof. by intros; red; f_equal/=. Qed.
+End wsubst.
+
+(** * The tactic *)
+Lemma do_subst {X} (x: string) (es: expr []) (e: expr (x :: X)) (er: expr X) :
+  WSubst x es (λ _, id) e er → subst x es e = er.
+Proof. done. Qed.
 
-Global Opaque subst.
+Ltac simpl_subst :=
+  repeat match goal with
+  | |- context [subst ?x ?es ?e] => progress rewrite (@do_subst _ x es e)
+  | |- _ => progress csimpl
+  end.
+Arguments wexpr : simpl never.
+Arguments subst : simpl never.
+Arguments wsubst : simpl never.
+Arguments of_val : simpl never.
+Arguments of_val' : simpl never.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 359c4c2b2..7eae3f631 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -1,4 +1,4 @@
-From heap_lang Require Export lang.
+From heap_lang Require Export substitution.
 From prelude Require Import fin_maps.
 Import heap_lang.
 
@@ -34,6 +34,7 @@ Ltac reshape_val e tac :=
   let rec go e :=
   match e with
   | of_val ?v => v
+  | of_val' ?v => v
   | Rec ?f ?x ?e => constr:(RecV f x e)
   | Lit ?l => constr:(LitV l)
   | Pair ?e1 ?e2 =>
@@ -83,7 +84,7 @@ Ltac do_step tac :=
   | |- 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];
+       first [apply alloc_fresh|econstructor; try reflexivity; simpl_subst];
        rewrite ?to_of_val; tac; fail)
   | |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
      first [apply alloc_fresh|econstructor];
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 45901ad1a..6aa456571 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -4,21 +4,15 @@ From heap_lang Require Import wp_tactics heap notation.
 Import uPred.
 
 Section LangTests.
-  Definition add := (#21 + #21)%E.
+  Definition add : expr [] := (#21 + #21)%E.
   Goal ∀ σ, prim_step add σ (#42) σ None.
   Proof. intros; do_step done. Qed.
-  Definition rec_app : expr := ((rec: "f" "x" := "f" "x") #0).
+  Definition rec_app : expr [] := ((rec: "f" "x" := '"f" '"x") #0)%E.
   Goal ∀ σ, prim_step rec_app σ rec_app σ None.
-  Proof.
-    intros. rewrite /rec_app. (* FIXME: do_step does not work here *)
-    by eapply (Ectx_step  _ _ _ _ _ []), (BetaS _ _ _ _ #0).
-  Qed.
-  Definition lam : expr := λ: "x", "x" + #21.
+  Proof. intros. rewrite /rec_app. do_step done. Qed.
+  Definition lam : expr [] := (λ: "x", '"x" + #21)%E.
   Goal ∀ σ, prim_step (lam #21)%E σ add σ None.
-  Proof.
-    intros. rewrite /lam. (* FIXME: do_step does not work here *)
-    by eapply (Ectx_step  _ _ _ _ _ []), (BetaS <> "x" ("x" + #21) _ #21).
-  Qed.
+  Proof. intros. rewrite /lam. do_step done. Qed.
 End LangTests.
 
 Section LiftingTests.
@@ -27,8 +21,8 @@ Section LiftingTests.
   Implicit Types P Q : iPropG heap_lang Σ.
   Implicit Types Φ : val → iPropG heap_lang Σ.
 
-  Definition heap_e  : expr :=
-    let: "x" := ref #1 in "x" <- !"x" + #1;; !"x".
+  Definition heap_e  : expr [] :=
+    let: "x" := ref #1 in '"x" <- !'"x" + #1 ;; !'"x".
   Lemma heap_e_spec E N :
      nclose N ⊆ E → heap_ctx N ⊑ || heap_e @ E {{ λ v, v = #2 }}.
   Proof.
@@ -42,16 +36,11 @@ Section LiftingTests.
 
   Definition FindPred : val :=
     rec: "pred" "x" "y" :=
-      let: "yp" := "y" + #1 in
-      if: "yp" < "x" then "pred" "x" "yp" else "y".
+      let: "yp" := '"y" + #1 in
+      if: '"yp" < '"x" then '"pred" '"x" '"yp" else '"y".
   Definition Pred : val :=
     λ: "x",
-      if: "x" ≤ #0 then -FindPred (-"x" + #2) #0 else FindPred "x" #0.
-
-  Instance FindPred_closed : Closed FindPred | 0.
-  Proof. solve_closed. Qed.
-  Instance Pred_closed : Closed Pred | 0.
-  Proof. solve_closed. Qed.
+      if: '"x" ≤ #0 then -^FindPred (-'"x" + #2) #0 else ^FindPred '"x" #0.
 
   Lemma FindPred_spec n1 n2 E Φ :
     n1 < n2 → 
@@ -74,7 +63,7 @@ Section LiftingTests.
   Qed.
 
   Lemma Pred_user E :
-    (True : iProp) ⊑ || let: "x" := Pred #42 in Pred "x" @ E {{ λ v, v = #40 }}.
+    (True : iProp) ⊑ || let: "x" := Pred #42 in ^Pred '"x" @ E {{ λ v, v = #40 }}.
   Proof.
     intros. ewp apply Pred_spec. wp_let. ewp apply Pred_spec. auto with I.
   Qed.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index c9b6bd404..cd3a74aa3 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -27,25 +27,25 @@ Tactic Notation "wp_rec" ">" :=
     idtac; (* <https://coq.inria.fr/bugs/show_bug.cgi?id=4584> *)
     lazymatch goal with
     | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-      match eval cbv in e' with
-      | App (Rec _ _ _) _ =>
-         wp_bind K; etrans;
-           [|first [eapply wp_rec' | eapply wp_rec];
-               repeat (reflexivity || rewrite /= to_of_val)];
-           simpl_subst; wp_finish
-      end)
+      match eval hnf in e' with App ?e1 _ =>
+(* hnf does not reduce through an of_val *)
+(*      match eval hnf in e1 with Rec _ _ _ => *)
+      wp_bind K; etrans;
+         [|eapply wp_rec'; repeat rewrite /= to_of_val; reflexivity];
+         simpl_subst; wp_finish
+(*      end *) end)
      end).
 Tactic Notation "wp_rec" := wp_rec>; try strip_later.
 
 Tactic Notation "wp_lam" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval cbv in e' with
-    | App (Rec BAnon _ _) _ =>
-       wp_bind K; etrans;
-         [|eapply wp_lam; repeat (reflexivity || rewrite /= to_of_val)];
-         simpl_subst; wp_finish
-    end)
+    match eval hnf in e' with App ?e1 _ =>
+(*    match eval hnf in e1 with Rec BAnon _ _ => *)
+    wp_bind K; etrans;
+       [|eapply wp_lam; repeat (reflexivity || rewrite /= to_of_val)];
+       simpl_subst; wp_finish
+(*    end *) end)
   end.
 Tactic Notation "wp_lam" := wp_lam>; try strip_later.
 
@@ -57,7 +57,7 @@ Tactic Notation "wp_seq" := wp_let.
 Tactic Notation "wp_op" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval cbv in e' with
+    match eval hnf in e' with
     | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
     | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
     | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
@@ -72,10 +72,9 @@ Tactic Notation "wp_op" := wp_op>; try strip_later.
 Tactic Notation "wp_if" ">" :=
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    match eval cbv in e' with
-    | If _ _ _ =>
-       wp_bind K;
-       etrans; [|apply wp_if_true || apply wp_if_false]; wp_finish
+    match eval hnf in e' with If _ _ _ =>
+    wp_bind K;
+    etrans; [|apply wp_if_true || apply wp_if_false]; wp_finish
     end)
   end.
 Tactic Notation "wp_if" := wp_if>; try strip_later.
-- 
GitLab