Left and right mononicity properties for uPred_sep.

d44228a5 · Robbert Krebbers · 4e8a8de6 · d44228a5
Commit d44228a5 authored Feb 14, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 4 additions and 0 deletions

algebra/upred.v algebra/upred.v +4 -0

No files found.
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -576,6 +576,10 @@ Proof. by intros x n ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.

 (* Derived BI Stuff *)
 Hint Resolve sep_mono.
+Lemma sep_mono_l P P' Q : P ⊑ Q → (P ★ P') ⊑ (Q ★ P').
+Proof. by intros; apply sep_mono. Qed.
+Lemma sep_mono_r P P' Q' : P' ⊑ Q' → (P ★ P') ⊑ (P ★ Q').
+Proof. by apply sep_mono. Qed.
 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' :