From 74cf33ae2d20a5bf7fbaf39dcd3a9508e98de4c7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 22 Feb 2018 01:44:52 +0100
Subject: [PATCH] Make filtering of `iAlways` more liberal.

It now no longer requires the modality to be absorbing by default; it
only should be absorbing when non-affine hypotheses have been cleared.
---
 theories/proofmode/classes.v       |  5 +-
 theories/proofmode/coq_tactics.v   | 84 ++++++++++++++++++------------
 theories/proofmode/monpred.v       | 22 ++------
 theories/proofmode/tactics.v       | 16 ++++--
 theories/tests/proofmode_monpred.v |  6 ++-
 5 files changed, 72 insertions(+), 61 deletions(-)

diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index 2f1826329..a8ee83568 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -132,7 +132,7 @@ Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
     match sspec with
     | AIEnvIsEmpty => True
     | AIEnvForall C => ∀ P, C P → P ⊢ M P
-    | AIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q) ∧ (∀ P, Absorbing (M P))
+    | AIEnvTransform C => (∀ P Q, C P Q → P ⊢ M Q)
     | AIEnvClear => ∀ P, Absorbing (M P)
     | AIEnvId => False
     end;
@@ -172,9 +172,6 @@ Section always_modality.
   Lemma always_modality_spatial_transform C P Q :
     always_modality_spatial_spec M = AIEnvTransform C → C P Q → P ⊢ M Q.
   Proof. destruct M as [??? []]; naive_solver. Qed.
-  Lemma always_modality_spatial_transform_absorbing C P :
-    always_modality_spatial_spec M = AIEnvTransform C → Absorbing (M P).
-  Proof. destruct M as [??? []]; naive_solver. Qed.
   Lemma always_modality_spatial_clear P :
     always_modality_spatial_spec M = AIEnvClear → Absorbing (M P).
   Proof. destruct M as [??? []]; naive_solver. Qed.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 5209a6815..9a9e4b145 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -620,45 +620,54 @@ Proof.
 Qed.
 
 Class TransformSpatialEnv
-    (M : always_modality PROP) (C : PROP → PROP → Prop) (Γ1 Γ2 : env PROP) := {
+    (M : always_modality PROP) (C : PROP → PROP → Prop)
+    (Γ1 Γ2 : env PROP) (filtered : bool) := {
   transform_spatial_env :
-    (∀ P Q, C P Q → P ⊢ M Q) → (∀ P, Absorbing (M P)) →
-    ([∗] Γ1) ⊢ M ([∗] Γ2);
+    (∀ P Q, C P Q → P ⊢ M Q) →
+    ([∗] Γ1) ⊢ M ([∗] Γ2) ∗ if filtered then True else emp;
   transform_spatial_env_wf : env_wf Γ1 → env_wf Γ2;
   transform_spatial_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
 }.
-Global Instance transform_spatial_env_nil M C : TransformSpatialEnv M C Enil Enil.
-Proof. split=> // HC /=. by rewrite -always_modality_emp. Qed.
-Global Instance transform_spatial_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q :
+Global Instance transform_spatial_env_nil M C :
+  TransformSpatialEnv M C Enil Enil false.
+Proof. split=> // HC /=. by rewrite right_id -always_modality_emp. Qed.
+Global Instance transform_spatial_env_snoc M (C : PROP → PROP → Prop) Γ Γ' i P Q fi :
   C P Q →
-  TransformSpatialEnv M C Γ Γ' →
-  TransformSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q).
+  TransformSpatialEnv M C Γ Γ' fi →
+  TransformSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i Q) fi.
 Proof.
   intros ? [HΓ Hwf Hdom]; split; simpl.
-  - intros HC ?. by rewrite {1}(HC P) // HΓ // always_modality_sep.
+  - intros HC. by rewrite {1}(HC P) // HΓ // assoc always_modality_sep.
   - inversion 1; constructor; auto.
   - intros j. destruct (ident_beq _ _); naive_solver.
 Qed.
 
-Global Instance transform_spatial_env_snoc_not M (C : PROP → PROP → Prop) Γ Γ' i P :
-  TransformSpatialEnv M C Γ Γ' →
-  TransformSpatialEnv M C (Esnoc Γ i P) Γ' | 100.
+Global Instance transform_spatial_env_snoc_not
+    M (C : PROP → PROP → Prop) Γ Γ' i P fi fi' :
+  TransformSpatialEnv M C Γ Γ' fi →
+  TCIf (TCEq fi false)
+    (TCIf (Affine P) (TCEq fi' false) (TCEq fi' true))
+    (TCEq fi' true) →
+  TransformSpatialEnv M C (Esnoc Γ i P) Γ' fi' | 100.
 Proof.
-  intros [HΓ Hwf Hdom]; split; simpl.
-  - intros HC ?. by rewrite HΓ // sep_elim_r.
+  intros [HΓ Hwf Hdom] Hif; split; simpl.
+  - intros ?. rewrite HΓ //. destruct Hif as [-> [? ->| ->]| ->].
+    + by rewrite (affine P) left_id.
+    + by rewrite right_id comm (True_intro P).
+    + by rewrite comm -assoc (True_intro (_ ∗ P)%I).
   - inversion 1; auto.
   - intros j. destruct (ident_beq _ _); naive_solver.
 Qed.
 
 (** The actual tactic *)
-Ltac tac_always_cases :=
+Ltac tac_always_cases fi :=
   simplify_eq/=;
   repeat match goal with
   | H : TCAnd _ _ |- _ => destruct H
   | H : TCEq ?x _ |- _ => inversion H; subst x; clear H
   | H : TCForall _ _ |- _ => apply TCForall_Forall in H
   | H : TransformPersistentEnv _ _ _ _ |- _ => destruct H
-  | H : TransformSpatialEnv _ _ _ _ |- _ => destruct H
+  | H : ∃ fi, TransformSpatialEnv _ _ _ _ fi ∧ _ |- _ => destruct H as [fi [[] ?]]
   end; simpl; auto using Enil_wf.
 
 Lemma tac_always_intro Γp Γs Γp' Γs' M Q Q' :
@@ -672,37 +681,46 @@ Lemma tac_always_intro Γp Γs Γp' Γs' M Q Q' :
   end →
   match always_modality_spatial_spec M with
   | AIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
-  | AIEnvTransform C => TransformSpatialEnv M C Γs Γs'
+  | AIEnvTransform C =>
+     ∃ fi, TransformSpatialEnv M C Γs Γs' fi ∧
+     if fi then Absorbing Q' else TCTrue
   | AIEnvIsEmpty => TCAnd (TCEq Γs Enil) (TCEq Γs' Enil)
   | AIEnvClear => TCEq Γs' Enil
   | AIEnvId => TCEq Γs Γs'
   end →
   envs_entails (Envs Γp' Γs') Q → envs_entails (Envs Γp Γs) Q'.
 Proof.
-  rewrite envs_entails_eq /FromAlways /of_envs /= => <- HΓp HΓs <-.
-  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')).
+  rewrite envs_entails_eq /FromAlways /of_envs /= => HQ' HΓp HΓs HQ.
+  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')) as Hwf.
   { split; simpl in *.
-    - destruct (always_modality_persistent_spec M); tac_always_cases.
-    - destruct (always_modality_spatial_spec M); tac_always_cases.
+    - destruct (always_modality_persistent_spec M); tac_always_cases fi.
+    - destruct (always_modality_spatial_spec M); tac_always_cases fi.
     - destruct (always_modality_persistent_spec M),
-        (always_modality_spatial_spec M); tac_always_cases; naive_solver. }
-  rewrite pure_True // left_id. rewrite -always_modality_sep. apply sep_mono.
-  - destruct (always_modality_persistent_spec M) eqn:?; tac_always_cases.
+        (always_modality_spatial_spec M); tac_always_cases fi; naive_solver. }
+  assert (□ [∧] Γp ⊢ M (□ [∧] Γp'))%I as HMp.
+  { destruct (always_modality_persistent_spec M) eqn:?; tac_always_cases fi.
     + by rewrite {1}affinely_elim_emp (always_modality_emp M)
         persistently_True_emp affinely_persistently_emp.
     + eauto using always_modality_persistent_forall_big_and.
     + eauto using always_modality_persistent_transform.
     + by rewrite {1}affinely_elim_emp (always_modality_emp M)
         persistently_True_emp affinely_persistently_emp.
-    + eauto using always_modality_persistent_id.
-  - destruct (always_modality_spatial_spec M) eqn:?; tac_always_cases.
-    + by rewrite -always_modality_emp.
-    + eauto using always_modality_spatial_forall_big_sep.
-    + eauto using always_modality_spatial_transform,
-        always_modality_spatial_transform_absorbing.
-    + rewrite -(always_modality_spatial_clear M) // -always_modality_emp.
-      by rewrite -absorbingly_True_emp absorbingly_pure -True_intro.
-    + by destruct (always_modality_spatial_id M).
+    + eauto using always_modality_persistent_id. }
+  move: HQ'; rewrite -HQ pure_True // left_id HMp=> HQ' {HQ Hwf HMp}.
+  destruct (always_modality_spatial_spec M) eqn:?; tac_always_cases fi.
+  + by rewrite -HQ' /= !right_id.
+  + rewrite -HQ' {1}(always_modality_spatial_forall_big_sep _ _ Γs') //.
+    by rewrite always_modality_sep.
+  + destruct fi.
+    - rewrite -(absorbing Q') /bi_absorbingly -HQ' (comm _ True%I).
+      rewrite -always_modality_sep -assoc. apply sep_mono_r.
+      eauto using always_modality_spatial_transform.
+    - rewrite -HQ' -always_modality_sep. apply sep_mono_r.
+      rewrite -(right_id emp%I bi_sep (M _)).
+      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).
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :
diff --git a/theories/proofmode/monpred.v b/theories/proofmode/monpred.v
index 7c21befe8..96890ce60 100644
--- a/theories/proofmode/monpred.v
+++ b/theories/proofmode/monpred.v
@@ -15,22 +15,9 @@ Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
             : typeclass_instances.
 
 Section always_modalities.
-Context {I : biIndex} {PROP : bi}.
+  Context {I : biIndex} {PROP : bi}.
 
   Lemma always_modality_absolutely_mixin :
-    always_modality_mixin (@monPred_absolutely I PROP)
-      (AIEnvFilter Absolute) (AIEnvForall Absolute).
-  Proof.
-    split; intros; try match goal with H : TCDiag _ _ _ |- _ => destruct H end;
-      eauto using bi.equiv_entails_sym, absolute_absolutely,
-        monPred_absolutely_mono, monPred_absolutely_and,
-        monPred_absolutely_sep_2 with typeclass_instances.
-  Qed.
-  Definition always_modality_absolutely :=
-    AlwaysModality _ always_modality_absolutely_mixin.
-
-  (* We can only filter the spatial context in case the BI is affine *)
-  Lemma always_modality_absolutely_filter_spatial_mixin `{BiAffine PROP} :
     always_modality_mixin (@monPred_absolutely I PROP)
       (AIEnvFilter Absolute) (AIEnvFilter Absolute).
   Proof.
@@ -39,8 +26,8 @@ Context {I : biIndex} {PROP : bi}.
         monPred_absolutely_mono, monPred_absolutely_and,
         monPred_absolutely_sep_2 with typeclass_instances.
   Qed.
-  Definition always_modality_absolutely_filter_spatial `{BiAffine PROP} :=
-    AlwaysModality _ always_modality_absolutely_filter_spatial_mixin.
+  Definition always_modality_absolutely :=
+    AlwaysModality _ always_modality_absolutely_mixin.
 End always_modalities.
 
 Section bi.
@@ -55,9 +42,6 @@ Implicit Types i j : I.
 Global Instance from_always_absolutely P :
   FromAlways always_modality_absolutely (∀ᵢ P) P | 1.
 Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_absolutely_filter_spatial `{BiAffine PROP} P :
-  FromAlways always_modality_absolutely_filter_spatial (∀ᵢ P) P | 0.
-Proof. by rewrite /FromAlways. Qed.
 
 Global Instance make_monPred_at_pure φ i : MakeMonPredAt i ⌜φ⌝ ⌜φ⌝.
 Proof. by rewrite /MakeMonPredAt monPred_at_pure. Qed.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index f7c535f5b..ddf62b66f 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -967,15 +967,23 @@ Tactic Notation "iAlways":=
   eapply tac_always_intro;
     [apply _  ||
      fail "iAlways: the goal is not an always-style modality"
-    |hnf; env_cbv; apply _ ||
+    |hnf; env_cbv;
+     apply _ ||
      lazymatch goal with
      | |- TCAnd (TCForall ?C _) _ => fail "iAlways: persistent context does not satisfy" C
      | |- TCAnd (TCEq _ Enil) _ => fail "iAlways: persistent context is non-empty"
      end
-    |hnf; env_cbv; apply _ ||
+    |hnf; env_cbv;
      lazymatch goal with
-     | |- TCAnd (TCForall ?C _) _ => fail "iAlways: spatial context does not satisfy" C
-     | |- TCAnd (TCEq _ Enil) _ => fail "iAlways: spatial context is non-empty"
+     | |- ∃ _, TransformSpatialEnv _ _ _ _ _ ∧ _ =>
+        eexists; split;
+          [apply _
+          |apply _ || fail "iAlways: cannot filter spatial context when goal is not absorbing"]
+     | |- TCAnd (TCForall ?C _) _ =>
+        apply _ || fail "iAlways: spatial context does not satisfy" C
+     | |- TCAnd (TCEq _ Enil) _ =>
+        apply _ || fail "iAlways: spatial context is non-empty"
+     | |- _ => apply _
      end
     |env_cbv].
 
diff --git a/theories/tests/proofmode_monpred.v b/theories/tests/proofmode_monpred.v
index 997f212c6..52451a74d 100644
--- a/theories/tests/proofmode_monpred.v
+++ b/theories/tests/proofmode_monpred.v
@@ -71,7 +71,11 @@ Section tests.
   Lemma test_absolutely P Q : ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ". iAlways. by iSplitL "HP". Qed.
 
-  Lemma test_absolutely_affine `{BiAffine PROP} P Q R :
+  Lemma test_absolutely_absorbing P Q R `{!Absorbing P} :
+    ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
+  Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
+
+  Lemma test_absolutely_affine P Q R `{!Affine R} :
     ∀ᵢ emp -∗ ∀ᵢ P -∗ ∀ᵢ Q -∗ R -∗ ∀ᵢ (P ∗ Q).
   Proof. iIntros "#? HP HQ HR". iAlways. by iSplitL "HP". Qed.
 
-- 
GitLab