From 697523ea57bd2a8405e4c62d417b9d594424a5d0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 19 Jul 2016 17:02:49 +0200
Subject: [PATCH] Also establish Closed and to_val _ = Some _ via reification.

---
 _CoqProject              |   1 -
 heap_lang/lang.v         |  87 ++----------------
 heap_lang/lib/par.v      |   2 +-
 heap_lang/substitution.v | 134 ---------------------------
 heap_lang/tactics.v      | 193 ++++++++++++++++++++++++++++++++++++++-
 heap_lang/wp_tactics.v   |  11 ++-
 6 files changed, 211 insertions(+), 217 deletions(-)
 delete mode 100644 heap_lang/substitution.v

diff --git a/_CoqProject b/_CoqProject
index df988bd6c..92fe4e429 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -88,7 +88,6 @@ heap_lang/wp_tactics.v
 heap_lang/lifting.v
 heap_lang/derived.v
 heap_lang/notation.v
-heap_lang/substitution.v
 heap_lang/heap.v
 heap_lang/lib/spawn.v
 heap_lang/lib/par.v
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index f67032a94..51787af1c 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -345,93 +345,24 @@ Lemma alloc_fresh e v σ :
   to_val e = Some v → head_step (Alloc e) σ (Lit (LitLoc l)) (<[l:=v]>σ) None.
 Proof. by intros; apply AllocS, (not_elem_of_dom (D:=gset _)), is_fresh. Qed.
 
-(** Value type class *)
-Class IntoValue (e : expr) (v : val) := into_value : to_val e = Some v.
-Instance into_value_of_val v : IntoValue (of_val v) v.
-Proof. by rewrite /IntoValue to_of_val. Qed.
-Instance into_value_rec f x e `{!Closed (f :b: x :b: []) e} :
-  IntoValue (Rec f x e) (RecV f x e).
-Proof.
-  rewrite /IntoValue /=; case_decide; last done.
-  do 2 f_equal. by apply (proof_irrel).
-Qed.
-Instance into_value_lit l : IntoValue (Lit l) (LitV l).
-Proof. done. Qed.
-Instance into_value_pair e1 e2 v1 v2 :
-  IntoValue e1 v1 → IntoValue e2 v2 → IntoValue (Pair e1 e2) (PairV v1 v2).
-Proof. by rewrite /IntoValue /= => -> /= ->. Qed.
-Instance into_value_injl e v : IntoValue e v → IntoValue (InjL e) (InjLV v).
-Proof. by rewrite /IntoValue /= => ->. Qed.
-Instance into_value_injr e v : IntoValue e v → IntoValue (InjR e) (InjRV v).
-Proof. by rewrite /IntoValue /= => ->. Qed.
-
 (** Closed expressions *)
 Lemma is_closed_weaken X Y e : is_closed X e → X `included` Y → is_closed Y e.
 Proof. revert X Y; induction e; naive_solver (eauto; set_solver). Qed.
 
-Lemma closed_subst X e x es : Closed X e → x ∉ X → subst x es e = e.
+Lemma is_closed_weaken_nil X e : is_closed [] e → is_closed X e.
+Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
+
+Lemma is_closed_subst X e x es : is_closed X e → x ∉ X → subst x es e = e.
 Proof.
-  rewrite /Closed. revert X.
-  induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
+  revert X. induction e=> X /=; rewrite ?bool_decide_spec ?andb_True=> ??;
     repeat case_decide; simplify_eq/=; f_equal; intuition eauto with set_solver.
 Qed.
 
-Lemma closed_nil_subst e x es : Closed [] e → subst x es e = e.
-Proof. intros. apply closed_subst with []; set_solver. Qed.
+Lemma is_closed_nil_subst e x es : is_closed [] e → subst x es e = e.
+Proof. intros. apply is_closed_subst with []; set_solver. Qed.
 
-Lemma closed_nil_closed X e : Closed [] e → Closed X e.
-Proof. intros. by apply is_closed_weaken with [], included_nil. Qed.
-Hint Immediate closed_nil_closed : typeclass_instances.
-
-Instance closed_of_val X v : Closed X (of_val v).
-Proof.
-  apply is_closed_weaken with []; last set_solver.
-  induction v; simpl; auto.
-Qed.
-Instance closed_rec X f x e : Closed (f :b: x :b: X) e → Closed X (Rec f x e).
-Proof. done. Qed.
-Lemma closed_var X x : bool_decide (x ∈ X) → Closed X (Var x).
-Proof. done. Qed.
-Hint Extern 1000 (Closed _ (Var _)) =>
-  apply closed_var; vm_compute; exact I : typeclass_instances.
-
-Section closed.
-  Context (X : list string).
-  Notation C := (Closed X).
-
-  Global Instance closed_lit l : C (Lit l).
-  Proof. done. Qed.
-  Global Instance closed_unop op e : C e → C (UnOp op e).
-  Proof. done. Qed.
-  Global Instance closed_fst e : C e → C (Fst e).
-  Proof. done. Qed.
-  Global Instance closed_snd e : C e → C (Snd e).
-  Proof. done. Qed.
-  Global Instance closed_injl e : C e → C (InjL e).
-  Proof. done. Qed.
-  Global Instance closed_injr e : C e → C (InjR e).
-  Proof. done. Qed.
-  Global Instance closed_fork e : C e → C (Fork e).
-  Proof. done. Qed.
-  Global Instance closed_load e : C e → C (Load e).
-  Proof. done. Qed.
-  Global Instance closed_alloc e : C e → C (Alloc e).
-  Proof. done. Qed.
-  Global Instance closed_app e1 e2 : C e1 → C e2 → C (App e1 e2).
-  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
-  Global Instance closed_binop op e1 e2 : C e1 → C e2 → C (BinOp op e1 e2).
-  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
-  Global Instance closed_pair e1 e2 : C e1 → C e2 → C (Pair e1 e2).
-  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
-  Global Instance closed_store e1 e2 : C e1 → C e2 → C (Store e1 e2).
-  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
-  Global Instance closed_if e0 e1 e2 : C e0 → C e1 → C e2 → C (If e0 e1 e2).
-  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
-  Global Instance closed_case e0 e1 e2 : C e0 → C e1 → C e2 → C (Case e0 e1 e2).
-  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
-  Global Instance closed_cas e0 e1 e2 : C e0 → C e1 → C e2 → C (CAS e0 e1 e2).
-  Proof. intros. by rewrite /Closed /= !andb_True. Qed.
-End closed.
+Lemma is_closed_of_val X v : is_closed X (of_val v).
+Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
 
 (** Equality and other typeclass stuff *)
 Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index de9ce75d4..cbd34ceb3 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -39,7 +39,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp)
    ∀ v1 v2, Ψ1 v1 ★ Ψ2 v2 -★ ▷ Φ (v1,v2)%V)
   ⊢ WP e1 || e2 {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); [done|apply into_value|].
+  iIntros (?) "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2); try wp_done.
   iFrame "Hh H". iSplitL "H1"; by wp_let.
 Qed.
 End proof.
diff --git a/heap_lang/substitution.v b/heap_lang/substitution.v
deleted file mode 100644
index 8e1b75cb8..000000000
--- a/heap_lang/substitution.v
+++ /dev/null
@@ -1,134 +0,0 @@
-From iris.heap_lang Require Export lang.
-Import heap_lang.
-
-Module W.
-Inductive expr :=
-  | ClosedExpr (e : heap_lang.expr) `{!Closed [] e}
-  (* Base lambda calculus *)
-  | Var (x : string)
-  | Rec (f x : binder) (e : expr)
-  | App (e1 e2 : expr)
-  (* 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)
-  (* Products *)
-  | Pair (e1 e2 : expr)
-  | Fst (e : expr)
-  | Snd (e : expr)
-  (* Sums *)
-  | InjL (e : expr)
-  | InjR (e : expr)
-  | Case (e0 : expr) (e1 : expr) (e2 : expr)
-  (* Concurrency *)
-  | Fork (e : expr)
-  (* Heap *)
-  | Alloc (e : expr)
-  | Load (e : expr)
-  | Store (e1 : expr) (e2 : expr)
-  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
-
-Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
-  match e with
-  | ClosedExpr e H => @ClosedExpr e H
-  | Var y => if decide (x = y) then es else Var y
-  | Rec f y e =>
-     Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
-  | App e1 e2 => App (subst x es e1) (subst x es e2)
-  | Lit l => Lit l
-  | UnOp op e => UnOp op (subst x es e)
-  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
-  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
-  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
-  | Fst e => Fst (subst x es e)
-  | Snd e => Snd (subst x es e)
-  | InjL e => InjL (subst x es e)
-  | InjR e => InjR (subst x es e)
-  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
-  | Fork e => Fork (subst x es e)
-  | Alloc e => Alloc (subst x es e)
-  | Load e => Load (subst x es e)
-  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
-  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
-  end.
-
-Fixpoint to_expr (e : expr) : heap_lang.expr :=
-  match e with
-  | ClosedExpr e _ => e
-  | Var x => heap_lang.Var x
-  | Rec f x e => heap_lang.Rec f x (to_expr e)
-  | App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
-  | Lit l => heap_lang.Lit l
-  | UnOp op e => heap_lang.UnOp op (to_expr e)
-  | BinOp op e1 e2 => heap_lang.BinOp op (to_expr e1) (to_expr e2)
-  | If e0 e1 e2 => heap_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
-  | Pair e1 e2 => heap_lang.Pair (to_expr e1) (to_expr e2)
-  | Fst e => heap_lang.Fst (to_expr e)
-  | Snd e => heap_lang.Snd (to_expr e)
-  | InjL e => heap_lang.InjL (to_expr e)
-  | InjR e => heap_lang.InjR (to_expr e)
-  | Case e0 e1 e2 => heap_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
-  | Fork e => heap_lang.Fork (to_expr e)
-  | Alloc e => heap_lang.Alloc (to_expr e)
-  | Load e => heap_lang.Load (to_expr e)
-  | Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
-  | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
-  end.
-
-Ltac of_expr e :=
-  lazymatch e with
-  | heap_lang.Var ?x => constr:(Var x)
-  | heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
-  | heap_lang.App ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
-  | heap_lang.Lit ?l => constr:(Lit l)
-  | heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
-  | heap_lang.BinOp ?op ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
-  | heap_lang.If ?e0 ?e1 ?e2 =>
-     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
-     constr:(If e0 e1 e2)
-  | heap_lang.Pair ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
-  | heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
-  | heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
-  | heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
-  | heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
-  | heap_lang.Case ?e0 ?e1 ?e2 =>
-     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
-     constr:(Case e0 e1 e2)
-  | heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
-  | heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
-  | heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
-  | heap_lang.Store ?e1 ?e2 =>
-     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
-  | heap_lang.CAS ?e0 ?e1 ?e2 =>
-     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
-     constr:(CAS e0 e1 e2)
-  | to_expr ?e => e
-  | of_val ?v => constr:(ClosedExpr (of_val v))
-  (* is_var e; constr:(Closed e) does not work *)
-  | _ => constr:(ltac:(is_var e; exact (ClosedExpr e)))
-  end.
-
-Lemma to_expr_subst x er e :
-  to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
-Proof.
-  induction e; simpl;
-    repeat case_decide; f_equal; auto using closed_nil_subst, eq_sym.
-Qed.
-End W.
-
-(** * The tactic *)
-Ltac simpl_subst :=
-  csimpl;
-  repeat match goal with
-  | |- context [subst ?x ?er ?e] =>
-      let er' := W.of_expr er in let e' := W.of_expr e in
-      change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
-      rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
-  end;
-  unfold W.to_expr.
-Arguments W.to_expr : simpl never.
-Arguments subst : simpl never.
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 1f669cc2e..1957ab14b 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -1,7 +1,198 @@
-From iris.heap_lang Require Export substitution.
+From iris.heap_lang Require Export lang.
 From iris.prelude Require Import fin_maps.
 Import heap_lang.
 
+Module W.
+Inductive expr :=
+  | Val (v : val)
+  | ClosedExpr (e : heap_lang.expr) `{!Closed [] e}
+  (* Base lambda calculus *)
+  | Var (x : string)
+  | Rec (f x : binder) (e : expr)
+  | App (e1 e2 : expr)
+  (* 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)
+  (* Products *)
+  | Pair (e1 e2 : expr)
+  | Fst (e : expr)
+  | Snd (e : expr)
+  (* Sums *)
+  | InjL (e : expr)
+  | InjR (e : expr)
+  | Case (e0 : expr) (e1 : expr) (e2 : expr)
+  (* Concurrency *)
+  | Fork (e : expr)
+  (* Heap *)
+  | Alloc (e : expr)
+  | Load (e : expr)
+  | Store (e1 : expr) (e2 : expr)
+  | CAS (e0 : expr) (e1 : expr) (e2 : expr).
+
+Fixpoint to_expr (e : expr) : heap_lang.expr :=
+  match e with
+  | Val v => of_val v
+  | ClosedExpr e _ => e
+  | Var x => heap_lang.Var x
+  | Rec f x e => heap_lang.Rec f x (to_expr e)
+  | App e1 e2 => heap_lang.App (to_expr e1) (to_expr e2)
+  | Lit l => heap_lang.Lit l
+  | UnOp op e => heap_lang.UnOp op (to_expr e)
+  | BinOp op e1 e2 => heap_lang.BinOp op (to_expr e1) (to_expr e2)
+  | If e0 e1 e2 => heap_lang.If (to_expr e0) (to_expr e1) (to_expr e2)
+  | Pair e1 e2 => heap_lang.Pair (to_expr e1) (to_expr e2)
+  | Fst e => heap_lang.Fst (to_expr e)
+  | Snd e => heap_lang.Snd (to_expr e)
+  | InjL e => heap_lang.InjL (to_expr e)
+  | InjR e => heap_lang.InjR (to_expr e)
+  | Case e0 e1 e2 => heap_lang.Case (to_expr e0) (to_expr e1) (to_expr e2)
+  | Fork e => heap_lang.Fork (to_expr e)
+  | Alloc e => heap_lang.Alloc (to_expr e)
+  | Load e => heap_lang.Load (to_expr e)
+  | Store e1 e2 => heap_lang.Store (to_expr e1) (to_expr e2)
+  | CAS e0 e1 e2 => heap_lang.CAS (to_expr e0) (to_expr e1) (to_expr e2)
+  end.
+
+Ltac of_expr e :=
+  lazymatch e with
+  | heap_lang.Var ?x => constr:(Var x)
+  | heap_lang.Rec ?f ?x ?e => let e := of_expr e in constr:(Rec f x e)
+  | heap_lang.App ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(App e1 e2)
+  | heap_lang.Lit ?l => constr:(Lit l)
+  | heap_lang.UnOp ?op ?e => let e := of_expr e in constr:(UnOp op e)
+  | heap_lang.BinOp ?op ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(BinOp op e1 e2)
+  | heap_lang.If ?e0 ?e1 ?e2 =>
+     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
+     constr:(If e0 e1 e2)
+  | heap_lang.Pair ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Pair e1 e2)
+  | heap_lang.Fst ?e => let e := of_expr e in constr:(Fst e)
+  | heap_lang.Snd ?e => let e := of_expr e in constr:(Snd e)
+  | heap_lang.InjL ?e => let e := of_expr e in constr:(InjL e)
+  | heap_lang.InjR ?e => let e := of_expr e in constr:(InjR e)
+  | heap_lang.Case ?e0 ?e1 ?e2 =>
+     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
+     constr:(Case e0 e1 e2)
+  | heap_lang.Fork ?e => let e := of_expr e in constr:(Fork e)
+  | heap_lang.Alloc ?e => let e := of_expr e in constr:(Alloc e)
+  | heap_lang.Load ?e => let e := of_expr e in constr:(Load e)
+  | heap_lang.Store ?e1 ?e2 =>
+     let e1 := of_expr e1 in let e2 := of_expr e2 in constr:(Store e1 e2)
+  | heap_lang.CAS ?e0 ?e1 ?e2 =>
+     let e0 := of_expr e0 in let e1 := of_expr e1 in let e2 := of_expr e2 in
+     constr:(CAS e0 e1 e2)
+  | to_expr ?e => e
+  | of_val ?v => constr:(Val v)
+  | _ => constr:(ltac:(
+     match goal with H : Closed [] e |- _ => exact (@ClosedExpr e H) end))
+  end.
+
+Fixpoint is_closed (X : list string) (e : expr) : bool :=
+  match e with
+  | Val _ | ClosedExpr _ _ => true
+  | Var x => bool_decide (x ∈ X)
+  | Rec f x e => is_closed (f :b: x :b: X) e
+  | Lit _ => true
+  | UnOp _ e | Fst e | Snd e | InjL e | InjR e | Fork e | Alloc e | Load e =>
+     is_closed X e
+  | App e1 e2 | BinOp _ e1 e2 | Pair e1 e2 | Store e1 e2 =>
+     is_closed X e1 && is_closed X e2
+  | If e0 e1 e2 | Case e0 e1 e2 | CAS e0 e1 e2 =>
+     is_closed X e0 && is_closed X e1 && is_closed X e2
+  end.
+Lemma is_closed_correct X e : is_closed X e → heap_lang.is_closed X (to_expr e).
+Proof.
+  revert X.
+  induction e; naive_solver eauto using is_closed_of_val, is_closed_weaken_nil.
+Qed.
+
+Fixpoint to_val (e : expr) : option val :=
+  match e with
+  | Val v => Some v
+  | Rec f x e =>
+     if decide (is_closed (f :b: x :b: []) e) is left H
+     then Some (@RecV f x (to_expr e) (is_closed_correct _ _ H)) else None
+  | Lit l => Some (LitV l)
+  | 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
+  | _ => None
+  end.
+Lemma to_val_Some e v :
+  to_val e = Some v → heap_lang.to_val (to_expr e) = Some v.
+Proof.
+  revert v. induction e; intros; simplify_option_eq; rewrite ?to_of_val; auto.
+  - do 2 f_equal. apply proof_irrel.
+  - exfalso. unfold Closed in *; eauto using is_closed_correct.
+Qed.
+
+Fixpoint subst (x : string) (es : expr) (e : expr)  : expr :=
+  match e with
+  | Val v => Val v
+  | ClosedExpr e H => @ClosedExpr e H
+  | Var y => if decide (x = y) then es else Var y
+  | Rec f y e =>
+     Rec f y $ if decide (BNamed x ≠ f ∧ BNamed x ≠ y) then subst x es e else e
+  | App e1 e2 => App (subst x es e1) (subst x es e2)
+  | Lit l => Lit l
+  | UnOp op e => UnOp op (subst x es e)
+  | BinOp op e1 e2 => BinOp op (subst x es e1) (subst x es e2)
+  | If e0 e1 e2 => If (subst x es e0) (subst x es e1) (subst x es e2)
+  | Pair e1 e2 => Pair (subst x es e1) (subst x es e2)
+  | Fst e => Fst (subst x es e)
+  | Snd e => Snd (subst x es e)
+  | InjL e => InjL (subst x es e)
+  | InjR e => InjR (subst x es e)
+  | Case e0 e1 e2 => Case (subst x es e0) (subst x es e1) (subst x es e2)
+  | Fork e => Fork (subst x es e)
+  | Alloc e => Alloc (subst x es e)
+  | Load e => Load (subst x es e)
+  | Store e1 e2 => Store (subst x es e1) (subst x es e2)
+  | CAS e0 e1 e2 => CAS (subst x es e0) (subst x es e1) (subst x es e2)
+  end.
+Lemma to_expr_subst x er e :
+  to_expr (subst x er e) = heap_lang.subst x (to_expr er) (to_expr e).
+Proof.
+  induction e; simpl; repeat case_decide;
+    f_equal; auto using is_closed_nil_subst, is_closed_of_val, eq_sym.
+Qed.
+End W.
+
+Ltac solve_closed :=
+  match goal with
+  | |- Closed ?X ?e =>
+     let e' := W.of_expr e in change (Closed X (W.to_expr e'));
+     apply W.is_closed_correct; vm_compute; exact I
+  end.
+Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
+
+Ltac solve_to_val :=
+  try match goal with
+  | |- language.to_val ?e = Some ?v => change (to_val e = Some v)
+  end;
+  match goal with
+  | |- to_val ?e = Some ?v =>
+     let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
+     apply W.to_val_Some; simpl; reflexivity
+  end.
+
+(** Substitution *)
+Ltac simpl_subst :=
+  csimpl;
+  repeat match goal with
+  | |- context [subst ?x ?er ?e] =>
+      let er' := W.of_expr er in let e' := W.of_expr e in
+      change (subst x er e) with (subst x (W.to_expr er') (W.to_expr e'));
+      rewrite <-(W.to_expr_subst x); simpl (* ssr rewrite is slower *)
+  end;
+  unfold W.to_expr.
+Arguments W.to_expr : simpl never.
+Arguments subst : simpl never.
+
 (** The tactic [inv_head_step] performs inversion on hypotheses of the
 shape [head_step]. The tactic will discharge head-reductions starting
 from values, and simplifies hypothesis related to conversions from and
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 3c71747b8..25da92820 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export upred_tactics.
-From iris.heap_lang Require Export tactics derived substitution.
+From iris.heap_lang Require Export tactics derived.
 Import uPred.
 
 (** wp-specific helper tactics *)
@@ -11,7 +11,14 @@ Ltac wp_bind K :=
 
 (* TODO: Do something better here *)
 Ltac wp_done :=
-  fast_done || apply into_value || apply _ || (rewrite /= ?to_of_val; fast_done).
+  match goal with
+  | |- Closed _ _ => solve_closed
+  | |- to_val _ = Some _ => solve_to_val
+  | |- language.to_val _ = Some _ => solve_to_val
+  | |- Is_true (atomic _) => rewrite /= ?to_of_val; fast_done
+  | |- Is_true (language.atomic _) => rewrite /= ?to_of_val; fast_done
+  | _ => fast_done
+  end.
 
 (* sometimes, we will have to do a final view shift, so only apply
 pvs_intro if we obtain a consecutive wp *)
-- 
GitLab