Simplify substitution stuff.

heap_lang/derived.v

@@ -20,7 +20,7 @@ Implicit Types Φ : val → iProp heap_lang Σ.
 Lemma wp_lam E x ef e v Φ :
   to_val e = Some v →
   ▷ WP subst' x e ef @ E {{ Φ }} ⊢ WP App (Lam x ef) e @ E {{ Φ }}.
-Proof. intros. by rewrite -wp_rec. Qed.
+Proof. intros. by rewrite -(wp_rec _ BAnon) //. Qed.
 
 Lemma wp_let E x e1 e2 v Φ :
   to_val e1 = Some v →

heap_lang/lib/spawn.v

@@ -57,7 +57,7 @@ Lemma spawn_spec (Ψ : val → iProp) e (f : val) (Φ : val → iProp) :
   ⊢ WP spawn e {{ Φ }}.
 Proof.
   iIntros {<-%of_to_val ?} "(#Hh&Hf&HΦ)". rewrite /spawn.
-  wp_let; wp_alloc l as "Hl"; wp_let.
+  wp_let. wp_alloc l as "Hl". wp_let.
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
   iPvs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?"; first done.
   { iNext. iExists (InjLV #0). iFrame "Hl". by iLeft. }

heap_lang/lifting.v

@@ -86,22 +86,16 @@ Proof.
   rewrite later_sep -(wp_value _ _ (Lit _)) //.
 Qed.
 
-Lemma wp_rec E f x e1 e2 v Φ :
-  to_val e2 = Some v →
-  ▷ WP subst' x e2 (subst' f (Rec f x e1) e1) @ E {{ Φ }}
-  ⊢ WP App (Rec f x e1) e2 @ E {{ Φ }}.
-Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (App _ _)
-    (subst' x e2 (subst' f (Rec f x e1) e1)) None) //= ?right_id;
-    intros; inv_head_step; eauto.
-Qed.
-
-Lemma wp_rec' E f x erec e1 e2 v2 Φ :
+Lemma wp_rec E f x erec e1 e2 v2 Φ :
   e1 = Rec f x erec →
   to_val e2 = Some v2 →
   ▷ WP subst' x e2 (subst' f e1 erec) @ E {{ Φ }}
   ⊢ WP App e1 e2 @ E {{ Φ }}.
-Proof. intros ->. apply wp_rec. Qed.
+Proof.
+  intros -> ?. rewrite -(wp_lift_pure_det_head_step (App _ _)
+    (subst' x e2 (subst' f (Rec f x erec) erec)) None) //= ?right_id;
+    intros; inv_head_step; eauto.
+Qed.
 
 Lemma wp_un_op E op l l' Φ :
   un_op_eval op l = Some l' →

heap_lang/notation.v

@@ -33,7 +33,7 @@ Notation "# l" := (LitV l%Z%V) (at level 8, format "# l").
 Notation "# l" := (Lit l%Z%V) (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.
+Notation "^ e" := (wexpr' e) (at level 8, format "^ e") : expr_scope.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)

heap_lang/substitution.v

@@ -20,18 +20,14 @@ Instance do_wexpr_rec_true {X Y f y e} {H : X `included` Y} er :
 Proof. intros; red; f_equal/=. by etrans; [apply wexpr_proof_irrel|]. Qed.
 
 (* Values *)
-Instance do_wexpr_of_val_nil (H : [] `included` []) v :
-  WExpr H (of_val v) (of_val v) | 0.
+Instance do_wexpr_wexpr X Y Z (H1 : X `included` Y) (H2 : Y `included` Z) e er :
+  WExpr (transitivity H1 H2) e er → WExpr H2 (wexpr H1 e) er | 0.
+Proof. by rewrite /WExpr wexpr_wexpr'. Qed.
+Instance do_wexpr_closed_closed (H : [] `included` []) e : WExpr H e e | 1.
 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.
+Instance do_wexpr_closed_wexpr Y (H : [] `included` Y) e :
+  WExpr H e (wexpr' e) | 2.
 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.
 
 (* Boring connectives *)
 Section do_wexpr.
@@ -129,32 +125,16 @@ Hint Extern 0 (WSubst ?x ?v _ (Rec ?f ?y ?e) _) =>
   end : typeclass_instances.
 
 (* Values *)
-Instance do_wsubst_of_val_nil x es (H : [] `included` [x]) w :
-  WSubst x es H (of_val w) (of_val w) | 0.
+Instance do_wsubst_wexpr X Y Z x es
+    (H1 : X `included` Y) (H2 : Y `included` x :: Z) e er :
+  WSubst x es (transitivity H1 H2) e er → WSubst x es H2 (wexpr H1 e) er | 0.
+Proof. by rewrite /WSubst wsubst_wexpr'. Qed.
+Instance do_wsubst_closed_closed x es (H : [] `included` [x]) e :
+  WSubst x es H e e | 1.
 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.
+Instance do_wsubst_closed_wexpr Y x es (H : [] `included` x :: Y) e :
+  WSubst x es H e (wexpr' e) | 2.
 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.
-
-(* Closed expressions *)
-Instance do_wsubst_expr_nil' {X} x es (H : X `included` [x]) e :
-  WSubst x es H (wexpr' e) e | 0.
-Proof. by rewrite /WSubst /wexpr' wsubst_wexpr' wsubst_closed_nil. Qed.
-Instance do_wsubst_wexpr' X Y x es (H : X `included` x :: Y) e :
-  WSubst x es H (wexpr' e) (wexpr' e) | 1.
-Proof.
-  rewrite /WSubst /wexpr' wsubst_wexpr'.
-  apply wsubst_closed, not_elem_of_nil.
-Qed.
 
 (* Boring connectives *)
 Section wsubst.
@@ -217,4 +197,3 @@ Arguments wexpr : simpl never.
 Arguments subst : simpl never.
 Arguments wsubst : simpl never.
 Arguments of_val : simpl never.
-Arguments of_val' : simpl never.

heap_lang/tactics.v

@@ -25,7 +25,7 @@ Ltac reshape_val e tac :=
   let rec go e :=
   match e with
   | of_val ?v => v
-  | of_val' ?v => v
+  | wexpr' ?e => reshape_val e tac
   | Rec ?f ?x ?e => constr:(RecV f x e)
   | Lit ?l => constr:(LitV l)
   | Pair ?e1 ?e2 =>

heap_lang/wp_tactics.v

@@ -38,7 +38,7 @@ Tactic Notation "wp_rec" :=
     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'; wp_done]; simpl_subst; wp_finish
+    wp_bind K; etrans; [|eapply wp_rec; wp_done]; simpl_subst; wp_finish
 (*      end *) end) || fail "wp_rec: cannot find 'Rec' in" e
   | _ => fail "wp_rec: not a 'wp'"
   end.