Add flipped mono instances for wand, impl, forall, exist.

This commit fixes #41.

Add flipped mono instances for wand, impl, forall, exist.
This commit fixes #41.
8c2608ed · Robbert Krebbers · f3222ba2 · 8c2608ed
Commit 8c2608ed authored Oct 28, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 13 additions and 1 deletion

base_logic/derived.v base_logic/derived.v +13 -1

No files found.
--- a/base_logic/derived.v
+++ b/base_logic/derived.v
@@ -113,11 +113,20 @@ 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.
+Global Instance impl_flip_mono' :
+  Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_impl M).
+Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
 Global Instance forall_mono' A :
  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_forall M A).
 Proof. intros P1 P2; apply forall_mono. Qed.
+Global Instance forall_flip_mono' A :
+  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_forall M A).
+Proof. intros P1 P2; apply forall_mono. Qed.
 Global Instance exist_mono' A :
-  Proper (pointwise_relation _ (⊢) ==> (⊢)) (@uPred_exist M A).
+  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_exist M A).
+Proof. intros P1 P2; apply exist_mono. Qed.
+Global Instance exist_flip_mono' A :
+  Proper (pointwise_relation _ (flip (⊢)) ==> flip (⊢)) (@uPred_exist M A).
 Proof. intros P1 P2; apply exist_mono. Qed.

 Global Instance and_idem : IdemP (⊣⊢) (@uPred_and M).
@@ -303,6 +312,9 @@ Proof.
 Qed.
 Global Instance wand_mono' : Proper (flip (⊢) ==> (⊢) ==> (⊢)) (@uPred_wand M).
 Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
+Global Instance wand_flip_mono' :
+  Proper ((⊢) ==> flip (⊢) ==> flip (⊢)) (@uPred_wand M).
+Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.

 Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M).
 Proof. intros P Q; apply (anti_symm _); auto using sep_comm'. Qed.