From f402c1ccfd99bbe82a245aaf2200f6e27146711e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 4 Feb 2016 19:28:08 +0100
Subject: [PATCH] Define some flipped monotonicity Propers for binary uPred
 connectives.

No idea why these aren't resolved automatically, for unary predicates
they do not seem necesarry.
---
 logic/upred.v           | 9 +++++++++
 program_logic/lifting.v | 4 +---
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/logic/upred.v b/logic/upred.v
index 01f467cb0..c8c4c26a6 100644
--- a/logic/upred.v
+++ b/logic/upred.v
@@ -486,8 +486,14 @@ Global Instance const_mono' : Proper (impl ==> (⊑)) (@uPred_const M).
 Proof. intros φ1 φ2; apply const_mono. Qed.
 Global Instance and_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_and M).
 Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
+Global Instance and_flip_mono' :
+  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_and M).
+Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
 Global Instance or_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_or M).
 Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
+Global Instance or_flip_mono' :
+  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_or M).
+Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
 Global Instance impl_mono' :
   Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_impl M).
 Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
@@ -591,6 +597,9 @@ Proof. by intros x [|n] ?; [done|intros (x1&x2&?&?&[a ?]); exists a,x1,x2]. Qed.
 Hint Resolve sep_mono.
 Global Instance sep_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_sep M).
 Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
+Global Instance sep_flip_mono' :
+  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_sep M).
+Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
 Lemma wand_mono P P' Q Q' : Q ⊑ P → P' ⊑ Q' → (P -★ P') ⊑ (Q -★ Q').
 Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
 Global Instance wand_mono' : Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_wand M).
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index c028b22ce..3618be406 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -74,9 +74,7 @@ Proof.
   apply const_elim_l=>-[v2' [Hv ?]] /=.
   rewrite -pvs_intro.
   rewrite (forall_elim v2') (forall_elim σ2') (forall_elim ef) const_equiv //.
-  rewrite left_id wand_elim_r. apply sep_mono; last done.
-  (* FIXME RJ why can't I do this rewrite before doing sep_mono? *)
-  by rewrite -(wp_value' _ _ e2').
+  by rewrite left_id wand_elim_r -(wp_value' _ _ e2').
 Qed.
 
 Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 ef :
-- 
GitLab