Implement substitution by reification.

We reify to a representation of expressions that includes an explicit
constructor for closed terms. Substitution can then be implemented as
the identify, which enables us to perform it using computation.

heap_lang/lang.v

@@ -369,12 +369,6 @@ Proof. by rewrite /IntoValue /= => ->. Qed.
 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.
 
-Instance of_val_closed X v : Closed X (of_val v).
-Proof.
-  apply is_closed_weaken with []; last set_solver.
-  induction v; simpl; auto.
-Qed.
-
 Lemma closed_subst X e x es : Closed X e → x ∉ X → subst x es e = e.
 Proof.
   rewrite /Closed. revert X.
@@ -390,7 +384,10 @@ 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 of_val_closed. Qed.
+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).

heap_lang/lib/assert.v

-From iris.heap_lang Require Export derived.
-From iris.heap_lang Require Import wp_tactics substitution notation.
+From iris.proofmode Require Import tactics.
+From iris.heap_lang Require Import proofmode notation.
 
-Definition Assert (e : expr) : expr :=
-  if: e then #() else #0 #0. (* #0 #0 is unsafe *)
+Definition assert : val :=
+  λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
+(* just below ;; *)
+Notation "'assert:' e" := (assert (λ: <>, e))%E (at level 99) : expr_scope.
+Global Opaque assert.
 
-Instance closed_assert X e : Closed X e → Closed X (Assert e) := _.
-Instance do_subst_assert x es e er :
-  Subst x es e er → Subst x es (Assert e) (Assert er).
-Proof. intros; red. by rewrite /Assert /subst -/subst; f_equal/=. Qed.
-Typeclasses Opaque Assert.
-
-Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) :
-  ▷ Φ #() ⊢ WP Assert #true {{ Φ }}.
-Proof. by rewrite -wp_if_true -wp_value. Qed.
-
-Lemma wp_assert' {Σ} (Φ : val → iProp heap_lang Σ) e :
-  WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP Assert e {{ Φ }}.
+Lemma wp_assert {Σ} (Φ : val → iProp heap_lang Σ) e `{!Closed [] e} :
+  WP e {{ v, v = #true ∧ ▷ Φ #() }} ⊢ WP assert: e {{ Φ }}.
 Proof.
-  rewrite /Assert. wp_focus e; apply wp_mono=>v.
-  apply uPred.pure_elim_l=>->. apply wp_assert.
+  iIntros "HΦ". rewrite /assert. wp_let. wp_seq.
+  iApply wp_wand_r; iFrame "HΦ"; iIntros (v) "[% ?]"; subst.
+  wp_if. done.
 Qed.

heap_lang/substitution.v

 From iris.heap_lang Require Export lang.
 Import heap_lang.
 
-(** The tactic [simpl_subst] performs substitutions in the goal. Its behavior
-can be tuned by declaring [Subst] instances. *)
-(** * Substitution *)
-Class Subst (x : string) (es : expr) (e : expr) (er : expr) :=
-  do_subst : subst x es e = er.
-Hint Mode Subst + + + - : typeclass_instances.
+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).
 
-(* Variables *)
-Lemma do_subst_var_eq x er : Subst x er (Var x) er.
-Proof. intros; red; simpl. by case_decide. Qed.
-Lemma do_subst_var_neq x y er : bool_decide (x ≠ y) → Subst x er (Var y) (Var y).
-Proof. rewrite bool_decide_spec. intros; red; simpl. by case_decide. Qed.
-
-Hint Extern 0 (Subst ?x ?v (Var ?y) _) =>
-  first [apply do_subst_var_eq
-        |apply do_subst_var_neq, I] : typeclass_instances.
-
-(** Rec *)
-Lemma do_subst_rec_true {x es f y e er} :
-  bool_decide (BNamed x ≠ f ∧ BNamed x ≠ y) →
-  Subst x es e er → Subst x es (Rec f y e) (Rec f y er).
-Proof. rewrite bool_decide_spec. intros; red; f_equal/=; by case_decide. Qed.
-Lemma do_subst_rec_false {x es f y e} :
-  bool_decide (¬(BNamed x ≠ f ∧ BNamed x ≠ y)) →
-  Subst x es (Rec f y e) (Rec f y e).
-Proof. rewrite bool_decide_spec. intros; red; f_equal/=; by case_decide. Qed.
-
-Local Ltac bool_decide_no_check := vm_cast_no_check I.
-Hint Extern 0 (Subst ?x ?v (Rec ?f ?y ?e) _) =>
-  match eval vm_compute in (bool_decide (BNamed x ≠ f ∧ BNamed x ≠ y)) with
-  | true => eapply (do_subst_rec_true ltac:(bool_decide_no_check))
-  | false => eapply (do_subst_rec_false ltac:(bool_decide_no_check))
-  end : typeclass_instances.
-
-Lemma do_subst_closed x es e : Closed [] e → Subst x es e e.
-Proof. apply closed_nil_subst. Qed.
-Hint Extern 10 (Subst ?x ?v ?e _) =>
-  is_var e; class_apply do_subst_closed : typeclass_instances.
+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.
 
-(* Values *)
-Instance do_subst_of_val x es v : Subst x es (of_val v) (of_val v) | 0.
-Proof. eapply closed_nil_subst, of_val_closed. Qed.
+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.
 
-(* Boring connectives *)
-Section subst.
-Context (x : string) (es : expr).
-Notation Sub := (Subst x es).
+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.
 
-(* Ground terms *)
-Global Instance do_subst_lit l : Sub (Lit l) (Lit l).
-Proof. done. Qed.
-Global Instance do_subst_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_subst. Qed.
-Global Instance do_subst_unop op e er : Sub e er → Sub (UnOp op e) (UnOp op er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_subst_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.
-Global Instance do_subst_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.
-Global Instance do_subst_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.
-Global Instance do_subst_fst e er : Sub e er → Sub (Fst e) (Fst er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_subst_snd e er : Sub e er → Sub (Snd e) (Snd er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_subst_injL e er : Sub e er → Sub (InjL e) (InjL er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_subst_injR e er : Sub e er → Sub (InjR e) (InjR er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_subst_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.
-Global Instance do_subst_fork e er : Sub e er → Sub (Fork e) (Fork er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_subst_alloc e er : Sub e er → Sub (Alloc e) (Alloc er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_subst_load e er : Sub e er → Sub (Load e) (Load er).
-Proof. by intros; red; f_equal/=. Qed.
-Global Instance do_subst_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.
-Global Instance do_subst_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 subst.
+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 ?es ?e] => progress rewrite (@do_subst x es e)
-  | |- _ => progress csimpl
-  end.
+  | |- 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.

tests/one_shot.v

@@ -14,8 +14,8 @@ Definition one_shot_example : val := λ: <>,
       InjL <> => #()
     | InjR "n" =>
        match: !"x" with
-         InjL <> => Assert #false
-       | InjR "m" => Assert ("n" = "m")
+         InjL <> => assert: #false
+       | InjR "m" => assert: "n" = "m"
        end
     end)).
 Global Opaque one_shot_example.
@@ -79,7 +79,7 @@ Proof.
     iCombine "Hγ" "Hγ'" as "Hγ".
     iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; by eauto|].
-    wp_match. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
+    wp_match. iApply wp_assert. wp_op=>?; simplify_eq/=; eauto.
 Qed.
 
 Lemma hoare_one_shot (Φ : val → iProp) :