From 887fcf1e4aee15e2dbdd1a49104fea2eec8b1b1c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 2 May 2019 08:08:05 +0200
Subject: [PATCH] Conditional `<absorb>?p P` modality.

---
 theories/bi/derived_connectives.v |  7 +++++
 theories/bi/derived_laws_bi.v     | 51 +++++++++++++++++++++++++++++++
 theories/bi/embedding.v           |  2 ++
 theories/bi/monpred.v             |  4 +++
 theories/bi/notation.v            |  2 ++
 theories/proofmode/monpred.v      |  4 +++
 theories/proofmode/reduction.v    |  2 +-
 7 files changed, 71 insertions(+), 1 deletion(-)

diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index d6a12d181..8576c1525 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -62,6 +62,13 @@ Instance: Params (@bi_affinely_if) 2 := {}.
 Typeclasses Opaque bi_affinely_if.
 Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
 
+Definition bi_absorbingly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
+  (if p then <absorb> P else P)%I.
+Arguments bi_absorbingly_if {_} !_ _%I /.
+Instance: Params (@bi_absorbingly_if) 2 := {}.
+Typeclasses Opaque bi_absorbingly_if.
+Notation "'<absorb>?' p P" := (bi_absorbingly_if p P) : bi_scope.
+
 Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
   (<affine> <pers> P)%I.
 Arguments bi_intuitionistically {_} _%I : simpl never.
diff --git a/theories/bi/derived_laws_bi.v b/theories/bi/derived_laws_bi.v
index a96754db2..e6aeeaf16 100644
--- a/theories/bi/derived_laws_bi.v
+++ b/theories/bi/derived_laws_bi.v
@@ -1144,6 +1144,57 @@ Proof. destruct p; simpl; auto using affinely_sep. Qed.
 Lemma affinely_if_idemp p P : <affine>?p <affine>?p P ⊣⊢ <affine>?p P.
 Proof. destruct p; simpl; auto using affinely_idemp. Qed.
 
+(* Conditional absorbingly modality *)
+Global Instance absorbingly_if_ne p : NonExpansive (@bi_absorbingly_if PROP p).
+Proof. solve_proper. Qed.
+Global Instance absorbingly_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@bi_absorbingly_if PROP p).
+Proof. solve_proper. Qed.
+Global Instance absorbingly_if_mono' p : Proper ((⊢) ==> (⊢)) (@bi_absorbingly_if PROP p).
+Proof. solve_proper. Qed.
+Global Instance absorbingly_if_flip_mono' p :
+  Proper (flip (⊢) ==> flip (⊢)) (@bi_absorbingly_if PROP p).
+Proof. solve_proper. Qed.
+
+Lemma absorbingly_if_absorbingly p P : <absorb>?p P ⊢ <absorb> P.
+Proof. destruct p; simpl; auto using absorbingly_intro. Qed.
+Lemma absorbingly_if_intro p P : P ⊢ <absorb>?p P.
+Proof. destruct p; simpl; auto using absorbingly_intro. Qed.
+Lemma absorbingly_if_mono p P Q : (P ⊢ Q) → <absorb>?p P ⊢ <absorb>?p Q.
+Proof. by intros ->. Qed.
+Lemma absorbingly_if_flag_mono (p q : bool) P : (p → q) → <absorb>?p P ⊢ <absorb>?q P.
+Proof. destruct p, q; try naive_solver auto using absorbingly_intro. Qed.
+Lemma absorbingly_if_idemp p P : <absorb>?p <absorb>?p P ⊣⊢ <absorb>?p P.
+Proof. destruct p; simpl; auto using absorbingly_idemp. Qed.
+
+Lemma absorbingly_if_pure p φ : <absorb>?p ⌜ φ ⌝ ⊣⊢ ⌜ φ ⌝.
+Proof. destruct p; simpl; auto using absorbingly_pure. Qed.
+Lemma absorbingly_if_or p P Q : <absorb>?p (P ∨ Q) ⊣⊢ <absorb>?p P ∨ <absorb>?p Q.
+Proof. destruct p; simpl; auto using absorbingly_or. Qed.
+Lemma absorbingly_if_and_1 p P Q : <absorb>?p (P ∧ Q) ⊢ <absorb>?p P ∧ <absorb>?p Q.
+Proof. destruct p; simpl; auto using absorbingly_and_1. Qed.
+Lemma absorbingly_if_forall {A} p (Φ : A → PROP) :
+  <absorb>?p (∀ a, Φ a) ⊢ ∀ a, <absorb>?p (Φ a).
+Proof. destruct p; simpl; auto using absorbingly_forall. Qed.
+Lemma absorbingly_if_exist {A} p (Φ : A → PROP) :
+  <absorb>?p (∃ a, Φ a) ⊣⊢ ∃ a, <absorb>?p (Φ a).
+Proof. destruct p; simpl; auto using absorbingly_exist. Qed.
+
+Lemma absorbingly_if_sep p P Q : <absorb>?p (P ∗ Q) ⊣⊢ <absorb>?p P ∗ <absorb>?p Q.
+Proof. destruct p; simpl; auto using absorbingly_sep. Qed.
+Lemma absorbingly_if_wand p P Q : <absorb>?p (P -∗ Q) ⊢ <absorb>?p P -∗ <absorb>?p Q.
+Proof. destruct p; simpl; auto using absorbingly_wand. Qed.
+
+Lemma absorbingly_if_sep_l p P Q : <absorb>?p P ∗ Q ⊣⊢ <absorb>?p (P ∗ Q).
+Proof. destruct p; simpl; auto using absorbingly_sep_l. Qed.
+Lemma absorbingly_if_sep_r p P Q : P ∗ <absorb>?p Q ⊣⊢ <absorb>?p (P ∗ Q).
+Proof. destruct p; simpl; auto using absorbingly_sep_r. Qed.
+Lemma absorbingly_if_sep_lr p P Q : <absorb>?p P ∗ Q ⊣⊢ P ∗ <absorb>?p Q.
+Proof. destruct p; simpl; auto using absorbingly_sep_lr. Qed.
+
+Lemma affinely_if_absorbingly_if_elim `{!BiPositive PROP} p P :
+  <affine>?p <absorb>?p P ⊣⊢ <affine>?p P.
+Proof. destruct p; simpl; auto using affinely_absorbingly_elim. Qed.
+
 (* Conditional persistently *)
 Global Instance persistently_if_ne p : NonExpansive (@bi_persistently_if PROP p).
 Proof. solve_proper. Qed.
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index a0b19edb8..2410b808b 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -188,6 +188,8 @@ Section embed.
   Lemma embed_affinely_if `{!BiEmbedEmp PROP1 PROP2} P b :
     ⎡<affine>?b P⎤ ⊣⊢ <affine>?b ⎡P⎤.
   Proof. destruct b; simpl; auto using embed_affinely. Qed.
+  Lemma embed_absorbingly_if b P : ⎡<absorb>?b P⎤ ⊣⊢ <absorb>?b ⎡P⎤.
+  Proof. destruct b; simpl; auto using embed_absorbingly. Qed.
   Lemma embed_intuitionistically_if_2 P b : □?b ⎡P⎤ ⊢ ⎡□?b P⎤.
   Proof. destruct b; simpl; auto using embed_intuitionistically_2. Qed.
   Lemma embed_intuitionistically_if `{!BiEmbedEmp PROP1 PROP2} P b :
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index d69656d03..6a75a8459 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -511,6 +511,8 @@ Proof. destruct p=>//=. apply monPred_at_intuitionistically. Qed.
 
 Lemma monPred_at_absorbingly i P : (<absorb> P) i ⊣⊢ <absorb> (P i).
 Proof. by rewrite /bi_absorbingly monPred_at_sep monPred_at_pure. Qed.
+Lemma monPred_at_absorbingly_if i p P : (<absorb>?p P) i ⊣⊢ <absorb>?p (P i).
+Proof. destruct p=>//=. apply monPred_at_absorbingly. Qed.
 
 Lemma monPred_wand_force i P Q : (P -∗ Q) i -∗ (P i -∗ Q i).
 Proof. unseal. rewrite bi.forall_elim bi.pure_impl_forall bi.forall_elim //. Qed.
@@ -651,6 +653,8 @@ Global Instance persistently_if_objective P p `{!Objective P} : Objective (<pers
 Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
 Global Instance affinely_if_objective P p `{!Objective P} : Objective (<affine>?p P).
 Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
+Global Instance absorbingly_if_objective P p `{!Objective P} : Objective (<absorb>?p P).
+Proof. rewrite /bi_absorbingly_if. destruct p; apply _. Qed.
 Global Instance intuitionistically_if_objective P p `{!Objective P} : Objective (â–¡?p P).
 Proof. rewrite /bi_intuitionistically_if. destruct p; apply _. Qed.
 
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 6a0671cd7..953448198 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -36,6 +36,8 @@ Reserved Notation "'<affine>?' p P" (at level 20, p at level 9, P at level 20,
    right associativity, format "'<affine>?' p  P").
 
 Reserved Notation "'<absorb>' P" (at level 20, right associativity).
+Reserved Notation "'<absorb>?' p P" (at level 20, p at level 9, P at level 20,
+   right associativity, format "'<absorb>?' p  P").
 
 Reserved Notation "â–¡ P" (at level 20, right associativity).
 Reserved Notation "'â–¡?' p P" (at level 20, p at level 9, P at level 20,
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 5d85ca71d..185eaf989 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -123,6 +123,10 @@ Global Instance make_monPred_at_affinely_if i P 𝓟 p :
   MakeMonPredAt i P 𝓟 →
   MakeMonPredAt i (<affine>?p P) (<affine>?p 𝓟).
 Proof. destruct p; simpl; apply _. Qed.
+Global Instance make_monPred_at_absorbingly_if i P 𝓟 p :
+  MakeMonPredAt i P 𝓟 →
+  MakeMonPredAt i (<absorb>?p P) (<absorb>?p 𝓟).
+Proof. destruct p; simpl; apply _. Qed.
 Global Instance make_monPred_at_intuitionistically_if i P 𝓟 p :
   MakeMonPredAt i P 𝓟 →
   MakeMonPredAt i (□?p P) (□?p 𝓟).
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 1c4860221..c126c9bab 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -31,7 +31,7 @@ Declare Reduction pm_prettify := cbn [
   (* telescope combinators *)
   tele_fold tele_bind tele_app
   (* BI connectives *)
-  bi_persistently_if bi_affinely_if bi_intuitionistically_if
+  bi_persistently_if bi_affinely_if bi_absorbingly_if bi_intuitionistically_if
   bi_wandM sbi_laterN
   bi_tforall bi_texist
 ].
-- 
GitLab