From b1fa82f0ef47d01f88b9032f265d3754adf5fa5b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Dec 2016 18:31:28 +0100
Subject: [PATCH] proofmode: show that quantifiers preserve purity

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

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 08d1ff595..998fab981 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -31,6 +31,19 @@ Global Instance into_pure_cmra_valid `{CMRADiscrete A} (a : A) :
   @IntoPure M (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
+Global Instance into_pure_exist {X : Type} (Φ : X → uPred M) φ :
+  (∀ x, @IntoPure M (Φ x) (φ x)) → @IntoPure M (∃ x, Φ x) (∃ x, φ x).
+Proof.
+  rewrite /IntoPure=>Hx. apply exist_elim=>x. rewrite Hx.
+  apply pure_elim'=>Hφ. apply pure_intro. eauto.
+Qed.
+
+Global Instance into_pure_forall {X : Type} (Φ : X → uPred M) φ :
+  (∀ x, @IntoPure M (Φ x) (φ x)) → @IntoPure M (∀ x, Φ x) (∀ x, φ x).
+Proof.
+  rewrite /IntoPure=>Hx. rewrite -pure_forall_2. by setoid_rewrite Hx.
+Qed.
+
 (* FromPure *)
 Global Instance from_pure_pure φ : @FromPure M ⌜φ⌝ φ.
 Proof. done. Qed.
-- 
GitLab