Merge branch 'robbert/super_iAlways' into 'gen_proofmode'

Generic `iAlways` tactic.

See merge request FP/iris-coq!111

theories/proofmode/class_instances.v

@@ -3,6 +3,56 @@ From iris.bi Require Import bi tactics.
 Set Default Proof Using "Type".
 Import bi.
 
+Section always_modalities.
+  Context {PROP : bi}.
+  Lemma always_modality_persistently_mixin :
+    always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
+  Proof.
+    split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
+      persistently_and, persistently_sep_2 with typeclass_instances.
+  Qed.
+  Definition always_modality_persistently :=
+    AlwaysModality _ always_modality_persistently_mixin.
+
+  Lemma always_modality_affinely_mixin :
+    always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
+  Proof.
+    split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
+      affinely_and, affinely_sep_2 with typeclass_instances.
+  Qed.
+  Definition always_modality_affinely :=
+    AlwaysModality _ always_modality_affinely_mixin.
+
+  Lemma always_modality_affinely_persistently_mixin :
+    always_modality_mixin (λ P : PROP, □ P)%I AIEnvId AIEnvIsEmpty.
+  Proof.
+    split; eauto using equiv_entails_sym, affinely_persistently_emp,
+      affinely_mono, persistently_mono, affinely_persistently_idemp,
+      affinely_persistently_and, affinely_persistently_sep_2 with typeclass_instances.
+  Qed.
+  Definition always_modality_affinely_persistently :=
+    AlwaysModality _ always_modality_affinely_persistently_mixin.
+
+  Lemma always_modality_plainly_mixin :
+    always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
+  Proof.
+    split; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
+      plainly_and, plainly_sep_2 with typeclass_instances.
+  Qed.
+  Definition always_modality_plainly :=
+    AlwaysModality _ always_modality_plainly_mixin.
+
+  Lemma always_modality_affinely_plainly_mixin :
+    always_modality_mixin (λ P : PROP, ■ P)%I (AIEnvForall Plain) AIEnvIsEmpty.
+  Proof.
+    split; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
+      plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
+      affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
+  Qed.
+  Definition always_modality_affinely_plainly :=
+    AlwaysModality _ always_modality_affinely_plainly_mixin.
+End always_modalities.
+
 Section bi_instances.
 Context {PROP : bi}.
 Implicit Types P Q R : PROP.
@@ -190,31 +240,53 @@ Global Instance into_persistent_persistent P :
 Proof. intros. by rewrite /IntoPersistent. Qed.
 
 (* FromAlways *)
-Global Instance from_always_here P : FromAlways false false false P P | 1.
+Global Instance from_always_affinely P :
+  FromAlways always_modality_affinely (bi_affinely P) P | 2.
 Proof. by rewrite /FromAlways. Qed.
-Global Instance from_always_plainly a pe pl P Q :
-  FromAlways a pe pl P Q → FromAlways false true true (bi_plainly P) Q | 0.
-Proof.
-  rewrite /FromAlways /= => <-.
-  destruct a, pe, pl; rewrite /= ?persistently_affinely ?plainly_affinely
-       !persistently_plainly ?plainly_idemp ?plainly_persistently //.
-Qed.
-Global Instance from_always_persistently a pe pl P Q :
-  FromAlways a pe pl P Q → FromAlways false true pl (bi_persistently P) Q | 0.
-Proof.
-  rewrite /FromAlways /= => <-.
-  destruct a, pe; rewrite /= ?persistently_affinely ?persistently_idemp //.
-Qed.
-Global Instance from_always_affinely a pe pl P Q :
-  FromAlways a pe pl P Q → FromAlways true pe pl (bi_affinely P) Q | 0.
-Proof.
-  rewrite /FromAlways /= => <-. destruct a; by rewrite /= ?affinely_idemp.
-Qed.
-Global Instance from_always_embed `{BiEmbedding PROP PROP'} a pe pl P Q :
-  FromAlways a pe pl P Q → FromAlways a pe pl ⎡P⎤ ⎡Q⎤ | 0.
-Proof.
-  rewrite /FromAlways=><-.
-  by rewrite bi_embed_affinely_if bi_embed_persistently_if bi_embed_plainly_if.
+
+Global Instance from_always_persistently P :
+  FromAlways always_modality_persistently (bi_persistently P) P | 2.
+Proof. by rewrite /FromAlways. Qed.
+Global Instance from_always_affinely_persistently P :
+  FromAlways always_modality_affinely_persistently (□ P) P | 1.
+Proof. by rewrite /FromAlways. Qed.
+Global Instance from_always_affinely_persistently_affine_bi P :
+  BiAffine PROP → FromAlways always_modality_persistently (□ P) P | 0.
+Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
+
+Global Instance from_always_plainly P :
+  FromAlways always_modality_plainly (bi_plainly P) P | 2.
+Proof. by rewrite /FromAlways. Qed.
+Global Instance from_always_affinely_plainly P :
+  FromAlways always_modality_affinely_plainly (■ P) P | 1.
+Proof. by rewrite /FromAlways. Qed.
+Global Instance from_always_affinely_plainly_affine_bi P :
+  BiAffine PROP → FromAlways always_modality_plainly (■ P) P | 0.
+Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
+
+Global Instance from_always_affinely_embed `{BiEmbedding PROP PROP'} P Q :
+  FromAlways always_modality_affinely P Q →
+  FromAlways always_modality_affinely ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely. Qed.
+Global Instance from_always_persistently_embed `{BiEmbedding PROP PROP'} P Q :
+  FromAlways always_modality_persistently P Q →
+  FromAlways always_modality_persistently ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_persistently. Qed.
+Global Instance from_always_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
+  FromAlways always_modality_affinely_persistently P Q →
+  FromAlways always_modality_affinely_persistently ⎡P⎤ ⎡Q⎤.
+Proof.
+  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
+Qed.
+Global Instance from_always_plainly_embed `{BiEmbedding PROP PROP'} P Q :
+  FromAlways always_modality_plainly P Q →
+  FromAlways always_modality_plainly ⎡P⎤ ⎡Q⎤.
+Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_plainly. Qed.
+Global Instance from_always_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
+  FromAlways always_modality_affinely_plainly P Q →
+  FromAlways always_modality_affinely_plainly ⎡P⎤ ⎡Q⎤.
+Proof.
+  rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
 Qed.
 
 (* IntoWand *)

theories/proofmode/classes.v

@@ -68,11 +68,138 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
 Arguments into_persistent {_} _ _%I _%I {_}.
 Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
-Class FromAlways {PROP : bi} (a pe pl : bool) (P Q : PROP) :=
-  from_always : bi_affinely_if a (bi_persistently_if pe (bi_plainly_if pl Q)) ⊢ P.
-Arguments FromAlways {_} _ _ _ _%I _%I : simpl never.
-Arguments from_always {_} _ _ _ _%I _%I {_}.
-Hint Mode FromAlways + - - - ! - : typeclass_instances.
+(* The `iAlways` tactic is not tied to `persistently` and `affinely`, but can be
+instantiated with a variety of comonadic (always-style) modalities.
+
+In order to plug in an always-style modality, one has to decide for both the
+persistent and spatial what action should be performed upon introducing the
+modality:
+
+- Introduction is only allowed when the context is empty.
+- Introduction is only allowed when all hypotheses satisfy some predicate
+  `C : PROP → Prop` (where `C` should be a type class).
+- Introduction will only keep the hypotheses that satisfy some predicate
+  `C : PROP → Prop` (where `C` should be a type class).
+- Introduction will clear the context.
+- Introduction will keep the context as-if.
+
+Formally, these actions correspond to the following inductive type: *)
+Inductive always_intro_spec (PROP : bi) :=
+  | AIEnvIsEmpty
+  | AIEnvForall (C : PROP → Prop)
+  | AIEnvFilter (C : PROP → Prop)
+  | AIEnvClear
+  | AIEnvId.
+Arguments AIEnvIsEmpty {_}.
+Arguments AIEnvForall {_} _.
+Arguments AIEnvFilter {_} _.
+Arguments AIEnvClear {_}.
+Arguments AIEnvId {_}.
+
+(* An always-style modality is then a record packing together the modality with
+the laws it should satisfy to justify the given actions for both contexts: *)
+Record always_modality_mixin {PROP : bi} (M : PROP → PROP)
+    (pspec sspec : always_intro_spec PROP) := {
+  always_modality_mixin_persistent :
+    match pspec with
+    | AIEnvIsEmpty => True
+    | AIEnvForall C | AIEnvFilter C => ∀ P, C P → □ P ⊢ M (□ P)
+    | AIEnvClear => True
+    | AIEnvId => ∀ P, □ P ⊢ M (□ P)
+    end;
+  always_modality_mixin_spatial :
+    match sspec with
+    | AIEnvIsEmpty => True
+    | AIEnvForall C => ∀ P, C P → P ⊢ M P
+    | AIEnvFilter C => (∀ P, C P → P ⊢ M P) ∧ (∀ P, Absorbing (M P))
+    | AIEnvClear => ∀ P, Absorbing (M P)
+    | AIEnvId => False
+    end;
+  always_modality_mixin_emp : emp ⊢ M emp;
+  always_modality_mixin_mono P Q : (P ⊢ Q) → M P ⊢ M Q;
+  always_modality_mixin_and P Q : M P ∧ M Q ⊢ M (P ∧ Q);
+  always_modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
+}.
+
+Record always_modality (PROP : bi) := AlwaysModality {
+  always_modality_car :> PROP → PROP;
+  always_modality_persistent_spec : always_intro_spec PROP;
+  always_modality_spatial_spec : always_intro_spec PROP;
+  always_modality_mixin_of : always_modality_mixin
+    always_modality_car
+    always_modality_persistent_spec always_modality_spatial_spec
+}.
+Arguments AlwaysModality {_} _ {_ _} _.
+Arguments always_modality_persistent_spec {_} _.
+Arguments always_modality_spatial_spec {_} _.
+
+Section always_modality.
+  Context {PROP} (M : always_modality PROP).
+
+  Lemma always_modality_persistent_forall C P :
+    always_modality_persistent_spec M = AIEnvForall C → C P → □ P ⊢ M (□ P).
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma always_modality_persistent_filter C P :
+    always_modality_persistent_spec M = AIEnvFilter C → C P → □ P ⊢ M (□ P).
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma always_modality_persistent_id P :
+    always_modality_persistent_spec M = AIEnvId → □ P ⊢ M (□ P).
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma always_modality_spatial_forall C P :
+    always_modality_spatial_spec M = AIEnvForall C → C P → P ⊢ M P.
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma always_modality_spatial_filter C P :
+    always_modality_spatial_spec M = AIEnvFilter C → C P → P ⊢ M P.
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+  Lemma always_modality_spatial_filter_absorbing C P :
+    always_modality_spatial_spec M = AIEnvFilter 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.
+  Lemma always_modality_spatial_id :
+    always_modality_spatial_spec M ≠ AIEnvId.
+  Proof. destruct M as [??? []]; naive_solver. Qed.
+
+  Lemma always_modality_emp : emp ⊢ M emp.
+  Proof. eapply always_modality_mixin_emp, always_modality_mixin_of. Qed.
+  Lemma always_modality_mono P Q : (P ⊢ Q) → M P ⊢ M Q.
+  Proof. eapply always_modality_mixin_mono, always_modality_mixin_of. Qed.
+  Lemma always_modality_and P Q : M P ∧ M Q ⊢ M (P ∧ Q).
+  Proof. eapply always_modality_mixin_and, always_modality_mixin_of. Qed.
+  Lemma always_modality_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q).
+  Proof. eapply always_modality_mixin_sep, always_modality_mixin_of. Qed.
+  Global Instance always_modality_mono' : Proper ((⊢) ==> (⊢)) M.
+  Proof. intros P Q. apply always_modality_mono. Qed.
+  Global Instance always_modality_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) M.
+  Proof. intros P Q. apply always_modality_mono. Qed.
+  Global Instance always_modality_proper : Proper ((≡) ==> (≡)) M.
+  Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using always_modality_mono. Qed.
+
+  Lemma always_modality_persistent_forall_big_and C Ps :
+    always_modality_persistent_spec M = AIEnvForall C →
+    Forall C Ps → □ [∧] Ps ⊢ M (□ [∧] Ps).
+  Proof.
+    induction 2 as [|P Ps ? _ IH]; simpl.
+    - by rewrite persistently_pure affinely_True_emp affinely_emp -always_modality_emp.
+    - rewrite affinely_persistently_and -always_modality_and -IH.
+      by rewrite {1}(always_modality_persistent_forall _ P).
+  Qed.
+  Lemma always_modality_spatial_forall_big_sep C Ps :
+    always_modality_spatial_spec M = AIEnvForall C →
+    Forall C Ps → [∗] Ps ⊢ M ([∗] Ps).
+  Proof.
+    induction 2 as [|P Ps ? _ IH]; simpl.
+    - by rewrite -always_modality_emp.
+    - by rewrite -always_modality_sep -IH {1}(always_modality_spatial_forall _ P).
+  Qed.
+End always_modality.
+
+Class FromAlways {PROP : bi} (M : always_modality PROP) (P Q : PROP) :=
+  from_always : M Q ⊢ P.
+Arguments FromAlways {_} _ _%I _%I : simpl never.
+Arguments from_always {_} _ _%I _%I {_}.
+Hint Mode FromAlways + - ! - : typeclass_instances.
 
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : bi_affinely Q ⊢ P.

theories/proofmode/coq_tactics.v

@@ -543,72 +543,124 @@ Qed.
 Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
 Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
-(** * Persistence and plainness modalities *)
-Class IntoPlainEnv (Γ1 Γ2 : env PROP) := {
-  into_plain_env_subenv : env_subenv Γ2 Γ1;
-  into_plain_env_plain : Plain ([∧] Γ2);
+(** * Always modalities *)
+Class FilterPersistentEnv
+    (M : always_modality PROP) (C : PROP → Prop) (Γ1 Γ2 : env PROP) := {
+  filter_persistent_env :
+    (∀ P, C P → □ P ⊢ M (□ P)) →
+    □ ([∧] Γ1) ⊢ M (□ ([∧] Γ2));
+  filter_persistent_env_wf : env_wf Γ1 → env_wf Γ2;
+  filter_persistent_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
 }.
-
-Global Instance into_plain_env_nil : IntoPlainEnv Enil Enil.
-Proof. constructor. constructor. simpl; apply _. Qed.
-Global Instance into_plain_env_snoc_plain Γ1 Γ2 i P :
-  Plain P → IntoPlainEnv Γ1 Γ2 →
-  IntoPlainEnv (Esnoc Γ1 i P) (Esnoc Γ2 i P) | 1.
-Proof. intros ? [??]; constructor. by constructor. simpl; apply _. Qed.
-Global Instance into_plain_env_snoc_skip Γ1 Γ2 i P :
-  IntoPlainEnv Γ1 Γ2 → IntoPlainEnv (Esnoc Γ1 i P) Γ2 | 2.
-Proof. intros [??]; constructor. by constructor. done. Qed.
-
-Lemma into_plain_env_sound Γ1 Γ2 :
-  IntoPlainEnv Γ1 Γ2 → of_envs (Envs Γ1 Enil) ⊢ bi_plainly $ of_envs $ Envs Γ2 Enil.
-Proof.
-  intros [Hsub ?]. rewrite !of_envs_eq plainly_and plainly_pure /=. f_equiv.
-  { f_equiv=>-[/= ???]. split; auto. by eapply env_subenv_wf. }
-  rewrite !(right_id emp%I). trans (□ [∧] Γ2)%I.
-  - do 2 f_equiv. clear -Hsub.
-    induction Hsub as [|????? IH|????? IH]=>//=; rewrite IH //. apply and_elim_r.
-  - by rewrite {1}(plain ([∧] Γ2)) affinely_elim plainly_affinely
-               plainly_persistently persistently_plainly.
-Qed.
-
-Class IntoAlwaysEnvs (pe : bool) (pl : bool) (Δ1 Δ2 : envs PROP) := {
-  into_persistent_envs_persistent :
-    if pl then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
-    else env_persistent Δ1 = env_persistent Δ2;
-  into_persistent_envs_spatial :
-    if pe || pl then env_spatial Δ2 = Enil else env_spatial Δ1 = env_spatial Δ2
+Global Instance filter_persistent_env_nil M C : FilterPersistentEnv M C Enil Enil.
+Proof.
+  split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
+  by rewrite affinely_emp -always_modality_emp.
+Qed.
+Global Instance filter_persistent_env_snoc M (C : PROP → Prop) Γ Γ' i P :
+  C P →
+  FilterPersistentEnv M C Γ Γ' →
+  FilterPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
+Proof.
+  intros ? [HΓ Hwf Hdom]; split; simpl.
+  - intros HC. rewrite affinely_persistently_and HC // HΓ //.
+    by rewrite always_modality_and -affinely_persistently_and.
+  - inversion 1; constructor; auto.
+  - intros j. destruct (ident_beq _ _); naive_solver.
+Qed.
+Global Instance filter_persistent_env_snoc_not M (C : PROP → Prop) Γ Γ' i P :
+  FilterPersistentEnv M C Γ Γ' →
+  FilterPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
+Proof.
+  intros [HΓ Hwf Hdom]; split; simpl.
+  - intros HC. by rewrite and_elim_r HΓ.
+  - inversion 1; auto.
+  - intros j. destruct (ident_beq _ _); naive_solver.
+Qed.
+
+Class FilterSpatialEnv
+    (M : always_modality PROP) (C : PROP → Prop) (Γ1 Γ2 : env PROP) := {
+  filter_spatial_env :
+    (∀ P, C P → P ⊢ M P) → (∀ P, Absorbing (M P)) →
+    ([∗] Γ1) ⊢ M ([∗] Γ2);
+  filter_spatial_env_wf : env_wf Γ1 → env_wf Γ2;
+  filter_spatial_env_dom i : Γ1 !! i = None → Γ2 !! i = None;
 }.
-
-Global Instance into_always_false_false Δ : IntoAlwaysEnvs false false Δ Δ.
-Proof. by split. Qed.
-Global Instance into_always_envs_true_false Γp Γs :
-  IntoAlwaysEnvs true false (Envs Γp Γs) (Envs Γp Enil).
-Proof. by split. Qed.
-Global Instance into_always_envs_x_true Γp1 Γp2 Γs1 pe :
-  IntoPlainEnv Γp1 Γp2 →
-  IntoAlwaysEnvs pe true (Envs Γp1 Γs1) (Envs Γp2 Enil).
-Proof. destruct pe; by split. Qed.
-
-Lemma tac_always_intro Δ Δ' a pe pl Q Q' :
-  FromAlways a pe pl Q' Q →
-  (if a then AffineEnv (env_spatial Δ') else TCTrue) →
-  IntoAlwaysEnvs pe pl Δ' Δ →
-  envs_entails Δ Q → envs_entails Δ' Q'.
-Proof.
-  rewrite /envs_entails => ? Haffine [Hep Hes] HQ.
-  rewrite -(from_always a pe pl Q') -HQ.
-  trans (bi_affinely_if a (of_envs Δ'));
-    [destruct a=>//; by apply: affinely_intro|f_equiv].
-  destruct pl; [|destruct pe].
-  - rewrite (envs_clear_spatial_sound Δ') into_plain_env_sound sep_elim_l.
-    destruct Δ as [Δ ?]. rewrite orb_true_r /= in Hes. rewrite Hes /=.
-    destruct pe=>/= //. by rewrite persistently_plainly.
-  - rewrite (envs_clear_spatial_sound Δ') /= /envs_clear_spatial Hep.
-    destruct Δ as [Δ ?]. simpl in Hes. subst. simpl.
-    rewrite -(sep_elim_l (bi_persistently _)). f_equiv.
-    rewrite {1}(env_spatial_is_nil_affinely_persistently (Envs Δ Enil)) //.
-    by rewrite affinely_elim.
-  - destruct Δ, Δ'; simpl in *. by subst.
+Global Instance filter_spatial_env_nil M C : FilterSpatialEnv M C Enil Enil.
+Proof. split=> // HC /=. by rewrite -always_modality_emp. Qed.
+Global Instance filter_spatial_env_snoc M (C : PROP → Prop) Γ Γ' i P :
+  C P →
+  FilterSpatialEnv M C Γ Γ' →
+  FilterSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
+Proof.
+  intros ? [HΓ Hwf Hdom]; split; simpl.
+  - intros HC ?. by rewrite {1}(HC P) // HΓ // always_modality_sep.
+  - inversion 1; constructor; auto.
+  - intros j. destruct (ident_beq _ _); naive_solver.
+Qed.
+
+Global Instance filter_spatial_env_snoc_not M (C : PROP → Prop) Γ Γ' i P :
+  FilterSpatialEnv M C Γ Γ' →
+  FilterSpatialEnv M C (Esnoc Γ i P) Γ' | 100.
+Proof.
+  intros [HΓ Hwf Hdom]; split; simpl.
+  - intros HC ?. by rewrite HΓ // sep_elim_r.
+  - inversion 1; auto.
+  - intros j. destruct (ident_beq _ _); naive_solver.
+Qed.
+
+Ltac tac_always_cases :=
+  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 : FilterPersistentEnv _ _ _ _ |- _ => destruct H
+  | H : FilterSpatialEnv _ _ _ _ |- _ => destruct H
+  end; simpl; auto using Enil_wf.
+
+Lemma tac_always_intro Γp Γs Γp' Γs' M Q Q' :
+  FromAlways M Q' Q →
+  match always_modality_persistent_spec M with
+  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γp)) (TCEq Γp Γp')
+  | AIEnvFilter C => FilterPersistentEnv M C Γp Γp'
+  | AIEnvIsEmpty => TCAnd (TCEq Γp Enil) (TCEq Γp' Enil)
+  | AIEnvClear => TCEq Γp' Enil
+  | AIEnvId => TCEq Γp Γp'
+  end →
+  match always_modality_spatial_spec M with
+  | AIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
+  | AIEnvFilter C => FilterSpatialEnv M C Γs Γs'
+  | 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 /FromAlways /of_envs /= => <- HΓp HΓs <-.
+  apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')).
+  { 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),
+        (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.
+    + 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_filter.
+    + 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_filter,
+        always_modality_spatial_filter_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).
 Qed.
 
 Lemma tac_persistent Δ Δ' i p P P' Q :

theories/proofmode/monpred.v

 From iris.bi Require Export monpred.
-From iris.proofmode Require Import tactics.
+From iris.proofmode Require Import tactics class_instances.
 
 Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
@@ -14,6 +14,33 @@ Proof. by rewrite /IsBiIndexRel. Qed.
 Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
             : typeclass_instances.
 
+Section always_modalities.
+Context {I : biIndex} {PROP : bi}.
+
+  Lemma always_modality_absolutely_mixin :
+    always_modality_mixin (@monPred_absolutely I PROP)
+      (AIEnvFilter Absolute) (AIEnvForall Absolute).
+  Proof.
+    split; 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.
+    split; 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_filter_spatial `{BiAffine PROP} :=
+    AlwaysModality _ always_modality_absolutely_filter_spatial_mixin.
+End always_modalities.
+
 Section bi.
 Context {I : biIndex} {PROP : bi}.
 Local Notation monPred := (monPred I PROP).
@@ -23,6 +50,13 @@ Implicit Types 𝓟 𝓠 𝓡 : PROP.
 Implicit Types φ : Prop.
 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.
 Global Instance make_monPred_at_emp i : MakeMonPredAt i emp emp.
@@ -137,12 +171,24 @@ Proof.
   by rewrite -monPred_at_persistently -monPred_at_persistently_if.
 Qed.
 
-Global Instance from_always_monPred_at a pe P Q 𝓠 i :
-  FromAlways a pe false P Q → MakeMonPredAt i Q 𝓠 →
-  FromAlways a pe false (P i) 𝓠 | 0.
+Global Instance from_always_affinely_monPred_at P Q 𝓠 i :
+  FromAlways always_modality_affinely P Q → MakeMonPredAt i Q 𝓠 →
+  FromAlways always_modality_affinely (P i) 𝓠 | 0.
+Proof.
+  rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
+Qed.
+Global Instance from_always_persistently_monPred_at P Q 𝓠 i :