Document gsubst function and move to separate file.

_CoqProject

@@ -72,3 +72,4 @@ heap_lang/lifting.v
 heap_lang/derived.v
 heap_lang/notation.v
 heap_lang/tests.v
+heap_lang/substitution.v

heap_lang/derived.v

@@ -16,20 +16,17 @@ Implicit Types Q : val → iProp heap_lang Σ.
 
 (** Proof rules for the sugar *)
 Lemma wp_lam E x ef e v Q :
-  to_val e = Some v → ▷ wp E (gsubst ef x e) Q ⊑ wp E (App (Lam x ef) e) Q.
-Proof.
-  intros <-%of_to_val; rewrite -wp_rec ?to_of_val //.
-  by rewrite (gsubst_correct _ _ (RecV _ _ _)) subst_empty.
-Qed.
+  to_val e = Some v → ▷ wp E (subst ef x v) Q ⊑ wp E (App (Lam x ef) e) Q.
+Proof. intros. by rewrite -wp_rec ?subst_empty. Qed.
 
 Lemma wp_let E x e1 e2 v Q :
-  to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Q ⊑ wp E (Let x e1 e2) Q.
+  to_val e1 = Some v → ▷ wp E (subst e2 x v) Q ⊑ wp E (Let x e1 e2) Q.
 Proof. apply wp_lam. Qed.
 
 Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
 Proof.
   rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.
-  by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val.
+  by rewrite -wp_let //= ?to_of_val ?subst_empty.
 Qed.
 
 Lemma wp_le E (n1 n2 : Z) P Q :
@@ -58,5 +55,4 @@ Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
 Qed.
-
 End derived.

heap_lang/lifting.v

-Require Import prelude.gmap program_logic.lifting program_logic.ownership.
-Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
+Require Export program_logic.weakestpre heap_lang.heap_lang.
+Require Import program_logic.lifting.
+Require Import program_logic.ownership. (* for ownP *)
+Require Import heap_lang.heap_lang_tactics.
 Export heap_lang. (* Prefer heap_lang names over language names. *)
 Import uPred.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
 
-(** The substitution operation [gsubst e x ev] behaves just as [subst] but
-in case [e] does not contain the free variable [x] it will return [e] in a
-way that is syntactically equal (i.e. without any Coq-level delta reduction
-performed) *)
-Arguments of_val : simpl never.
-Definition gsubst_lift {A B C} (f : A → B → C)
-    (x : A) (y : B) (mx : option A) (my : option B) : option C :=
-  match mx, my with
-  | Some x, Some y => Some (f x y)
-  | Some x, None => Some (f x y)
-  | None, Some y => Some (f x y)
-  | None, None => None
-  end.
-Fixpoint gsubst_go (e : expr) (x : string) (ev : expr) : option expr :=
-  match e with
-  | Var y => if decide (x = y ∧ x ≠ "") then Some ev else None
-  | Rec f y e =>
-     if decide (x ≠ f ∧ x ≠ y) then Rec f y <$> gsubst_go e x ev else None
-  | App e1 e2 => gsubst_lift App e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
-  | Lit l => None
-  | UnOp op e => UnOp op <$> gsubst_go e x ev
-  | BinOp op e1 e2 =>
-     gsubst_lift (BinOp op) e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
-  | If e0 e1 e2 =>
-     gsubst_lift id (If e0 e1) e2
-       (gsubst_lift If e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev))
-       (gsubst_go e2 x ev)
-  | Pair e1 e2 => gsubst_lift Pair e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
-  | Fst e => Fst <$> gsubst_go e x ev
-  | Snd e => Snd <$> gsubst_go e x ev
-  | InjL e => InjL <$> gsubst_go e x ev
-  | InjR e => InjR <$> gsubst_go e x ev
-  | Case e0 x1 e1 x2 e2 =>
-     gsubst_lift id (Case e0 x1 e1 x2) e2
-       (gsubst_lift (λ e0' e1', Case e0' x1 e1' x2) e0 e1
-         (gsubst_go e0 x ev)
-         (if decide (x ≠ x1) then gsubst_go e1 x ev else None))
-       (if decide (x ≠ x2) then gsubst_go e2 x ev else None)
-  | Fork e => Fork <$> gsubst_go e x ev
-  | Loc l => None
-  | Alloc e => Alloc <$> gsubst_go e x ev
-  | Load e => Load <$> gsubst_go e x ev
-  | Store e1 e2 => gsubst_lift Store e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
-  | Cas e0 e1 e2 =>
-     gsubst_lift id (Cas e0 e1) e2
-       (gsubst_lift Cas e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev))
-       (gsubst_go e2 x ev)
-  end.
-Definition gsubst (e : expr) (x : string) (ev : expr) : expr :=
-  from_option e (gsubst_go e x ev).
-Arguments gsubst !_ _ _/.
-
 Section lifting.
 Context {Σ : iFunctor}.
 Implicit Types P : iProp heap_lang Σ.
@@ -63,20 +13,6 @@ Implicit Types Q : val → iProp heap_lang Σ.
 Implicit Types K : ectx.
 Implicit Types ef : option expr.
 
-Lemma gsubst_None e x v : gsubst_go e x (of_val v) = None → e = subst e x v.
-Proof.
-  induction e; simpl; unfold gsubst_lift; intros;
-    repeat (simplify_option_equality || case_match); f_equal; auto.
-Qed.
-Lemma gsubst_correct e x v : gsubst e x (of_val v) = subst e x v.
-Proof.
-  unfold gsubst; destruct (gsubst_go e x (of_val v)) as [e'|] eqn:He; simpl;
-    last by apply gsubst_None.
-  revert e' He; induction e; simpl; unfold gsubst_lift; intros;
-    repeat (simplify_option_equality || case_match);
-    f_equal; auto using gsubst_None.
-Qed.
-
 (** Bind. *)
 Lemma wp_bind {E e} K Q :
   wp E e (λ v, wp E (fill K (of_val v)) Q) ⊑ wp E (fill K e) Q.
@@ -150,18 +86,12 @@ Qed.
 
 Lemma wp_rec E f x e1 e2 v Q :
   to_val e2 = Some v →
-  ▷ wp E (gsubst (gsubst e1 f (Rec f x e1)) x e2) Q ⊑ wp E (App (Rec f x e1) e2) Q.
+  ▷ wp E (subst (subst e1 f (RecV f x e1)) x v) Q ⊑ wp E (App (Rec f x e1) e2) Q.
 Proof.
-  intros <-%of_to_val; rewrite gsubst_correct (gsubst_correct _ _ (RecV _ _ _)).
-  rewrite -(wp_lift_pure_det_step (App _ _)
+  intros. rewrite -(wp_lift_pure_det_step (App _ _)
     (subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
     intros; inv_step; eauto.
 Qed.
-Lemma wp_rec' E e1 f x erec e2 v Q :
-  e1 = Rec f x erec →
-  to_val e2 = Some v →
-  ▷ wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q.
-Proof. intros ->; apply wp_rec. Qed.
 
 Lemma wp_un_op E op l l' Q :
   un_op_eval op l = Some l' →
@@ -209,20 +139,18 @@ Qed.
 
 Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
   to_val e0 = Some v0 →
-  ▷ wp E (gsubst e1 x1 e0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
+  ▷ wp E (subst e1 x1 v0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
 Proof.
-  intros <-%of_to_val; rewrite gsubst_correct.
-  rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e1 x1 v0) None)
-    ?right_id //; intros; inv_step; eauto.
+  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
+    (subst e1 x1 v0) None) ?right_id //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
   to_val e0 = Some v0 →
-  ▷ wp E (gsubst e2 x2 e0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
+  ▷ wp E (subst e2 x2 v0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
 Proof.
-  intros <-%of_to_val; rewrite gsubst_correct.
-  rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e2 x2 v0) None)
-    ?right_id //; intros; inv_step; eauto.
+  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _)
+    (subst e2 x2 v0) None) ?right_id //; intros; inv_step; eauto.
 Qed.
 
 End lifting.

heap_lang/substitution.v

+Require Export heap_lang.derived.
+
+(** We define an alternative notion of substitution [gsubst e x ev] that
+preserves the expression [e] syntactically in case the variable [x] does not
+occur freely in [e]. By syntactically, we mean that [e] is preserved without
+unfolding any Coq definitions. For example:
+
+<<
+  Definition id : val := λ: "x", "x".
+  Eval simpl in subst (id "y") "y" '10.   (* (Lam "x" "x") '10 *)
+  Eval simpl in gsubst (id "y") "y" '10.  (* id '10 *)
+>>
+
+For [gsubst e x ev] to work, [e] should not contain any opaque parts.
+
+The function [gsubst e x ev] differs in yet another way from [subst e x v].
+The function [gsubst] substitutes an expression [ev] whereas [subst]
+substitutes a value [v]. This way we avoid unnecessary conversion back and
+forth between values and expressions, which could also cause Coq definitions
+to be unfolded. For example, consider the rule [wp_rec'] from below:
+
+<<
+  Definition foo : val := rec: "f" "x" := ... .
+
+  Lemma wp_rec' E e1 f x erec e2 v Q :
+    e1 = Rec f x erec →
+    to_val e2 = Some v →
+    ▷ wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q.
+>>
+
+We ensure that [e1] is substituted instead of [RecV f x erec]. So, for example
+when taking [e1 := foo] we ensure that [foo] is substituted without being
+unfolded. *)
+
+(** * Implementation *)
+(** The core of [gsubst e x ev] is the partial function [gsubst_go e x ev] that
+returns [None] in case [x] does not occur freely in [e] and [Some e'] in case
+[x] occurs in [e]. The function [gsubst e x ev] is then simply defined as
+[from_option e (gsubst_go e x ev)]. *)
+Definition gsubst_lift {A B C} (f : A → B → C)
+    (x : A) (y : B) (mx : option A) (my : option B) : option C :=
+  match mx, my with
+  | Some x, Some y => Some (f x y)
+  | Some x, None => Some (f x y)
+  | None, Some y => Some (f x y)
+  | None, None => None
+  end.
+Fixpoint gsubst_go (e : expr) (x : string) (ev : expr) : option expr :=
+  match e with
+  | Var y => if decide (x = y ∧ x ≠ "") then Some ev else None
+  | Rec f y e =>
+     if decide (x ≠ f ∧ x ≠ y) then Rec f y <$> gsubst_go e x ev else None
+  | App e1 e2 => gsubst_lift App e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
+  | Lit l => None
+  | UnOp op e => UnOp op <$> gsubst_go e x ev
+  | BinOp op e1 e2 =>
+     gsubst_lift (BinOp op) e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
+  | If e0 e1 e2 =>
+     gsubst_lift id (If e0 e1) e2
+       (gsubst_lift If e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev))
+       (gsubst_go e2 x ev)
+  | Pair e1 e2 => gsubst_lift Pair e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
+  | Fst e => Fst <$> gsubst_go e x ev
+  | Snd e => Snd <$> gsubst_go e x ev
+  | InjL e => InjL <$> gsubst_go e x ev
+  | InjR e => InjR <$> gsubst_go e x ev
+  | Case e0 x1 e1 x2 e2 =>
+     gsubst_lift id (Case e0 x1 e1 x2) e2
+       (gsubst_lift (λ e0' e1', Case e0' x1 e1' x2) e0 e1
+         (gsubst_go e0 x ev)
+         (if decide (x ≠ x1) then gsubst_go e1 x ev else None))
+       (if decide (x ≠ x2) then gsubst_go e2 x ev else None)
+  | Fork e => Fork <$> gsubst_go e x ev
+  | Loc l => None
+  | Alloc e => Alloc <$> gsubst_go e x ev
+  | Load e => Load <$> gsubst_go e x ev
+  | Store e1 e2 => gsubst_lift Store e1 e2 (gsubst_go e1 x ev) (gsubst_go e2 x ev)
+  | Cas e0 e1 e2 =>
+     gsubst_lift id (Cas e0 e1) e2
+       (gsubst_lift Cas e0 e1 (gsubst_go e0 x ev) (gsubst_go e1 x ev))
+       (gsubst_go e2 x ev)
+  end.
+Definition gsubst (e : expr) (x : string) (ev : expr) : expr :=
+  from_option e (gsubst_go e x ev).
+
+(** * Simpl  *)
+(** Ensure that [simpl] unfolds [gsubst e x ev] when applied to a concrete term
+[e] and use [simpl nomatch] to ensure that it does not reduce in case [e]
+contains any opaque parts that block reduction. *)
+Arguments gsubst !_ _ _/ : simpl nomatch.
+
+(** We define heap_lang functions as values (see [id] above). In order to
+ensure too eager conversion to expressions, we block [simpl]. *)
+Arguments of_val : simpl never.
+
+(** * Correctness *)
+(** We prove that [gsubst] behaves like [subst] when substituting values. *)
+Lemma gsubst_None e x v : gsubst_go e x (of_val v) = None → e = subst e x v.
+Proof.
+  induction e; simpl; unfold gsubst_lift; intros;
+    repeat (simplify_option_equality || case_match); f_equal; auto.
+Qed.
+Lemma gsubst_correct e x v : gsubst e x (of_val v) = subst e x v.
+Proof.
+  unfold gsubst; destruct (gsubst_go e x (of_val v)) as [e'|] eqn:He; simpl;
+    last by apply gsubst_None.
+  revert e' He; induction e; simpl; unfold gsubst_lift; intros;
+    repeat (simplify_option_equality || case_match);
+    f_equal; auto using gsubst_None.
+Qed.
+
+(** * Weakest precondition rules *)
+Section wp.
+Context {Σ : iFunctor}.
+Implicit Types P : iProp heap_lang Σ.
+Implicit Types Q : val → iProp heap_lang Σ.
+Hint Resolve to_of_val.
+
+Lemma wp_rec' E e1 f x erec e2 v Q :
+  e1 = Rec f x erec →
+  to_val e2 = Some v →
+  ▷ wp E (gsubst (gsubst erec f e1) x e2) Q ⊑ wp E (App e1 e2) Q.
+Proof.
+  intros -> <-%of_to_val.
+  rewrite (gsubst_correct _ _ (RecV _ _ _)) gsubst_correct.
+  by apply wp_rec.
+Qed.
+
+Lemma wp_lam' E x ef e v Q :
+  to_val e = Some v → ▷ wp E (gsubst ef x e) Q ⊑ wp E (App (Lam x ef) e) Q.
+Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_lam. Qed.
+
+Lemma wp_let' E x e1 e2 v Q :
+  to_val e1 = Some v → ▷ wp E (gsubst e2 x e1) Q ⊑ wp E (Let x e1 e2) Q.
+Proof. apply wp_lam'. Qed.
+
+Lemma wp_case_inl' E e0 v0 x1 e1 x2 e2 Q :
+  to_val e0 = Some v0 →
+  ▷ wp E (gsubst e1 x1 e0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
+Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inl. Qed.
+
+Lemma wp_case_inr' E e0 v0 x1 e1 x2 e2 Q :
+  to_val e0 = Some v0 →
+  ▷ wp E (gsubst e2 x2 e0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
+Proof. intros <-%of_to_val; rewrite gsubst_correct. by apply wp_case_inr. Qed.
+End wp.
+

heap_lang/tests.v

 (** This file is essentially a bunch of testcases. *)
 Require Import program_logic.ownership.
-Require Import heap_lang.notation.
+Require Import heap_lang.notation heap_lang.substitution heap_lang.heap_lang_tactics.
 Import uPred.
 
 Module LangTests.
@@ -59,7 +59,8 @@ Module LiftingTests.
       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.
+    λ: "x",
+      if "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
 
   Lemma FindPred_spec n1 n2 E Q :
     (■ (n1 < n2) ∧ Q '(n2 - 1)) ⊑ wp E (FindPred 'n2 'n1)%L Q.
@@ -73,21 +74,21 @@ Module LiftingTests.
     rewrite ->(later_intro (Q _)).
     rewrite -!later_and; apply later_mono.
     (* Go on *)
-    rewrite -wp_let //= -later_intro.
-    rewrite -(wp_bindi (LetCtx _ _)) -wp_bin_op //= -wp_let //=.
-    rewrite -(wp_bindi (IfCtx _ _)) /= -!later_intro.
+    rewrite -wp_let' //= -later_intro.
+    rewrite -(wp_bindi (LetCtx _ _)) -wp_bin_op //= -wp_let' //= -!later_intro.
+    rewrite -(wp_bindi (IfCtx _ _)) /=.
     apply wp_lt=> ?.
-    - rewrite -wp_if_true.
-      rewrite -!later_intro (forall_elim (n1 + 1)) const_equiv; last omega.
+    - rewrite -wp_if_true -!later_intro.
+      rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
       by rewrite left_id impl_elim_l.
     - assert (n1 = n2 - 1) as -> by omega.
-      rewrite -wp_if_false.
-      by rewrite -!later_intro -wp_value' // and_elim_r.
+      rewrite -wp_if_false -!later_intro.
+      by rewrite -wp_value' // and_elim_r.
   Qed.
 
   Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
   Proof.
-    rewrite -wp_lam //=.
+    rewrite -wp_lam' //=.
     rewrite -(wp_bindi (IfCtx _ _)) /=.
     apply later_mono, wp_le=> Hn.
     - rewrite -wp_if_true.
@@ -99,8 +100,8 @@ Module LiftingTests.
       rewrite -FindPred_spec. apply and_intro; first by (apply const_intro; omega).
       rewrite -wp_un_op //= -later_intro.
       by assert (n - 1 = - (- n + 2 - 1)) as -> by omega.
-    - rewrite -wp_if_false.
-      rewrite -!later_intro -FindPred_spec.
+    - rewrite -wp_if_false -!later_intro.
+      rewrite -FindPred_spec.
       auto using and_intro, const_intro with omega.
   Qed.
 
@@ -108,7 +109,7 @@ Module LiftingTests.
     True ⊑ wp (Σ:=Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
   Proof.
     intros E.
-    rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let //=.
+    rewrite -(wp_bindi (LetCtx _ _)) -Pred_spec //= -wp_let' //=.
     by rewrite -Pred_spec -!later_intro /=.
   Qed.
 End LiftingTests.