From 8c2608ed4152bee3ed36715afa1f007e76e94bb8 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Fri, 28 Oct 2016 10:27:49 +0200 Subject: [PATCH] Add flipped mono instances for wand, impl, forall, exist. This commit fixes #41. --- base_logic/derived.v | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/base_logic/derived.v b/base_logic/derived.v index a485b335a..d3debb15f 100644 --- 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. -- GitLab