Expressions as dependent type.

barrier/barrier.v

-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".

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. *)

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))) →

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' Φ :

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.

heap_lang/substitution.v

 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.

heap_lang/tactics.v

-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];

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.

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.