From 39f190a7c4110dfeb92d0e11036452070db37790 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Wed, 7 Feb 2018 10:59:40 +0100 Subject: [PATCH] More consistent names for `mono` lemmas for `absolutely`/`relatively`. In the same style as most of the BI lemmas, e.g. `or_mono`, `and_mono`, ... --- theories/bi/monpred.v | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v index 1acfd53c6..4305ae2c2 100644 --- a/theories/bi/monpred.v +++ b/theories/bi/monpred.v @@ -488,9 +488,11 @@ Global Instance monPred_absolutely_ne : NonExpansive (@monPred_absolutely I PROP Proof. rewrite /monPred_absolutely /=. solve_proper. Qed. Global Instance monPred_absolutely_proper : Proper ((≡) ==> (≡)) (@monPred_absolutely I PROP). Proof. apply (ne_proper _). Qed. -Global Instance monPred_absolutely_mono : Proper ((⊢) ==> (⊢)) (@monPred_absolutely I PROP). +Lemma monPred_absolutely_mono P Q : (P ⊢ Q) → (∀ᵢ P ⊢ ∀ᵢ Q). Proof. rewrite /monPred_absolutely /=. solve_proper. Qed. -Global Instance monPred_absolutely_mono_flip : +Global Instance monPred_absolutely_mono' : Proper ((⊢) ==> (⊢)) (@monPred_absolutely I PROP). +Proof. rewrite /monPred_absolutely /=. solve_proper. Qed. +Global Instance monPred_absolutely_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@monPred_absolutely I PROP). Proof. solve_proper. Qed. @@ -510,9 +512,11 @@ Global Instance monPred_relatively_ne : NonExpansive (@monPred_relatively I PROP Proof. rewrite /monPred_relatively /=. solve_proper. Qed. Global Instance monPred_relatively_proper : Proper ((≡) ==> (≡)) (@monPred_relatively I PROP). Proof. apply (ne_proper _). Qed. -Global Instance monPred_relatively_mono : Proper ((⊢) ==> (⊢)) (@monPred_relatively I PROP). +Lemma monPred_relatively_mono P Q : (P ⊢ Q) → (∃ᵢ P ⊢ ∃ᵢ Q). +Proof. rewrite /monPred_relatively /=. solve_proper. Qed. +Global Instance monPred_relatively_mono' : Proper ((⊢) ==> (⊢)) (@monPred_relatively I PROP). Proof. rewrite /monPred_relatively /=. solve_proper. Qed. -Global Instance monPred_relatively_mono_flip : +Global Instance monPred_relatively_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@monPred_relatively I PROP). Proof. solve_proper. Qed. -- GitLab