Hack to avoid substitution perform Coq-level delta reduction.

heap_lang/lifting.v

@@ -3,6 +3,57 @@ Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
 Import uPred heap_lang.
 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) *)
+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 Σ.
@@ -10,6 +61,20 @@ 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.
@@ -83,20 +148,25 @@ Qed.
 
 Lemma wp_rec E f x e1 e2 v Q :
   to_val e2 = Some v →
-  ▷ wp E (subst (subst e1 f (RecV f x e1)) x v) Q ⊑ wp E (App (Rec f x e1) e2) Q.
+  ▷ wp E (gsubst (gsubst e1 f (Rec f x e1)) x e2) Q ⊑ wp E (App (Rec f x e1) e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (App _ _)
+  intros <-%of_to_val; rewrite gsubst_correct (gsubst_correct _ _ (RecV _ _ _)).
+  rewrite -(wp_lift_pure_det_step (App _ _)
     (subst (subst e1 f (RecV f x e1)) x v) None) ?right_id //=;
-    last by intros; inv_step; eauto.
+    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' →
   ▷ Q (LitV l') ⊑ wp E (UnOp op (Lit l)) Q.
 Proof.
   intros. rewrite -(wp_lift_pure_det_step (UnOp op _) (Lit l') None)
-    ?right_id //; last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
+    ?right_id -?wp_value' //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_bin_op E op l1 l2 l' Q :
@@ -104,54 +174,53 @@ Lemma wp_bin_op E op l1 l2 l' Q :
   ▷ Q (LitV l') ⊑ wp E (BinOp op (Lit l1) (Lit l2)) Q.
 Proof.
   intros Heval. rewrite -(wp_lift_pure_det_step (BinOp op _ _) (Lit l') None)
-    ?right_id //; last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
+    ?right_id -?wp_value' //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_true E e1 e2 Q : ▷ wp E e1 Q ⊑ wp E (If (Lit LitTrue) e1 e2) Q.
 Proof.
   rewrite -(wp_lift_pure_det_step (If _ _ _) e1 None)
-    ?right_id //; last by intros; inv_step; eauto.
+    ?right_id //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_if_false E e1 e2 Q : ▷ wp E e2 Q ⊑ wp E (If (Lit LitFalse) e1 e2) Q.
 Proof.
   rewrite -(wp_lift_pure_det_step (If _ _ _) e2 None)
-    ?right_id //; last by intros; inv_step; eauto.
+    ?right_id //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_fst E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Q v1 ⊑ wp E (Fst $ Pair e1 e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None) ?right_id //;
-    last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
+  intros. rewrite -(wp_lift_pure_det_step (Fst _) e1 None)
+    ?right_id -?wp_value' //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_snd E e1 v1 e2 v2 Q :
   to_val e1 = Some v1 → to_val e2 = Some v2 →
   ▷ Q v2 ⊑ wp E (Snd $ Pair e1 e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None) ?right_id //;
-    last by intros; inv_step; eauto.
-  by rewrite -wp_value'.
+  intros. rewrite -(wp_lift_pure_det_step (Snd _) e2 None)
+    ?right_id -?wp_value' //; intros; inv_step; eauto.
 Qed.
 
 Lemma wp_case_inl E e0 v0 x1 e1 x2 e2 Q :
   to_val e0 = Some v0 →
-  ▷ wp E (subst e1 x1 v0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
+  ▷ wp E (gsubst e1 x1 e0) Q ⊑ wp E (Case (InjL e0) x1 e1 x2 e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e1 x1 v0) None)
-    ?right_id //; last by intros; inv_step; eauto.
+  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.
 Qed.
 
 Lemma wp_case_inr E e0 v0 x1 e1 x2 e2 Q :
   to_val e0 = Some v0 →
-  ▷ wp E (subst e2 x2 v0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
+  ▷ wp E (gsubst e2 x2 e0) Q ⊑ wp E (Case (InjR e0) x1 e1 x2 e2) Q.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Case _ _ _ _ _) (subst e2 x2 v0) None)
-    ?right_id //; last by intros; inv_step; eauto.
+  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.
 Qed.
 
 End lifting.

heap_lang/sugar.v

@@ -60,17 +60,20 @@ 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 (subst ef x v) Q ⊑ wp E (App (Lam x ef) e) Q.
-Proof. intros. by rewrite -wp_rec ?subst_empty; eauto. Qed.
+  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.
 
 Lemma wp_let E x e1 e2 v Q :
-  to_val e1 = Some v → ▷ wp E (subst e2 x v) Q ⊑ wp E (Let x e1 e2) 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_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 //= ?subst_empty ?to_of_val.
+  by rewrite -wp_let //= ?gsubst_correct ?subst_empty ?to_of_val.
 Qed.
 
 Lemma wp_le E (n1 n2 : nat) P Q :

heap_lang/tests.v

@@ -62,11 +62,11 @@ Module LiftingTests.
     λ: "x", if "x" ≤ '0 then '0 else FindPred "x" '0.
 
   Lemma FindPred_spec n1 n2 E Q :
-    (■ (n1 < n2) ∧ Q (LitV (pred n2))) ⊑ wp E (FindPred 'n2 'n1)%L Q.
+    (■ (n1 < n2) ∧ Q (LitV (n2 - 1))) ⊑ wp E (FindPred 'n2 'n1)%L Q.
   Proof.
     revert n1. apply löb_all_1=>n1.
     rewrite (commutative uPred_and (■ _)%I) associative; apply const_elim_r=>?.
-    rewrite -wp_rec //=.
+    rewrite -wp_rec' // =>-/=.
     (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
     rewrite ->(later_intro (Q _)).
     rewrite -!later_and; apply later_mono.
@@ -77,15 +77,15 @@ Module LiftingTests.
     - rewrite -wp_if_true.
       rewrite -!later_intro (forall_elim (n1 + 1)) const_equiv; last omega.
       by rewrite left_id impl_elim_l.
-    - assert (n1 = pred n2) as -> by omega.
+    - assert (n1 = n2 - 1) as -> by omega.
       rewrite -wp_if_false.
       by rewrite -!later_intro -wp_value' // and_elim_r.
   Qed.
 
-  Lemma Pred_spec n E Q : ▷ Q (LitV (pred n)) ⊑ wp E (Pred 'n)%L Q.
+  Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
   Proof.
     rewrite -wp_lam //=.
-    rewrite -(wp_bindi (IfCtx _ _)).
+    rewrite -(wp_bindi (IfCtx _ _)) /=.
     apply later_mono, wp_le=> Hn.
     - rewrite -wp_if_true.
       rewrite -!later_intro -wp_value' //=.