diff --git a/base_logic/derived.v b/base_logic/derived.v index a485b335a8fc86af8a242fa4238b04b549e0be62..d3debb15f99b56d654520ada30b32adf88fc1df7 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.