From 7dcb321721284057b595054af2ce0b1402c99511 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 22 Feb 2018 02:11:20 +0100
Subject: [PATCH] Support `AIEnvId` for the spatial context.

---
 theories/proofmode/classes.v     | 6 +++---
 theories/proofmode/coq_tactics.v | 3 ++-
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index a8ee83568..02d79e6f9 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -134,7 +134,7 @@ Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
     | AIEnvForall C => ∀ P, C P → P ⊢ M P
     | AIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
     | AIEnvClear => ∀ P, Absorbing (M P)
-    | AIEnvId => False
+    | AIEnvId => ∀ P, P ⊢ M P
     end;
   always_modality_mixin_emp : emp ⊢ M emp;
   always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
@@ -175,8 +175,8 @@ Section always_modality.
   Lemma always_modality_spatial_clear P :
     always_modality_spatial_spec M = AIEnvClear → Absorbing (M P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_id :
-    always_modality_spatial_spec M ≠ AIEnvId.
+  Lemma always_modality_spatial_id P :
+    always_modality_spatial_spec M = AIEnvId → P ⊢ M P.
   Proof. destruct M as [??? []]; naive_solver. Qed.
 
   Lemma always_modality_emp : emp ⊢ M emp.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 9a9e4b145..4696f8422 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -720,7 +720,8 @@ Proof.
       eauto using always_modality_spatial_transform.
   + rewrite -HQ' /= right_id comm -{2}(always_modality_spatial_clear M) //.
     by rewrite (True_intro ([∗] Γs)%I).
-  + by destruct (always_modality_spatial_id M).
+  + rewrite -HQ' {1}(always_modality_spatial_id M ([∗] Γs')%I) //.
+    by rewrite -always_modality_sep.
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
-- 
GitLab