From 066354af6345fba425c69b1708620ea8df9d4ab0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 6 Sep 2019 14:02:39 +0200
Subject: [PATCH] Add `flip` version of `Proper` for entailment of `wp`.

We have these instances for all other logical operations too to support
setoid rewriting in both directions.
---
 theories/program_logic/weakestpre.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 134ce595b..f7554040d 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -192,6 +192,9 @@ Proof. iIntros (?) "H"; iApply (wp_strong_mono with "H"); auto. Qed.
 Global Instance wp_mono' s E e :
   Proper (pointwise_relation _ (⊢) ==> (⊢)) (wp (PROP:=iProp Σ) s E e).
 Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
+Global Instance wp_flip_mono' s E e :
+  Proper (pointwise_relation _ (flip (⊢)) ==> (flip (⊢))) (wp (PROP:=iProp Σ) s E e).
+Proof. by intros Φ Φ' ?; apply wp_mono. Qed.
 
 Lemma wp_value s E Φ e v : IntoVal e v → Φ v ⊢ WP e @ s; E {{ Φ }}.
 Proof. intros <-. by apply wp_value'. Qed.
-- 
GitLab