From 55294a275cc03823d941c678d236e36e00b785a5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 13 Apr 2017 15:00:28 +0200
Subject: [PATCH] Reverse direction of wp_bind.

---
 theories/program_logic/weakestpre.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 7e7dcaa69..ddb9bee2e 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -189,6 +189,20 @@ Proof.
   by iApply "IH".
 Qed.
 
+Lemma wp_bind_inv K `{!LanguageCtx Λ K} E e Φ :
+  WP K e @ E {{ Φ }} ⊢ WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }}.
+Proof.
+  iIntros "H". iLöb as "IH" forall (E e Φ). rewrite !wp_unfold /wp_pre.
+  destruct (to_val e) as [v|] eqn:He.
+  { apply of_to_val in He as <-. by rewrite !wp_unfold /wp_pre. }
+  rewrite fill_not_val //.
+  iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
+  { eauto using reducible_fill. }
+  iNext; iIntros (e2 σ2 efs Hstep).
+  iMod ("H" $! (K e2) σ2 efs with "[]") as "($ & H & $)"; eauto using fill_step.
+  by iApply "IH".
+Qed.
+
 (** * Derived rules *)
 Lemma wp_mono E e Φ Ψ : (∀ v, Φ v ⊢ Ψ v) → WP e @ E {{ Φ }} ⊢ WP e @ E {{ Ψ }}.
 Proof.
-- 
GitLab