From 0de297e176aecb406130ac042097d802dd4cc042 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Feb 2017 19:25:59 +0100
Subject: [PATCH] more FromPure and IntoPure instances

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

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 2fd3fa1ca..db9633a91 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -43,6 +43,24 @@ 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_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.
+Global Instance into_pure_pure_impl (Ï†1 Ï†2 : uPred M) P1 P2 :
+  FromPure Ï†1 P1 -> IntoPure Ï†2 P2 -> IntoPure (Ï†1 â†’ Ï†2) (P1 â†’ P2).
+Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
+Global Instance into_pure_pure_wand (Ï†1 Ï†2 : uPred M) P1 P2 :
+  FromPure Ï†1 P1 -> IntoPure Ï†2 P2 -> IntoPure (Ï†1 -âˆ— Ï†2) (P1 â†’ P2).
+Proof.
+  rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
+Qed.
+
 Global Instance into_pure_exist {X : Type} (Î¦ : X â†’ uPred M) Ï† :
   (âˆ€ x, @IntoPure M (Î¦ x) (Ï† x)) â†’ @IntoPure M (âˆƒ x, Î¦ x) (âˆƒ x, Ï† x).
 Proof.
@@ -55,15 +73,6 @@ 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 âŒœÏ†âŒ Ï†.
@@ -82,6 +91,38 @@ Qed.
 Global Instance from_pure_bupd P Ï† : FromPure P Ï† â†’ FromPure (|==> P) Ï†.
 Proof. rewrite /FromPure=> ->. apply bupd_intro. Qed.
 
+
+Global Instance from_pure_pure_conj (Ï†1 Ï†2 : uPred M) P1 P2 :
+  FromPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 âˆ§ Ï†2) (P1 âˆ§ P2).
+Proof. rewrite /FromPure pure_and. by intros -> ->. Qed.
+Global Instance from_pure_pure_sep (Ï†1 Ï†2 : uPred M) P1 P2 :
+  FromPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 âˆ— Ï†2) (P1 âˆ§ P2).
+Proof. rewrite /FromPure pure_and always_and_sep_l. by intros -> ->. Qed.
+Global Instance from_pure_pure_disj (Ï†1 Ï†2 : uPred M) P1 P2 :
+  FromPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 âˆ¨ Ï†2) (P1 âˆ¨ P2).
+Proof. rewrite /FromPure pure_or. by intros -> ->. Qed.
+Global Instance from_pure_pure_impl (Ï†1 Ï†2 : uPred M) P1 P2 :
+  IntoPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 â†’ Ï†2) (P1 â†’ P2).
+Proof. rewrite /FromPure /IntoPure pure_impl. by intros -> ->. Qed.
+Global Instance from_pure_pure_wand (Ï†1 Ï†2 : uPred M) P1 P2 :
+  IntoPure Ï†1 P1 -> FromPure Ï†2 P2 -> FromPure (Ï†1 -âˆ— Ï†2) (P1 â†’ P2).
+Proof.
+  rewrite /FromPure /IntoPure pure_impl always_impl_wand. by intros -> ->.
+Qed.
+
+Global Instance from_pure_exist {X : Type} (Î¦ : X â†’ uPred M) Ï† :
+  (âˆ€ x, @FromPure M (Î¦ x) (Ï† x)) â†’ @FromPure M (âˆƒ x, Î¦ x) (âˆƒ x, Ï† x).
+Proof.
+  rewrite /FromPure=>Hx. apply pure_elim'=>-[x ?]. rewrite -(exist_intro x).
+  rewrite -Hx. apply pure_intro. done.
+Qed.
+Global Instance from_pure_forall {X : Type} (Î¦ : X â†’ uPred M) Ï† :
+  (âˆ€ x, @FromPure M (Î¦ x) (Ï† x)) â†’ @FromPure M (âˆ€ x, Î¦ x) (âˆ€ x, Ï† x).
+Proof.
+  rewrite /FromPure=>Hx. apply forall_intro=>x. apply pure_elim'=>HÏ†.
+  rewrite -Hx. apply pure_intro. done.
+Qed.
+
 (* IntoPersistentP *)
 Global Instance into_persistentP_always_trans P Q :
   IntoPersistentP P Q â†’ IntoPersistentP (â–¡ P) Q | 0.
-- 
GitLab