From d9cad5bfa9af8938ce09247d4b0f39893ba2a59a Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Wed, 15 Feb 2017 15:25:01 +0100
Subject: [PATCH] =?UTF-8?q?Add=20IntoPure=20instances=20for=20=E2=88=97,?=
 =?UTF-8?q?=20=E2=88=A7,=20and=20=E2=88=A8.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/proofmode/class_instances.v | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 7694c59b6..2fd3fa1ca 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -55,6 +55,15 @@ Global Instance into_pure_forall {X : Type} (Φ : X → uPred M) φ :
 Proof.
   rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
 Qed.
+Global Instance into_pure_pure_conj (φ1 φ2 : uPred M) P1 P2 :
+  IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 ∧ φ2) (P1 ∧ P2).
+Proof. rewrite /IntoPure pure_and. by intros -> ->. Qed.
+Global Instance into_pure_pure_sep (φ1 φ2 : uPred M) P1 P2 :
+  IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 ∗ φ2) (P1 ∧ P2).
+Proof. rewrite /IntoPure sep_and pure_and. by intros -> ->. Qed.
+Global Instance into_pure_pure_disj (φ1 φ2 : uPred M) P1 P2 :
+  IntoPure φ1 P1 -> IntoPure φ2 P2 -> IntoPure (φ1 ∨ φ2) (P1 ∨ P2).
+Proof. rewrite /IntoPure pure_or. by intros -> ->. Qed.
 
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure M ⌜φ⌝ φ.
-- 
GitLab