From f6664df5754f7a53fdc689dd9d0c900182f3e451 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 14 Feb 2016 22:14:41 +0100
Subject: [PATCH] Left and right mononicity properties for uPred_and and
 uPred_or.

---
 algebra/upred.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/algebra/upred.v b/algebra/upred.v
index 848ba2ad5..0befa1889 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -436,8 +436,16 @@ Lemma const_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊑ ■ φ2.
 Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
 Lemma and_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∧ P') ⊑ (Q ∧ Q').
 Proof. auto. Qed.
+Lemma and_mono_l P P' Q : P ⊑ Q → (P ∧ P') ⊑ (Q ∧ P').
+Proof. by intros; apply and_mono. Qed.
+Lemma and_mono_r P P' Q' : P' ⊑ Q' → (P ∧ P') ⊑ (P ∧ Q').
+Proof. by apply and_mono. Qed.
 Lemma or_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∨ P') ⊑ (Q ∨ Q').
 Proof. auto. Qed.
+Lemma or_mono_l P P' Q : P ⊑ Q → (P ∨ P') ⊑ (Q ∨ P').
+Proof. by intros; apply or_mono. Qed.
+Lemma or_mono_r P P' Q' : P' ⊑ Q' → (P ∨ P') ⊑ (P ∨ Q').
+Proof. by apply or_mono. Qed.
 Lemma impl_mono P P' Q Q' : Q ⊑ P → P' ⊑ Q' → (P → P') ⊑ (Q → Q').
 Proof.
   intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
-- 
GitLab