From 7ddfabf679a60f6ccc68dec5775a73eae2e9e066 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Feb 2018 01:44:24 +0100
Subject: [PATCH] More `IntoSep` and `IntoAnd` instances.

For better support for eliminating affine/absorbing separating
conjunctions in the persistent context/under a plainness/persistence
modality.
---
 theories/proofmode/class_instances.v | 43 ++++++++++++++++++++++++----
 1 file changed, 37 insertions(+), 6 deletions(-)

diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index c365846e5..bee7b8abe 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -531,6 +531,10 @@ Global Instance into_and_sep `{BiPositive PROP} P Q : IntoAnd true (P ∗ Q) P Q
 Proof.
   by rewrite /IntoAnd /= persistently_sep -and_sep_persistently persistently_and.
 Qed.
+Global Instance into_and_sep_affine P Q :
+  TCOr (TCAnd (Affine P) (Affine Q)) (TCAnd (Absorbing P) (Absorbing Q)) →
+  IntoAnd true (P ∗ Q) P Q.
+Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoAnd pure_and affinely_persistently_if_and. Qed.
@@ -595,7 +599,6 @@ Proof.
   - by rewrite persistent_and_affinely_sep_r_1.
 Qed.
 
-
 Global Instance into_sep_pure φ ψ : @IntoSep PROP ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
 Proof. by rewrite /IntoSep pure_and persistent_and_sep_1. Qed.
 
@@ -603,19 +606,47 @@ Global Instance into_sep_embed `{BiEmbedding PROP PROP'} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep ⎡P⎤ ⎡Q1⎤ ⎡Q2⎤.
 Proof. rewrite /IntoSep -bi_embed_sep=> -> //. Qed.
 
-(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely. Also, it
-overlaps with `into_sep_affinely_later`, and hence has lower precedence. *)
-Global Instance into_sep_affinely P Q1 Q2 :
+Global Instance into_sep_affinely `{BiPositive PROP} P Q1 Q2 :
+  IntoSep P Q1 Q2 → IntoSep (bi_affinely P) (bi_affinely Q1) (bi_affinely Q2) | 0.
+Proof. rewrite /IntoSep /= => ->. by rewrite affinely_sep. Qed.
+(* FIXME: This instance is kind of strange, it just gets rid of the bi_affinely.
+Also, it overlaps with `into_sep_affinely_later`, and hence has lower
+precedence. *)
+Global Instance into_sep_affinely_trim P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (bi_affinely P) Q1 Q2 | 20.
 Proof. rewrite /IntoSep /= => ->. by rewrite affinely_elim. Qed.
 
 Global Instance into_sep_plainly `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 → IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite plainly_sep. Qed.
+Global Instance into_sep_plainly_affine P Q1 Q2 :
+  IntoSep P Q1 Q2 →
+  TCOr (TCAnd (Affine Q1) (Affine Q2)) (TCAnd (Absorbing Q1) (Absorbing Q2)) →
+  IntoSep (bi_plainly P) (bi_plainly Q1) (bi_plainly Q2).
+Proof.
+  rewrite /IntoSep /= => -> ?. by rewrite sep_and plainly_and plainly_and_sep_l_1.
+Qed.
+
 Global Instance into_sep_persistently `{BiPositive PROP} P Q1 Q2 :
   IntoSep P Q1 Q2 →
   IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
 Proof. rewrite /IntoSep /= => ->. by rewrite persistently_sep. Qed.
+Global Instance into_sep_persistently_affine P Q1 Q2 :
+  IntoSep P Q1 Q2 →
+  TCOr (TCAnd (Affine Q1) (Affine Q2)) (TCAnd (Absorbing Q1) (Absorbing Q2)) →
+  IntoSep (bi_persistently P) (bi_persistently Q1) (bi_persistently Q2).
+Proof.
+  rewrite /IntoSep /= => -> ?.
+  by rewrite sep_and persistently_and persistently_and_sep_l_1.
+Qed.
+Global Instance into_sep_affinely_persistently_affine P Q1 Q2 :
+  IntoSep P Q1 Q2 →
+  TCOr (TCAnd (Affine Q1) (Affine Q2)) (TCAnd (Absorbing Q1) (Absorbing Q2)) →
+  IntoSep (â–¡ P) (â–¡ Q1) (â–¡ Q2).
+Proof.
+  rewrite /IntoSep /= => -> ?.
+  by rewrite sep_and affinely_persistently_and and_sep_affinely_persistently.
+Qed.
 
 (* We use [IsCons] and [IsApp] to make sure that [frame_big_sepL_cons] and
 [frame_big_sepL_app] cannot be applied repeatedly often when having
@@ -1261,10 +1292,10 @@ Proof. rewrite /IntoSep=> ->. by rewrite except_0_sep. Qed.
 
 (* FIXME: This instance is overly specific, generalize it. *)
 Global Instance into_sep_affinely_later `{!Timeless (emp%I : PROP)} P Q1 Q2 :
-  Affine Q1 → Affine Q2 → IntoSep P Q1 Q2 →
+  IntoSep P Q1 Q2 → Affine Q1 → Affine Q2 →
   IntoSep (bi_affinely (â–· P)) (bi_affinely (â–· Q1)) (bi_affinely (â–· Q2)).
 Proof.
-  rewrite /IntoSep /= => ?? ->.
+  rewrite /IntoSep /= => -> ??.
   rewrite -{1}(affine_affinely Q1) -{1}(affine_affinely Q2) later_sep !later_affinely_1.
   rewrite -except_0_sep /sbi_except_0 affinely_or. apply or_elim, affinely_elim.
   rewrite -(idemp bi_and (bi_affinely (â–· False))%I) persistent_and_sep_1.
-- 
GitLab